Add SemihashMap interface, rename proof commands to goal commands, allow deletion

Pantograph.lean

@@ -38,6 +38,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
   | "options.print"  => run options_print
   | "goal.start"     => run goal_start
   | "goal.tactic"    => run goal_tactic
+  | "goal.delete"    => run goal_delete
   | cmd =>
     let error: Commands.InteractionError :=
       errorCommand s!"Unknown command {cmd}"
@@ -117,7 +118,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
     return .ok {  }
   options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
     return .ok (← get).options
-  goal_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do
+  goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
@@ -142,10 +143,10 @@ def execute (command: Commands.Command): MainM Lean.Json := do
       let (goalStates, goalId) := state.goalStates.insert goalState
       set { state with goalStates }
       return .ok { goalId }
-  goal_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do
+  goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do
     let state ← get
     match state.goalStates.get? args.goalId with
-    | .none => return .error $ errorIndex "Invalid goal index {args.goalId}"
+    | .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}"
     | .some goalState =>
       let result ← GoalState.execute goalState args.tactic |>.run state.options
       match result with
@@ -164,5 +165,10 @@ def execute (command: Commands.Command): MainM Lean.Json := do
           return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray }
       | .failure messages =>
         return .ok { tacticErrors? := .some messages }
+  goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do
+    let state ← get
+    let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates
+    set { state with goalStates }
+    return .ok {}
 
 end Pantograph

Pantograph/Commands.lean

@@ -130,20 +130,20 @@ structure OptionsPrint where
   deriving Lean.FromJson
 abbrev OptionsPrintResult := Options
 
-structure ProofStart where
+structure GoalStart where
   -- Only one of the fields below may be populated.
   expr: Option String     -- Proof expression
   copyFrom: Option String -- Theorem name
   deriving Lean.FromJson
-structure ProofStartResult where
+structure GoalStartResult where
   goalId: Nat := 0 -- Proof tree id
   deriving Lean.ToJson
-structure ProofTactic where
+structure GoalTactic where
   -- Identifiers for tree, state, and goal
   goalId: Nat
   tactic: String
   deriving Lean.FromJson
-structure ProofTacticResult where
+structure GoalTacticResult where
   -- Existence of this field shows success
   goals?: Option (Array Goal)          := .none
   -- Next proof state id, if successful
@@ -152,5 +152,12 @@ structure ProofTacticResult where
   tacticErrors?: Option (Array String) := .none
   deriving Lean.ToJson
 
+-- Remove a bunch of goals.
+structure GoalDelete where
+  goalIds: List Nat
+  deriving Lean.FromJson
+structure GoalDeleteResult where
+  deriving Lean.ToJson
+
 
 end Pantograph.Commands

Pantograph/SemihashMap.lean

@@ -18,7 +18,56 @@ structure Imp (β: Type u) where
 
 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
@@ -53,8 +102,9 @@ namespace Imp
     }
     (result, nextIndex)
 
-@[inline] def remove (map: Imp β) (index: Nat): Imp β :=
+@[inline] def remove (map: Imp β) (index: Fin (map.size)): Imp β :=
-  match map.data.getD index .none with
+  have h: index.val < map.data.size := by sorry
+  match map.data.get ⟨index.val, h⟩ with
   | .none => map
   | .some _ =>
     {
@@ -66,24 +116,34 @@ namespace Imp
     }
 
 /-- Retrieval is efficient -/
-@[inline] def get? (map: Imp β) (index: Nat): Option β :=
+@[inline] def get? (map: Imp β) (index: Fin (map.size)): Option β :=
-  map.data.getD index .none
+  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
 
-def empty (capacity := 16): Imp β :=
-  {
-    data := mkArray capacity .none,
-    size := 0,
-    allocFront := 0,
-    deallocs := mkArray capacity 0,
-    lastDealloc := 0,
-  }
 
 /--
 This is like a hashmap but you cannot control the keys.
 -/
-def _root_.Pantograph.SemihashMap β := Imp β
+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

README.md

@@ -56,6 +56,7 @@ $ env build/bin/Pantograph Init
 goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
 goal.tactic {"goalId": 0, "tactic": "intro n m"}
 goal.tactic {"goalId": 1, "tactic": "assumption"}
+goal.delete {"goalIds": [0]}
 stat {}
 goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
 stat
@@ -76,6 +77,7 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
 - `options.print`: Display the current set of options
 - `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
 - `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
+- `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals.
 - `stat`: Display resource usage
 
 ## Errors