Get Syntax & InfoTree for declaration

Stream: lean4

[Max Nowak 🐉]

Can I obtain the original Syntax and the InfoTree with all the elaborated goodies for a given declaration? I do not want to delaborate an expression, as I might wrap some expressions in marker syntax to fine-tune how the generated typst will look like (e.g. text color).

elab "#typst" n:ident : command => do
  -- get `Syntax` and infoTree for `n`
  -- generate some typst based on that

[Eric Wieser]

What should it return for src#add_right_comm?

[Max Nowak 🐉]

I have not thought that far... I guess just throw an error is fine, or default to the delaborated version? I was going to use this for making a presentation.

[Max Nowak 🐉]

The idea is to have

syntax color := "red" <|> "green"
macro "#text" "(" color ")" "[" t:term "]" : term => return t
def f := 5 + #text(green)[2 * 2]

and then generate typst from that.

[Eric Wieser]

You might find #typst def easier to work with, if you're only applying this to code that is yours

[Eric Wieser]

That way you get the stx:command directly as an argument to your elaborator

[Max Nowak 🐉]

Yeah that is what I have settled on so far. However, then I don't have access to the InfoTree with the elaborated goodies, so I can't generate typst based on semantic information. I can elaborate certain expressions myself via elabTerm, yes, but that feels very hacky.

[Max Nowak 🐉]

I know the information I need exists somewhere, since that is how the language server works. You work in the RequestM monad which has the syntactic document, Snapshots between each command, InfoTree, and so on.

[Max Nowak 🐉]

And I know you add addTermInfo to the InfoTree during elaboration, but I can't figure out how to get stuff from the InfoTree.

[Kim Morrison]

You can't (?) do this from within the document you are trying to extract information from. Instead you need to run a source document (or generally, text) through a frontend.

[Kim Morrison]

e.g. https://github.com/semorrison/lean-training-data/blob/master/TrainingData/Frontend.lean

[Kim Morrison]

I can find you some other examples later if you need them.

[Kyle Miller]

Here's how to get the info trees from within a command. I probably didn't need to reset info trees and restore them, but this guarantees that we're only looking at the info trees from elaborating the inner command.

open Lean Elab Command in
elab "#info " c:command : command => do
  let initInfoTrees ← getResetInfoTrees
  try
    elabCommand c
    let trees ← getInfoTrees
    for tree in trees do
      logInfo m!"{← tree.format}"
  finally
    modify fun st =>
      { st with infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } }


#info
def f (x y : Nat) : Nat := x + y
/-
• command @ ⟨36, 0⟩-⟨36, 32⟩ @ Lean.Elab.Command.elabDeclaration
  • ℕ : Type @ ⟨36, 13⟩-⟨36, 16⟩ @ Lean.Elab.Term.elabIdent
    • [.] Nat : some Sort.{?_uniq.33235} @ ⟨36, 13⟩-⟨36, 16⟩
    • ℕ : Type @ ⟨36, 13⟩-⟨36, 16⟩
  • x (isBinder := true) : ℕ @ ⟨36, 7⟩-⟨36, 8⟩
  • ℕ : Type @ ⟨36, 13⟩-⟨36, 16⟩ @ Lean.Elab.Term.elabIdent
    • [.] Nat : some Sort.{?_uniq.33237} @ ⟨36, 13⟩-⟨36, 16⟩
    • ℕ : Type @ ⟨36, 13⟩-⟨36, 16⟩
  • y (isBinder := true) : ℕ @ ⟨36, 9⟩-⟨36, 10⟩
  • ℕ : Type @ ⟨36, 20⟩-⟨36, 23⟩ @ Lean.Elab.Term.elabIdent
    • [.] Nat : some Sort.{?_uniq.33239} @ ⟨36, 20⟩-⟨36, 23⟩
    • ℕ : Type @ ⟨36, 20⟩-⟨36, 23⟩
  • f (isBinder := true) : ℕ → ℕ → ℕ @ ⟨36, 4⟩-⟨36, 5⟩
  • x (isBinder := true) : ℕ @ ⟨36, 7⟩-⟨36, 8⟩
  • y (isBinder := true) : ℕ @ ⟨36, 9⟩-⟨36, 10⟩
  • x + y : ℕ @ ⟨36, 27⟩-⟨36, 32⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
    • Macro expansion
      x + y
      ===>
      binop% HAdd.hAdd✝ x y
      • x + y : ℕ @ ⟨36, 27⟩†-⟨36, 32⟩† @ Lean.Elab.Term.Op.elabBinOp
        • x + y : ℕ @ ⟨36, 27⟩†-⟨36, 32⟩†
          • [.] HAdd.hAdd✝ : none @ ⟨36, 27⟩†-⟨36, 32⟩†
          • x : ℕ @ ⟨36, 27⟩-⟨36, 28⟩ @ Lean.Elab.Term.elabIdent
            • [.] x : none @ ⟨36, 27⟩-⟨36, 28⟩
            • x : ℕ @ ⟨36, 27⟩-⟨36, 28⟩
          • y : ℕ @ ⟨36, 31⟩-⟨36, 32⟩ @ Lean.Elab.Term.elabIdent
            • [.] y : none @ ⟨36, 31⟩-⟨36, 32⟩
            • y : ℕ @ ⟨36, 31⟩-⟨36, 32⟩
  • f (isBinder := true) : ℕ → ℕ → ℕ @ ⟨36, 4⟩-⟨36, 5⟩
-/

[Kyle Miller]

(By the way, set_option trace.Elab.info true causes infotrees to be dumped in this format. That's not useful for programming — instead you want to work with the info tree objects directly — but I thought I'd mention it.)

[Max Nowak 🐉]

Oh, amazing, this is ideal!

[Max Nowak 🐉]

And that is also very useful to know. Thank you tons!

[Max Nowak 🐉]

The Frontend approach is also very useful to know! Sounds like what I'm trying to do is way more doable than I thought.