From 9fa89a73dfbca87e2d876953c7178c66846154aa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Apr 2021 17:47:13 -0700
Subject: [PATCH] feat: add helper functions for syntax match

Motivation: improve error recovery.
---
 src/Init/Prelude.lean        | 14 ++++++++++++++
 src/Lean/Elab/Quotation.lean |  2 +-
 src/Lean/Syntax.lean         |  4 ----
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 493741997d..2df3b2347a 100644
--- a/src/Init/Prelude.lean
+++ b/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
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index bb2f7118b7..1454349d29 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/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))
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index ec49b4e18c..27fa4d21fb 100644
--- a/src/Lean/Syntax.lean
+++ b/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)