From fdbec9101fcd614aaf88a93d92f2dd0497384c3e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 20 Dec 2020 13:52:25 +0100
Subject: [PATCH] fix: pattern reordering in syntax `match`

---
 src/Lean/Elab/Quotation.lean         | 38 ++++++++++++++++++----------
 tests/lean/StxQuot.lean              |  6 +++++
 tests/lean/StxQuot.lean.expected.out |  3 ++-
 3 files changed, 32 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 9d83b9032a..2eae9b2c5b 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -335,27 +335,37 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
     let info ← getHeadInfo alt
     let pat  := alt.1.head!
     let alts ← (alt::alts).mapM fun alt => do ((← getHeadInfo alt).onMatch info.check, alt)
+    let mut yesAlts           := #[]
+    let mut undecidedAlts     := #[]
+    let mut nonExhaustiveAlts := #[]
+    for alt in alts do match alt with
+      | (covered f exh, alt) =>
+        -- we can only factor out a common check if there are no undecided patterns in between;
+        -- otherwise we would change the order of alternatives
+        if undecidedAlts.isEmpty then
+          yesAlts ← yesAlts.push <$> f (alt.1.tail!, alt.2)
+          if !exh then
+            nonExhaustiveAlts := nonExhaustiveAlts.push alt
+        else
+          undecidedAlts := undecidedAlts.push alt
+          nonExhaustiveAlts := nonExhaustiveAlts.push alt
+      | (undecided, alt) =>
+        undecidedAlts := undecidedAlts.push alt
+        nonExhaustiveAlts := nonExhaustiveAlts.push alt
+      | (uncovered, alt) =>
+        nonExhaustiveAlts := nonExhaustiveAlts.push alt
     let m ← info.doMatch
       (yes := fun newDiscrs => do
-        let mut yesAlts ← alts.filterMapM fun
-          | (covered f _, (_::pats, rhs)) => some <$> f (pats, rhs)
-          | _                             => pure none
-        let undecidedAlts := alts.filterMap fun
-          | (undecided, alt) => some alt
-          | _                => none
+        let mut yesAlts := yesAlts
         if !undecidedAlts.isEmpty then
           -- group undecided alternatives in a new default case `| discr2, ... => match discr, discr2, ... with ...`
           let vars ← discrs.mapM fun _ => withFreshMacroScope `(discr)
           let pats := List.replicate newDiscrs.length (Unhygienic.run `(_)) ++ vars
-          let alts ← undecidedAlts.toArray.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => $(alt.2))
+          let alts ← undecidedAlts.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => $(alt.2))
           let rhs  ← `(match discr, $[$(vars.toArray):term],* with $alts:matchAlt*)
-          yesAlts := yesAlts ++ [(pats, rhs)]
-        withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts)
-      (no := do
-        let nonExhaustiveAlts := alts.filterMap fun
-          | (covered f (exhaustive := true), alt) => none
-          | (_,                              alt) => some alt
-        withFreshMacroScope $ compileStxMatch (discr::discrs) nonExhaustiveAlts)
+          yesAlts := yesAlts.push (pats, rhs)
+        withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts.toList)
+      (no := withFreshMacroScope $ compileStxMatch (discr::discrs) nonExhaustiveAlts.toList)
     `(let discr := $discr; $m)
   | _, _ => unreachable!
 
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 952b1692d9..34a458d472 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -68,4 +68,10 @@ open Parser.Term
   | `(Parser.Term.structInstField| $lhs:ident := $rhs) => #[lhs, rhs]
   | _ => unreachable!
 
+#eval run do
+  match ← `({ a := a : a }) with
+  | `({ a := a : 0 })      => "0"
+  | `({ a := a $[: $a?]?}) => "1"
+  | stx                    => "2"
+
 #eval run `(sufficesDecl|x from x)
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index f2ab494a46..fc7d07336a 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -35,4 +35,5 @@
 "(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n    \"=>\"\n    (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
 "(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n    \"=>\"\n    (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
 "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]"
-StxQuot.lean:71:33: error: expected parser to return exactly one syntax object
+"1"
+StxQuot.lean:77:33: error: expected parser to return exactly one syntax object