declare_config_elab in term elaborator

Stream: metaprogramming / tactics

[Chris Henson]

There's not a monad lift between TacticM and TermElabM, right? So what is the best way to use the function generated by declare_config_elab in a term elaborator?

[Jannis Limperg]

The underlying function of declare_config_elab actually operates in TermElabM; declare_config_elab just requires TacticM for no reason that I can see. (This should perhaps be changed.) So you can easily define a variant that declares config elaborators in TermElabM:

macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command => do
  mkConfigElaborator doc? elabName type (mkCIdent ``TacticM /- ! -/) (mkCIdent ``id) (← `((← read).recover))

[Kyle Miller]

The reason it uses TacticM is the recover flag is only in TacticM. That's used to decide what sort of error recovery should be done if the tactic configuration has errors.

You can see in declare_command_config_elab how you might adapt this to a monad that doesn't have recovery. The TermElabM monad sort of has recovery in the form of errToSorry. It would be nice if "recovery" was a more well-developed concept (for example if there were a typeclass that gave the current recovery state, then declare_config_elab could run in any monad extending CoreM that implemented it).

I'm not remembering exactly why Lean.Elab.Tactic.mkConfigElaborator is private. At least Lean.Elab.Tactic.elabConfig is public...

[Kyle Miller]

Chris Henson said:

There's not a monad lift between TacticM and TermElabM, right?

That's correct, but TacticM is TermElabM with some additional monad transformers wrapped around it. You can use the run functions for these with whatever reader/state objects you want, and it should work. Just think about what you want from error recovery and set recover appropriately. I believe you can use Name.anonymous for the elaborator, and the goals can be [].

[Chris Henson]

Kyle Miller said:

That's correct, but TacticM is TermElabM with some additional monad transformers wrapped around it. You can use the run functions for these with whatever reader/state objects you want, and it should work. Just think about what you want from error recovery and set recover appropriately. I believe you can use Name.anonymous for the elaborator, and the goals can be [].

That works, thanks!