Zulip Chat Archive

Stream: lean4

Topic: unexpanders


view this post on Zulip Alexander Bentkamp (Jan 07 2021 at 15:40):

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?

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 06:08):

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

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 06:32):

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

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 06:38):

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

view this post on Zulip Alexander Bentkamp (Jan 08 2021 at 09:05):

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

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

view this post on Zulip Alexander Bentkamp (Jan 08 2021 at 09:08):

`(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.

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 22:21):

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

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 23:05):

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.

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 23:08):

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

view this post on Zulip Sebastian Ullrich (Jan 09 2021 at 10:10):

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

view this post on Zulip Sebastian Ullrich (Jan 09 2021 at 10:15):

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

view this post on Zulip Sebastian Ullrich (Jan 09 2021 at 10:18):

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

view this post on Zulip Alexander Bentkamp (Jan 11 2021 at 10:39):

Ok, thanks!


Last updated: May 18 2021 at 22:15 UTC