Simplify goal bookkeeping mechanism #10

Merged
aniva merged 5 commits from tactic/book into dev 2023-08-30 19:18:37 -07:00
4 changed files with 95 additions and 20 deletions
Showing only changes of commit 46347d8244 - Show all commits

View File

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

View File

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

View File

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

View File

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