Backwards compat option

Author: nomeata

src/Lean/Meta/Match/Match.lean

@@ -17,6 +17,15 @@ public section
 
 namespace Lean.Meta.Match
 
+register_builtin_option backwards.match.rowMajor : Bool := {
+  defValue := true
+  group := "bootstrap"
+  descr := "If true (the default), match compilation will split the discrimnants based \
+    on position of the first constructor pattern in the first alternative. If false, \
+    it splits them from left to right, which can lead to unnecessary code bloat."
+}
+
+
 private def mkIncorrectNumberOfPatternsMsg [ToMessageData α]
     (discrepancyKind : String) (expected actual : Nat) (pats : List α) :=
   let patternsMsg := MessageData.joinSep (pats.map toMessageData) ", "
@@ -818,19 +827,20 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
     process p
     return
 
-  match firstRefutablePattern p with
-  | some i =>
-    if i > 0 then
-      traceStep ("move var to front")
-      process (moveToFront p i)
-      return
-  | none =>
-    if 1 < p.alts.length then
-      traceStep ("drop all but first alt")
-      -- all patterns are irrefutable, we can drop all other alts
-      let p := { p with alts := p.alts.take 1 }
-      process p
-      return
+  if backwards.match.rowMajor.get (← getOptions) then
+    match firstRefutablePattern p with
+    | some i =>
+      if i > 0 then
+        traceStep ("move var to front")
+        process (moveToFront p i)
+        return
+    | none =>
+      if 1 < p.alts.length then
+        traceStep ("drop all but first alt")
+        -- all patterns are irrefutable, we can drop all other alts
+        let p := { p with alts := p.alts.take 1 }
+        process p
+        return
 
   if (← isNatValueTransition p) then
     traceStep ("nat value to constructor")

tests/lean/run/issue10749.lean

@@ -89,3 +89,22 @@ fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 =>
 -/
 #guard_msgs in
 #print test4.match_1
+
+-- Just testing the backwards compatibility option
+
+set_option match.ignoreUnusedAlts true in
+set_option backwards.match.rowMajor false in
+def testOld (a : List Nat) : Nat :=
+  match a with
+  | _ => 3
+  | [] => 4
+
+-- Has unnecessary `casesOn`
+
+/--
+info: def testOld.match_1.{u_1} : (motive : List Nat → Sort u_1) →
+  (a : List Nat) → ((x : List Nat) → motive x) → (Unit → motive []) → motive a :=
+fun motive a h_1 h_2 => List.casesOn a (h_1 []) fun head tail => h_1 (head :: tail)
+-/
+#guard_msgs in
+#print testOld.match_1