From e9473722b1dfe873dfd9e8aa22b49f0efbacb998 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 14 Aug 2020 17:44:29 +0200
Subject: [PATCH] feat: elaborate new quotation kinds, make macro_rules
 elaborator work with them

---
 src/Lean/Elab/Quotation.lean |  6 ++++--
 src/Lean/Elab/Syntax.lean    | 41 +++++++++++++++++++-----------------
 2 files changed, 26 insertions(+), 21 deletions(-)

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 7a98032c29..c7f4ae16a6 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -138,8 +138,10 @@ stx ← quoteSyntax (elimAntiquotChoices quoted);
    implementation is "self-stabilizing". It was in fact originally compiled
    by an unhygienic prototype implementation. -/
 
-@[builtinTermElab stxQuot] def elabStxQuot : TermElab :=
-adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Level.quot] def elabLevelQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Term.quot] def elabTermQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Term.funBinder.quot] def elabfunBinderQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Tactic.quot] def elabTacticQuot : TermElab := adaptExpander stxQuot.expand
 
 /- match_syntax -/
 
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 2406d0128c..57e749fa46 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -250,28 +250,31 @@ def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM
 alts ← alts.mapSepElemsM $ fun alt => do {
   let lhs := alt.getArg 0;
   let pat := lhs.getArg 0;
-  match_syntax pat with
-  | `(`($quot)) =>
-     let k' := quot.getKind;
-     if k' == k then
-       pure alt
-     else if k' == choiceKind then do
-        match quot.getArgs.find? $ fun quotAlt => quotAlt.getKind == k with
-        | none      => throwErrorAt alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
-        | some quot => do
-          pat ← `(`($quot));
-          let lhs := lhs.setArg 0 pat;
-          pure $ alt.setArg 0 lhs
-     else
-       throwErrorAt alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
-  | stx => throwUnsupportedSyntax
+  when (!Term.Quotation.isQuot pat) $
+    throwUnsupportedSyntax;
+  let quot := pat.getArg 1;
+  let k' := quot.getKind;
+  if k' == k then
+    pure alt
+  else if k' == choiceKind then do
+     match quot.getArgs.find? $ fun quotAlt => quotAlt.getKind == k with
+     | none      => throwErrorAt alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
+     | some quot => do
+       let pat := pat.setArg 1 quot;
+       let lhs := lhs.setArg 0 pat;
+       pure $ alt.setArg 0 lhs
+  else
+    throwErrorAt alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
 };
 `(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
 
-def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind :=
-match_syntax (alt.getArg 0).getArg 0 with
-| `(`($quot)) => pure quot.getKind
-| stx         => throwUnsupportedSyntax
+def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
+let lhs := alt.getArg 0;
+let pat := lhs.getArg 0;
+when (!Term.Quotation.isQuot pat) $
+  throwUnsupportedSyntax;
+let quot := pat.getArg 1;
+pure quot.getKind
 
 def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
 k ← inferMacroRulesAltKind (alts.get! 0);