Command to print the Expr of a Lean term?

Stream: metaprogramming / tactics

[Markus de Medeiros]

Apologies for the basic question, which might be an #xy. I have Lean terms that I want to manipulate using metaprogramming, so I'm trying to understand how to construct them using MkAppN. Is there a command I can run that will print out the underlying Expr for a term?

[Kyle Miller]

Options:

• logInfo m!"e = {e}" will pretty print the expression, and if you hover over things you can figure out how the expressions are constructed, if you know how surface syntax corresponds to lean terms (e.g. @c.{u,v} is Expr.const c [u,v], @f a b c is mkAppN f #[a, b, c], etc.). It's helpful to set pp.explicit and pp.universes.
• logInfo m!"e = {repr e}" will show the constructors.
• If you do deriving instance Lean.ToExpr for ... enough times on all the types involved on Lean.Expr, then you can do logInfo m!"e = {Lean.toExpr e}", which is like repr, but it'll be pretty printed nicer.

[Markus de Medeiros]

Thanks! It seems kind of strange to me that you need to instantiate more typeclasses to get Lean to display a Expr it already has access to, but this is good to know.

[Kyle Miller]

To be clear, this is to get it to use Lean.toExpr, to make an Expr that represents the Expr term, to use the pretty printer. That's fancier output than the pre-existing Repr — doesn't seem so strange to me that fancier output might need some more work?

[Kyle Miller]

You can already do {e} to include the expression, but for your purpose, the problem is that it's giving you what the expression represents (that's what we usually want when debugging metaprograms), but you're wanting to see what a representation of the expression represents (that's to say, you want to pretty print Lean terms that represent an Expr that creates the Expr, rather than pretty print the Expr itself).

[Kyle Miller]

I'm not sure why exactly we don't have a ToExpr Expr instance in core yet, other than there haven't been any core applications that need it. (At least we've got the deriving handler so it doesn't have to be written by hand!)

[Markus de Medeiros]

Yeah it seems that you still need add Repr instances for some terms though, here's a (not self-contained) example

def idk : NML.ExecState DataT := .run [.ret <| (.val .unit)] (.emp DataT)
#check idk
-- idk {DataT : Type} : NML.ExecState DataT
def test : MetaM Unit := do
  Lean.logInfo m!"e = {repr idk}"
-- failed to synthesize
--   Repr (NML.ExecState ?m.163)
-- #eval test

I am looking for something even more unsophisticated, like "if I can #check X then I can #showexpr X, even for open terms or for terms that are paramaterized by types that don't have Repr. It's fine if that doesn't exist, I can use it as a basic metaprogramming exercise anyways :)

[Kyle Miller]

I see, I thought your question was "I have an Expr, and I want to understand it" not "I have a run-time value, and I want to construct an Expr that represent it", since you used the word "term". With metaprogramming, "staging" is very important to keep straight: is it a compile-time value (an Expr) or a runtime value (an NML.ExecState DataT).

[Kyle Miller]

The ToExpr deriving handler is a way to generate code to reflect runtime values back into Exprs that accurately represent those values.

[Kyle Miller]

When you write idk inside that do, you are evaluating idk, not accessing the Expr that represents it.

[Kyle Miller]

Here's a good metaprogramming exercise: look at the source code of #check and #reduce, and make a #showexpr that does what you want. Possibly you want to look at #print too, since that's able to print the bodies of definitions.

[Kyle Miller]

The broader point here is that Lean does not represent runtime values as Exprs, so there's no Expr to get.

[Markus de Medeiros]

That makes a lot of sense and was definitely a misconception I've been struggling with (I think specifically coming from Racket). Thank you for explaining it!

[Kenny Lau]

@Markus de Medeiros the definition of something is stored in an "eq" theorem

[Kenny Lau]

import Lean
import Qq

open Lean Elab Tactic Qq

def e : Nat := 37
#check e.eq_1

def test : MetaM Unit := do
  let ident : Expr := q(e.eq_1)
  let ⟨0, P, h⟩ ← inferTypeQ ident | return ()
  trace[debug] m!"{P}"
  let ~q($lhs = $rhs) := P | return ()
  trace[debug] m!"{rhs}"
  trace[debug] s!"{rhs}"

set_option trace.debug true
#eval test
/-
[debug] e = 37
[debug] 37
[debug] OfNat.ofNat.{0} Nat 37 (instOfNatNat 37)
-/

[Kenny Lau]

@Markus de Medeiros is this closer to what you want?

[Kyle Miller]

Kenny, the definition is stored in the declaration in the environment. The eq theorems are largely for reasoning about recursive functions, to hide the way the recursion was encoded. (In particular, the function can appear both on the LHS and RHS.) I would not use these here.

[Kenny Lau]

well, I wrote a suboptimal code in the hopes that someone would improve upon it, because having a bad code is better than no code

[Alfredo Moreira-Rosa]

i think there is ppExpr as an helper to pretty print an Expr