pp.unambiguous

Stream: general

[Johan Commelin]

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?

[Jason Rute]

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

[Johan Commelin]

Typical examples are ambiguous 0 that need a type ascription

[Mario Carneiro]

it needs more than a type ascription in general

[Johan Commelin]

why?

[Mario Carneiro]

I would start from pp.all as a baseline

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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.

[Jason Rute]

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

[Jason Rute]

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

[Mario Carneiro]

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

[Mario Carneiro]

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...)