feat: nary nomatch (#3285)

Base for #3279 --------- Co-authored-by: Scott Morrison <[email protected]>
leanprover · Feb 9, 2024 · 1f54722 · 1f54722
1 parent 09a4399
commit 1f54722
Show file tree

Hide file tree

Showing 25 changed files with 12,163 additions and 5,791 deletions.
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
@@ -1236,16 +1236,29 @@ where
 builtin_initialize
   registerTraceClass `Elab.match
 
--- leading_parser:leadPrec "nomatch " >> termParser
+-- leading_parser:leadPrec "nomatch " >> sepBy1 termParser ", "
 @[builtin_term_elab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => do
   match stx with
-  | `(nomatch $discrExpr) =>
-    if (← isAtomicDiscr discrExpr) then
+  | `(nomatch $discrs,*) =>
+    let discrs := discrs.getElems
+    if (← discrs.allM fun discr => isAtomicDiscr discr.raw) then
       let expectedType ← waitExpectedType expectedType?
-      let discr := mkNode ``Lean.Parser.Term.matchDiscr #[mkNullNode, discrExpr]
-      elabMatchAux none #[discr] #[] mkNullNode expectedType
+      let discrs := discrs.map fun discr => mkNode ``Lean.Parser.Term.matchDiscr #[mkNullNode, discr.raw]
+      elabMatchAux none discrs #[] mkNullNode expectedType
     else
-      let stxNew ← `(let_mvar% ?x := $discrExpr; nomatch ?x)
+      let rec loop (discrs : List Term) (discrsNew : Array Syntax) : TermElabM Term := do
+        match discrs with
+        | [] =>
+          return ⟨stx.setArg 1 (Syntax.mkSep discrsNew (mkAtomFrom stx ", "))⟩
+        | discr :: discrs =>
+          if (← isAtomicDiscr discr) then
+            loop discrs (discrsNew.push discr)
+          else
+            withFreshMacroScope do
+              let discrNew ← `(?x)
+              let r ← loop discrs (discrsNew.push discrNew)
+              `(let_mvar% ?x := $discr; $r)
+      let stxNew ← loop discrs.toList #[]
       withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   | _ => throwUnsupportedSyntax
 

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
@@ -432,7 +432,7 @@ Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
 Lean can show that an empty set of patterns is exhaustive given `e`'s type,
 e.g. because it has no constructors.
 -/
-@[builtin_term_parser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
+@[builtin_term_parser] def «nomatch» := leading_parser:leadPrec "nomatch " >> sepBy1 termParser ", "
 
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder

diff --git a/stage0/stdlib/Init.c b/stage0/stdlib/Init.c
diff --git a/stage0/stdlib/Init/Data/Array/Basic.c b/stage0/stdlib/Init/Data/Array/Basic.c
diff --git a/stage0/stdlib/Init/Notation.c b/stage0/stdlib/Init/Notation.c
diff --git a/stage0/stdlib/Init/Tactics.c b/stage0/stdlib/Init/Tactics.c
diff --git a/stage0/stdlib/Init/TacticsExtra.c b/stage0/stdlib/Init/TacticsExtra.c
diff --git a/stage0/stdlib/Lean/Attributes.c b/stage0/stdlib/Lean/Attributes.c
diff --git a/stage0/stdlib/Lean/Compiler/IR/Basic.c b/stage0/stdlib/Lean/Compiler/IR/Basic.c
diff --git a/stage0/stdlib/Lean/Data/Json.c b/stage0/stdlib/Lean/Data/Json.c