Pantograph.lean

@@ -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
+      let stateId := state.nextId
-      set { state with goalStates }
+      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
+        let nextStateId := state.nextId
-        set { state with goalStates }
+        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
+        let nextStateId := state.nextId
-        set { state with goalStates }
+        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)

Pantograph/SemihashMap.lean

@@ -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