From 5a4226f2bdcc6299df76285b1d30f238546c09fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Nov 2025 16:33:38 -0800 Subject: [PATCH] refactor: remove old `grind``SearchM` framework (#11226) This PR finally removes the old `grind` framework `SearchM`. It has been replaced with the new `Action` framework. --- src/Lean/Elab/Tactic/Grind/Basic.lean | 37 ++- src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 33 ++- src/Lean/Elab/Tactic/Grind/Have.lean | 8 +- src/Lean/Meta/Tactic/Grind/Intro.lean | 111 --------- src/Lean/Meta/Tactic/Grind/Lookahead.lean | 41 ++-- src/Lean/Meta/Tactic/Grind/SearchM.lean | 216 ------------------ src/Lean/Meta/Tactic/Grind/Split.lean | 59 ----- 7 files changed, 51 insertions(+), 454 deletions(-) delete mode 100644 src/Lean/Meta/Tactic/Grind/SearchM.lean diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean index 2e60d556b6..ec8e4fc285 100644 --- a/src/Lean/Elab/Tactic/Grind/Basic.lean +++ b/src/Lean/Elab/Tactic/Grind/Basic.lean @@ -7,7 +7,6 @@ module prelude public import Lean.Elab.Tactic.Basic public import Lean.Meta.Tactic.Grind.Main -public import Lean.Meta.Tactic.Grind.SearchM import Lean.CoreM import Lean.Meta.Tactic.Grind.Intro import Lean.Meta.Tactic.Grind.PP @@ -301,15 +300,6 @@ def liftGoalM (k : GoalM α) : GrindTacticM α := do replaceMainGoal [goal] return a -def liftSearchM (k : SearchM α) : GrindTacticM α := do - let goal ← getMainGoal - let (a, state) ← liftGrindM <| SearchM.run goal k - unless state.choiceStack.isEmpty do - -- **TODO**: Convert pending goals into new subgoals. - throwError "`grind` internal error, `SearchM` action has pending choices, this is not supported yet." - replaceMainGoal [state.goal] - return a - def liftAction (a : Action) : GrindTacticM Unit := do let goal ← getMainGoal let ka := fun _ => throwError "tactic is not applicable" @@ -382,17 +372,22 @@ def mkEvalTactic (params : Params) : TacticM (Goal → TSyntax `grind → GrindM def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) : TacticM (α × State) := do let evalTactic ← mkEvalTactic params - let (methods, ctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params (evalTactic? := some evalTactic) fun goal => do - let methods ← getMethods - -- **Note**: We use `withCheapCasesOnly` to ensure multiple goals are not created. - -- We will add support for this case in the future. - let (goal, _) ← withCheapCasesOnly <| SearchM.run goal do - intros 0; discard <| assertAll - getGoal - let goals := if goal.inconsistent then [] else [goal] - let ctx ← readThe Meta.Grind.Context - let state ← get - pure (methods, ctx, { state, goals }) + /- + **Note**: We don't want to close branches using `sorry` after applying `intros + assertAll`. + Reconsider the option `useSorry`. + -/ + let params' := { params with config.useSorry := false } + let (methods, ctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params' (evalTactic? := some evalTactic) fun goal => do + let a : Action := Action.intros 0 >> Action.assertAll + let goals ← match (← a.run goal) with + | .closed _ => pure [] + | .stuck gs => pure gs + let methods ← getMethods + let ctx ← readThe Meta.Grind.Context + /- Restore original config -/ + let ctx := { ctx with config := params.config } + let state ← get + pure (methods, ctx, { state, goals }) let tctx ← read k { tctx with methods, ctx, params } |>.run state diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean index 44b9bff8c0..8dee415764 100644 --- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean @@ -135,16 +135,13 @@ def logTheoremAnchor (proof : Expr) : TermElabM Unit := do Term.addTermInfo' stx proof def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit := do + -- **TODO**: add `instantiate` action that takes `thms` let progress ← liftGoalM do let thms ← thms.mapM (preprocessTheorem · 0) if only then ematchOnly thms else ematch thms unless progress do throwError "`instantiate` tactic failed to instantiate new facts, use `show_patterns` to see active theorems and their patterns." - let goal ← getMainGoal - let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do - discard <| assertAll - getGoal - replaceMainGoal [goal] + liftAction Action.assertAll @[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do let `(grind| instantiate $[ only%$only ]? $[ approx ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax @@ -268,30 +265,28 @@ def logAnchor (c : SplitInfo) : TermElabM Unit := do -/ Term.addTermInfo' stx e (isDisplayableTerm := True) +def split? (c : SplitInfo) : Action := fun goal kna kp => do + let (.ready numCases isRec _, goal) ← GoalM.run goal (checkSplitStatus c) + | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}" + let gen := goal.getGeneration c.getExpr + let genNew := if numCases > 1 || isRec then gen+1 else gen + let a : Action := + Action.splitCore c numCases isRec (stopAtFirstFailure := false) (compress := false) >> Action.intros genNew >> Action.assertAll + a goal kna kp + @[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax let anchorRef ← elabAnchorRef anchor let goal ← getMainGoal let candidates := goal.split.candidates - let (c, goals, genNew) ← liftSearchM do + let c ← liftGrindM <| goal.withContext do for c in candidates do let anchor ← c.getAnchor if anchorRef.matches anchor then - let some result ← split? c - | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}" - return (c, result) + return c throwError "`cases` tactic failed, invalid anchor" goal.withContext <| withRef anchor <| logAnchor c - let goals ← goals.filterMapM fun goal => do - let goal := { goal with ematch.num := 0 } - let (goal, _) ← liftGrindM <| SearchM.run goal do - intros genNew; discard <| assertAll - getGoal - if goal.inconsistent then - return none - else - return some goal - replaceMainGoal goals + liftAction <| split? c def mkCasesSuggestions (candidates : Array SplitCandidateWithAnchor) (numDigits : Nat) : MetaM (Array Tactic.TryThis.Suggestion) := do candidates.mapM fun { anchor, e, .. } => do diff --git a/src/Lean/Elab/Tactic/Grind/Have.lean b/src/Lean/Elab/Tactic/Grind/Have.lean index f5dcf3c145..7779096189 100644 --- a/src/Lean/Elab/Tactic/Grind/Have.lean +++ b/src/Lean/Elab/Tactic/Grind/Have.lean @@ -39,10 +39,8 @@ where let goal ← getMainGoal let mvarId ← goal.mvarId.assert n t v let goal := { goal with mvarId } - let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do - intros 0 - getGoal replaceMainGoal [goal] + liftAction <| Action.intros 0 @[builtin_grind_tactic Parser.Tactic.Grind.haveSilent] def evalHaveSilent : GrindTactic := fun stx => withMainContext do let `(grind| have $[$id?:ident]? : $prop:term) := stx | throwUnsupportedSyntax @@ -61,9 +59,7 @@ where let v ← instantiateMVars mvar let mvarId ← goal.mvarId.assert id prop v let goal := { goal with mvarId } - let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do - intros 0 - getGoal setGoals (goal :: goals) + liftAction <| Action.intros 0 end Lean.Elab.Tactic.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean index 055159d4e2..5e30a4cd7b 100644 --- a/src/Lean/Meta/Tactic/Grind/Intro.lean +++ b/src/Lean/Meta/Tactic/Grind/Intro.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura module prelude public import Init.Grind.Lemmas -public import Lean.Meta.Tactic.Grind.SearchM public import Lean.Meta.Tactic.Grind.Action import Lean.Meta.Tactic.Apply import Lean.Meta.Tactic.Grind.Simp @@ -300,114 +299,4 @@ def assertAll : Action := end Action -/-! -**------------------------------------------** -**------------------------------------------** -**TODO** Delete rest of the file -**------------------------------------------** -**------------------------------------------** --/ - -private def applyCases? (fvarId : FVarId) (generation : Nat) : SearchM Bool := withCurrGoalContext do - /- - Remark: we used to use `whnfD`. This was a mistake, we don't want to unfold user-defined abstractions. - Example: `a ∣ b` is defined as `∃ x, b = a * x` - -/ - let type ← whnf (← fvarId.getType) - if isEagerCasesCandidate (← getGoal) type then - if (← cheapCasesOnly) then - unless (← isCheapInductive type) do - return false - if let .const declName _ := type.getAppFn then - saveCases declName - let goal ← getGoal - let mvarId ← goal.mkAuxMVar - let mvarIds ← cases mvarId (mkFVar fvarId) - let goals := mvarIds.map fun mvarId => { goal with mvarId } - mkChoice (mkMVar mvarId) goals generation - return true - return false - -/-- -Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -or is inconsistent. --/ -def intros (generation : Nat) : SearchM Unit := withCurrGoalContext do - repeat - if (← isInconsistent) then - return () - match (← introNext (← getGoal) generation) with - | .done goal => - let goal ← exfalsoIfNotProp goal - if let some mvarId ← goal.mvarId.byContra? then - setGoal { goal with mvarId } - else - setGoal goal - return () - | .newDepHyp goal => - setGoal goal - | .newLocal fvarId goal => - setGoal goal - discard <| applyCases? fvarId generation - | .newHyp fvarId goal => - if let some goal ← applyInjection? goal fvarId then - setGoal goal - else - setGoal goal - if (← applyCases? fvarId generation) then - pure () - else - addHypothesis fvarId generation - -/-- -Similar to `intros`, but returns `true` if new hypotheses have been added, -and `false` otherwise. --/ -def intros' (generation : Nat) : SearchM Bool := do - let target ← (← getGoal).mvarId.getType - if target.isFalse then return false - intros generation - return true - -/-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/ -private def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : SearchM Unit := do - if isEagerCasesCandidate (← getGoal) prop then - let goal ← getGoal - let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof - setGoal { goal with mvarId } - intros generation - else withCurrGoalContext do - let r ← preprocess prop - let prop' := r.expr - let proof' := mkApp4 (mkConst ``Eq.mp [levelZero]) prop r.expr (← r.getProof) proof - add prop' proof' generation - -/-- -Asserts next fact in the `goal` fact queue. -Returns `true` if the queue was not empty and `false` otherwise. --/ -def assertNext : SearchM Bool := do - if (← isInconsistent) then return false - let goal ← getGoal - let some (fact, newRawFacts) := goal.newRawFacts.dequeue? - | return false - setGoal { goal with newRawFacts } - withSplitSource fact.splitSource do - -- Remark: we should probably add `withGeneration` - assertAt fact.proof fact.prop fact.generation - return true - -/-- -Asserts all facts in the `goal` fact queue. -Returns `true` if the queue was not empty and `false` otherwise. --/ -def assertAll : SearchM Bool := do - let mut progress := false - repeat - if (← assertNext) then - progress := true - else - return progress - unreachable! - end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Lookahead.lean b/src/Lean/Meta/Tactic/Grind/Lookahead.lean index 2393bdea0e..11302108c6 100644 --- a/src/Lean/Meta/Tactic/Grind/Lookahead.lean +++ b/src/Lean/Meta/Tactic/Grind/Lookahead.lean @@ -14,18 +14,24 @@ import Lean.Meta.Tactic.Grind.EMatchAction public section namespace Lean.Meta.Grind -private partial def solve (generation : Nat) : SearchM Bool := withIncRecDepth do - unless (← get).choiceStack.isEmpty do - return false -- `splitNext` should have been configured to not create choice points - if (← getGoal).inconsistent then - return true - if (← intros' generation <||> assertAll <||> Solvers.check <||> splitNext <||> ematch) then - solve generation - else - return false +/- +This code is not used anymore. +TODO: Decide whether we should delete it or not. +-/ --- **TODO**: use `_action` instead of `solve` -private def tryLookahead (e : Expr) (_action : Action) : GoalM Bool := +private abbrev maxIterations := 10000 -- **TODO**: Add option + +private def solve (goal : Goal) (generation : Nat) : GrindM (Option Goal) := do + let solvers ← Solvers.mkAction + let step : Action := solvers <|> Action.splitNext <|> Action.instantiate + let a := Action.intros generation >> Action.assertAll >> step.loop maxIterations + match (← a.run goal) with + | .closed _ => return none + | .stuck gs => + let goal :: _ := gs | return some goal + return some goal + +private def tryLookahead (e : Expr) : GoalM Bool := withTheReader Grind.Context (fun ctx => { ctx with config.qlia := true, cheapCases := true }) do -- TODO: if `e` is an arithmetic expression, we can avoid creating an auxiliary goal. @@ -39,8 +45,7 @@ private def tryLookahead (e : Expr) (_action : Action) : GoalM Bool := let mvar ← mkFreshExprSyntheticOpaqueMVar target tag let goalAux := { goal with mvarId := mvar.mvarId!, newFacts := {} } let gen ← getGeneration e - let (ok, _) ← (solve gen).run goalAux - if ok then + if (← solve goalAux gen).isNone then return some (← instantiateMVars mvar) else return none @@ -52,13 +57,6 @@ private def tryLookahead (e : Expr) (_action : Action) : GoalM Bool := else return false -public abbrev maxIterations := 1000 -- **TODO**: Add option - -private def mkLookaheadAction : IO Action := do - let solvers ← Solvers.mkAction - let step : Action := Action.done <|> solvers <|> Action.splitNext <|> Action.instantiate - return step.loop maxIterations - def lookahead : GoalM Bool := do unless (← getConfig).lookahead do return false @@ -67,7 +65,6 @@ def lookahead : GoalM Bool := do let mut postponed := [] let mut progress := false let infos := (← get).split.lookaheads - let action ← mkLookaheadAction modify fun s => { s with split.lookaheads := [] } for info in infos do if (← isInconsistent) then @@ -77,7 +74,7 @@ def lookahead : GoalM Bool := do | .ready _ _ true | .notReady => postponed := info :: postponed | .ready _ _ false => - if (← tryLookahead info.getExpr action) then + if (← tryLookahead info.getExpr) then progress := true else postponed := info :: postponed diff --git a/src/Lean/Meta/Tactic/Grind/SearchM.lean b/src/Lean/Meta/Tactic/Grind/SearchM.lean deleted file mode 100644 index 17db7f874d..0000000000 --- a/src/Lean/Meta/Tactic/Grind/SearchM.lean +++ /dev/null @@ -1,216 +0,0 @@ -/- -Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -module -prelude -public import Lean.Meta.Tactic.Grind.Types -import Lean.Util.ForEachExpr -public section -namespace Lean.Meta.Grind -/-- -A `choice` (aka backtracking) point in the search tree. --/ -structure Choice where - info? : Option SplitInfo - /-- - Goal where the case-split was performed. - Invariant: `goalPending.mvarId` is not assigned. - -/ - goalPending : Goal - /-- - Expression to be assigned to `goalPending.mvarId` if it is not possible to perform - non-chronological backtracking. - `proof` is often a `casesOn` application containing meta-variables. - -/ - proof : Expr - /-- - Subgoals that still need to be processed. - -/ - todo : List Goal - generation : Nat - deriving Inhabited - -structure SearchM.State where - goal : Goal - choiceStack : List Choice := [] - -abbrev SearchM := StateRefT SearchM.State GrindM - -def getGoal : SearchM Goal := - return (← get).goal - -def setGoal (goal : Goal) : SearchM Unit := - modify fun s => { s with goal } - -abbrev withCurrGoalContext (x : SearchM α) : SearchM α := do - (← getGoal).mvarId.withContext x - -abbrev liftGoalM (x : GoalM α) : SearchM α := do - let (a, goal) ← withCurrGoalContext do x.runCore (← get).goal - modify fun s => { s with goal } - return a - -instance : MonadLift GoalM SearchM where - monadLift := liftGoalM - -@[inline] def SearchM.run (goal : Goal) (x : SearchM α) : GrindM (α × SearchM.State) := - goal.mvarId.withContext do StateRefT'.run x { goal } - -/-- -Given a proof containing meta-variables corresponding to the given subgoals, -create a choice point. -- If there are no choice points, we just close the current goal using `proof`. -- If there is only one subgoal `s`, we close the current goal using `proof`, and -update current goal using `s`. -- If there are more than one `s :: ss`, we create a choice point using the current -goal as the pending goal, and update the current goal with `s`. --/ -def mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) (info? : Option SplitInfo := none) : SearchM Unit := do - assert! !(← isInconsistent) - match subgoals with - | [] => - (← getGoal).mvarId.assign proof - modify fun s => { s with goal.inconsistent := true } - | [subgoal] => - (← getGoal).mvarId.assign proof - setGoal subgoal - | subgoal :: subgoals => - let goalPending ← getGoal - modify fun s => { s with - goal := subgoal - choiceStack := { info?, goalPending, proof, generation, todo := subgoals } :: s.choiceStack - } - -/-- -Returns the maximum free variable id occurring in `e` --/ -private def findMaxFVarIdx? (e : Expr) : MetaM (Option Nat) := do - let go (e : Expr) : StateT (Option Nat) MetaM Bool := do - unless e.hasFVar do return false - let .fvar fvarId := e | return true - let localDecl ← fvarId.getDecl - modify fun - | none => some localDecl.index - | some index => some (max index localDecl.index) - return false - let (_, s?) ← e.forEach' go |>.run none - return s? - -private def resetChoiceStack : SearchM Unit := - modify fun s => { s with choiceStack := [] } - -/-- -Use `falseProof` to close the last pending goal in the choice stack, -and reset it. -We use this function when `falseProof` does not have free variables. --/ -private def closeLastPending (falseProof : Expr) : SearchM Unit := do - let choices := (← get).choiceStack - if h : choices.isEmpty then - return - else - let last := choices.getLast (ne_of_apply_ne List.isEmpty h) |>.goalPending - last.mvarId.assignFalseProof falseProof - resetChoiceStack - -/-- -Auxiliary function for implementing `nextGoal`. -It is similar to `nextGoal`, but uses chronological backtracking. -We use it when we cannot extract a proof of `False` from proof used to close the current goal. -Returns `some gen` if a new goal was found for a choice point with generation `gen`, -and returns `none` otherwise. --/ -private def nextChronoGoal? : SearchM (Option Nat) := do - let mut choices := (← get).choiceStack - repeat - match choices with - | [] => return none - | choice :: choices' => - match choice.todo with - | [] => - -- Choice point has been fully resolved. - -- Go to next one. - choice.goalPending.mvarId.assign choice.proof - choices := choices' - | goal :: todo => - let choice := { choice with todo } - modify fun s => { s with - goal - choiceStack := choice :: choices' - } - return some choice.generation - unreachable! - -private def isTargetFalse (mvarId : MVarId) : MetaM Bool := do - return (← mvarId.getType).isFalse - -private def getFalseProof? (mvarId : MVarId) : MetaM (Option Expr) := mvarId.withContext do - let proof ← instantiateMVars (mkMVar mvarId) - if (← isTargetFalse mvarId) then - return some proof - else if proof.isAppOfArity ``False.elim 2 || proof.isAppOfArity ``False.casesOn 2 then - return some proof.appArg! - else - return none - -/-- -Select the next goal to be processed from the `choiceStack`. -This function assumes the current goal has been closed (i.e., `inconsistent` is `true`) -Returns `some gen` if a new goal was found for a choice point with generation `gen`, -and returns `none` otherwise. --/ -def nextGoal? : SearchM (Option Nat) := do - let mut choices := (← get).choiceStack - if choices.isEmpty then - return none -- done - let goal := (← get).goal - assert! goal.inconsistent - let some falseProof ← getFalseProof? goal.mvarId - | nextChronoGoal? - let mut falseProof := falseProof - let some max ← goal.mvarId.withContext <| findMaxFVarIdx? falseProof - | closeLastPending falseProof; return none - let mut maxFVarIdx := max - repeat - let choice :: choices' := choices - | resetChoiceStack; return none - let mvarDecl ← choice.goalPending.mvarId.getDecl - let numIndices := mvarDecl.lctx.numIndices - if maxFVarIdx < numIndices then - -- `falseProof` can close `choice.goalPending` since all its free-variables are in scope. - choice.goalPending.mvarId.assignFalseProof falseProof - -- keep looking at next choice point - -- Remark: we may be able to find other choice points using falseProof. - choices := choices' - else match choice.todo with - | [] => - -- All subgoals have been solved. We can finally assign `choice.proof` to `goalPending.mvarId`. - let proof ← instantiateMVars choice.proof - choice.goalPending.mvarId.assign proof - if (← isTargetFalse choice.goalPending.mvarId) then - -- `proof` is a proof of `False`, we can continue using non-chronological backtracking - falseProof := proof - let some max ← choice.goalPending.mvarId.withContext <| findMaxFVarIdx? falseProof - | closeLastPending falseProof; return none - maxFVarIdx := max - choices := choices' - else - -- `proof` is not a proof of `False`. Thus, we switch to chronological backtracking. - -- This case can only happen if we are using eager case-splitting with types with - -- more than one constructor. - modify fun s => { s with choiceStack := choices' } - return (← nextChronoGoal?) - | goal :: todo => - -- Found `next` goal to be processed. - -- Update the current choice point, and current goal. - let choice := { choice with todo } - modify fun s => { s with - goal - choiceStack := choice :: choices' - } - return some choice.generation - unreachable! - -end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean index 67e6b1d150..8b66155b68 100644 --- a/src/Lean/Meta/Tactic/Grind/Split.lean +++ b/src/Lean/Meta/Tactic/Grind/Split.lean @@ -5,7 +5,6 @@ Authors: Leonardo de Moura -/ module prelude -public import Lean.Meta.Tactic.Grind.SearchM public import Lean.Meta.Tactic.Grind.Action public import Lean.Meta.Tactic.Grind.Anchor import Lean.Meta.Tactic.Grind.Intro @@ -491,62 +490,4 @@ def splitNext (stopAtFirstFailure := true) (compress := true) : Action := fun go end Action -/-! -**------------------------------------------** -**------------------------------------------** -**TODO** Delete rest of the file -**------------------------------------------** -**------------------------------------------** --/ - -/-- -Performs a case-split using `c`. -Remarks: -- `mvarId` is not necessarily `(← getGoal).mvarId`, `splitNext` creates an auxiliary meta-variable - to be able to implement non-chronological backtracking. -- `numCases` and `isRec` are computed using `checkSplitStatus`. --/ -private def splitCore (mvarId : MVarId) (c : SplitInfo) (numCases : Nat) (isRec : Bool) : SearchM (List Goal × Nat) := do - let cExpr := c.getExpr - let gen ← getGeneration cExpr - let genNew := if numCases > 1 || isRec then gen+1 else gen - saveSplitDiagInfo cExpr genNew numCases c.source - markCaseSplitAsResolved cExpr - trace_goal[grind.split] "{cExpr}, generation: {gen}" - let mvarIds ← if let .imp e h _ := c then - casesWithTrace mvarId (mkGrindEM (e.forallDomain h)) - else if (← isMatcherApp cExpr) then - casesMatch mvarId cExpr - else - casesWithTrace mvarId (← mkCasesMajor cExpr) - let goal ← getGoal - let numSubgoals := mvarIds.length - let goals := mvarIds.mapIdx fun i mvarId => { goal with - mvarId - split.trace := { expr := cExpr, i, num := numSubgoals, source := c.source } :: goal.split.trace - } - return (goals, genNew) - -/-- -Selects a case-split from the list of candidates, and adds new choice point -(aka backtracking point). Returns true if successful. --/ -def splitNext : SearchM Bool := withCurrGoalContext do - let .some info numCases isRec _ ← selectNextSplit? - | return false - let mvarId ← (← getGoal).mkAuxMVar - let (goals, genNew) ← splitCore mvarId info numCases isRec - mkChoice (mkMVar mvarId) goals genNew (info? := some info) - intros genNew - return true - -/-- -Tries to perform a case-split using `c`. Returns `none` if `c` has already been resolved or -is not ready. --/ -def split? (c : SplitInfo) : SearchM (Option (List Goal × Nat)) := do - let .ready numCases isRec _ ← checkSplitStatus c | return none - let mvarId := (← getGoal).mvarId - return some (← splitCore mvarId c numCases isRec) - end Lean.Meta.Grind