08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
128 lines
4.4 KiB
Text
128 lines
4.4 KiB
Text
import Std.Data.HashMap
|
||
set_option warn.sorry false
|
||
macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
|
||
|
||
open Std
|
||
|
||
structure IndexMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
|
||
private indices : HashMap α Nat
|
||
private keys : Array α
|
||
private values : Array β
|
||
private size_keys' : keys.size = values.size := by grind
|
||
private WF : ∀ (i : Nat) (a : α), keys[i]? = some a ↔ indices[a]? = some i := by grind
|
||
|
||
namespace IndexMap
|
||
|
||
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
|
||
variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}
|
||
|
||
@[inline] def size (m : IndexMap α β) : Nat :=
|
||
m.values.size
|
||
|
||
@[local grind =] private theorem size_keys : m.keys.size = m.size := m.size_keys'
|
||
|
||
def emptyWithCapacity (capacity := 8) : IndexMap α β where
|
||
indices := HashMap.emptyWithCapacity capacity
|
||
keys := Array.emptyWithCapacity capacity
|
||
values := Array.emptyWithCapacity capacity
|
||
|
||
instance : EmptyCollection (IndexMap α β) where
|
||
emptyCollection := emptyWithCapacity
|
||
|
||
instance : Inhabited (IndexMap α β) where
|
||
default := ∅
|
||
|
||
@[inline] def contains (m : IndexMap α β)
|
||
(a : α) : Bool :=
|
||
m.indices.contains a
|
||
|
||
instance : Membership α (IndexMap α β) where
|
||
mem m a := a ∈ m.indices
|
||
|
||
instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
|
||
inferInstanceAs (Decidable (a ∈ m.indices))
|
||
|
||
@[local grind =] private theorem mem_indices_of_mem {m : IndexMap α β} {a : α} :
|
||
a ∈ m ↔ a ∈ m.indices := Iff.rfl
|
||
|
||
@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat := m.indices[a]?
|
||
|
||
@[inline] def findIdx (m : IndexMap α β) (a : α) (h : a ∈ m := by get_elem_tactic) : Nat := m.indices[a]
|
||
|
||
@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β := m.values[i]?
|
||
|
||
@[inline] def getIdx (m : IndexMap α β) (i : Nat) (h : i < m.size := by get_elem_tactic) : β :=
|
||
m.values[i]
|
||
|
||
variable [LawfulBEq α] [LawfulHashable α]
|
||
|
||
attribute [local grind _=_] IndexMap.WF
|
||
|
||
private theorem getElem_indices_lt {h : a ∈ m} : m.indices[a] < m.size := by
|
||
have : m.indices[a]? = some m.indices[a] := by grind
|
||
grind
|
||
|
||
grind_pattern getElem_indices_lt => m.indices[a]
|
||
|
||
attribute [local grind] size
|
||
|
||
instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
|
||
getElem m a h := m.values[m.indices[a]'h]
|
||
getElem? m a := m.indices[a]?.bind (fun i => (m.values[i]?))
|
||
getElem! m a := m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
|
||
|
||
@[local grind =] private theorem getElem_def (m : IndexMap α β) (a : α) (h : a ∈ m) : m[a] = m.values[m.indices[a]'h] := rfl
|
||
@[local grind =] private theorem getElem?_def (m : IndexMap α β) (a : α) :
|
||
m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) := rfl
|
||
@[local grind =] private theorem getElem!_def [Inhabited β] (m : IndexMap α β) (a : α) :
|
||
m[a]! = (m.indices[a]?.bind (fun i => (m.values[i]?))).getD default := rfl
|
||
|
||
instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
|
||
getElem?_def := by grind
|
||
getElem!_def := by grind
|
||
|
||
@[inline] def insert [LawfulBEq α] (m : IndexMap α β) (a : α) (b : β) :
|
||
IndexMap α β :=
|
||
match h : m.indices[a]? with
|
||
| some i =>
|
||
{ indices := m.indices
|
||
keys := m.keys.set i a
|
||
values := m.values.set i b }
|
||
| none =>
|
||
{ indices := m.indices.insert a m.size
|
||
keys := m.keys.push a
|
||
values := m.values.push b }
|
||
|
||
/-! ### Verification theorems -/
|
||
|
||
attribute [local grind] getIdx findIdx insert
|
||
|
||
example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
|
||
(m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
|
||
grind -ring -linarith -lia =>
|
||
instantiate only [= getElem_def, insert]
|
||
cases #dbaf
|
||
next =>
|
||
cases #54dd
|
||
next => sorry
|
||
next =>
|
||
instantiate only
|
||
instantiate only [= HashMap.getElem_insert]
|
||
instantiate only [= size]
|
||
instantiate only [= Array.getElem_push, = mem_indices_of_mem]
|
||
next => sorry
|
||
|
||
example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
|
||
(m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
|
||
grind -ring -linarith -lia =>
|
||
instantiate only [= getElem_def, insert]
|
||
cases #dbaf
|
||
next =>
|
||
cases #54dd
|
||
next => sorry
|
||
next =>
|
||
instantiate only
|
||
instantiate only [= HashMap.getElem_insert]
|
||
instantiate only [= size]
|
||
instantiate only [= mem_indices_of_mem, = Array.getElem_push]
|
||
next => sorry
|