|
|
@ -14,7 +14,7 @@ structure Context where
|
|
|
|
structure State where
|
|
|
|
structure State where
|
|
|
|
options : Protocol.Options := {}
|
|
|
|
options : Protocol.Options := {}
|
|
|
|
nextId : Nat := 0
|
|
|
|
nextId : Nat := 0
|
|
|
|
goalStates : Std.HashMap Nat GoalState := Std.HashMap.empty
|
|
|
|
goalStates : Std.HashMap Nat GoalState := Std.HashMap.emptyWithCapacity
|
|
|
|
|
|
|
|
|
|
|
|
env : Environment
|
|
|
|
env : Environment
|
|
|
|
-- Parser state
|
|
|
|
-- Parser state
|
|
|
@ -225,7 +225,7 @@ def execute (command: Protocol.Command): MainM Json := do
|
|
|
|
reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
|
|
|
|
reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
|
|
|
|
let state ← getMainState
|
|
|
|
let state ← getMainState
|
|
|
|
let nGoals := state.goalStates.size
|
|
|
|
let nGoals := state.goalStates.size
|
|
|
|
set { state with nextId := 0, goalStates := .empty }
|
|
|
|
set { state with nextId := 0, goalStates := .emptyWithCapacity }
|
|
|
|
return { nGoals }
|
|
|
|
return { nGoals }
|
|
|
|
stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
|
|
|
|
stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
|
|
|
|
let state ← getMainState
|
|
|
|
let state ← getMainState
|
|
|
|