How to run CommandElabM in an attribute handler?

Stream: lean4

[Edward Ayers]

Hi I have a CommandElabM α that I want to run in the add method of an AttributeImpl, but it's AttrM = CoreM, is there a lift/run? I found Lean.Elab.Command.liftCoreM : CoreM α → CommandElabM α so I need the co of this.

[Mario Carneiro]

I don't think you can, at least not without fabricating a whole lot of dubious dummy state

[Mario Carneiro]

like what would it mean if you did elabCommand `(namespace Foo) in an attribute?

[Henrik Böving]

Yeah CommandElabM wants to carry around a docs4#Lean.Elab.Command.Context while core only carries a docs4#Lean.Core.Context so you'd have to make up a lot of dummy variables

[Edward Ayers]

Eg you might declare a definition with an attribute and then run some commands afterwards

[Edward Ayers]

I guess you could do it all as a custom command and then add the attribute in the custom command

[Edward Ayers]

having it as an attribute seemed nicer but I'm ok with that

[Mario Carneiro]

you can create definitions from CoreM, just not through elabCommand

[Edward Ayers]

Ok let me just say what the concrete problem is: at the moment if you want to register an RPC you have to run a command like

#eval (do
  registerRpcProcedure
    `myHandler
    α
    β
    myHandler
  : CoreM Unit)

where myHandler : α → RequestM (ResponseTask β) for some fixed α, β. I was having a go at writing an attribute @[rpc] that you stick in front of myHandler that would do this. The simplest way seems to be to have a quoted command and then run it. Because if you try to do it in CoreM you end up needing evalExpr. Maybe the way is to do a termElab on the do block and then evalExpr.

But now I am thinking that doing this with an attribute is just wrong and it should be a command macro.

[Mario Carneiro]

If registerRpcProcedure is in CoreM then what's the problem? You can just call that function directly from AttrM

[Mario Carneiro]

you only need evalExpr if either α or β is supplied from the input syntax to the attribute itself

[Mario Carneiro]

you can also run evalConst in CoreM

[Edward Ayers]

The problem with calling registerRpcProcedure directly is you don't know the types α, β (you can get them as Exprs with some faff but still need to unreflect them) so you can't get an unreflected myHandler. Also registerRpcProcedure needs to synthesize a load of typeclass instances on α and β.

[Edward Ayers]

(by the way I have no idea if 'unreflect' is the appropriate terminology, maybe 'unquote'?)