feat: save original node kind in antiquot node kind for checking in match_syntax

src/Init/Lean/Elab/Quotation.lean

@@ -59,13 +59,17 @@ instance Array.HasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
 namespace Elab
 namespace Term
 
+def isAntiquot : Syntax → Bool
+| Syntax.node (Name.str _ "antiquot" _) _ => true
+| _                                       => false
+
 -- `$e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes
-private def isAntiquotSplice (stx : Syntax) : Bool :=
-stx.isOfKind `Lean.Parser.Term.antiquot && (stx.getArg 3).getOptional.isSome
+def isAntiquotSplice (stx : Syntax) : Bool :=
+isAntiquot stx && (stx.getArg 3).getOptional.isSome
 
 -- If an antiquotation splice is the sole item of a `many` node, its result should
 -- be substituted for the `many` node
-private def isAntiquotSplicePat (stx : Syntax) : Bool :=
+def isAntiquotSplicePat (stx : Syntax) : Bool :=
 stx.isOfKind nullKind && stx.getArgs.size == 1 && isAntiquotSplice (stx.getArg 0)
 
 -- Elaborate the content of a syntax quotation term
@@ -85,7 +89,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
   `(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) $val $args)
 -- if antiquotation, insert contents as-is, else recurse
 | stx@(Syntax.node k args) =>
-  if k == `Lean.Parser.Term.antiquot then
+  if isAntiquot stx then
     -- splices must occur in a `many` node
     if isAntiquotSplice stx then throwError stx "unexpected antiquotation splice"
     else pure $ stx.getArg 1
@@ -148,7 +152,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
   -- We assume that atoms are uniquely determined by the surrounding node and never have to be checked
   if quoted.isAtom then some pure
   -- TODO: antiquotations with kinds (`$id:id`) probably can't be handled as unconditional patterns
-  else if quoted.isOfKind `Lean.Parser.Term.antiquot then
+  else if isAntiquot quoted then
     let anti := quoted.getArg 1;
     if isAntiquotSplice quoted then some $ fun _ => throwError quoted "unexpected antiquotation splice"
     else if anti.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let $anti := discr; $rhs)

src/Init/Lean/Parser/Term.lean

@@ -44,9 +44,11 @@ def dollarSymbol {k : ParserKind} : Parser k := symbol "$" 1
 
 -- Define parser for `$e` (if name = none) or `$e:n` (if name = some n). Both
 -- forms can also be used with an appended `*` to turn them into an
--- antiquotation "splice".
-def mkAntiquot (name : Option String) : Parser leading :=
-leadingNode `Lean.Parser.Term.antiquot $ dollarSymbol >> checkNoWsBefore "no space before" >> termParser appPrec >> (
+-- antiquotation "splice". If `kind` is given, it will additionally be checked
+-- when evaluating `match_syntax`.
+def mkAntiquot (name : Option String) (kind : Option SyntaxNodeKind) : Parser leading :=
+let kind := (kind.getD Name.anonymous) ++ `antiquot;
+leadingNode kind $ dollarSymbol >> checkNoWsBefore "no space before" >> termParser appPrec >> (
   match name with
   | some name => let sym := ":" ++ name; checkNoWsBefore ("no space before '" ++ sym ++ "'") >> sym
   -- make sure to generate as many children (1) as in the first case to keep arity constant
@@ -56,7 +58,7 @@ leadingNode `Lean.Parser.Term.antiquot $ dollarSymbol >> checkNoWsBefore "no spa
 /- Built-in parsers -/
 def explicitUniv   := parser! ".{" >> sepBy1 levelParser ", " >> "}"
 def namedPattern := parser! checkNoWsBefore "no space before '@'" >> "@" >> termParser appPrec
-@[builtinTermParser] def id := mkAntiquot "id" <|> parser! ident >> optional (explicitUniv <|> namedPattern)
+@[builtinTermParser] def id := mkAntiquot "id" `Lean.Parser.Term.id <|> parser! ident >> optional (explicitUniv <|> namedPattern)
 @[builtinTermParser] def num : Parser := parser! numLit
 @[builtinTermParser] def str : Parser := parser! strLit
 @[builtinTermParser] def char : Parser := parser! charLit
@@ -109,7 +111,7 @@ def matchAlt := parser! " | " >> sepBy1 termParser ", " >> unicodeSymbol "⇒" "
 @[builtinTermParser] def borrowed   := parser! symbol "@&" appPrec >> termParser (appPrec - 1)
 @[builtinTermParser] def quotedName := parser! symbol "`" appPrec >> rawIdent
 @[builtinTermParser] def stxQuot    := parser! symbol "`(" appPrec >> termParser >> ")"
-@[builtinTermParser] def antiquot   := mkAntiquot none
+@[builtinTermParser] def antiquot   := mkAntiquot none none
 @[builtinTermParser] def «match_syntax» := parser! "match_syntax" >> termParser >> " with " >> many1Indent matchAlt "'match_syntax' alternatives must be indented"
 
 /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/

tests/lean/StxQuot.lean

@@ -19,13 +19,11 @@ end Syntax
 #eval run $ do a ← `(Nat.one); `(f $ f $a 1)
 #eval run $ do a ← `(Nat.one); `(f $(id a))
 #eval run $ do a ← `(1 + 2); match_syntax a with `($a + $b) => `($b + $a) | _ => pure Syntax.missing
+
 #eval run $ do a ← `(aa); match_syntax a with `($id:id) => pure 0 | `($e) => pure 1 | _ => pure 2
+#eval run $ do a ← `(1 + 2); match_syntax a with `($id:id) => pure 0 | `($e) => pure 1 | _ => pure 2
 
 #eval run $ do params ← #[`(a), `((b : Nat))].mapM id; `(fun $params* => 1)
 #eval run $ do a ← `(fun (a : Nat) b => c); match_syntax a with `(fun $aa* => $e) => pure aa | _ => pure #[]
 
--- TODO
--- returns "0" because the antiquotation kind is only checked at parse time, not match time
---#eval run $ do a ← `(1 + 2); match_syntax a with `($id:id) => pure 0 | `($e) => pure 1 | _ => pure 2
-
 end Lean

tests/lean/StxQuot.lean.expected.out

@@ -11,5 +11,6 @@
 "(Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null)))"
 "(Term.add (Term.num (numLit \"2\")) \"+\" (Term.num (numLit \"1\")))"
 "0"
+"1"
 "(Term.fun\n \"fun\"\n (null\n  (Term.id `a.0 (null))\n  (Term.paren \"(\" (null (Term.id `b.0 (null)) (null (Term.typeAscription \":\" (Term.id `Nat.0 (null))))) \")\"))\n \"=>\"\n (Term.num (numLit \"1\")))"
 "#[(Term.paren \"(\" (null (Term.id `a.0 (null)) (null (Term.typeAscription \":\" (Term.id `Nat.0 (null))))) \")\"), (Term.id `b.0 (null))]"