Zulip Chat Archive

Stream: general

Topic: pp.unambiguous


view this post on Zulip Johan Commelin (May 30 2020 at 14:23):

How hard would it be to write a tactic that takes an expr and prints a string that is close to the standard pretty printed version, but ready for copy-pasting into the current editor window?

view this post on Zulip Jason Rute (May 30 2020 at 14:26):

Relevant: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pp.2Eall.20with.20more.20.40

view this post on Zulip Johan Commelin (May 30 2020 at 14:29):

Typical examples are ambiguous 0 that need a type ascription

view this post on Zulip Mario Carneiro (May 30 2020 at 14:29):

it needs more than a type ascription in general

view this post on Zulip Johan Commelin (May 30 2020 at 14:29):

why?

view this post on Zulip Mario Carneiro (May 30 2020 at 14:30):

I would start from pp.all as a baseline

view this post on Zulip Mario Carneiro (May 30 2020 at 14:31):

You can try to take pp.all output and progressively try to remove @ signs while ensuring that the elaborator still produces the right term, but this is pretty expensive since you have to typecheck hundreds of variations of the term

view this post on Zulip Mario Carneiro (May 30 2020 at 14:32):

Johan Commelin said:

why?

You could have a zero with a non-canonical instance, or one that was provided manually and can't be found by instance search

view this post on Zulip Johan Commelin (May 30 2020 at 14:39):

Mario Carneiro said:

You can try to take pp.all output and progressively try to remove @ signs while ensuring that the elaborator still produces the right term, but this is pretty expensive since you have to typecheck hundreds of variations of the term

Expensive is fine if it's only used occasionally, say in extract_goal.

view this post on Zulip Jason Rute (May 30 2020 at 14:39):

I believe Lean 4 is making sure the pp.all round trip succeeds. See https://github.com/leanprover/lean4/blob/50fc9610379243e419f75de7e281cbeb61287324/src/Lean/Delaborator.lean

view this post on Zulip Jason Rute (May 30 2020 at 14:41):

Sorry, I misunderstood. You want something closer to standard pp.

view this post on Zulip Mario Carneiro (May 30 2020 at 14:42):

It's not hard to make something like pp.all that round-trips. I am pretty sure the "delaborator" is doing what I outlined above, trying to get closer to an unmarked term

view this post on Zulip Mario Carneiro (May 30 2020 at 14:47):

I think if you design it well you can get delaboration to be "only" as expensive as elaboration. (Still pretty expensive for something that is doing printing...)


Last updated: May 17 2021 at 22:15 UTC