inspect expressions

Stream: lean4

[Damiano Testa]

Dear All,

I often find myself wanting how a term of some inductive type is build out of its constructors. Is there a command that prints this information?

I would especially like this to work on Exprs, since my main motivation is as a help to debug meta-code.

My current approach is a simple-minded recursion into Exprs. Here is an example:

example : 3 ≠ 0 := by
  inspect
/-
inspect: '3 ≠ 0'

'Ne' -- app
|-'Nat' -- const
|-'OfNat.ofNat' -- app
| |-'Nat' -- const
| |-'3' -- natLit
| |-'instOfNatNat' -- app
| | |-'3' -- natLit
|-'OfNat.ofNat' -- app
| |-'Nat' -- const
| |-'0' -- natLit
| |-'instOfNatNat' -- app
| | |-'0' -- natLit
-/

[Damiano Testa]

Before I try anything deeper, is this already available, in some form or other?

Thanks!

[Damiano Testa]

In case you are wondering, this is the simple-minded code that I used for the example above:

inspect

import Mathlib.Lean.Expr.Basic

open Lean Elab Tactic

def treeM (ex : Expr) : String × MessageData × Array Expr :=
match ex with
  | .bvar n                 => ("bvar", m!"'{n}'", #[])
  | .fvar fv                => ("fvar", fv.name,  #[])
  | .mvar mv                => ("mvar", mv.name, #[])
  | .sort u                 => ("sort", u, #[])
  | .const na ..            => ("const", m!"'{na}'", #[])
  | .app ..                 => ("app", m!"'{ex.getAppFn.constName}'", ex.getAppArgs)
  | .lam na t b i           => ("lam", m!"{i.brackets.1}'{na}'{i.brackets.2}", #[t, b])
  | .forallE na t b i       => ("forallE", m!"{i.brackets.1}'{na}'{i.brackets.2}", #[t, b])
  | .letE na t v b i        => ("letE", m!"'{na}' {t} {v} {b} {i}", #[t, v, b])
  | .lit (Literal.natVal n) => ("natLit", m!"'{n}'", #[])
  | .lit (Literal.strVal n) => ("strLit", m!"'{n}'", #[])
  | .mdata _ e              => ("mdata", m!"'{e}'", #[e])
  | .proj na id e           => ("proj", m!"'{na}' {id} {e}", #[e])

partial
def treeR (e : Expr)
    (withCtorName : Bool := true) (indent : MessageData := "\n") (sep : MessageData := "  ") :
    MessageData :=
let (ctorN, msg, es) := treeM e
let ctorN : MessageData := if withCtorName then (" -- " ++ ctorN ++ "") else .nil
let mes := es.map (treeR (withCtorName := withCtorName) (indent := indent ++ sep) (sep := sep))
mes.foldl (fun x y => (x.compose indent).compose ((m!"|-").compose y)) (msg.compose ctorN)

def inspect {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m]
  [MonadOptions m] (e : Expr) (withCtorName : Bool := true) : m Unit :=
  logInfo (m!"inspect: '{e}'\n\n".compose (treeR e (withCtorName := withCtorName) (sep := "| ")))

syntax "inspect" (colGt ident)? : tactic

elab_rules : tactic | `(tactic| inspect $[$bang]?) => focus do
  let expr := ← match bang with
    | none => getMainTarget
    | some id => do
      let loc := ← Term.elabTerm id none
      let decl := (← getLCtx).getFVar! loc
      return decl.type
  inspect expr

example {h : 1 ≠ 0} : 3 ≠ 0 := by
  inspect
  inspect h
  exact Nat.succ_ne_zero 2

[Kyle Miller]

Mathlib.Tactic.Explode has a command that's meant for showing the structure of proofs. By default it filters out anything that's not a proof though, and it flattens out the hierarchical structure of an expression, which is probably not what you want.

[Kyle Miller]

Here's something that simple that also gives you the Expr structure of an expression:

import Mathlib.Tactic.ToExpr

open Lean Elab Tactic

elab "inspect" : tactic =>
  withMainContext do
    let ty ← instantiateMVars (← getMainTarget)
    logInfo m!"{toExpr ty}"

example : 3 ≠ 0 := by
  inspect
/-
Expr.app
  (Expr.app (Expr.app (Expr.const `Ne [Level.succ Level.zero]) (Expr.const `Nat []))
    (Expr.app
      (Expr.app (Expr.app (Expr.const `OfNat.ofNat [Level.zero]) (Expr.const `Nat [])) (Expr.lit (Literal.natVal 3)))
      (Expr.app (Expr.const `instOfNatNat []) (Expr.lit (Literal.natVal 3)))))
  (Expr.app
    (Expr.app (Expr.app (Expr.const `OfNat.ofNat [Level.zero]) (Expr.const `Nat [])) (Expr.lit (Literal.natVal 0)))
    (Expr.app (Expr.const `instOfNatNat []) (Expr.lit (Literal.natVal 0))))
-/

[Damiano Testa]

Kyle, thank you! This is close, and, had I known about it, I would have probably stuck with ExplodeToExpr.

[Damiano Testa]

I think that I prefer inspect, but ExplodeToExpr is good to know!

[Kyle Miller]

(It might be nice to tweak the ToExpr instance to use mkApp* functions. It's a derived instance though, so I'm not sure the best way to do this...)

[Damiano Testa]

(Mostly, my preference is out of aesthetics, the information about proofs is likely rarely relevant for my intended application anyway.)

[Damiano Testa]

As far as I can tell, ToExpr works for several of the other inductives that I would like. For the moment, I will debug with a combination of inspect and ToExpr.

To be fair, it is rare that I need to inspect much more than just the head-symbol, but I still find that displaying the information line-by-line is better suited for my application.