defining notations with an attribute

Stream: metaprogramming / tactics

[Chris Henson]

Is it possible to define a notation with an attribute? As an example I defined this command macro:

import Mathlib
import Lean

syntax "reduce_notation" ident Lean.Parser.Command.notationItem : command
macro_rules
  | `(reduce_notation $rel $sym) =>
    `(
      notation:39 t " ⇢"$sym t' => $rel t t'
      notation:39 t " ↠"$sym t' => Relation.ReflTransGen $rel t t'
      notation:39 t " ≈"$sym t' => Relation.EqvGen $rel t t'
     )

def foo : Nat → Nat → Prop := λ _ _ ↦ False

reduce_notation foo "β"

#check 0 ⇢β 0 -- 0 ⇢β 0 : Prop
#check 0 ↠β 0 -- Relation.ReflTransGen foo 0 0 : Prop
#check 0 ≈β 0 -- Relation.EqvGen foo 0 0 : Prop

Instead of a command, I would want to annotate foo with @[reduce_notation β]. I was not sure if this is possible in the AttrM monad.

[Aaron Liu]

It is possible to do this probably

[Chris Henson]

With the above command definition the following works to assemble a TSyntax `command:

syntax (name := reduce_notation_attr) "reduce_notation" Lean.Parser.Command.notationItem : attr

initialize Lean.registerBuiltinAttribute {
  name := `reduce_notation_attr
  descr := ""
  add := fun decl stx _attrKind =>
    match stx with
    | `(attr | reduce_notation $sym) => do
      let cmd ← `(reduce_notation decl sym)
    | _ => throwUnsupportedSyntax
}

but I don't know how to actually "run" the command from within AttrM.

[Adam Topaz]

I think you can use liftCommandElabM

[Adam Topaz]

Lean.liftCommandElabM

[Chris Henson]

Thanks Adam, that worked. For the benefit of those that come after, here's the full mwe I ended with:

import Mathlib

open Lean Lean.Elab Lean.Elab.Command Lean.Meta

syntax "reduce_notation" ident Lean.Parser.Command.notationItem : command
macro_rules
  | `(reduce_notation $rel $sym) =>
    `(
      notation:39 t " ⇢"$sym t' => $rel t t'
      notation:39 t " ↠"$sym t' => Relation.ReflTransGen $rel t t'
      notation:39 t " ≈"$sym t' => Relation.EqvGen $rel t t'
     )

syntax (name := reduce_notation_attr) "reduce_notation" Lean.Parser.Command.notationItem : attr

initialize Lean.registerBuiltinAttribute {
  name := `reduce_notation_attr
  descr := ""
  add := fun decl stx kind => MetaM.run' do
    let `(attr | reduce_notation $sym) := stx
     | throwError "invalid syntax for 'reduce_notation' attribute"
    let cmd ← `(reduce_notation $(mkIdent decl) $sym)
    liftCommandElabM <| Command.elabCommand cmd
}