refactor: use match compilation to generate splitter

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -8,10 +8,12 @@ module
 prelude
 public import Lean.Elab.PreDefinition.FixedParams
 import Lean.Elab.PreDefinition.EqnsUtils
-import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.CasesOnStuckLHS
+import Lean.Meta.Tactic.Delta
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Delta
 import Lean.Meta.Tactic.CasesOnStuckLHS
+import Lean.Meta.Tactic.Split
 
 namespace Lean.Elab
 open Meta

src/Lean/Meta/Constructions/CasesOnSameCtor.lean

@@ -213,7 +213,9 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
           numDiscrs := info.numIndices + 3
           altInfos
           uElimPos? := some 0
-          discrInfos := #[{}, {}, {}]}
+          discrInfos := #[{}, {}, {}]
+          overlaps := {}
+        }
 
         -- Compare attributes with `mkMatcherAuxDefinition`
         withExporting (isExporting := !isPrivateName declName) do

src/Lean/Meta/IndPredBelow.lean

@@ -319,7 +319,7 @@ public partial def mkBelowMatcher (matcherApp : MatcherApp) (belowParams : Array
     (ctx : RecursionContext) (transformAlt : RecursionContext → Expr → MetaM Expr) :
     MetaM (Option (Expr × MetaM Unit)) :=
   withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} {matcherApp.toExpr} and {belowParams}") do
-  let mut input ← getMkMatcherInputInContext matcherApp
+  let mut input ← getMkMatcherInputInContext matcherApp (unfoldNamed := false)
   let mut discrs := matcherApp.discrs
   let mut matchTypeAdd := #[] -- #[(discrIdx, ), ...]
   let mut i := discrs.size

src/Lean/Meta/Match/Basic.lean

@@ -150,6 +150,11 @@ structure Alt where
   After we perform additional case analysis, their types become definitionally equal.
   -/
   cnstrs    : List (Expr × Expr)
+  /--
+  Indices of previous alternatives that this alternative expects a not-that-proofs.
+  (When producing a splitter, and in the future also for source-level overlap hypotheses.)
+  -/
+  notAltIdxs : Array Nat
   deriving Inhabited
 
 namespace Alt

src/Lean/Meta/Match/MatcherApp/Basic.lean

@@ -67,6 +67,7 @@ def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCases
         matcherName   := declName
         matcherLevels := declLevels.toArray
         uElimPos?, discrInfos, params, motive, discrs, alts, remaining, altInfos
+        overlaps := {} -- CasesOn constructor have no overlaps
       }
 
   return none

src/Lean/Meta/Match/MatcherInfo.lean

@@ -23,6 +23,9 @@ structure Overlaps where
   map : Std.HashMap Nat (Std.TreeSet Nat) := {}
 deriving Inhabited, Repr
 
+def Overlaps.isEmpty (o : Overlaps) : Bool :=
+  o.map.isEmpty
+
 def Overlaps.insert (o : Overlaps) (overlapping overlapped : Nat) : Overlaps where
   map := o.map.alter overlapped fun s? => some ((s?.getD {}).insert overlapping)
 
@@ -41,29 +44,32 @@ structure AltParamInfo where
   numOverlaps : Nat
   /-- Whether this alternatie has an artifcial `Unit` parameter -/
   hasUnitThunk : Bool
-deriving Inhabited, Repr
+deriving Inhabited, Repr, BEq
 
 /--
-A "matcher" auxiliary declaration has the following structure:
-- `numParams` parameters
-- motive
-- `numDiscrs` discriminators (aka major premises)
-- `altInfos.size` alternatives (aka minor premises) with parameter structure information
-- `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and
-   `pos` is the position of the universe level parameter that specifies the elimination universe.
-   It is `none` if the matcher only eliminates into `Prop`.
-- `overlaps` indicates which alternatives may overlap another
+Information about the structure of a matcher declaration
 -/
 structure MatcherInfo where
+  /-- Number of parameters -/
   numParams    : Nat
+  /-- Number of discriminants -/
   numDiscrs    : Nat
+  /-- Parameter structure information for each alternative -/
   altInfos     : Array AltParamInfo
+  /--
+  `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and
+  `pos` is the position of the universe level parameter that specifies the elimination universe.
+  It is `none` if the matcher only eliminates into `Prop`.
+  -/
   uElimPos?    : Option Nat
   /--
