refactor: use distinct syntax kinds for quotations

src/Lean/Elab/Quotation.lean

@@ -26,6 +26,11 @@ namespace Elab
 namespace Term
 namespace Quotation
 
+-- quotation node kinds are formed from a unique quotation name plus "quot"
+def isQuot : Syntax → Bool
+| Syntax.node (Name.str _ "quot" _) _ => true
+| _                                   => false
+
 -- antiquotation node kinds are formed from the original node kind (if any) plus "antiquot"
 def isAntiquot : Syntax → Bool
 | Syntax.node (Name.str _ "antiquot" _) _ => true
@@ -174,7 +179,7 @@ if pat.isOfKind `Lean.Parser.Term.id then unconditional $ fun rhs => `(let $pat
 -- wildcard pattern
 else if pat.isOfKind `Lean.Parser.Term.hole then unconditional pure
 -- quotation pattern
-else if pat.isOfKind `Lean.Parser.Term.stxQuot then
+else if isQuot pat then
   let quoted := pat.getArg 1;
   if quoted.isAtom then
     -- We assume that atoms are uniquely determined by the node kind and never have to be checked
@@ -206,7 +211,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
   else
     -- not an antiquotation or escaped antiquotation: match head shape
     let quoted := unescapeAntiquot quoted;
-    let argPats := quoted.getArgs.map $ fun arg => Syntax.node `Lean.Parser.Term.stxQuot #[mkAtom "`(", arg, mkAtom ")"];
+    let argPats := quoted.getArgs.map (pat.setArg 1);
     { kind := quoted.getKind, argPats := argPats }
 else
   unconditional $ fun _ => throwErrorAt pat ("match_syntax: unexpected pattern kind " ++ toString pat)
@@ -265,7 +270,7 @@ private partial def getPatternVarsAux : Syntax → List Syntax
 
 -- Get all pattern vars (as Term.id nodes) in `stx`
 partial def getPatternVars (stx : Syntax) : List Syntax :=
-if stx.isOfKind `Lean.Parser.Term.stxQuot then do
+if isQuot stx then do
   let quoted := stx.getArg 1;
   getPatternVarsAux stx
 else if stx.isOfKind `Lean.Parser.Term.id then
@@ -300,7 +305,7 @@ alts ← alts.getArgs.getSepElems.mapM $ fun alt => do {
   let pats := alt.getArg 0;
   pat ← if pats.getArgs.size == 1 then pure $ pats.getArg 0
     else throwError "match_syntax: expected exactly one pattern per alternative";
-  let pat := if pat.isOfKind `Lean.Parser.Term.stxQuot then pat.setArg 1 $ elimAntiquotChoices $ pat.getArg 1 else pat;
+  let pat := if isQuot pat then pat.setArg 1 $ elimAntiquotChoices $ pat.getArg 1 else pat;
   match pat.find? $ fun stx => stx.getKind == choiceKind with
   | some choiceStx => throwErrorAt choiceStx "invalid pattern, nested syntax has multiple interpretations"
   | none           =>

src/Lean/Elab/Syntax.lean

@@ -181,7 +181,8 @@ match catName with
 
 private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
 let quotSymbol := "`(" ++ getCatSuffix catName ++ "|";
-cmd ← `(@[termParser] def catStxQuot : Lean.ParserDescr := Lean.ParserDescr.node `Lean.Parser.Term.stxQuot $(quote Lean.Parser.maxPrec) (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol)) (Lean.ParserDescr.andthen (Lean.ParserDescr.cat $(quote catName) 0) (Lean.ParserDescr.symbol ")"))));
+let kind := catName ++ `quot;
+cmd ← `(@[termParser] def $(mkIdent kind) : Lean.ParserDescr := Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec) (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol)) (Lean.ParserDescr.andthen (Lean.ParserDescr.cat $(quote catName) 0) (Lean.ParserDescr.symbol ")"))));
 elabCommand cmd
 
 @[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=

src/Lean/Parser/Command.lean

@@ -22,7 +22,7 @@ categoryParser `command rbp
   `($x $y) will be parsed as an application, not two commands. Use `($x:command $y:command) instead.
   Multiple command will be put in a `null node, but a single command will not (so that you can directly
   match against a quotation in a command kind's elaborator). -/
-@[builtinTermParser] def Term.stxQuot := parser! "`(" >> (termParser <|> many1 commandParser true) >> ")"
+@[builtinTermParser] def Term.quot := parser! "`(" >> (termParser <|> many1 commandParser true) >> ")"
 
 namespace Command
 def commentBody : Parser :=

src/Lean/Parser/Term.lean

@@ -207,14 +207,13 @@ def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
 
 @[builtinTermParser] def tacticBlock := parser! "begin " >> Tactic.seq >> "end"
 @[builtinTermParser] def byTactic    := parser!:leadPrec "by " >> Tactic.nonEmptySeq
--- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
-@[builtinTermParser] def tacticStxQuot    : Parser :=
-checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")")
-@[builtinTermParser] def levelStxQuot     : Parser :=
-checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ "`(level|" >> levelParser >> ")")
-@[builtinTermParser] def funBinderStxQuot : Parser :=
-checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ "`(funBinder|"  >> funBinder >> ")")
 
+@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> funBinder >> ")"
 end Term
+
+-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.quot`
+@[builtinTermParser] def Tactic.quot : Parser := parser! "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")"
+@[builtinTermParser] def Level.quot  : Parser := parser! "`(level|" >> levelParser >> ")"
+
 end Parser
 end Lean