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
2 changed files with 22 additions and 163 deletions
Showing only changes of commit 764be6d14b - Show all commits

View File

@ -1,8 +1,8 @@
import Pantograph.Goal
import Pantograph.Protocol
import Pantograph.SemihashMap
import Pantograph.Serial
import Pantograph.Symbol
import Lean.Data.HashMap
namespace Pantograph
@ -12,7 +12,8 @@ structure Context where
/-- Stores state of the REPL -/
structure State where
options: Protocol.Options := {}
goalStates: SemihashMap GoalState := SemihashMap.empty
nextId: Nat := 0
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
/-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
@ -53,7 +54,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
set { state with goalStates := SemihashMap.empty }
set { state with goalStates := Lean.HashMap.empty }
return .ok { nGoals }
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get
@ -141,12 +142,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .error error => return .error error
| .ok expr =>
let goalState ← GoalState.create expr
let (goalStates, stateId) := state.goalStates.insert goalState
set { state with goalStates }
let stateId := state.nextId
set { state with
goalStates := state.goalStates.insert stateId goalState,
nextId := state.nextId + 1
}
return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get
match state.goalStates.get? args.stateId with
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
@ -158,8 +162,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
match nextGoalState? with
| .error error => return .error error
| .ok (.success nextGoalState) =>
let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
set { state with goalStates }
let nextStateId := state.nextId
let goalStates := state.goalStates.insert state.nextId goalState
set { state with goalStates, nextId := state.nextId + 1 }
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
return .ok {
nextStateId? := .some nextStateId,
@ -173,12 +178,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get
match state.goalStates.get? args.target with
match state.goalStates.find? args.target with
| .none => return .error $ errorIndex s!"Invalid state index {args.target}"
| .some target => do
let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates.get? branchId with
match state.goalStates.find? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
@ -188,8 +193,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
match nextState? with
| .error error => return .ok { error? := .some error }
| .ok nextGoalState =>
let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
set { state with goalStates }
let nextStateId := state.nextId
set { state with
goalStates := state.goalStates.insert nextStateId nextGoalState,
nextId := state.nextId + 1
}
let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options)
return .ok {
nextStateId? := .some nextStateId,
@ -197,12 +205,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
}
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get
let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates
let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
set { state with goalStates }
return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
match state.goalStates.get? args.stateId with
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)

View File

@ -1,149 +0,0 @@
namespace Pantograph.SemihashMap
structure Imp (β: Type u) where
data: Array (Option β)
-- Number of elements currently in use
size: Nat
-- Next index that has never been touched
allocFront: Nat
-- Deallocated indices
deallocs: Array Nat
-- Number of valid entries in `deallocs` array
lastDealloc: Nat
namespace Imp
structure WF (m: Imp β): Prop where
capacity: m.data.size = m.deallocs.size
front_dealloc: ∀ i: Fin m.deallocs.size, (i < m.allocFront) → (m.deallocs.get i) < m.allocFront
front_data: ∀ i: Fin m.data.size, (i ≥ m.allocFront) → (m.data.get i).isNone
def empty (capacity := 16): Imp β :=
{
data := mkArray capacity .none,
size := 0,
allocFront := 0,
deallocs := mkArray capacity 0,
lastDealloc := 0,
}
private theorem list_get_replicate (x: α) (i: Fin (List.replicate n x).length):
List.get (List.replicate n x) i = x := by
sorry
theorem empty_wf : WF (empty n: Imp β) := by
unfold empty
apply WF.mk
case capacity =>
conv =>
lhs
congr
simp
conv =>
rhs
congr
simp
simp
case front_dealloc =>
simp_all
intro i
intro a
contradiction
case front_data =>
simp_all
intro i
unfold Imp.data at i
simp at i
conv =>
lhs
unfold Array.get
unfold mkArray
simp [List.replicate]
rewrite [list_get_replicate]
-- FIXME: Merge this with the well-formed versions below so proof and code can
-- mesh seamlessly.
@[inline] def insert (map: Imp β) (v: β): (Imp β × Nat) :=
match map.lastDealloc with
| 0 => -- Capacity is full, buffer expansion is required
if map.size == map.data.size then
let nextIndex := map.data.size
let extendCapacity := map.size
let result: Imp β := {
data := (map.data.append #[Option.some v]).append (mkArray extendCapacity .none),
size := map.size + 1,
allocFront := map.size + 1,
deallocs := mkArray (map.data.size + 1 + extendCapacity) 0,
lastDealloc := 0,
}
(result, nextIndex)
else
let nextIndex := map.size
let result: Imp β := {
map
with
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
size := map.size + 1,
allocFront := map.allocFront + 1,
}
(result, nextIndex)
| (.succ k) => -- Allocation list has space
let nextIndex := map.deallocs.get! k
let result: Imp β := {
map with
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
size := map.size + 1,
lastDealloc := map.lastDealloc - 1
}
(result, nextIndex)
@[inline] def remove (map: Imp β) (index: Fin (map.size)): Imp β :=
have h: index.val < map.data.size := by sorry
match map.data.get ⟨index.val, h⟩ with
| .none => map
| .some _ =>
{
map with
data := map.data.set ⟨index, sorry⟩ .none,
size := map.size - 1,
deallocs := map.deallocs.set ⟨map.lastDealloc, sorry⟩ index,
lastDealloc := map.lastDealloc + 1,
}
/-- Retrieval is efficient -/
@[inline] def get? (map: Imp β) (index: Fin (map.size)): Option β :=
have h: index.val < map.data.size := by sorry
map.data.get ⟨index.val, h⟩
@[inline] def capacity (map: Imp β): Nat := map.data.size
end Imp
/--
This is like a hashmap but you cannot control the keys.
-/
def _root_.Pantograph.SemihashMap β := {m: Imp β // m.WF}
@[inline] def empty (capacity := 16): SemihashMap β :=
⟨ Imp.empty capacity, Imp.empty_wf ⟩
@[inline] def insert (map: SemihashMap β) (v: β): (SemihashMap β × Nat) :=
let ⟨imp, pre⟩ := map
let ⟨result, id⟩ := imp.insert v
( ⟨ result, sorry ⟩, id)
@[inline] def remove (map: SemihashMap β) (index: Nat): SemihashMap β :=
let ⟨imp, pre⟩ := map
let result := imp.remove ⟨index, sorry⟩
⟨ result, sorry ⟩
@[inline] def get? (map: SemihashMap β) (index: Nat): Option β :=
let ⟨imp, _⟩ := map
imp.get? ⟨index, sorry⟩
@[inline] def size (map: SemihashMap β): Nat :=
let ⟨imp, _⟩ := map
imp.size
end Pantograph.SemihashMap