InfoTree with ContextInfo from liftTermElabM

Stream: metaprogramming / tactics

[Max Nowak 🐉]

I want to elaborate a term t and access its ti : TermInfo, and be able to ti.runMetaM. It seems like no context is saved in this case. Or, more likely, I do not know the go-to way of giving it the root context.

def printTrees : CoreM Unit := do for t in (<- getInfoTrees) do logInfo m!"{<- t.format}"

elab "#foo" t:term : command => do
  liftTermElabM do
    let e <- elabTerm t none
    printTrees

#foo 123 -- prints `• <context-not-available>`

[Aaron Liu]

Why do you want to do this?

[Max Nowak 🐉]

I'm making a small typst DSL, and want to be able to have a command like #typst[And therefore {x * 2 = 5}] which contains lean terms. I want to elaborate these lean terms and render them in a nice way as typst, for this I match on the syntax and get the term info from the infotree.

[Max Nowak 🐉]

There is InfoTree.findInfo?, but it does not give you the ContextInfo.

[Thomas Murrills]

The context node is actually missing here because the infostate has been reset (and saved) by liftTermElabM. The new infotrees are saved inside a fresh context node by liftTermElabM when it finishes. EDIT: rewording!

[Max Nowak 🐉]

I suppose the proper solution would be to add a .context InfoTree node myself, right after the liftTermElabM?

[Thomas Murrills]

(I've edited my message a bit to be more accurate!) The context should already be saved when outside of liftTermElabM; if you change the type signature of printTrees to be in CommandElabM, you should see the trees without any issue. Does doing this afterwards in CommandElabM work for you?

[Max Nowak 🐉]

Ohhhh! That explains a lot. Lemme see if that'll work for what I'm doing.

[Thomas Murrills]

(Note also that I think liftCoreM does something similar, because liftCoreM printTreesout in CommandElabM after liftTermElabM doesn't seem to show any infotrees. :sweat_smile:)

[Max Nowak 🐉]

I don't think that will work, since I will have a sequence of interleaved and potentially nested typst and lean. #[Hello {x * #text(red)[123]} is just {3}.], so when I start looking at the word "is", I already want to have finished processing the stuff before.

[Max Nowak 🐉]

I could make it work anyhow, but it would be very different from the code I have so far.

[Thomas Murrills]

Hmmm, interesting...I wonder if the right solution is to create your own context nodes, or just to grab the state you need directly from the TermElabM monad in order to run MetaM (if that's your primary goal).

[Aaron Liu]

looks like you can get some command context info with docs#Lean.Elab.CommandContextInfo.save

[Thomas Murrills]

You also might be able to wrap your elabTerm in withSaveInfoContext—that's what liftTermElabM does ultimately (and relies on docs#Lean.Elab.CommandContextInfo.save as a component)

[Thomas Murrills]

Testing it, it seems like withSaveInfoContext works; but I actually still wonder if maybe there's a better approach in general? What information are you getting from the infotree that you don't have in the course of elaboration itself already?

[Max Nowak 🐉]

If I have a stx : Term which is a function application with a bunch of implicit arguments, I can elaborate it and obtain the Expr equivalent, that works, sure. But now I want to generate typst from this, and for example hide the implicit arguments. Or I want to distinguish @f 1 2 from f 2, which elaborate to the same expression, but should render differently to typst. So looking at the Expr is not enough, I need to look at the original Syntax. And I am using InfoTree to associate Syntax with its elaborated Expr.

[Max Nowak 🐉]

Yeah, withSaveInfoContext works! I would not have found this myself, thank you so much!

[Thomas Murrills]

No problem, happy to help! :D

[Max Nowak 🐉]

I have packaged it into as the following, which I am happy with. Just in case anyone finds this thread in the future.

def elabTermAndGetInfoTree (t : Term) (expected : Option Expr := none) : TermElabM (Expr × InfoTree) := withRef t do
  let oldTrees <- getResetInfoTrees -- wipe existing trees
  try
    let e <- withSaveInfoContext do -- https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/InfoTree.20with.20ContextInfo.20from.20liftTermElabM/near/569812053s
      elabTerm t expected
    let trees <- getResetInfoTrees -- should just be the latest one
    if h : trees.size = 1 then
      return ⟨e, trees[0]⟩
    else
      throwError "[elabTermAndGetInfo] somehow got {trees.size} trees instead of 1."
  finally
    modifyInfoState fun s => { s with trees := oldTrees }

Edit: Ah, damn, nevermind, this prevents any infos from getting attached to the term, so that semantic highlighting and on-hover type info break :/.

[Thomas Murrills]

I think that's because you're resetting the infotrees in the end; note that withSaveInfoContext already saves then resets the infotree context, then restores the earlier infotrees afterwards. I'd avoid calling getResetInfoTrees manually and instead rely on withSaveInfoContext; note also that getInfoTrees can let you inspect the size without destroying the trees!

(You can also use withInfoTreeContext/withInfoContext as combinators for resetting/restoring infotrees with new additions, but my suspicion is that you probably don't need to! :grinning_face_with_smiling_eyes:)