From 43284cc5fa57be0e0df4a0ba3db458939234cfde Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Dec 2020 09:09:00 -0800
Subject: [PATCH] feat: improve notation for setting parser names and
 priorities

---
 src/Lean/Elab/Syntax.lean                  | 162 +++++++++++----------
 src/Lean/Parser/Syntax.lean                |  23 +--
 tests/lean/macroPrio.lean                  |   4 +-
 tests/lean/parserPrio.lean                 |   6 +-
 tests/lean/resolveGlobalName.lean          |   2 +-
 tests/lean/run/175.lean                    |   2 +-
 tests/lean/run/CommandExtOverlap.lean      |   2 +-
 tests/lean/run/balg.lean                   |   2 +-
 tests/lean/run/choiceExpectedTypeBug.lean  |   2 +-
 tests/lean/run/choiceMacroRules.lean       |   4 +-
 tests/lean/run/doNotation1.lean            |   2 +-
 tests/lean/run/infixprio.lean              |   2 +-
 tests/lean/run/localParsers.lean           |   4 +-
 tests/lean/run/prioDSL.lean                |   8 +-
 tests/lean/run/scopedParsers.lean          |   2 +-
 tests/lean/run/stxKindInsideNamespace.lean |   2 +-
 tests/lean/run/syntaxPrio.lean             |   2 +-
 tests/lean/run/tacticExtOverlap.lean       |   2 +-
 tests/lean/run/termParserAttr.lean         |   2 +-
 tests/lean/run/unifhint3.lean              |   4 +-
 tests/lean/scopedunifhint.lean             |   2 +-
 tests/lean/syntaxInNamespacesAndPP.lean    |   2 +-
 22 files changed, 124 insertions(+), 119 deletions(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 7fbfe86699..a8457eda5e 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -230,23 +230,20 @@ where
     | Name.str _ s _ => s ++ str
     | _ => str
 
-private def elabKindPrio (stx : Syntax) (catName : Name) : CommandElabM (Option Name × Nat) := do
+
+def expandOptNamedPrio (stx : Syntax) : MacroM Nat :=
   if stx.isNone then
-    pure (none, evalPrio! default)
-  else
-    let arg := stx[1]
-    if arg.getKind == `Lean.Parser.Command.parserKind then
-      let k := arg[0].getId
-      pure (k, evalPrio! default)
-    else if arg.getKind == `Lean.Parser.Command.parserPrio then
-      let prio ← liftMacroM <| evalPrio arg[0]
-      pure (none, prio)
-    else if arg.getKind == `Lean.Parser.Command.parserKindPrio then
-      let k := arg[0].getId
-      let prio ← liftMacroM <| evalPrio arg[2]
-      pure (k, prio)
-    else
-      throwError "unexpected syntax kind/priority"
+    return evalPrio! default
+  else match stx[0] with
+    | `(Parser.Command.namedPrio| (priority := $prio)) => evalPrio prio
+    | _ => Macro.throwUnsupported
+
+def expandOptNamedName (stx : Syntax) : MacroM (Option Name) := do
+  if stx.isNone then
+    return none
+  else match stx[0] with
+    | `(Parser.Command.namedName| (name := $name)) => return name.getId
+    | _ => Macro.throwUnsupported
 
 /- We assume a new syntax can be treated as an atom when it starts and ends with a token.
    Here are examples of atom-like syntax.
@@ -268,29 +265,27 @@ private partial def isAtomLikeSyntax (stx : Syntax) : Bool :=
     kind == `Lean.Parser.Syntax.atom
 
 /-
-def «syntax»      := parser! attrKind >> "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident
+def «syntax»      := parser! attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
 -/
 @[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
   let env ← getEnv
   let attrKind ← toAttributeKind stx[0]
-  let cat      := stx[6].getId.eraseMacroScopes
+  let cat      := stx[7].getId.eraseMacroScopes
   unless (Parser.isParserCategory env cat) do
-    throwErrorAt! stx[6] "unknown category '{cat}'"
-  let syntaxParser := stx[4]
+    throwErrorAt! stx[7] "unknown category '{cat}'"
+  let syntaxParser := stx[5]
   -- If the user did not provide an explicit precedence, we assign `maxPrec` to atom-like syntax and `leadPrec` otherwise.
   let precDefault  := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec
   let prec := (← liftMacroM (Term.expandOptPrecedence stx[2])).getD precDefault
-  let (kind?, prio) ← elabKindPrio stx[3] cat
-  let kind ← match kind? with
-    | some kind => pure kind
-    | none      => mkNameFromParserSyntax cat syntaxParser
-  /-
-    The declaration name and the syntax node kind should be the same.
-    We are using `def $kind ...`. So, we must append the current namespace to create the name fo the Syntax `node`. -/
-  let stxNodeKind := (← getCurrNamespace) ++ kind
+  let name ←
+    match (← liftMacroM <| expandOptNamedName stx[3]) with
+    | some name => pure name
+    | none => mkNameFromParserSyntax cat syntaxParser
+  let prio ← liftMacroM <| expandOptNamedPrio stx[4]
+  let stxNodeKind := (← getCurrNamespace) ++ name
   let catParserId := mkIdentFrom stx (cat.appendAfter "Parser")
   let (val, trailingParser) ← runTermElabM none fun _ => Term.toParserDescr syntaxParser cat
-  let declName := mkIdentFrom stx kind
+  let declName := mkIdentFrom stx name
   let d ←
     match trailingParser, attrKind with
     | true, AttributeKind.global =>
@@ -385,13 +380,17 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
   withAttrKindGlobal stx fun stx => do
     match stx with
-    | `(infix $[: $prec]? $[[$prio]]? $op => $f)   => `(infixl $[: $prec]? $[[$prio]]? $op => $f)
-    | `(infixr $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
-    | `(infixl $[: $prec]? $[[$prio]]? $op => $f)  =>
+    | `(infix $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
+      `(infixl $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f)
+    | `(infixr $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
+      `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
+    | `(infixl $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
        let prec1 := quote <| (← evalOptPrec prec) + 1
-       `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
-    | `(prefix $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? $op:strLit arg $[: $prec]? => $f arg)
-    | `(postfix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? arg $op:strLit => $f arg)
+       `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
+    | `(prefix $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
+       `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op:strLit arg $[: $prec]? => $f arg)
+    | `(postfix $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
+      `(notation $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? arg $op:strLit => $f arg)
     | _ => Macro.throwUnsupported
 where
   -- set "global" `attrKind`, apply `f`, and restore `attrKind` to result
@@ -457,12 +456,15 @@ def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandEla
        | _        => throw ())
 
 private def expandNotationAux (ref : Syntax)
-    (currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
+    (currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
   let prio ← liftMacroM <| evalOptPrio prio?
   -- build parser
   let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
   let cat := mkIdentFrom ref `term
-  let kind ← mkNameFromParserSyntax `term (mkNullNode syntaxParts)
+  let name ←
+    match name? with
+    | some name => pure name.getId
+    | none => mkNameFromParserSyntax `term (mkNullNode syntaxParts)
   -- build macro rules
   let vars := items.filter fun item => item.getKind == `Lean.Parser.Command.identPrec
   let vars := vars.map fun var => var[0]
@@ -470,12 +472,12 @@ private def expandNotationAux (ref : Syntax)
   let patArgs ← items.mapM expandNotationItemIntoPattern
   /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
-  let fullKind := currNamespace ++ kind
-  let pat := Syntax.node fullKind patArgs
+  let fullName := currNamespace ++ name
+  let pat := Syntax.node fullName patArgs
   let stxDecl ← match attrKind with
-    | AttributeKind.global => `(syntax $[: $prec?]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
-    | AttributeKind.scoped => `(scoped syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
-    | AttributeKind.local  => `(local syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
+    | AttributeKind.global => `(syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):numLit) $[$syntaxParts]* : $cat)
+    | AttributeKind.scoped => `(scoped syntax $[: $prec? ]? (name := $(mkIdent name)) (priority := $(quote prio):numLit) $[$syntaxParts]* : $cat)
+    | AttributeKind.local  => `(local syntax $[: $prec? ]? (name := $(mkIdent name)) (priority := $(quote prio):numLit) $[$syntaxParts]* : $cat)
   let macroDecl ← `(macro_rules | `($pat) => `($qrhs))
   match (← mkSimpleDelab vars pat qrhs |>.run) with
   | some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
@@ -487,7 +489,8 @@ private def expandNotationAux (ref : Syntax)
     let stx := stx.setArg 0 mkAttrKindGlobal
     let currNamespace ← getCurrNamespace
     match stx with
-    | `(notation $[: $prec? ]? $[[ $prio? ]]? $items* => $rhs) => expandNotationAux stx currNamespace attrKind prec? prio? items rhs
+    | `(notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) =>
+      expandNotationAux stx currNamespace attrKind prec? name? prio? items rhs
     | _ => throwUnsupportedSyntax
 
 /- Convert `macro` argument into a `syntax` command item -/
@@ -519,40 +522,39 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := do
   where mkSplicePat kind id suffix :=
     mkNullNode #[mkAntiquotSuffixSpliceNode kind (mkAntiquotNode id) suffix]
 
-def expandOptPrio (stx : Syntax) : MacroM Nat :=
-  if stx.isNone then
-    return evalPrio! default
-  else
-    evalPrio stx[1]
 
+/- «macro» := parser! suppressInsideQuot ("macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail) -/
 def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
   let prec := stx[1].getOptional?
-  let prio ← liftMacroM <| expandOptPrio stx[2]
-  let head := stx[3]
-  let args := stx[4].getArgs
-  let cat  := stx[6]
+  let name? ← liftMacroM <| expandOptNamedName stx[2]
+  let prio  ← liftMacroM <| expandOptNamedPrio stx[3]
+  let head := stx[4]
+  let args := stx[5].getArgs
+  let cat  := stx[7]
   -- build parser
   let stxPart  ← liftMacroM <| expandMacroArgIntoSyntaxItem head
   let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem
   let stxParts := #[stxPart] ++ stxParts
-  -- kind
-  let kind ← mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
+  -- name
+  let name ← match name? with
+    | some name => pure name
+    | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
   -- build macro rules
   let patHead ← liftMacroM <| expandMacroArgIntoPattern head
   let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern
   /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
-  let pat := Syntax.node (currNamespace ++ kind) (#[patHead] ++ patArgs)
-  if stx.getArgs.size == 9 then
+  let pat := Syntax.node (currNamespace ++ name) (#[patHead] ++ patArgs)
+  if stx.getArgs.size == 10 then
     -- `stx` is of the form `macro $head $args* : $cat => term`
-    let rhs := stx[8]
+    let rhs := stx[9]
     -- NOTE: can't use `$stxParts*` here because it would interpret as a single antiquotation with the `stx` star postfix operator
-    `(syntax $(prec)? [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $[$stxParts]* : $cat
+    `(syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat
       macro_rules | `($pat) => $rhs)
   else
     -- `stx` is of the form `macro $head $args* : $cat => `( $body )`
-    let rhsBody := stx[9]
-    `(syntax $(prec)? [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $[$stxParts]* : $cat
+    let rhsBody := stx[10]
+    `(syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat
       macro_rules | `($pat) => `($rhsBody))
 
 @[builtinCommandElab «macro»] def elabMacro : CommandElab :=
@@ -570,54 +572,56 @@ builtin_initialize
 
 /-
 def elabTail := try (" : " >> ident) >> darrow >> termParser
-parser! "elab " >> optPrecedence >> optPrio >> elabHead >> many elabArg >> elabTail
+def «elab» := parser! suppressInsideQuot ("elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
 -/
 def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
   let ref := stx
   let prec    := stx[1].getOptional?
-  let prio    ←  liftMacroM <| expandOptPrio stx[2]
-  let head    := stx[3]
-  let args    := stx[4].getArgs
-  let cat     := stx[6]
-  let expectedTypeSpec := stx[7]
-  let rhs     := stx[9]
+  let name?   ← liftMacroM <| expandOptNamedName stx[2]
+  let prio    ← liftMacroM <| expandOptNamedPrio stx[3]
+  let head    := stx[4]
+  let args    := stx[5].getArgs
+  let cat     := stx[7]
+  let expectedTypeSpec := stx[8]
+  let rhs     := stx[10]
   let catName := cat.getId
   -- build parser
   let stxPart  ← liftMacroM <| expandMacroArgIntoSyntaxItem head
   let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem
   let stxParts := #[stxPart] ++ stxParts
-  -- kind
-  let kind ← mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
+  -- name
+  let name ← match name? with
+    | some name => pure name
+    | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
   -- build pattern for `martch_syntax
   let patHead ← liftMacroM <| expandMacroArgIntoPattern head
   let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern
-  let pat := Syntax.node (currNamespace ++ kind) (#[patHead] ++ patArgs)
-  let kindId    := mkIdentFrom ref kind
+  let pat := Syntax.node (currNamespace ++ name) (#[patHead] ++ patArgs)
   if expectedTypeSpec.hasArgs then
     if catName == `term then
       let expId := expectedTypeSpec[1]
-      `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
-        @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
+      `(syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat
+        @[termElab $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Term.TermElab :=
         fun stx expectedType? => match stx with
           | `($pat) => Lean.Elab.Command.withExpectedType expectedType? fun $expId => $rhs
           | _ => throwUnsupportedSyntax)
     else
       throwErrorAt! expectedTypeSpec "syntax category '{catName}' does not support expected type specification"
   else if catName == `term then
-    `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
-      @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
+    `(syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat
+      @[termElab $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Term.TermElab :=
       fun stx _ => match stx with
         | `($pat) => $rhs
         | _ => throwUnsupportedSyntax)
   else if catName == `command then
-    `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
-      @[commandElab $kindId:ident] def elabFn : Lean.Elab.Command.CommandElab :=
+    `(syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat
+      @[commandElab $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Command.CommandElab :=
       fun
         | `($pat) => $rhs
         | _ => throwUnsupportedSyntax)
   else if catName == `tactic then
-    `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
-      @[tactic $kindId:ident] def elabFn : Lean.Elab.Tactic.Tactic :=
+    `(syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat
+      @[tactic $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Tactic.Tactic :=
       fun
         | `(tactic|$pat) => $rhs
         | _ => throwUnsupportedSyntax)
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index fef3d7a624..09678854ff 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -50,7 +50,10 @@ end Term
 
 namespace Command
 
-def optPrio   := optional ("[" >> priorityParser >> "]")
+def namedPrio := parser! (atomic ("(" >> nonReservedSymbol "priority") >> " := " >> priorityParser >> ")")
+def namedName := parser! (atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")")
+def optNamedPrio := optional namedPrio
+def optNamedName := optional namedName
 
 def «prefix»   := parser! "prefix"
 def «infix»    := parser! "infix"
@@ -58,19 +61,17 @@ def «infixl»   := parser! "infixl"
 def «infixr»   := parser! "infixr"
 def «postfix»  := parser! "postfix"
 def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
-@[builtinCommandParser] def «mixfix»   := parser! Term.attrKind >> mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser
+@[builtinCommandParser] def «mixfix»   := parser! Term.attrKind >> mixfixKind >> optPrecedence >> optNamedName >> optNamedPrio >> ppSpace >> strLit >> darrow >> termParser
 -- NOTE: We use `suppressInsideQuot` in the following parsers because quotations inside them are evaluated in the same stage and
 -- thus should be ignored when we use `checkInsideQuot` to prepare the next stage for a builtin syntax change
 def identPrec  := parser! ident >> optPrecedence
+
 def optKind : Parser := optional ("[" >> ident >> "]")
+
 def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
-@[builtinCommandParser] def «notation»    := parser! Term.attrKind >> "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser
-@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts)
-def parserKind     := parser! ident
-def parserPrio     := parser! priorityParser
-def parserKindPrio := parser! atomic (ident >> ", ") >> priorityParser
-def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserPrio <|> parserKind) >> "]")
-@[builtinCommandParser] def «syntax»      := parser! Term.attrKind >> "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident
+@[builtinCommandParser] def «notation»    := parser! Term.attrKind >> "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
+@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >>  optKind >> Term.matchAlts)
+@[builtinCommandParser] def «syntax»      := parser! Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
 @[builtinCommandParser] def syntaxAbbrev  := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
 @[builtinCommandParser] def syntaxCat     := parser! "declare_syntax_cat " >> ident
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
@@ -80,13 +81,13 @@ def macroTailTactic   : Parser := atomic (" : " >> identEq "tactic") >> darrow >
 def macroTailCommand  : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
 def macroTailDefault  : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
-@[builtinCommandParser] def «macro»       := parser! suppressInsideQuot ("macro " >> optPrecedence >> optPrio >> macroHead >> many macroArg >> macroTail)
+@[builtinCommandParser] def «macro»       := parser! suppressInsideQuot ("macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail)
 
 @[builtinCommandParser] def «elab_rules» := parser! suppressInsideQuot ("elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts)
 def elabHead := macroHead
 def elabArg  := macroArg
 def elabTail := atomic (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> termParser
-@[builtinCommandParser] def «elab»       := parser! suppressInsideQuot ("elab " >> optPrecedence >> optPrio >> elabHead >> many elabArg >> elabTail)
+@[builtinCommandParser] def «elab»       := parser! suppressInsideQuot ("elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
 
 end Command
 
diff --git a/tests/lean/macroPrio.lean b/tests/lean/macroPrio.lean
index ccd8ef0a92..6ff84b47d8 100644
--- a/tests/lean/macroPrio.lean
+++ b/tests/lean/macroPrio.lean
@@ -12,7 +12,7 @@ macro "foo!" x:term:max : term => `($x * 2)
 #check foo! 1 -- ambiguous
 
 -- macro with higher priority
-macro [high] "foo!" x:term:max : term => `($x - 2)
+macro (priority := high) "foo!" x:term:max : term => `($x - 2)
 
 #check foo! 2
 
@@ -20,7 +20,7 @@ theorem ex2 : foo! 2 = 0 :=
   rfl
 
 -- Define elaborator with even higher priority
-elab [high+1] "foo!" x:term:max : term <= expectedType =>
+elab (priority := high+1) "foo!" x:term:max : term <= expectedType =>
   Lean.Elab.Term.elabTerm x expectedType
 
 theorem ex3 : foo! 3 = 3 :=
diff --git a/tests/lean/parserPrio.lean b/tests/lean/parserPrio.lean
index 625a149be1..34e7be1fd7 100644
--- a/tests/lean/parserPrio.lean
+++ b/tests/lean/parserPrio.lean
@@ -1,7 +1,7 @@
 --
 
 -- New notation that overlaps with existing notation
-syntax [myPair, high] "(" term "," term ")" : term
+syntax (name := myPair) (priority := high) "(" term "," term ")" : term
 
 macro_rules[myPair]
 | `(($a, $b)) => `([$a, $b])
@@ -18,7 +18,7 @@ macro_rules
 
 #eval (1, 2, 3)
 
-syntax [mySingleton] "[" term "]" : term
+syntax (name := mySingleton) "[" term "]" : term
 
 macro_rules[mySingleton]
 | `([$a]) => `(2 * $a)
@@ -26,7 +26,7 @@ macro_rules[mySingleton]
 #check [1] -- ambiguous it can be `mySingleton` or the singleton list
 
 
-syntax [100] "(" term "," term ", " term ")" : term -- priority without a kind
+syntax (priority := 100) "(" term "," term ", " term ")" : term -- priority without a kind
 
 macro_rules
 | `(($a, $b, $c)) => `([$a, $b, $c])
diff --git a/tests/lean/resolveGlobalName.lean b/tests/lean/resolveGlobalName.lean
index 07fa54e1a8..4218a786dc 100644
--- a/tests/lean/resolveGlobalName.lean
+++ b/tests/lean/resolveGlobalName.lean
@@ -14,7 +14,7 @@ open Lean
 open Lean.Elab.Term
 open Lean.Elab.Command
 
-syntax[resolveKind] "#resolve " ident : command
+syntax (name := resolveKind) "#resolve " ident : command
 
 @[commandElab resolveKind] def elabResolve : CommandElab :=
 fun stx => liftTermElabM none do
diff --git a/tests/lean/run/175.lean b/tests/lean/run/175.lean
index b5353fb7a7..e78a4bb1de 100644
--- a/tests/lean/run/175.lean
+++ b/tests/lean/run/175.lean
@@ -4,7 +4,7 @@ import Lean
 namespace Foo
 open Lean.Elab.Term
 
-syntax[fooKind] "foo!" term : term
+syntax (name := fooKind) "foo!" term : term
 
 @[termElab fooKind] def elabFoo : TermElab :=
 fun stx expectedType? => elabTerm (stx.getArg 1) expectedType?
diff --git a/tests/lean/run/CommandExtOverlap.lean b/tests/lean/run/CommandExtOverlap.lean
index 233ac89bb0..312a801efc 100644
--- a/tests/lean/run/CommandExtOverlap.lean
+++ b/tests/lean/run/CommandExtOverlap.lean
@@ -1,4 +1,4 @@
-syntax [mycheck] "#check" sepBy(term, ",") : command
+syntax (name := mycheck) "#check" sepBy(term, ",") : command
 
 open Lean
 
diff --git a/tests/lean/run/balg.lean b/tests/lean/run/balg.lean
index 82cb4886bb..0110088893 100644
--- a/tests/lean/run/balg.lean
+++ b/tests/lean/run/balg.lean
@@ -14,7 +14,7 @@ abbrev mul {M : Magma} (a b : M) : M :=
 
 set_option pp.all true
 
-infix:70 [high] "*" => mul
+infix:70 (priority := high) "*" => mul
 
 structure Semigroup extends Magma where
   mul_assoc (a b c : α) : a * b * c = a * (b * c)
diff --git a/tests/lean/run/choiceExpectedTypeBug.lean b/tests/lean/run/choiceExpectedTypeBug.lean
index 1137207df4..490925dcfd 100644
--- a/tests/lean/run/choiceExpectedTypeBug.lean
+++ b/tests/lean/run/choiceExpectedTypeBug.lean
@@ -13,7 +13,7 @@ rfl
 
 #check f
 
-syntax [emptyS] "⟨" "⟩"  : term -- overload `⟨ ⟩` notation
+syntax (name := emptyS) "⟨" "⟩"  : term -- overload `⟨ ⟩` notation
 
 open Lean
 open Lean.Elab
diff --git a/tests/lean/run/choiceMacroRules.lean b/tests/lean/run/choiceMacroRules.lean
index fd3eb63705..197c206168 100644
--- a/tests/lean/run/choiceMacroRules.lean
+++ b/tests/lean/run/choiceMacroRules.lean
@@ -1,5 +1,5 @@
-syntax:65 [myAdd1] term "+++" term:65 : term
-syntax:65 [myAdd2] term "+++" term:65 : term
+syntax:65 (name := myAdd1) term "+++" term:65 : term
+syntax:65 (name := myAdd2) term "+++" term:65 : term
 
 macro_rules [myAdd1]
 | `($a +++ $b) => `(Nat.add $a $b)
diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index 467d50c559..41228deb6d 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -92,7 +92,7 @@ if x > 10 then pure x else pure none
 def tst6 (x : Nat) : StateT Nat IO (Option Nat) :=
 if x > 10 then g x else pure none
 
-syntax:max [doHash] "#" : term
+syntax:max (name := doHash) "#" : term
 
 partial def expandHash : Syntax → StateT Bool MacroM Syntax
 | Syntax.node k args =>
diff --git a/tests/lean/run/infixprio.lean b/tests/lean/run/infixprio.lean
index 76ed1056e6..ef882389fa 100644
--- a/tests/lean/run/infixprio.lean
+++ b/tests/lean/run/infixprio.lean
@@ -2,7 +2,7 @@ def f (x y : Nat) : Nat :=
   x + 2*y
 
 -- "+" with priority higher than the builtin "+" notation
-infix:65 [high] "+" => f
+infix:65 (priority := high) "+" => f
 
 #check 1 + 2
 
diff --git a/tests/lean/run/localParsers.lean b/tests/lean/run/localParsers.lean
index f0d841c92f..a057428f7a 100644
--- a/tests/lean/run/localParsers.lean
+++ b/tests/lean/run/localParsers.lean
@@ -2,7 +2,7 @@ def f (x y : Nat) := x + 2*y
 
 namespace Foo
 
-local infix:65 [high] "+" => f
+local infix:65 (priority := high) "+" => f
 
 theorem ex1 (x y : Nat) : x + y = f x y := rfl
 
@@ -21,7 +21,7 @@ theorem ex3 (x y : Nat) : x + y = HAdd.hAdd x y := rfl
 section
 def g (x y : Nat) := 3*(x+y)
 
-local infix:65 [high] "  +  " => g
+local infix:65 (priority := high) "  +  " => g
 
 theorem ex4 (x y : Nat) : x + y = g x y := rfl
 
diff --git a/tests/lean/run/prioDSL.lean b/tests/lean/run/prioDSL.lean
index 96e54a1f5e..c05ae32ad0 100644
--- a/tests/lean/run/prioDSL.lean
+++ b/tests/lean/run/prioDSL.lean
@@ -2,18 +2,18 @@ macro "foo!" x:term:max : term => `($x - 1)
 
 theorem ex1 : foo! 10 = 9 := rfl
 
-macro [high] "foo! " x:term:max : term => `($x + 1)
+macro (priority := high) "foo! " x:term:max : term => `($x + 1)
 
 theorem ex2 : foo! 10 = 11 := rfl
 
-macro [low] "foo! " x:term:max : term => `($x * 2)
+macro (priority := low) "foo! " x:term:max : term => `($x * 2)
 
 theorem ex3 : foo! 10 = 11 := rfl
 
-macro [high+1] "foo! " x:term:max : term => `($x * 2)
+macro (priority := high+1) "foo! " x:term:max : term => `($x * 2)
 
 theorem ex4 : foo! 10 = 20 := rfl
 
-macro [high+4-2] "foo! " x:term:max : term => `($x * 3)
+macro (priority := high+4-2) "foo! " x:term:max : term => `($x * 3)
 
 theorem ex5 : foo! 10 = 30 := rfl
diff --git a/tests/lean/run/scopedParsers.lean b/tests/lean/run/scopedParsers.lean
index 215c351824..44122fd648 100644
--- a/tests/lean/run/scopedParsers.lean
+++ b/tests/lean/run/scopedParsers.lean
@@ -2,7 +2,7 @@ def f (x y : Nat) := x + 2*y
 
 namespace Foo
 
-scoped infix:65 [default+1] "+" => f
+scoped infix:65 (priority := default+1) "+" => f
 
 theorem ex1 (x y : Nat) : x + y = f x y := rfl
 
diff --git a/tests/lean/run/stxKindInsideNamespace.lean b/tests/lean/run/stxKindInsideNamespace.lean
index bcd5d6556c..fa59c18cfb 100644
--- a/tests/lean/run/stxKindInsideNamespace.lean
+++ b/tests/lean/run/stxKindInsideNamespace.lean
@@ -2,7 +2,7 @@ import Lean
 
 namespace Foo
 
-syntax[foo] "bla!" term : term
+syntax (name := foo) "bla!" term : term
 
 macro_rules[foo]
 | `(bla! $x) => pure x
diff --git a/tests/lean/run/syntaxPrio.lean b/tests/lean/run/syntaxPrio.lean
index f483ae1460..08adc4dcc1 100644
--- a/tests/lean/run/syntaxPrio.lean
+++ b/tests/lean/run/syntaxPrio.lean
@@ -7,7 +7,7 @@ macro_rules
 theorem ex1 : foo! 2 = 3 :=
   rfl
 
-syntax [high] "foo!" term:max : term
+syntax (priority := high) "foo!" term:max : term
 
 macro_rules
   | `(foo! $x) => `($x * 2)
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
index f0255be001..c3608f2d99 100644
--- a/tests/lean/run/tacticExtOverlap.lean
+++ b/tests/lean/run/tacticExtOverlap.lean
@@ -1,6 +1,6 @@
 open Lean
 
-syntax [myintro] "intros" sepBy(ident, ",") : tactic
+syntax (name := myintro) "intros" sepBy(ident, ",") : tactic
 
 macro_rules [myintro]
 | `(tactic| intros $x,*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom {} "intros", mkNullNode x]
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index cdfbe3c372..5fb6780a2d 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -68,7 +68,7 @@ syntax "⟨|" term "|⟩" : foo
 syntax term : foo
 syntax term ">>>" term : foo
 
-syntax [tst3] "FOO " foo : term
+syntax (name := tst3) "FOO " foo : term
 
 macro_rules
 | `(FOO ⟨| $t |⟩) => `($t+1)
diff --git a/tests/lean/run/unifhint3.lean b/tests/lean/run/unifhint3.lean
index 43e492e025..8e341c26eb 100644
--- a/tests/lean/run/unifhint3.lean
+++ b/tests/lean/run/unifhint3.lean
@@ -47,8 +47,8 @@ def gop {s : Group} (a b : s) : s :=
 def mop {s : Monoid} (a b : s) : s :=
   s.op a b
 
-infix:70 [high] "*" => mop
-infix:65 [high] "+" => gop
+infix:70 (priority := high) "*" => mop
+infix:65 (priority := high) "+" => gop
 
 unif_hint (r : Ring) (g : Group) where
   g =?= Group.ofRing r
diff --git a/tests/lean/scopedunifhint.lean b/tests/lean/scopedunifhint.lean
index 0fd3eee645..9837d870df 100644
--- a/tests/lean/scopedunifhint.lean
+++ b/tests/lean/scopedunifhint.lean
@@ -28,7 +28,7 @@ def x : Nat := 10
 #check mul x x           -- Error: unification hint is not active
 #check mul (x, x) (x, x) -- Error: no unification hint
 
-local infix:65 [high] "*" => mul
+local infix:65 (priority := high) "*" => mul
 
 #check x*x -- Error: unification hint is not active
 
diff --git a/tests/lean/syntaxInNamespacesAndPP.lean b/tests/lean/syntaxInNamespacesAndPP.lean
index 0bce0325fe..effec3aa65 100644
--- a/tests/lean/syntaxInNamespacesAndPP.lean
+++ b/tests/lean/syntaxInNamespacesAndPP.lean
@@ -12,7 +12,7 @@ end Foo
 
 namespace Bla
 
-syntax[bla] "bla" term : term
+syntax (name := bla) "bla" term : term
 
 macro_rules
   | `(bla $x) => x