presence of decl in env.constants of InfoTree of decl

Stream: metaprogramming / tactics

[llllvvuu]

In the following code, foo is in TreeConstants but not Constants. That is, it is in env.constants of the ctx surrounding the InfoTree, but it is not in the getEnv when actually doing things in the theorem body.

In particular,

• the getEnv has: foo.match_1, foo.match_1._cstage1
• the InfoTree has: foo.match_1, foo.match_1._cstage1, foo.

What is the reason for this?

(question motivated by repl#66)

import Lean
open Lean Elab Term Command

elab "foo_tac" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let env ← getEnv
    dbg_trace "Constants: {env.constants.map₂.toList.map Prod.fst}"

def indentStr (n : Nat) (s : String) : String :=
  (s.splitOn "\n").foldl (init := "") fun r line => r ++ (List.replicate n ' ').asString ++ line ++ "\n"

partial def printTree : InfoTree → Nat → CommandElabM Unit
  | .context ctx t, indent => do
    if let .commandCtx ctx := ctx then
      dbg_trace indentStr indent s!"TreeConstants: {ctx.env.constants.map₂.toList.map Prod.fst}"
      printTree t (indent + 1)
  | .node i children, indent => do
    dbg_trace indentStr indent s!"{i.stx}"
    children.forM (printTree · (indent + 1))
  | .hole mvarId, indent => do
    dbg_trace indentStr indent s!"{mvarId.name}"

elab "#info " c:command : command => do
  let initInfoTrees ← getResetInfoTrees
  try
    elabCommand c
    let trees ← getInfoTrees
    for tree in trees do
      printTree tree 0
  finally
    modify fun st =>
      { st with infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } }

#info
def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by
  foo_tac
  sorry

[Sebastian Ullrich]

As far as I understood, you are comparing the environment inside the command to the info tree strictly after the command, so I'm not surprised foo is listed only in the latter