From 754fb69cffa23f97cd917bf9a59d88bb72c71b3a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 Nov 2023 15:33:53 -0700 Subject: [PATCH] feat: Partial state continuation --- Pantograph/Goal.lean | 32 ++++++++++++++++-------------- Test/Holes.lean | 46 ++++++++++++++++++++++++++++++++++++++++++-- Test/Proofs.lean | 2 +- 3 files changed, 63 insertions(+), 17 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index eeb5a10..fd24232 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -169,30 +169,34 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String return .failure #[← exception.toMessageData.toString] 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 := - let goals := match goals with - | .some goals => goals - | .none => target.goals - if target.root != graftee.root then - .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" +/-- +Brings into scope a list of goals +-/ +protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := + if ¬ (goals.all (λ goal => state.mvars.contains goal)) then + .error s!"Goals not in scope" else -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. let unassigned := goals.filter (λ goal => - let mctx := graftee.mctx + let mctx := state.mctx ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) .ok { + state with savedState := { - term := graftee.savedState.term, + term := state.savedState.term, 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 := let expr := goalState.mctx.eAssignment.find! goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) diff --git a/Test/Holes.lean b/Test/Holes.lean index 9b38087..8692c2a 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -85,7 +85,7 @@ def test_m_couple: TestM Unit := do addTest $ assertUnreachable $ other.toString return () 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 addTest $ assertUnreachable $ msg return () @@ -136,6 +136,47 @@ def test_proposition_generation: TestM Unit := do addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome 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 let env: Lean.Environment ← Lean.importModules @@ -144,7 +185,8 @@ def suite: IO LSpec.TestSeq := do (trustLevel := 1) let tests := [ ("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 (name, tests) := tests diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8ec01a7..0d5fb4e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -253,7 +253,7 @@ def proof_or_comm: TestM Unit := do addTest $ LSpec.check " assumption" state4_2.goals.isEmpty addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone -- 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 addTest $ assertUnreachable $ msg return ()