aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Allow selective continuation of goals #27

Merged
aniva merged 14 commits from goal/continuation into dev 2023-11-07 16:49:56 -08:00
Conversation 1 Commits 14 Files Changed 13 +22 -5
2 changed files with 22 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 736e68639f - Show all commits

8
Pantograph.lean
View File

@ -54,7 +54,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get let state ← get
let nGoals := state.goalStates.size let nGoals := state.goalStates.size
set { state with goalStates := Lean.HashMap.empty } set { state with nextId := 0, goalStates := Lean.HashMap.empty }
return .ok { nGoals } return .ok { nGoals }
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get let state ← get
@ -163,8 +163,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .error error => return .error error | .error error => return .error error
| .ok (.success nextGoalState) => | .ok (.success nextGoalState) =>
let nextStateId := state.nextId let nextStateId := state.nextId
let goalStates := state.goalStates.insert state.nextId goalState set { state with
set { state with goalStates, nextId := state.nextId + 1 } goalStates := state.goalStates.insert state.nextId nextGoalState,
nextId := state.nextId + 1,
}
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
return .ok { return .ok {
nextStateId? := .some nextStateId, nextStateId? := .some nextStateId,

19
Test/Integration.lean
View File

@ -83,11 +83,19 @@ def test_malformed_command : IO LSpec.TestSeq :=
Protocol.InteractionError)) Protocol.InteractionError))
] ]
def test_tactic : IO LSpec.TestSeq := def test_tactic : IO LSpec.TestSeq :=
let goal: Protocol.Goal := { let goal1: Protocol.Goal := {
name := "_uniq.10", name := "_uniq.10",
target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
} }
let goal2: Protocol.Goal := {
name := "_uniq.13",
target := { pp? := .some "x ∨ y → y ∨ x" },
vars := #[
{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
],
}
subroutine_runner [ subroutine_runner [
subroutine_step "goal.start" subroutine_step "goal.start"
[("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
@ -97,7 +105,14 @@ def test_tactic : IO LSpec.TestSeq :=
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
(Lean.toJson ({ (Lean.toJson ({
nextStateId? := .some 1, nextStateId? := .some 1,
goals? := #[goal], goals? := #[goal1],
}:
Protocol.GoalTacticResult)),
subroutine_step "goal.tactic"
[("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
(Lean.toJson ({
nextStateId? := .some 2,
goals? := #[goal2],
}: }:
Protocol.GoalTacticResult)) Protocol.GoalTacticResult))
] ]