expression printer implemented in pure Lean

Stream: metaprogramming / tactics

[Xavier Martinet]

Is there a way to print an expr directly in Lean, to get results similar to tactic.pp e ? I mean, without using some meta constant written in C++ such as expr.to_string or tactic_state.pp_tagged ?

[Mario Carneiro]

The closest thing is expr.to_raw_fmt. It's not really possible to replicate pp e if expr is your only input because you need access to the local context to resolve some types

[Xavier Martinet]

Thanks. That would output the AST, not the pretty print though.

And if I were able to feed the local context in a format that Lean would understand, I suppose there is no off-the-shelf pure-Lean function, right? I would have to re-implement the C++ pretty printer in Lean (God forbid me!)

[Patrick Massot]

I don't think that writing an approximate pretty printer in Lean would be that bad

[Xavier Martinet]

That is something I am interested in, because I would like to add some type annotation to disambiguate expressions (ie, having a bijection pretty-print <-> expr), without writing too many of them or too many parentheses. There are tricks I can use by leveraging the eformat, however everything related to precedence or infix gets lost in this format :(

[Kyle Miller]

@Xavier Martinet What's an example of something you want to do? I was thinking about modifying the pretty printer from the C++ side to have an option to add type annotations for numerals (like (5 : zmod 7)).

[Patrick Massot]

This goal is surprisingly tricky to achieve (except by printing every argument explicitly of course). It is an explicit goal of the Lean 4 project.

[Xavier Martinet]

Kyle Miller said:

Xavier Martinet What's an example of something you want to do? I was thinking about modifying the pretty printer from the C++ side to have an option to add type annotations for numerals (like (5 : zmod 7)).

typically, I would like to copy-paste the pretty-print of the tactic state to resume a tactic-mode proof at a given point without having to go through all the steps
also, if I extract some lemmas from a proof (e.g., the haves within a tactic-mode proof), or even the final actual theorem), I would like to be able to copy-paste their statements without caring about the actual context they were written in

What I do so far:

• I traverse the eformat graph
• if within a tagged_format.tag, the expression is a coercion, I add parentheses + type annotations around its pretty print
• a special case is indeed for numerals, as their type depends on the context while parsing: in that case, I just check if the type returned by parsing with no context is different from actual one, and if so I add parentheses + type annotation
• eventually there is a check to verify if the new pretty print, when parsed back to an expr, is alpha-equivalent to the original expression

For instance , if the input string is (1 : ℝ) + (x : ℝ) where x : ℕ, the current pp would return 1 + ↑x while the algorithm described above would return (1 : ℝ) + (↑x : ℝ) :

• 1 is indeed parsed as a ℝ, and not as a ℕ coerced to a ℝ,
• x is parsed as ℕ coerced to a ℝ

[Patrick Massot]

Xavier Martinet said:

typically, I would like to copy-paste the pretty-print of the tactic state to resume a tactic-mode proof at a given point without having to go through all the steps
also, if I extract some lemmas from a proof (e.g., the haves within a tactic-mode proof), or even the final actual theorem), I would like to be able to copy-paste their statements without caring about the actual context they were written in

This is precisely the goal that is difficult. You can search for "round tripping" for many discussions about that.