feat: add helper functions for syntax match

Motivation: improve error recovery.

src/Init/Prelude.lean

@@ -1722,6 +1722,20 @@ def getNumArgs (stx : Syntax) : Nat :=
   | Syntax.node _ args => args.size
   | _                  => 0
 
+def isMissing : Syntax → Bool
+  | Syntax.missing => true
+  | _ => false
+
+def isNodeOf (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) : Bool :=
+  and (stx.isOfKind k) (beq stx.getNumArgs n)
+
+/--
+  Similar to `isNodeOf`, but also succeeds if `stx` is `Syntax.missing`.
+  We use this function to implement `Syntax` pattern matching.
+  TODO: is this too liberal? -/
+def isNodeOf' (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) : Bool :=
+  or (stx.isNodeOf k n) stx.isMissing
+
 def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
   match stx with
   | node k _ => node k args

src/Lean/Elab/Quotation.lean

@@ -373,7 +373,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             uncovered,
         doMatch := fun yes no => do
           let cond ← match kind with
-          | `null => `(and (Syntax.isOfKind discr $(quote kind)) (BEq.beq (Array.size (Syntax.getArgs discr)) $(quote argPats.size)))
+          | `null => `(Syntax.isNodeOf' discr $(quote kind) $(quote argPats.size)) -- `isNodeOf'` also succeeds if discr is `Syntax.missing`, use `isNodeOf` to disable this
           | `ident => `(and (Syntax.isIdent discr) (BEq.beq (Syntax.getId discr) $(quote quoted.getId)))
           | _     => `(Syntax.isOfKind discr $(quote kind))
           let newDiscrs ← (List.range argPats.size).mapM fun i => `(Syntax.getArg discr $(quote i))

src/Lean/Syntax.lean

@@ -14,10 +14,6 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
 
 /- Syntax AST -/
 
-def Syntax.isMissing : Syntax → Bool
-  | Syntax.missing => true
-  | _ => false
-
 inductive IsNode : Syntax → Prop where
   | mk (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node kind args)