feat: $_ antiquotation pattern

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* Add unnamed antiquotation `$_` for use in syntax quotation patterns.
+
 * [Add unused variables linter](https://github.com/leanprover/lean4/pull/1159). Feedback welcome!
 
 * Lean now generates an error if the body of a declaration body contains a universe parameter that does not occur in the declaration type, nor is an explicit parameter.

src/Lean/Elab/Quotation/Util.lean

@@ -19,6 +19,7 @@ def getAntiquotationIds (stx : Syntax) : TermElabM (Array Syntax) := do
     if (isAntiquot stx || isTokenAntiquot stx) && !isEscapedAntiquot stx then
       let anti := getAntiquotTerm stx
       if anti.isIdent then ids := ids.push anti
+      else if anti.isOfKind ``Parser.Term.hole then pure ()
       else throwErrorAt stx "complex antiquotation not allowed here"
   return ids
 

src/Lean/Parser/Basic.lean

@@ -1670,9 +1670,9 @@ def setExpected (expected : List String) (p : Parser) : Parser :=
 def pushNone : Parser :=
   { fn := fun c s => s.pushSyntax mkNullNode }
 
--- We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
+-- We support three kinds of antiquotations: `$id`, `$_`, and `$(t)`, where `id` is a term identifier and `t` is a term.
 def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> decQuotDepth termParser >> symbolNoAntiquot ")")
-def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
+def antiquotExpr : Parser       := identNoAntiquot <|> symbolNoAntiquot "_" <|> antiquotNestedExpr
 
 def tokenAntiquotFn : ParserFn := fun c s => Id.run do
   if s.hasError then

src/Lean/Syntax.lean

@@ -384,9 +384,10 @@ def isAntiquot : Syntax → Bool
 
 def mkAntiquotNode (term : Syntax) (nesting := 0) (name : Option String := none) (kind := Name.anonymous) : Syntax :=
   let nesting := mkNullNode (mkArray nesting (mkAtom "$"))
-  let term := match term.isIdent with
-    | true  => term
-    | false => mkNode `antiquotNestedExpr #[mkAtom "(", term, mkAtom ")"]
+  let term :=
+    if term.isIdent then term
+    else if term.isOfKind `Lean.Parser.Term.hole then term[0]
+    else mkNode `antiquotNestedExpr #[mkAtom "(", term, mkAtom ")"]
   let name := match name with
     | some name => mkNode `antiquotName #[mkAtom ":", mkAtom name]
     | none      => mkNullNode
@@ -407,6 +408,7 @@ def unescapeAntiquot (stx : Syntax) : Syntax :=
 def getAntiquotTerm (stx : Syntax) : Syntax :=
   let e := if stx.isAntiquot then stx[2] else stx[3]
   if e.isIdent then e
+  else if e.isAtom then mkNode `Lean.Parser.Term.hole #[e]
   else
     -- `e` is from `"(" >> termParser >> ")"`
     e[1]

tests/lean/StxQuot.lean

@@ -30,7 +30,7 @@ end Lean.Syntax
 #eval run $ do let a ← `(def foo := 1); match a with | `($f:command) => pure f | _ => pure Syntax.missing
 #eval run $ do let a ← `(def foo := 1 def bar := 2); match a with | `($f:command $g:command) => `($g:command $f:command) | _ => pure Syntax.missing
 
-#eval run $ do let a ← `(aa); match a with | `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
+#eval run $ do let a ← `(aa); match a with | `($_:ident) => pure 0 | `($_) => pure 1 | _ => pure 2
 #eval match mkIdent `aa with | `(aa) => 0 | _ => 1
 #eval match mkIdent `aa with | `(ab) => 0 | _ => 1
 #eval run $ do let a ← `(1 + 2); match a with | `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2