From 764be6d14b5e77771e8233e12c83b1c40125f861 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 7 Nov 2023 12:09:54 -0800 Subject: [PATCH] fix: Remove the error prone SemihashMap --- Pantograph.lean | 36 +++++---- Pantograph/SemihashMap.lean | 149 ------------------------------------ 2 files changed, 22 insertions(+), 163 deletions(-) delete mode 100644 Pantograph/SemihashMap.lean diff --git a/Pantograph.lean b/Pantograph.lean index a1f2602..0ae8192 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) @@ -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) 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