From 46347d8244f7e9c7b84b5276bd8f303a8a236ce6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 30 Aug 2023 19:16:33 -0700 Subject: [PATCH] Add SemihashMap interface, rename proof commands to goal commands, allow deletion --- Pantograph.lean | 12 ++++-- Pantograph/Commands.lean | 15 +++++-- Pantograph/SemihashMap.lean | 86 +++++++++++++++++++++++++++++++------ README.md | 2 + 4 files changed, 95 insertions(+), 20 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index bb2635e..3e53859 100644 --- a/Pantograph.lean +++ b/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 diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index f9abf9d..72194b0 100644 --- a/Pantograph/Commands.lean +++ b/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 diff --git a/Pantograph/SemihashMap.lean b/Pantograph/SemihashMap.lean index 362be94..1d9ebae 100644 --- a/Pantograph/SemihashMap.lean +++ b/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 β := - match map.data.getD index .none with +@[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 _ => { @@ -66,24 +116,34 @@ namespace Imp } /-- Retrieval is efficient -/ -@[inline] def get? (map: Imp β) (index: Nat): Option β := - map.data.getD index .none +@[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 -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 diff --git a/README.md b/README.md index 9a2ec5b..273e865 100644 --- a/README.md +++ b/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": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol - `goal.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given goal +- `goal.remove {"goalIds": []}"`: Remove a bunch of stored goals. - `stat`: Display resource usage ## Errors