feat: Add REPL command for assigning an expression
This commit is contained in:
parent
b381d89ff9
commit
82f5494718
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue