Pretty printer parentheses

Stream: metaprogramming / tactics

[Snir Broshi]

How does the pretty-printer decide when to drop the parentheses of an expression?

import Mathlib
open Nat

/--
error: unsolved goals
n : ℕ
p : ℕ × ℕ
⊢ Nat.Prime (n ! + p.1!)
-/
#guard_msgs in
theorem foo (n : ℕ) (p : ℕ × ℕ) : (n)! + (p.fst)! |>.Prime := by {}

[Aaron Liu]

It's the parenthesizer which adds them back, see docs#Lean.PrettyPrinter.Parenthesizer

[Aaron Liu]

I spent a while writing a custom parenthesizer for docs#Nat.term_!, it worked but felt really hacky

[Snir Broshi]

Aaron Liu said:

It's the parenthesizer which adds them back, see docs#Lean.PrettyPrinter.Parenthesizer

Wdym "adds them back", who drops them in the first place?
I know that the Syntax objects contain parentheses, so something drops them somewhere.

[Kyle Miller]

In particular, the flow is:

String --parsing--> Syntax --elaboration--> Expr

and

Expr --delaboration--> Syntax --parenthesization--> Syntax --formatting--> String

[Kyle Miller]

If you imaging going from String to String by applying both sequences, there's some sense in which it "adds them back", but to be more precise, parenthesization is a step of the pretty printing process for Expr's.

[Kyle Miller]

The Expr type doesn't have any concept of parentheses at all. It's the raw fully-elaborated expression that Lean works with internally.

[Snir Broshi]

Ooh so the problem is going through Expr, thanks!
Which parts are called "pretty printing", the entire reverse process or just the parnthesization+formatting?
Is it possible specifically for the infoview to skip Expr and only do parsing+formatting? Or will skipping elaboration give wrong goals?

[Kyle Miller]

The entire second line of operations in my message is pretty printing of expressions.

[Kyle Miller]

And no, there's no way to skip Exprs. The Syntax is just surface representation. Lean only operates on Exprs.

[Aaron Liu]

Snir Broshi said:

Wdym "adds them back", who drops them in the first place?

That would be the elaborator, which turn the Syntax into an Expr

[Snir Broshi]

In usual programming-language terms, would Syntax be a CST and Expr an AST, or is the elab/delab terminology very Lean-specific and I should not try to fit Lean into such boxes?

[Kyle Miller]

Syntax is like the CST, and it's got enough information to know exactly how it lines up with the source.

[Kyle Miller]

The Expr is like an AST after typechecking/inference.

[Aaron Liu]

Snir Broshi said:

Is it possible specifically for the infoview to skip Expr and only do parsing+formatting? Or will skipping elaboration give wrong goals?

You can skip Expr and just parenthesize and format Syntax objects, but not in the infoview since many parts of Lean (including the infoview) only work with Expr

[Kyle Miller]

By the way, it would be possible to preserve parentheses by creating a new elaborator for parenthesis notation that inserts metadata into the expressions, and have that metadata pretty print using parentheses. It's something you can hack together as a user.

[Snir Broshi]

I guess that'll only work for the first goal, since only it really comes from parsing a string, since tactics would work with Expr?

[Snir Broshi]

Aaron Liu said:

You can skip Expr and just parenthesize and format Syntax objects

Would formatting be Lean.PrettyPrinter.formatCategory `command stx for stx : Syntax?

[Aaron Liu]

yes that's just formatting (without parenthesizing)