From 5ac5198f514ffc62ede1fddc8d752ce2ff9b82e2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 7 Nov 2023 12:04:17 -0800
Subject: [PATCH] fix: Remove the error prone SemihashMap
---
Pantograph.lean | 23 +++---
Pantograph/SemihashMap.lean | 149 ------------------------------------
2 files changed, 13 insertions(+), 159 deletions(-)
delete mode 100644 Pantograph/SemihashMap.lean
diff --git a/Pantograph.lean b/Pantograph.lean
index 00782d5..b719ca9 100644
--- a/Pantograph.lean
+++ b/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)
@@ -52,7 +53,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
@@ -140,12 +141,13 @@ 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
+ let goalStates := state.goalStates.insert stateId goalState
+ set { state with goalStates, nextId := state.nextId + 1 }
return .ok { stateId }
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
@@ -157,8 +159,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,
@@ -172,12 +175,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok { tacticErrors? := .some messages }
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)
diff --git a/Pantograph/SemihashMap.lean b/Pantograph/SemihashMap.lean
deleted file mode 100644
index 1d9ebae..0000000
--- a/Pantograph/SemihashMap.lean
+++ /dev/null
@@ -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
--
2.44.1