unexpanders

Stream: lean4

[Alexander Bentkamp]

I am experimenting with unexpanders, which allow macros to appear in pretty printing. When trying to implement one for a binder I get this error message:

open Lean

def myfun (f : α → β) := f

macro "bindme" x:ident ", " b:term : term => `(myfun (fun $x => $b))

@[appUnexpander myfun] def unexpand : PrettyPrinter.Unexpander := fun
| `(myfun fun $x => $p) => `(bindme $x, $p)
| _ => throw ()

#check bindme x, x
--[Error pretty printing expression: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
-- myfun.{u_1 u_1} ?_uniq.952 ?_uniq.952 (fun (x : ?_uniq.952) => x) : ?m.952 → ?m.952

Any ideas?

[Mohamed Al-Fahim]

@Alexander Bentkamp To be sure, what is the expected output of #check that should replace the error?

[Mohamed Al-Fahim]

Should it be myfun fun (x : ?m.1129) => x : ?m.1129 → ?m.1129?

[Mohamed Al-Fahim]

I think this should be a step in the right direction:

open Lean

def myfun (f : α → β) := f

macro "bindme" x:ident ", " b:term : term => `(myfun (fun $x => $b))

@[appUnexpander myfun] def unexpand : PrettyPrinter.Unexpander := fun
| `(myfun (fun $x => $p)) => `(bindme $x, $p)
| _ => throw ()

#check bindme x, x

[Alexander Bentkamp]

I would like the macro "bindme" to appear in the output. Something like:

bindme x, x : ?m.1129 → ?m.1129

[Alexander Bentkamp]

`(myfun (fun $x => $p))

Adding these parentheses just stops the unexpander from working at all. Adding them has the same effect as removing def unexpand entirely.

[Mohamed Al-Fahim]

I was able to narrow down the problem to fixing the $i part.

open Lean

def myfun (f : α → β) := f

macro "bindme" x:ident ", " b:term : term => `(myfun (fun $x => $b))

@[appUnexpander myfun] def unexpand : PrettyPrinter.Unexpander := fun
| `(myfun fun $i => $o) => `(bindme i, $o)
| _ => throw ()

#check bindme x, x
#check bindme y, y

gives bindme i✝, x : ?m.957 → ?m.957 and bindme i✝, y : ?m.967 → ?m.967, that's still not quite the expected result...

[Mohamed Al-Fahim]

I am not sure if this is relevant, but:

open Lean

def myfun (f : α → β) := f

macro "bindme" x:ident ", " b:term : term => `(myfun (fun $x => $b))

@[appUnexpander myfun] def unexpand : PrettyPrinter.Unexpander := fun
| `(myfun fun $i => $o) => #check $i
| _ => throw ()

gives elaboration function for 'antiquot' has not been implemented.

[Mohamed Al-Fahim]

@Sebastian Ullrich Does this mean that elaboration for 'antiquot' will be implemented in the future?

[Sebastian Ullrich]

@Mohamed Al-Fahim You forgot the quotation around #check $i

[Sebastian Ullrich]

@Alexander Bentkamp Your $x is capturing the full (x : ?m.1129) binder as shown in @Mohamed Al-Fahim's output, which will break the bindme syntax after being inserted. You could do something like

@[appUnexpander myfun] def unexpand : PrettyPrinter.Unexpander := fun
| `(myfun fun ($x:ident : $ty) => $p) => `(bindme $x, $p)
| _ => throw ()

instead, but at this point it should be clear that analysing anything but the raw arguments in an appUnexpander is very brittle since it is dependent on the behavior on the pretty printers that came before it. It would be better to write a full delaborator here working directly on Expr, though that means importing Lean.

[Sebastian Ullrich]

Or make the bindme syntax less restrictive by using x:term :)

[Alexander Bentkamp]

Ok, thanks!

[Chris B]

Is the "collapsing" of brackets in unexpanders (e.g. the unexpander for List will show[0, 1, 2] instead of [0, [1, [2]]]` just a built-in behavior that does this for matching pairs of brackets, or is there something more to it?

[Mac]

it is just how the unexpander is defined, the definition of which you can find here in the Lean 4 source code. You could define a custom unexpander in a similar manner. For example:

open Lean PrettyPrinter

syntax (priority := high) "(" term,* ")" : term

@[appUnexpander List.nil]
def unexpandListNilAlt : Unexpander
| `($(_)) => `(())
| _       => throw Unit.unit

@[appUnexpander List.cons]
def unexpandListConsAlt : Unexpander
| `($(_) $x ())      => `(($x))
| `($(_) $x ($xs,*)) => `(($x, $xs,*))
| _                  => throw Unit.unit

#check [1,2,3] -- (1, 2, 3) : List Nat

[Chris B]

Thanks, I think I'm almost there. I was (am?) confused by how that lets you print stuff that doesn't otherwise have an instance of ToString, like the set notation unexpander in Mathlib4 lets you print sets declared with the macro. I guess it's just turning the macro invocation back into the token tree from which it was expanded and showing it to you again. That's interesting.

[Mac]

Chris B said:

I guess it's just turning the macro invocation back into the token tree from which it was expanded and showing it to you again. That's interesting.

Exactly! An unexpander is a pretty printer takes the expanded syntax and (ideally) reverts it back to the syntax it come frame (i.e., it 'unexpands` it) and then prints the resulting syntax.

[Chris B]

Got it, thanks.