feat: Partial state continuation

This commit is contained in:
Leni Aniva 2023-11-04 15:33:53 -07:00
parent dc2cc5be77
commit 754fb69cff
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 63 additions and 17 deletions

View File

@ -169,30 +169,34 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
/-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/ /--
protected def GoalState.continue (target: GoalState) (graftee: GoalState) (goals: Option (List MVarId) := .none): Except String GoalState := Brings into scope a list of goals
let goals := match goals with -/
| .some goals => goals protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
| .none => target.goals if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
if target.root != graftee.root then .error s!"Goals not in scope"
.error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}"
-- Ensure goals are not dangling
else if ¬ (goals.all (λ goal => graftee.mvars.contains goal)) then
.error s!"Some goals in target are not present in the graftee"
else else
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
let unassigned := goals.filter (λ goal => let unassigned := goals.filter (λ goal =>
let mctx := graftee.mctx let mctx := state.mctx
¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
.ok { .ok {
state with
savedState := { savedState := {
term := graftee.savedState.term, term := state.savedState.term,
tactic := { goals := unassigned }, tactic := { goals := unassigned },
}, },
root := target.root,
newMVars := graftee.newMVars,
} }
/--
Brings into scope all goals from `branch`
-/
protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
if target.root != branch.root then
.error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
else
target.resume (goals := branch.goals)
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
let expr := goalState.mctx.eAssignment.find! goalState.root let expr := goalState.mctx.eAssignment.find! goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)

View File

@ -85,7 +85,7 @@ def test_m_couple: TestM Unit := do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
let state1b ← match state1.continue state2 with let state1b ← match state2.continue state1 with
| .error msg => do | .error msg => do
addTest $ assertUnreachable $ msg addTest $ assertUnreachable $ msg
return () return ()
@ -136,6 +136,47 @@ def test_proposition_generation: TestM Unit := do
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
return () return ()
def test_partial_continuation: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "Nat"])
-- Execute a partial continuation
let coupled_goals := state1.goals ++ state2.goals
let state1b ← match state2.resume (goals := coupled_goals) with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Continuation should fail if the state does not exist:
match state0.resume coupled_goals with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
return ()
def suite: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules let env: Lean.Environment ← Lean.importModules
@ -144,7 +185,8 @@ def suite: IO LSpec.TestSeq := do
(trustLevel := 1) (trustLevel := 1)
let tests := [ let tests := [
("2 < 5", test_m_couple), ("2 < 5", test_m_couple),
("Proposition Generation", test_proposition_generation) ("Proposition Generation", test_proposition_generation),
("Partial Continuation", test_partial_continuation)
] ]
let tests ← tests.foldlM (fun acc tests => do let tests ← tests.foldlM (fun acc tests => do
let (name, tests) := tests let (name, tests) := tests

View File

@ -253,7 +253,7 @@ def proof_or_comm: TestM Unit := do
addTest $ LSpec.check " assumption" state4_2.goals.isEmpty addTest $ LSpec.check " assumption" state4_2.goals.isEmpty
addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
-- Ensure the proof can continue from `state4_2`. -- Ensure the proof can continue from `state4_2`.
let state2b ← match state2.continue state4_2 with let state2b ← match state4_2.continue state2 with
| .error msg => do | .error msg => do
addTest $ assertUnreachable $ msg addTest $ assertUnreachable $ msg
return () return ()