From a4f19aac3285081616ff261f3fff9dc801869027 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Jun 2020 13:25:05 -0700
Subject: [PATCH] fix: `macro` command

---
 src/Lean/Elab/Syntax.lean   | 36 +++++++++++++++++-------------------
 src/Lean/Parser/Syntax.lean |  4 ++--
 2 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index d29127b233..1096040ce8 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -341,18 +341,17 @@ if k == `Lean.Parser.Command.macroArgSimple then
   | Syntax.atom _ "char"  => pure $ Syntax.node `Lean.Parser.Syntax.char #[argType]
   | Syntax.ident _ _ _ _  => pure $ Syntax.node `Lean.Parser.Syntax.cat #[stx.getArg 2,  stx.getArg 3]
   | _                     => Macro.throwUnsupported
-else if k == `Lean.Parser.Command.strLitPrec then
-  pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs
+else if k == strLitKind then
+  pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
 else
   Macro.throwUnsupported
 
 /- Convert `macro` head into a `syntax` command item -/
 def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
-let k := stx.getKind;
-if k == `Lean.Parser.Command.identPrec then
+if stx.isIdent then
   let info := stx.getHeadInfo.getD {};
-  let id   := (stx.getArg 0).getId;
-  pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info, stx.getArg 1]
+  let id   := stx.getId;
+  pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info]
 else
   expandMacroArgIntoSyntaxItem stx
 
@@ -362,25 +361,24 @@ let k := stx.getKind;
 if k == `Lean.Parser.Command.macroArgSimple then
   let item := stx.getArg 0;
   pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
-else if k == `Lean.Parser.Command.strLit then
+else if k == strLitKind then
   strLitToPattern stx
 else
   Macro.throwUnsupported
 
 /- Convert `macro` head into a pattern element -/
 def expandMacroHeadIntoPattern (stx : Syntax) : MacroM Syntax :=
-let k := stx.getKind;
-if k == `Lean.Parser.Command.identPrec then
-  let str := toString (stx.getArg 0).getId;
-  pure $ mkAtomFrom stx str
+if stx.isIdent then
+  pure $ mkAtomFrom stx (toString stx.getId)
 else
   expandMacroArgIntoPattern stx
 
 @[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro :=
 fun stx => do
-  let head := stx.getArg 1;
-  let args := (stx.getArg 2).getArgs;
-  let cat  := stx.getArg 4;
+  let prec := stx.getArg 1;
+  let head := stx.getArg 2;
+  let args := (stx.getArg 3).getArgs;
+  let cat  := stx.getArg 5;
   kind ← Macro.mkFreshKind (cat.getId).eraseMacroScopes;
   -- build parser
   stxPart  ← expandMacroHeadIntoSyntaxItem head;
@@ -390,14 +388,14 @@ fun stx => do
   patHead ← expandMacroHeadIntoPattern head;
   patArgs ← args.mapM expandMacroArgIntoPattern;
   let pat := Syntax.node kind (#[patHead] ++ patArgs);
-  if stx.getArgs.size == 7 then
+  if stx.getArgs.size == 8 then
     -- `stx` is of the form `macro $head $args* : $cat => term`
-    let rhs := stx.getArg 6;
-    `(syntax [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => $rhs)
+    let rhs := stx.getArg 7;
+    `(syntax $prec [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => $rhs)
   else
     -- `stx` is of the form `macro $head $args* : $cat => `( $body )`
-    let rhsBody := stx.getArg 7;
-    `(syntax [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
+    let rhsBody := stx.getArg 8;
+    `(syntax $prec [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab.syntax;
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 6452f7d357..4c08be987d 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -67,12 +67,12 @@ def optKind : Parser := optional ("[" >> ident >> "]")
 def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> ident
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
 def macroArg  := try strLit <|> try macroArgSimple
-def macroHead := macroArg <|> try identPrec
+def macroHead := macroArg <|> try ident
 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 >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
-@[builtinCommandParser] def «macro»       := parser! "macro " >> optPrecedence <|> macroHead >> many macroArg >> macroTail
+@[builtinCommandParser] def «macro»       := parser! "macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail
 
 end Command