TacticCodeAction

Stream: std4

[Patrick Massot]

When defining a TacticCodeAction I get access to (param : CodeActionParams) (snap : Snapshot) (ctx : ContextInfo) (stack : Syntax.Stack) (node : InfoTree) and need to produce something in RequestM. More specifically, the lazy? field will work in IO. The question is: how to access the current goal? In this case I know node will give me info : TacticInfo and I have info.goalsBefore that a list of MVarId. I know I also have ctx.runMetaM but I don't know where to find a LocalContextto feed to that function. For instance how to write a code action that will simply take the current goal and output 'show ... where ...` is the current goal (approximately) as displayed in the infoview.

[Scott Morrison]

I haven't look at this recently, but you might see what I did in #4109 (hooking up exact? to every sorry).

[Patrick Massot]

Sorry, I got distracted. In your case you get a TermInfo and not a TacticInfo so you do have a local context right there. I'm sure I can get one too, I just don't know where.

[Jannis Limperg]

Presumably the first MVarId in goalsBefore represents the current goal. You can get its local context with mvarId.getLCtx.

[Patrick Massot]

This function doesn't seem to exist.

[Patrick Massot]

There is a globally defined getLCtx function but it requires to be already in a monad providing a context.

[Patrick Massot]

There is no way I'll be able to magically get a local context from a MVarId since a MVarId simply stores a name. The context has to come from somewhere else, this is why I wrote that long message listing everything I have floating around.

[Patrick Massot]

@Mario Carneiro any hint for me?

[Jannis Limperg]

Ah, sorry. You can do mvarId.withContext do getLCtx or (<- mvarId.getDecl).lctx.

While an MVarId is just a name, the metavariable context always associates this name with a MetavarDecl containing a local context, the target type and additional metadata. getDecl obtains this information.

[Patrick Massot]

Again all those suggestions assume I'm already in a monad who knows more stuff than what IO does.

[Patrick Massot]

Forget about it, Kyle helped me.

[Kyle Miller]

If ctx : ContextInfo and goal : MVarId then it's

ctx.runMetaM {} do
  goal.withContext do
    -- ... now you have the local context of the goal ...

[Kyle Miller]

ctx.runMetaM sort of bootstraps the MetaM monad by giving you a metavariable context, and that lets goal.withContext find its local context and local instances