elab a term within a tactic

Stream: lean4

[Thomas Murrills]

This might be a basic question, but let's say I want to define a term elaboration meant to be used within a tactic (in such a way that it depends on the current goals). Is that possible?

I get a type mismatch error when I try to use Tactic.getMainDeclwithin a term elaboration, and a different one if I try to return an Expr within a tactic elab. (Can monad lifting can help out here somehow? Or do I need a different type of elaboration?)

[Jannis Limperg]

MetaM lifts into TermElabM lifts into TacticM. To use a TermElabM computation which depends on the current goals, you'll have to use getGoals first and pass this to the TermElabM computation (which gets auto-lifted into TacticM). To lift a MetaM tactic into TacticM, use liftMetaTactic. Does that help?

[Thomas Murrills]

Just to make sure we're on the same page, getGoals has type TacticM (List MVarId), right? If I try to use this within the TermElabM computation, e.g. let goals ← Tactic.getGoals, I get hit with a type mismatch, saying that it should have type TermElabM .... To pass the result to the TermElabM computation, we'd have to be in a TacticM computation "on the outside", right? My problem then is being able to return an expression from the TacticM computation, since it seems like that's fundamentally not what TacticM Unit can do. Unless...is there a way to define a TacticM Expr elaboration somehow?

[Sebastian Ullrich]

Terms and tactics are distinct. A term elaborator cannot depend on the current goal.

[Mario Carneiro]

This cannot be done, and moreover it is a really weird thing to do. The closest approximation would be a tactic with a term argument, which uses a side channel to pass its list of goals to a subterm of the input argument. (squeeze_scope has to do something like this because it passes information about the scope to all nested simp calls.)

[Mario Carneiro]

I think it might help to explain what you want to do (#xy)

[Thomas Murrills]

So, the actual application was just to see if I could "improve on" have_field and, instead of having it have things into the context, be able to simply use something like currentFieldProj in syntax to represent the projection itself. Currently, this would have to read off some metadata from the current goal. (I do wonder if there's a better way to do this, though—something in the environment, maybe?)

I was mostly just trying to see if I could do it for fun/learning/experience—as far as I can tell, have_field isn't used once in mathlib3 :upside_down: (in contrast to refine_struct, which is used occasionally.) Not spending too much time on it, though, since there are other, more useful things to be done... :)