Using custom `Repr` of inductive type

Stream: new members

[Richard Kiss]

I define Node with a custom Repr to reduce output size during proofs.

inductive Node
  | atom : Atom → Node
  | pair : Node → Node → Node


def repr_node (n: Node) : String :=
  match n with
  | Node.atom a => b2h a.data
  | Node.pair a b => s!"({repr_node a} . {repr_node b})"


instance : Repr Node where
  reprPrec (n : Node) (_ : Nat) := repr_node n

When I do #eval n where with n: Node my custom Repr works just fine. But in proofs it uses the default verbose Node.pair .... What am I missing?

[Michal Wallace (tangentstorm)]

I don't know the answer, but what happens if you also implement ToString?

[Richard Kiss]

I gave it a shot, but it didn't help. Looks like #eval toString n for n: Node does the same as repr_node except it puts double quotes around the whole thing

[Daniel Weber]

Could you make a #mwe? Anyway, I believe what you need is a delaborator, see https://leanprover-community.github.io/lean4-metaprogramming-book/extra/03_pretty-printing.html .

[Daniel Weber]

@[app_unexpander Node.pair]
def unexpNodePair : Lean.PrettyPrinter.Unexpander
  | `($(_) $a $b) => `(($a . $b))
  | _ => throw ()

should work

[Richard Kiss]

here's a simplified #mwe

structure Atom := mk :: (data: Nat)

def repr_atom (a: Atom) : String := s!"*{a.data}*"
  -- put stars around the nat to make it clear it's working

instance : Repr Atom where
  reprPrec (n : Atom) (_ : Nat) := repr_atom n


def a1 := Atom.mk 1
def a2 := Atom.mk 2

#eval a1 -- this works fine

theorem different: a1 ≠ a2 := by
  unfold a1
  unfold a2
  -- put cursor on this line and look at `Tactic state` in the Infoview
  -- it doesn't match the `#eval a1` output
  sorry

[Richard Kiss]

I tried playing around a bit with @[app_unexpander Atom] in the #mwe, adding

@[app_unexpander Atom]
def unexpNodePair : Lean.PrettyPrinter.Unexpander
  | `($(_) $a) => `(($a))
  | _ => throw ()

but it didn't seem to have any effect.

[Richard Kiss]

I'll read up more on elaborator, delaborator and the pretty-printing link above.

[Henrik Böving]

Daniel Weber said:

Could you make a #mwe? Anyway, I believe what you need is a delaborator, see https://leanprover-community.github.io/lean4-metaprogramming-book/extra/03_pretty-printing.html .

This is the correct direciton to go into.

There are two distinct ways to look at a datatype. One is Repr which you can implement to turn a value of your type to a string at runtime of a program (which is what eval is simulating). The other is controlled by the delaborator which determines how Lean shows you values etc. in its interactive editing facilities such as the LSP. Both of these facilities are inherently disconnected.

For your concrete use case you will need to put the delaborator on the constructor of Atom, Atom.mk instead of the type Atom which can of course have a custom interactive representation as well:

@[app_unexpander Atom.mk]
def unexpNodePair : Lean.PrettyPrinter.Unexpander
  | `($(_) $a) => `(($a))
  | _ => throw ()

[Richard Kiss]

got it! That worked. So I think I'm unblocked, thank you

[Richard Kiss]

is there a place I can read more about @[...] attributes? It smells like python decorators to me, but I haven't seen a formal definition of what it means

[Henrik Böving]

They are called attributes and they are quite different from decorators. If you wish to know how they work internally you can read up on it in the meta programming book that is linked above. If you just wish to work with them the answer is approximately the following: Tagging a declaration with an attribute will put it into a sort of mini database (potentially with additional meta information, in the case of app_unexpander that meta information is Atom.mk) within a Lean meta programming extension which can then do a kind of job. For app_unexpander that extension is the (surprise) unexpander which is part of the delaborator.

[Richard Kiss]

on further reflection, this makes sense. During proofs, we have to revert to how Atom is defined in their original context rather than creating instances of Atom and Repring them.

[Henrik Böving]

Precisley, note that in proofs your terms may have variables in them that you got from e.g. a function argument. You cannot Repr these variables as they are opaque values, you are doing symbolic reasoning after all.