feat: improve macro command parser

src/Init/Lean/Parser/Parser.lean

@@ -1083,6 +1083,20 @@ fun _ c s =>
 @[inline] def rawIdentNoAntiquot {k : ParserKind} : Parser k :=
 { fn := fun _ => rawIdentFn }
 
+def identEqFn {k : ParserKind} (id : Name) : ParserFn k :=
+fun _ c s =>
+  let iniPos := s.pos;
+  let s      := tokenFn c s;
+  if s.hasError then
+    s.mkErrorAt "identifier" iniPos
+  else match s.stxStack.back with
+    | Syntax.ident _ _ val _ => if val != id then s.mkErrorAt ("expected identifier '" ++ toString id ++ "'") iniPos else s
+    | _ => s.mkErrorAt "identifier" iniPos
+
+@[inline] def identEq {k : ParserKind} (id : Name) : Parser k :=
+{ fn   := identEqFn id,
+  info := mkAtomicInfo "ident" }
+
 def quotedSymbolFn {k : ParserKind} : ParserFn k :=
 nodeFn `quotedSymbol (andthenFn (andthenFn (chFn '`') (rawFn (fun _ => takeUntilFn (fun c => c == '`')))) (chFn '`' true))
 
@@ -1365,6 +1379,19 @@ fun rbp ctx s => categoryParserFnExtension.getState ctx.env catName rbp ctx s
 def categoryParser {k} (catName : Name) (rbp : Nat) : Parser k :=
 { fn := fun _ => categoryParserFn catName rbp }
 
+def categoryParserOfStackFn (offset : Nat) : ParserFn leading :=
+fun rbp ctx s =>
+  let stack := s.stxStack;
+  if stack.size < offset + 1 then
+    s.mkUnexpectedError ("failed to determine parser category using syntax stack, stack is too small")
+  else
+    match stack.get! (stack.size - offset - 1) with
+    | Syntax.ident _ _ catName _ => categoryParserFn catName rbp ctx s
+    | _ => s.mkUnexpectedError ("failed to determine parser category using syntax stack, the specified element on the stack is not an identifier")
+
+def categoryParserOfStack {k} (offset : Nat) (rbp : Nat := 0) : Parser k :=
+{ fn := fun _ => categoryParserOfStackFn offset rbp }
+
 def mkBuiltinTokenTable : IO (IO.Ref TokenTable) := IO.mkRef {}
 @[init mkBuiltinTokenTable] constant builtinTokenTable : IO.Ref TokenTable := arbitrary _
 

src/Init/Lean/Parser/Syntax.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.Lean.Parser.Command
+import Init.Lean.Parser.Tactic
 
 namespace Lean
 namespace Parser
