How to get unreflected value of declaration from an attribut

Stream: lean4

[Edward Ayers]

I am trying to make an attribute that will run a command after a definition has been made.

def myAttributeImpl : AttributeImpl where
  name := `myattr
  descr := "my attr"
  applicationTime := AttributeApplicationTime.afterCompilation
  add decl stx kind := do
    -- assert that the type of decl is `Nat → String`
    let value ← evalConst (Nat → String) decl
    dbg_trace "hello {value 4}"
    return ()

initialize registerBuiltinAttribute myAttributeImpl

@[myattr]
def myDef : Nat → String
  | x => "from myDef"

In the body of add, I want to be able to get the value safely (evalConst is unsafe) by doing some checks. What's the best way of doing this? It looks like something like this is done in KeyedDeclsAttribute but I couldn't figure it out and it looks like it only works when we have def myDef : C where C is a const.

[Edward Ayers]

I would quite like a solution that works with generic types, eg @[myattr] myDef1 : Nat → Bool, @[myattr] myDef2 : Nat → String, and the body of add will find the α such that value : Nat → α and then find the instance ToString α and run toString $ value 4.

[Sebastian Ullrich]

evalConst(Check) is the way to go, you just have to pinky-swear that you upheld its invariants by putting the call inside of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Util/TermUnsafe.html

[Wojciech Nawrocki]

Sebastian Ullrich said:

evalConst(Check) is the way to go, you just have to pinky-swear that you upheld its invariants by putting the call inside of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Util/TermUnsafe.html

How would you evalConst something that belongs to a family of types? In this case it looks like we would have to evalConst (Nat → Bool) in one case, evalConst (Nat → String) in another, etc.

[Sebastian Ullrich]

Ah, I was completely focused on the safety! Then you'll probably want to first compose that with toString into an Expr of type Nat -> String (or just String if you put the 4 into the term as well), put that in a new (temporary) declaration, compile it, and finally evaluate it.

[Edward Ayers]

@Sebastian Ullrich how you would finish implementing this:

import Lean.Meta
import Lean.Server.Rpc
import Lean.Elab.Term
open Lean Meta Elab Term System Server Tactic

def rpcAttributeImpl : AttributeImpl where
  name := `rpc
  descr := "Marks a function as a Lean server RPC method."
  applicationTime := AttributeApplicationTime.afterCompilation
  add decl stx kind := do
    let t ← MetaM.run' $ TermElabM.run' do
      let a ← Lean.Elab.Term.elabTerm `(registerRpcProcedure $(quote decl) _ _ $decl) none
      return a
    -- run t as a CoreM Unit here?
    return ()

[Edward Ayers]

Maybe the answer is "you shouldn't use attributes for this".

[Edward Ayers]

I've now done this as a command macro instead because I couldn't get it working in an attribute:

syntax "register_rpc" ident : command
macro_rules
  | `(register_rpc $decl) => `(#eval Lean.Server.registerRpcProcedure $(quote decl.getId) _ _ $decl )

[Mario Carneiro]

import Lean
import Mathlib.Util.Eval
import Mathlib.Util.TermUnsafe

open Lean Server Meta Elab Term

def myhandler (a : Nat) : RequestM (RequestTask Int) := pure $ Task.pure $ pure 0

#eval show CoreM Unit from do
  let decl := ``myhandler
  let cmd ← MetaM.run' <| TermElabM.run' <| withoutModifyingEnv <| unsafe
    Mathlib.Eval.evalTerm (CoreM Unit) (mkApp (mkConst ``CoreM) (mkConst ``Unit))
      (← `(registerRpcProcedure $(quote decl) _ _ $(mkIdent decl)))
  cmd

[Edward Ayers]

evalTerm +1 +1 +1 +1

[Edward Ayers]

I got it working thanks to liftCommandElabM

import Mathlib.Tactic.Ext
open Lean

macro "register_rpc" decl:ident : command => `(#eval Lean.Server.registerRpcProcedure $(quote decl.getId) _ _ $decl )

def rpcAttributeImpl : AttributeImpl where
  name := `rpc
  descr := "Marks a function as a Lean server RPC method."
  applicationTime := AttributeApplicationTime.afterCompilation
  add decl stx kind := do
    Mathlib.Tactic.Ext.liftCommandElabM <| Elab.Command.elabCommand <| ← `(register_rpc $(mkIdent decl))
    return ()

initialize registerBuiltinAttribute rpcAttributeImpl