controlling delaboration

Stream: lean4

[David Renshaw]

I can define custom syntax via infix like this, and it gets printed back nicely when I do #check:

infix " ♫ "  => LE.le
#check  (1 ♫ 2)
-- 1 ♫ 2 : Prop

If I instead define the syntax like this, then it does not get printed back nicely:

syntax term " ♫♫ " term : term
macro_rules
|`( $a ♫♫ $b ) => `( LT.lt $a $b )

#check 1 ♫♫ 2
-- 1 < 2 : Prop

What could I add to the second example to make it behave like the first?

[Daniel Selsam]

syntax term " ♫♫ " term : term
macro_rules
|`( $a ♫♫ $b ) => `( LT.lt $a $b )

#check 1 ♫♫ 2 -- 1 < 2 : Prop

@[appUnexpander LT.lt] def unexpandMusic : Lean.PrettyPrinter.Unexpander
  | `(LT.lt $a $b) => `($a ♫♫ $b)
  | _              => throw ()

#check 1 ♫♫ 2 -- 1 ♫♫ 2 : Prop

[David Renshaw]

Is it possible to do something like that for a structure? It's not working for me:

structure Foo where
  x : Nat
  y : Nat

syntax term " ♬ " term : term

macro_rules
| `( $a ♬ $b ) => `(Foo.mk $a $b)

#check 1 ♬ 2 -- { x := 1, y := 2 }

@[appUnexpander Foo] def unexpandFoo : Lean.PrettyPrinter.Unexpander
  | `({ x:= $a, y:= $b }) => `($a ♬ $b)
  | _ => throw ()

#check 3 ♬ 4 -- { x := 3, y := 4 }

[Mario Carneiro]

I managed to make it work with a delaborator:

open Lean PrettyPrinter.Delaborator
@[delab app.Foo.mk] def delabFoo : Delab := do
  let e ← getExpr
  guard $ e.getAppNumArgs == 2
  let a ← withAppFn $ withAppArg delab
  let b ← withAppArg delab
  `($a ♬ $b)

#check 3 ♬ 4 -- 3 ♬ 4 : Foo

[Daniel Selsam]

Currently, appUnexpanding does not work if a more specialized delaborator applies (in this case, the structure delaborator).

[Daniel Selsam]

I think users may expect custom unexpanders to take priority over builtin delaborators, so it may be worth addressing. It seems like an easy fix: just fail in these two cases (https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Builtins.lean#L163-L165) and put it at the end of the list.

[Daniel Selsam]

It might also make sense to use the first unexpander that works rather than giving up after the first.

[Daniel Selsam]

Actually, this proposal would introduce a major perf problem unless it caches the delabAppImplicit calls. Probably not worth it.

[Daniel Selsam]

Not so bad actually https://github.com/dselsam/lean4/tree/unexpand

[Sebastian Ullrich]

@Daniel Selsam Can't we just move the delabAppImplicit call into the some expanders branch? Then I would not be worried about overhead.

[Sebastian Ullrich]

Assuming that most unexpanders succeed, given that most function applications are saturated

[David Renshaw]

How do I go from a value (numLit "3") : Syntax to a value 3 : Nat?

[David Renshaw]

E.g.

structure Foo where
  x : Nat
  y : Nat

syntax term " ♬ " term : term

macro_rules
| `( $a ♬ $b ) => `(Foo.mk $a $b)

open Lean PrettyPrinter.Delaborator
@[delab app.Foo.mk] def delabFoo : Delab := do
  let e ← getExpr
  guard $ e.getAppNumArgs == 2
  let a ← withAppFn $ withAppArg delab
  let b ← withAppArg delab
  let x : Nat := a -- Doesn't work. Probably need to invoke some kind of parser?
  -- do something with x ...
  `($a ♬ $b)

[Mario Carneiro]

Is it a guaranteed literal, or can it be a closed expression that requires evaluation?

[David Renshaw]

For now I think I only care about the guaranteed literal case.

[Mario Carneiro]

easiest way seems to be a.isNatLit?.get!

[David Renshaw]

How did you look that up? Using code completion in VSCode? (I'm using emacs.)

[Mario Carneiro]

No, grepping the source for useful looking things

[Mario Carneiro]

specifically I found numLitKind and looked for references to it

[Mario Carneiro]

code completion does work but the list of things you can do to a Syntax is pretty large

[David Renshaw]

Aha -- apparently Lean.Meta.whnf lets me handle cases where a is not guaranteed to be a literal

[Daniel Selsam]

Sebastian Ullrich said:

Daniel Selsam Can't we just move the delabAppImplicit call into the some expanders branch? Then I would not be worried about overhead.

That might be an acceptable trade-off, but the following would take exponential time to delaborate:

def foo (k : Nat → Nat) (n : Nat) : Nat := k (n+1)

set_option hygiene false in
@[appUnexpander foo] def unexpandFooApp : Lean.PrettyPrinter.Unexpander
  | `(foo $k $a) => `(My.foo $k $a)
  | _ => throw ()

#check foo id 0 -- My.foo id
#check foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo id -- exp-time