@@ -16,13 +17,15 @@ registerBuiltinParserAttribute `builtinSyntaxParser `syntax leadingIdentAsSymbol
 @[inline] def syntaxParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 categoryParser `syntax rbp
 
-namespace Syntax
 def maxPrec := parser! nonReservedSymbol "max" true
 def precedenceLit : Parser := numLit <|> maxPrec
 def «precedence» := parser! ":" >> precedenceLit
+def optPrecedence := optional (try «precedence»)
+
+namespace Syntax
 @[builtinSyntaxParser] def paren     := parser! "(" >> many1 syntaxParser >> ")"
-@[builtinSyntaxParser] def cat       := parser! ident >> optional (try «precedence»)
-@[builtinSyntaxParser] def atom      := parser! strLit >> optional (try «precedence»)
+@[builtinSyntaxParser] def cat       := parser! ident >> optPrecedence
+@[builtinSyntaxParser] def atom      := parser! strLit >> optPrecedence
 @[builtinSyntaxParser] def num       := parser! nonReservedSymbol "num"
 @[builtinSyntaxParser] def str       := parser! nonReservedSymbol "str"
 @[builtinSyntaxParser] def char      := parser! nonReservedSymbol "char"
@@ -41,7 +44,7 @@ end Syntax
 
 namespace Command
 
-def quotedSymbolPrec := parser! quotedSymbol >> optional Syntax.precedence
+def quotedSymbolPrec := parser! quotedSymbol >> optPrecedence
 def «prefix»   := parser! "prefix"
 def «infix»    := parser! "infix"
 def «infixl»   := parser! "infixl"
@@ -51,17 +54,22 @@ def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «p
 -- TODO delete reserve
 @[builtinCommandParser] def «reserve»  := parser! "reserve " >> mixfixKind >> quotedSymbolPrec
 def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol
-@[builtinCommandParser] def «mixfix»   := parser! mixfixKind >> mixfixSymbol >> unicodeSymbol "⇒" "=>" >> termParser
-def strLitPrec := parser! strLit >> optional Syntax.precedence
-def identPrec  := parser! ident >> optional Syntax.precedence
+@[builtinCommandParser] def «mixfix»   := parser! mixfixKind >> mixfixSymbol >> darrow >> termParser
+def strLitPrec := parser! strLit >> optPrecedence
+def identPrec  := parser! ident >> optPrecedence
 
-@[builtinCommandParser] def «notation»    := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> unicodeSymbol "⇒" "=>" >> termParser
+@[builtinCommandParser] def «notation»    := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> darrow >> termParser
 @[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented"
 @[builtinCommandParser] def «syntax»      := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
 @[builtinCommandParser] def syntaxCat     := parser! "declare_syntax_cat " >> ident
-def macroArgSimple := parser! ident >> ":" >> ident >> optional Syntax.precedence
-def macroArg := try (strLitPrec <|> macroArgSimple)
-@[builtinCommandParser] def «macro»       := parser! "macro " >> (strLitPrec <|> identPrec) >> many macroArg >> " : " >> ident >> unicodeSymbol "⇒" "=>" >> termParser
+def macroArgSimple := parser! ident >> ":" >> ident >> optPrecedence
+def macroArg := try strLitPrec <|> try macroArgSimple
+def macroHead := try strLitPrec <|> try identPrec
+def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
+def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"
+def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> "`(" >> categoryParserOfStack 2 >> ")"
+def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
+@[builtinCommandParser] def «macro»       := parser! "macro " >> macroHead >> many macroArg >> macroTail
 
 end Command
 

src/Init/Lean/Parser/Term.lean

@@ -9,6 +9,9 @@ import Init.Lean.Parser.Level
 
 namespace Lean
 namespace Parser
+
+def darrow : Parser := unicodeSymbol "⇒" "=>"
+
 namespace Term
 
 /- Helper functions for defining simple parsers -/
@@ -53,7 +56,7 @@ def haveAssign := parser! " := " >> termParser
 @[builtinTermParser] def «have» := parser! "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
 @[builtinTermParser] def «suffices» := parser! "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
 @[builtinTermParser] def «show»     := parser! "show " >> termParser >> fromTerm
-@[builtinTermParser] def «fun»      := parser! unicodeSymbol "λ" "fun" >> many1 (termParser appPrec) >> unicodeSymbol "⇒" "=>" >> termParser
+@[builtinTermParser] def «fun»      := parser! unicodeSymbol "λ" "fun" >> many1 (termParser appPrec) >> darrow >> termParser
 def structInstField  := parser! ident >> " := " >> termParser
 def structInstSource := parser! ".." >> optional termParser
 @[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}"
@@ -75,7 +78,7 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl
 @[builtinTermParser] def depArrow := parser! bracktedBinder true >> unicodeSymbolCheckPrec " → " " -> " 25 >> termParser
 def simpleBinder := parser! many1 binderIdent
 @[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser
-def matchAlt := parser! " | " >> sepBy1 termParser ", " >> unicodeSymbol "⇒" "=>" >> termParser
+def matchAlt := parser! " | " >> sepBy1 termParser ", " >> darrow >> termParser
 @[builtinTermParser] def «match» := parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> many1Indent matchAlt "'match' alternatives must be indented"
 @[builtinTermParser] def «nomatch»  := parser! "nomatch " >> termParser
 @[builtinTermParser] def «parser!»  := parser! "parser! " >> termParser

tests/lean/run/newfrontend1.lean

@@ -62,3 +62,10 @@ begin
   intro2;
   assumption
 end
+
+-- set_option trace.Elab true
+-- set_option syntaxMaxDepth 100
+
+-- macro intro3 : tactic => `(intro; intro)
+-- macro check2 x: term : command => `(#check $x #check $x)
+-- macro foo x: term ", " y: term : term => `($x + $y + $x)