-    `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
+  `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
   -/
   discrInfos   : Array DiscrInfo
-  overlaps     : Overlaps := {}
+  /--
+  (Conservative approximation of) which alternatives may overlap another.
+  -/
+  overlaps     : Overlaps
 deriving Inhabited, Repr
 
 @[expose] def MatcherInfo.numAlts (info : MatcherInfo) : Nat :=

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/casesOnSameCtor.lean

@@ -38,8 +38,8 @@ info: Vec.match_on_same_ctor.{u_1, u} {α : Type u}
 /--
 info: Vec.match_on_same_ctor.splitter.{u_1, u} {α : Type u}
   {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
-  (h : t.ctorIdx = t✝.ctorIdx) (h_1 : Unit → motive nil nil ⋯)
-  (h_2 : (a : α) → (n : Nat) → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
+  (h : t.ctorIdx = t✝.ctorIdx) (nil : Unit → motive nil nil ⋯)
+  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
   motive t t✝ h
 -/
 #guard_msgs in

tests/lean/run/issue8274.lean

@@ -11,7 +11,7 @@ info: private def myTest.match_1.splitter.{u_1} : (motive : List Bool → Sort u
   (x : List Bool) →
     ((x_1 : Bool) → (xs : List Bool) → x = x_1 :: xs → motive (x_1 :: xs)) → (x = [] → motive []) → motive x :=
 fun motive x h_1 h_2 =>
-  List.casesOn (motive := fun x_1 => x = x_1 → motive x_1) x h_2 (fun head tail => h_1 head tail) ⋯
+  (fun x_1 => List.casesOn (motive := fun x_2 => x = x_2 → motive x_2) x_1 h_2 fun head tail => h_1 head tail) x ⋯
 -/
 #guard_msgs in
 #print myTest.match_1.splitter

tests/lean/run/match2.lean

@@ -1,7 +1,9 @@
 import Lean
 
+set_option linter.unusedVariables false
+
 def checkWithMkMatcherInput (matcher : Lean.Name) : Lean.MetaM Unit :=
-  Lean.Meta.Match.withMkMatcherInput matcher fun input => do
+  Lean.Meta.Match.withMkMatcherInput matcher (unfoldNamed := false) fun input => do
   let res ← Lean.Meta.Match.mkMatcher input
   let origMatcher ← Lean.getConstInfo matcher
   if not <| input.matcherName == matcher then

tests/lean/run/matchSparse.lean

@@ -9,6 +9,25 @@ def simple : Lean.Expr → Bool
   | .sort _ => true
   | _      => false
 
+/--
+info: def simple.match_1.{u_1} : (motive : Expr → Sort u_1) →
+  (x : Expr) → ((u : Level) → motive (sort u)) → ((x : Expr) → motive x) → motive x :=
+fun motive x h_1 h_2 => simple._sparseCasesOn_1 x (fun u => h_1 u) fun h => h_2 x
+-/
+#guard_msgs in
+#print simple.match_1
+
+-- Check that the splitter re-uses the sparseCasesOn generated for the matcher:
+
+/--
+info: private def simple.match_1.splitter.{u_1} : (motive : Expr → Sort u_1) →
+  (x : Expr) →
+    ((u : Level) → motive (sort u)) → ((x : Expr) → (∀ (u : Level), x = sort u → False) → motive x) → motive x :=
+fun motive x h_1 h_2 => simple._sparseCasesOn_1 x (fun u => h_1 u) fun h => h_2 x ⋯
+-/
+#guard_msgs in
+#print simple.match_1.splitter
+
 def expensive : Lean.Expr → Lean.Expr → Bool
   | .app (.app (.sort 1) (.sort 1)) (.sort 1), .app (.app (.sort 1) (.sort 1)) (.sort 1) => false
   | _, _ => true
@@ -49,6 +68,7 @@ info: expensive.match_1.splitter.{u_1} (motive : Expr → Expr → Sort u_1) (x
 -/
 #guard_msgs in
 #check expensive.match_1.splitter
+
 /--
 info: expensive.match_1.eq_1.{u_1} (motive : Expr → Expr → Sort u_1)
   (h_1 :

tests/lean/run/split1.lean

@@ -1,3 +1,6 @@
+-- set_option trace.Meta.Match.match true
+-- set_option trace.Meta.Match.matchEqs true
+
 def f (xs : List Nat) : Nat :=
   match xs with
   | [] => 1