feat: Add REPL command for assigning an expression

This commit is contained in:
Leni Aniva 2023-10-27 15:32:59 -07:00
parent f064bb21a4
commit 3b1746490d
3 changed files with 38 additions and 11 deletions

View File

@ -133,9 +133,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
(match env.find? <| str_to_name copyFrom with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok cInfo.type)
| .none, .none =>
return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
| _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
| _, _ =>
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
match expr? with
| .error error => return .error error
| .ok expr =>
@ -147,9 +146,16 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get
match state.goalStates.get? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState =>
match ← GoalState.execute goalState args.goalId args.tactic with
| .success nextGoalState =>
| .some goalState => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
| .some tactic, .none => do
pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
| .none, .some expr => do
pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr))
| _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
match nextGoalState? with
| .error error => return .error error
| .ok (.success nextGoalState) =>
let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
set { state with goalStates }
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
@ -157,11 +163,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
nextStateId? := .some nextStateId,
goals? := .some goals,
}
| .parseError message =>
| .ok (.parseError message) =>
return .ok { parseError? := .some message }
| .indexError goalId =>
| .ok (.indexError goalId) =>
return .error $ errorIndex s!"Invalid goal id index {goalId}"
| .failure messages =>
| .ok (.failure messages) =>
return .ok { tacticErrors? := .some messages }
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get

View File

@ -146,7 +146,9 @@ structure GoalTactic where
-- Identifiers for tree, state, and goal
stateId: Nat
goalId: Nat := 0
tactic: String
-- One of the fields here must be filled
tactic?: Option String := .none
expr?: Option String := .none
deriving Lean.FromJson
structure GoalTacticResult where
-- The next goal state id. Existence of this field shows success

View File

@ -82,12 +82,31 @@ def test_malformed_command : IO LSpec.TestSeq :=
error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
Protocol.InteractionError))
]
def test_tactic : IO LSpec.TestSeq :=
let goal: Protocol.Goal := {
target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
subroutine_runner [
subroutine_step "goal.start"
[("expr", .str "∀ (p q: Prop), p q → q p")]
(Lean.toJson ({stateId := 0}:
Protocol.GoalStartResult)),
subroutine_step "goal.tactic"
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
(Lean.toJson ({
nextStateId? := .some 1,
goals? := #[goal],
}:
Protocol.GoalTacticResult))
]
def suite: IO LSpec.TestSeq := do
return LSpec.group "Integration" $
(LSpec.group "Option modify" (← test_option_modify)) ++
(LSpec.group "Malformed command" (← test_malformed_command))
(LSpec.group "Malformed command" (← test_malformed_command)) ++
(LSpec.group "Tactic" (← test_tactic))
end Pantograph.Test.Integration