Debugging Exprs

Stream: lean4

[Henrik Böving]

In doc-gen4 I have to work with Expr a few time to e.g. get the type of a field of a structure (which doesn't seem to be in the compiler as of now? But feel free to correct me on that), extracting arguments from functions to display them separately etc. For that purpose I would sometimes find it extremly useful to view the actual structure of the Expr so I can see where my algorithms are fucking up instead of guessing around with dbg_trace and the string representation of Expr. At the moment I basically slap:

deriving instance Repr for DataValue
deriving instance Repr for KVMap
deriving instance Repr for MData
deriving instance Repr for Level.Data
deriving instance Repr for Level
deriving instance Repr for Expr.Data
deriving instance Repr for Expr

and then repr myexpr in the debug prints to see what is happening. Is there a nicer way to do this?

[Gabriel Ebner]

See https://github.com/leanprover/lean4/issues/619#issuecomment-895678882

[Sebastian Ullrich]

Is it only mdata that's missing from pp.all? We could add some pseudo-syntax (or an actual macro that takes a KVMap term) to print it, Lean 3 had something like that.

[Gabriel Ebner]

There is other differences that are hard/impossible to see in pp.all: is x.1 a constant, a free variable, or a projection? And if it is a projection, what is the structure name? Does a let have the nonDep-flag set? I believe pp.all also renames bound variables.

[Henrik Böving]

Yeah this is exactly the type of stuff I can see in repr since it shows the actual Expr tree.

[Henrik Böving]

Related to my statement about getting the type of a structure field, it appears there is already a method here: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Structure.lean#L317 but it's and all its friends are private, is there a good reason for this? Or could we just get them public so I can use it as well? Alternatively if there is a good reason I guess I will just copy the stuff out haha.