More cleanup (and couldn’t-resist-to-shake)

Author: nomeata

src/Lean/Elab/Match.lean

@@ -12,6 +12,7 @@ public import Lean.Elab.BindersUtil
 public import Lean.Elab.PatternVar
 public import Lean.Elab.Quotation.Precheck
 public import Lean.Elab.SyntheticMVars
+import Lean.Meta.Match.Value
 
 public section
 

src/Lean/Meta/Match/Basic.lean

@@ -6,8 +6,14 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Lean.Meta.Basic
+public import Lean.Meta.Tactic.FVarSubst
 public import Lean.Meta.CollectFVars
-public import Lean.Meta.Match.CaseArraySizes
+import Lean.Meta.Match.Value
+import Lean.Meta.AppBuilder
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Assert
+import Lean.Meta.Tactic.Subst
 
 public section
 

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -6,32 +6,36 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Match.CaseValues
-
-public section
+public import Lean.Meta.Basic
+public import Lean.Meta.Tactic.FVarSubst
+import Lean.Meta.Match.CaseValues
+import Lean.Meta.AppBuilder
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Assert
+import Lean.Meta.Tactic.Subst
 
 namespace Lean.Meta
 
-structure CaseArraySizesSubgoal where
+public structure CaseArraySizesSubgoal where
   mvarId : MVarId
   elems  : Array FVarId := #[]
   diseqs : Array FVarId := #[]
   subst  : FVarSubst := {}
   deriving Inhabited
 
-def getArrayArgType (a : Expr) : MetaM Expr := do
+public def getArrayArgType (a : Expr) : MetaM Expr := do
   let aType ← inferType a
   let aType ← whnfD aType
   unless aType.isAppOfArity ``Array 1 do
     throwError "array expected{indentExpr a}"
   pure aType.appArg!
 
-private def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
+def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
   let lt    ← mkLt (mkRawNatLit i) (mkRawNatLit n)
   let ltPrf ← mkDecideProof lt
   mkAppM `Array.getLit #[a, mkRawNatLit i, h, ltPrf]
 
-private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
+partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
   let α ← getArrayArgType a
   let rec loop (i : Nat) (xs : Array Expr) (args : Array Expr) := do
     if i < n then
@@ -61,7 +65,7 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP
   n) `..., x_1 ... x_{sizes[n-1]}  |- C #[x_1, ..., x_{sizes[n-1]}]`
   n+1) `..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a`
   where `n = sizes.size` -/
-def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
+public def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
   mvarId.withContext do
     let a := mkFVar fvarId
     let aSize ← mkAppM `Array.size #[a]

src/Lean/Meta/Match/CaseValues.lean

@@ -6,29 +6,25 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Tactic.Subst
-public import Lean.Meta.Match.Value
-
-public section
+public import Lean.Meta.Basic
+public import Lean.Meta.Tactic.FVarSubst
+import Lean.Meta.Tactic.Subst
 
 namespace Lean.Meta
 
 structure CaseValueSubgoal where
   mvarId : MVarId
   newH   : FVarId
-  subst  : FVarSubst := {}
   deriving Inhabited
 
 /--
   Split goal `... |- C x` into two subgoals
-  `..., (h : x = value)  |- C value`
+  `..., (h : x = value)  |- C x`
   `..., (h : x != value) |- C x`
   where `fvarId` is `x`s id.
   The type of `x` must have decidable equality.
-
-  Remark: `subst` field of the second subgoal is equal to the input `subst`. -/
-private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h)
-    (subst : FVarSubst := {})
+ -/
+def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h)
     : MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
   mvarId.withContext do
     let tag ← mvarId.getTag
@@ -43,18 +39,16 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar]
     mvarId.assign val
     let (elseH, elseMVarId) ← elseMVar.mvarId!.intro1P
-    let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }
+    let elseSubgoal := { mvarId := elseMVarId, newH := elseH }
     let (thenH, thenMVarId) ← thenMVar.mvarId!.intro1P
     thenMVarId.withContext do
-      trace[Meta] "subst domain: {subst.domain.map (·.name)}"
-      let thenH := (subst.get thenH).fvarId!
       trace[Meta] "searching for decl"
       let _ ← thenH.getDecl
       trace[Meta] "found decl"
-    let thenSubgoal := { mvarId := thenMVarId, newH := (subst.get thenH).fvarId!, subst : CaseValueSubgoal }
+    let thenSubgoal := { mvarId := thenMVarId, newH := thenH }
     pure (thenSubgoal, elseSubgoal)
 
-structure CaseValuesSubgoal where
+public structure CaseValuesSubgoal where
   mvarId : MVarId
   newHs  : Array FVarId := #[]
   subst  : FVarSubst := {}
@@ -75,18 +69,14 @@ structure CaseValuesSubgoal where
 
   If `substNewEqs = true`, then the new `h_i` equality hypotheses are substituted in the first `n` cases.
 -/
-def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) : MetaM (Array CaseValuesSubgoal) :=
+public def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) : MetaM (Array CaseValuesSubgoal) :=
   let rec loop : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal)
     | _, mvarId, [],    _,  _        => throwTacticEx `caseValues mvarId "list of values must not be empty"
     | i, mvarId, v::vs, hs, subgoals => do
-      let (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {}
+      let (thenSubgoal, elseSubgoal) ← caseValue mvarId fvarId v (hNamePrefix.appendIndexAfter i)
       appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
-      let thenMVarId ← hs.foldlM
-        (fun thenMVarId h => match thenSubgoal.subst.get h with
-          | Expr.fvar fvarId => thenMVarId.tryClear fvarId
-          | _                => pure thenMVarId)
-        thenSubgoal.mvarId
-      let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH (symm := false) thenSubgoal.subst (clearH := true)
+      let thenMVarId ← thenSubgoal.mvarId.tryClearMany  hs
+      let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH (symm := false) {} (clearH := true)
       let subgoals := subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
       match vs with
       | [] => do

src/Lean/Meta/Match/Match.lean

@@ -13,6 +13,8 @@ public import Lean.Meta.Match.Basic
 public import Lean.Meta.Match.MatcherApp.Basic
 public import Lean.Meta.Match.MVarRenaming
 import Lean.Meta.HasNotBit
+import Lean.Meta.Match.CaseArraySizes
+import Lean.Meta.Match.CaseValues
 
 public section
 

src/Lean/Meta/Match/MatchEqsExt.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Basic
 public import Lean.Meta.Match.Basic
+public import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Eqns
 
 public section