Making a KeyedDeclsAttribute

Stream: metaprogramming / tactics

[Max Nowak 🐉]

Can someone give me a "hello world" example of a custom KeyedDeclsAttribute? So far I have managed to piece together the following, but it still doesn't let me use the attribute.

import Lean
open Lean

syntax (name := greeterAttr) "greeter" : attr

abbrev Greeter := Syntax -> CoreM Bool

unsafe builtin_initialize greeters : KeyedDeclsAttribute Greeter <-
  mkElabAttribute Greeter `builtin_greeter `greeter  .anonymous ``Greeter "greeter" decl_name%

And then in another file:

@[greeter] -- unknown attribute `greeterAttr`
def hello : Greeter := ...

[Aaron Liu]

maybe don't use builtin initialize?

[Max Nowak 🐉]

Using initialize instead doesn't help unfortunately.

[Aaron Liu]

I'll try take a look at the code

[Aaron Liu]

wow I can't tell if this is supposed to be used

[Aaron Liu]

reading the docs really gives the impression it's only for builtin attributes

[Robin Arnez]

your `greeter might need to be a ``greeterAttr

[Robin Arnez]

and yes, definitely not builtin_initialize

[Robin Arnez]

that's for bootstrapping stuff

[Patrick Massot]

KeyedDeclsAttribute does not appear anywhere in Mathlib. This is a very bad omen.

[Max Nowak 🐉]

With ''greeterAttr I now get "Unexpected attribute argument" when using the attribute. At least that's a different error message, so, progress!

[Max Nowak 🐉]

How does the @[macro] attribute work? In the Lean compiler source, there is:

unsafe def mkMacroAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Macro) :=
  mkElabAttribute Macro `builtin_macro `macro Name.anonymous `Lean.Macro "macro" ref

builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute decl_name%

Which seems almost exactly like what I'm doing, and yet my version doesn't work :(.

[Robin Arnez]

Well you need to specify an argument. I'll give you a rough idea of how to use elab attributes:

import Lean

open Lean Elab

abbrev Greeter := Syntax → CoreM Bool

declare_syntax_cat greeting

unsafe initialize greeters : KeyedDeclsAttribute Greeter <-
  mkElabAttribute Greeter `builtin_greeter `greeter  .anonymous ``Greeter "greeter" decl_name%

-- idk why core doesn't have this
instance : MonadMacroAdapter CoreM where
  getNextMacroScope := return (← getThe Core.State).nextMacroScope
  setNextMacroScope next := modifyThe Core.State fun s => { s with nextMacroScope := next }

partial def runGreeterFor (stx : Syntax) : CoreM Bool := withRef stx do
  match ← liftMacroM (expandMacroImpl? (← getEnv) stx) with
  | some (_decl, stxNew?) =>
    let stxNew ← liftMacroM <| liftExcept stxNew?
    runGreeterFor stxNew
  | _ =>
    let kind := stx.getKind
    let candidates := greeters.getEntries (← getEnv) kind
    let state ← Core.saveState
    for candidate in candidates do
      try
        return ← candidate.value stx
      catch ex => match ex with
        | .internal id _ =>
          if id == unsupportedSyntaxExceptionId then
            state.restore
          else
            throw ex
        | _ => throw ex
    return false

Other file:

syntax (name := hiThere) "hi!" : greeting

@[greeter hiThere]
public meta def greetHiThere : Greeter
  | `(greeting| hi!) => do
    Lean.logInfo "Hi, there!"
    return true
  | _ => Lean.Elab.throwUnsupportedSyntax

run_meta
  runGreeterFor (← `(greeting| hi!))

[Robin Arnez]

(code adjusted from the definition of elabTerm)

[Max Nowak 🐉]

Is that also using syntax (name := greeterAttr) "greeter" : attr ?

[Robin Arnez]

No, not at all

[Robin Arnez]

We don't define syntax for the attribute

[Robin Arnez]

I think if we did, it would be confused because it already expects a certain builtin attribute syntax

[Robin Arnez]

Now, you probably also want

Basically, code copied from Lean.Elab.ElabRules

open Lean Parser Elab Command Syntax Term
def elabElabRulesGreetingAux (doc? : Option (TSyntax ``docComment))
    (attrs? : Option (TSepArray ``attrInstance ",")) (attrKind : TSyntax ``attrKind)
    (k : SyntaxNodeKind) (alts : Array (TSyntax ``matchAlt)) :
    CommandElabM Syntax := do
  let alts ← alts.mapM fun (alt : TSyntax ``matchAlt) => match alt with
    | `(matchAltExpr| | $pats,* => $rhs) => do
      let pat := pats.elemsAndSeps[0]!
      if !pat.isQuot then
        throwUnsupportedSyntax
      let quoted := getQuotContent pat
      let k' := quoted.getKind
      if checkRuleKind k' k then
        pure alt
      else if k' == choiceKind then
         match quoted.getArgs.find? fun quotAlt => checkRuleKind quotAlt.getKind k with
         | none        => throwErrorAt alt "invalid elab_rules alternative, expected syntax node kind `{k}`"
         | some quoted =>
           let pat := pat.setArg 1 quoted
           let pats := ⟨pats.elemsAndSeps.set! 0 pat⟩
           `(matchAltExpr| | $pats,* => $rhs)
      else
        throwErrorAt alt "invalid elab_rules alternative, unexpected syntax node kind `{k'}`"
    | _ => throwUnsupportedSyntax
  let mkAttrs (kind : Name) : CommandElabM (TSyntaxArray ``attrInstance) := do
    let attr ← `(attrInstance| $attrKind:attrKind $(mkIdent kind):ident $(← mkIdentFromRef k):ident)
    pure <| match attrs? with
      | some attrs => attrs.getElems.push attr
      | none => #[attr]
  let vis := Parser.Command.visibility.ofAttrKind attrKind
  `($[$doc?:docComment]? @[$(← mkAttrs `greeter),*] $vis:visibility
    aux_def elabRules $(mkIdent k) : Greeter :=
    fun stx => match stx with
      $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)

@[command_elab «elab_rules»]
def elabElabRulesGreeting : CommandElab :=
  adaptExpander fun
  | `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind elab_rules (kind := $kind) : greeting $alts:matchAlt*) => do
    elabElabRulesGreetingAux doc? attrs? attrKind (← resolveSyntaxKind kind.getId) alts
  | _ => throwUnsupportedSyntax

so you can do

elab "hi!" : greeting => do
  Lean.logInfo "Hi, there!"
  return true

run_meta
  runGreeterFor (← `(greeting| hi!))

[Max Nowak 🐉]

Oh huh, I was not aware these attributes take an argument. But this actually solves a second issue I was about to have, so that's great!

[Max Nowak 🐉]

So, if I understand it correctly, for example macro_rules generates a @[macro theParser] def ... for every match arm, where theParser is the top level parser of the match arm?

[Max Nowak 🐉]

(or elab_rules, either way)

[Max Nowak 🐉]

All right I think I get it! This is cool! Thanks a lot for the help!