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
3 changed files with 4 additions and 2 deletions
Showing only changes of commit 245e76b2f1 - Show all commits

View File

@ -143,7 +143,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let goalState ← GoalState.create expr let goalState ← GoalState.create expr
let (goalStates, stateId) := state.goalStates.insert goalState let (goalStates, stateId) := state.goalStates.insert goalState
set { state with goalStates } set { state with goalStates }
return .ok { stateId } return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get let state ← get
match state.goalStates.get? args.stateId with match state.goalStates.get? args.stateId with

View File

@ -142,6 +142,8 @@ structure GoalStart where
deriving Lean.FromJson deriving Lean.FromJson
structure GoalStartResult where structure GoalStartResult where
stateId: Nat := 0 stateId: Nat := 0
-- Name of the root metavariable
root: String
deriving Lean.ToJson deriving Lean.ToJson
structure GoalTactic where structure GoalTactic where
-- Identifiers for tree, state, and goal -- Identifiers for tree, state, and goal

View File

@ -91,7 +91,7 @@ def test_tactic : IO LSpec.TestSeq :=
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")]
(Lean.toJson ({stateId := 0}: (Lean.toJson ({stateId := 0, root := "_uniq.8"}:
Protocol.GoalStartResult)), Protocol.GoalStartResult)),
subroutine_step "goal.tactic" subroutine_step "goal.tactic"
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]