Delaborator request

Stream: metaprogramming / tactics

[Heather Macbeth]

I'd love to have a delaborator which pretty-prints quantified statements

• with type annotations
• without parentheses
• paired up when relevant

So, for example,

∃ a b : Nat, ∀ c : Nat, a + b = c

In the standard setup this pretty-prints as

∃ a b, ∀ (c : Nat), a + b = c

and with set_option pp.funBinderTypes true this pretty-prints as

∃ (a : Nat), ∃ (b : Nat), ∀ (c : Nat), a + b = c

[Kyle Miller]

Something I'm hoping we can find a general solution for is giving pretty printer hints for unexpanders. Generally notations using binders use a lambda function, which means whether they get to pretty print with a binder is at the mercy of whether pp.funBinderTypes is set.

Here's hack that we can use on a case-by-case basis to ensure binder types. This can be generalized to be a command to attach binder type information to a particular argument.

import Mathlib.Lean.PrettyPrinter.Delaborator

open Lean PrettyPrinter.Delaborator SubExpr in
/-- "Pre-delaborator" for `Exists` that adds a `funBinderTypes` hint to its last argument. -/
@[delab app.Exists]
def preDelabExists : Delab :=
  whenPPOption getPPNotation <|
  whenPPOption getPPPiBinderTypes <|
  whenNotPPOption getPPAnalysisSkip <|
  withOptionAtCurrPos `pp.analysis.skip true do
    let e ← getExpr
    guard <| e.isAppOfArity ``Exists 2
    let optionsPerPos ← withAppArg do
      return (← read).optionsPerPos.setBool (← getPos) pp.funBinderTypes.name true
    withTheReader Context ({· with optionsPerPos}) delab

#check ∃ x, x = 0
/-
∃ (x : ℕ), x = 0 : Prop
-/

-- Maybe this should be its own pp option, but I hooked it into `piBinderTypes`
-- since it seems to me that you want to control binders for everything quantifier-like.
set_option pp.piBinderTypes false in
#check ∃ x, x = 0
/-
∃ x, x = 0 : Prop
-/

-- The hack avoids setting `pp.funBinderTypes` globally:
#check fun x => x + 1
/-
fun x ↦ x + 1 : ℕ → ℕ
-/

[Kyle Miller]

The parentheses in the type ascription come from the core app unexpander. If you paste this version in, you can see it without parens:

@[app_unexpander Exists] def unexpandExists' : Lean.PrettyPrinter.Unexpander
  | `($(_) fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
  | `($(_) fun $x:ident => $b)                     => `(∃ $x:ident, $b)
  | `($(_) fun ($x:ident : $t) => $b)              => `(∃ $x:ident : $t, $b) -- removed parens
  | _                                              => throw ()

[Heather Macbeth]

@Kyle Miller Thanks for looking at this! So to check that I'm following your directions: If I now use your

@[delab app.Exists] def preDelabExists : Delab := ...
@[app_unexpander Exists] def unexpandExists' : Lean.PrettyPrinter.Unexpander := ...

and set set_option pp.piBinderTypes true, then I get a single existential to pretty-print exactly as I wanted:

#check ∃ x : Nat, x = 0 -- ∃ x : Nat, x = 0

But double existentials still don't get merged:

#check ∃ x y : Nat, x = y -- ∃ x : Nat, ∃ y : Nat, x = y

and universal quantifiers still don't hide their parentheses:

#check ∀ x : Nat, x = 0 -- ∀ (x : Nat), x = 0

Is this what you would expect?

[Kyle Miller]

Yes, that's right (with the understanding that piBinderTypes is true by default)