bucket_array α β is the underlying data type for hash_map α β,
an array of linked lists of key-value pairs.
Equations
- bucket_array α β n = array ↑n (list (Σ (a : α), β a))
@[instance]
def
bucket_array.read
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
{n : ℕ+} :
bucket_array α β n → α → list (Σ (a : α), β a)
Read the bucket corresponding to an element
Equations
- bucket_array.read hash_fn data a = let bidx : fin ↑n := hash_map.mk_idx n (hash_fn a) in array.read data bidx
def
bucket_array.write
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
{n : ℕ+} :
bucket_array α β n → α → list (Σ (a : α), β a) → bucket_array α β n
Write the bucket corresponding to an element
Equations
- bucket_array.write hash_fn data a l = let bidx : fin ↑n := hash_map.mk_idx n (hash_fn a) in array.write data bidx l
def
bucket_array.modify
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
{n : ℕ+} :
bucket_array α β n → α → (list (Σ (a : α), β a) → list (Σ (a : α), β a)) → bucket_array α β n
Modify (read, apply f, and write) the bucket corresponding to an element
Equations
- bucket_array.modify hash_fn data a f = let bidx : fin ↑n := hash_map.mk_idx n (hash_fn a) in array.write data bidx (f (array.read data bidx))
def
bucket_array.as_list
{α : Type u}
{β : α → Type v}
{n : ℕ+} :
bucket_array α β n → list (Σ (a : α), β a)
The list of all key-value pairs in the bucket list
Equations
- data.as_list = (array.to_list data).join
theorem
bucket_array.mem_as_list
{α : Type u}
{β : α → Type v}
{n : ℕ+}
(data : bucket_array α β n)
{a : Σ (a : α), β a} :
def
bucket_array.foldl
{α : Type u}
{β : α → Type v}
{n : ℕ+}
(data : bucket_array α β n)
{δ : Type w} :
δ → (δ → Π (a : α), β a → δ) → δ
Fold a function f over the key-value pairs in the bucket list
Equations
- data.foldl d f = array.foldl data d (λ (b : list (Σ (a : α), β a)) (d : δ), list.foldl (λ (r : δ) (a : Σ (a : α), β a), f r a.fst a.snd) d b)
theorem
bucket_array.foldl_eq
{α : Type u}
{β : α → Type v}
{n : ℕ+}
(data : bucket_array α β n)
{δ : Type w}
(d : δ)
(f : δ → Π (a : α), β a → δ) :
def
hash_map.reinsert_aux
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
{n : ℕ+}
(data : bucket_array α β n)
(a : α) :
β a → bucket_array α β n
Insert the pair ⟨a, b⟩ into the correct location in the bucket array
(without checking for duplication)
Equations
- hash_map.reinsert_aux hash_fn data a b = bucket_array.modify hash_fn data a (λ (l : list (Σ (a : α), β a)), ⟨a, b⟩ :: l)
Search a bucket for a key a and return the value
Equations
- hash_map.find_aux a (⟨a', b⟩ :: t) = dite (a' = a) (λ (h : a' = a), option.some (h.rec_on b)) (λ (h : ¬a' = a), hash_map.find_aux a t)
- hash_map.find_aux a list.nil = option.none
theorem
hash_map.find_aux_iff
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{l : list (Σ (a : α), β a)} :
(list.map sigma.fst l).nodup → (hash_map.find_aux a l = option.some b ↔ ⟨a, b⟩ ∈ l)
Returns tt if the bucket l contains the key a
Equations
- hash_map.contains_aux a l = (hash_map.find_aux a l).is_some
theorem
hash_map.contains_aux_iff
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l : list (Σ (a : α), β a)} :
Modify a bucket to replace a value in the list. Leaves the list unchanged if the key is not found.
Equations
- hash_map.replace_aux a b (⟨a', b'⟩ :: t) = ite (a' = a) (⟨a, b⟩ :: t) (⟨a', b'⟩ :: hash_map.replace_aux a b t)
- hash_map.replace_aux a b list.nil = list.nil
Modify a bucket to remove a key, if it exists.
Equations
- hash_map.erase_aux a (⟨a', b'⟩ :: t) = ite (a' = a) t (⟨a', b'⟩ :: hash_map.erase_aux a t)
- hash_map.erase_aux a list.nil = list.nil
structure
hash_map.valid
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+} :
bucket_array α β n → ℕ → Prop
- len : bkts.as_list.length = sz
- idx : ∀ {i : fin ↑n} {a : Σ (a : α), β a}, a ∈ array.read bkts i → hash_map.mk_idx n (hash_fn a.fst) = i
- nodup : ∀ (i : fin ↑n), (list.map sigma.fst (array.read bkts i)).nodup
The predicate valid bkts sz means that bkts satisfies the hash_map
invariants: There are exactly sz elements in it, every pair is in the
bucket determined by its key and the hash function, and no key appears
multiple times in the list.
theorem
hash_map.valid.idx_enum
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ}
(v : hash_map.valid hash_fn bkts sz)
{i : ℕ}
{l : list (Σ (a : α), β a)}
(he : (i, l) ∈ (array.to_list bkts).enum)
{a : α}
{b : β a} :
theorem
hash_map.valid.idx_enum_1
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ}
(v : hash_map.valid hash_fn bkts sz)
{i : ℕ}
{l : list (Σ (a : α), β a)}
(he : (i, l) ∈ (array.to_list bkts).enum)
{a : α}
{b : β a} :
⟨a, b⟩ ∈ l → (hash_map.mk_idx n (hash_fn a)).val = i
theorem
hash_map.valid.as_list_nodup
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ} :
hash_map.valid hash_fn bkts sz → (list.map sigma.fst bkts.as_list).nodup
theorem
hash_map.mk_valid
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
(n : ℕ+) :
hash_map.valid hash_fn (mk_array ↑n list.nil) 0
theorem
hash_map.valid.find_aux_iff
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ}
(v : hash_map.valid hash_fn bkts sz)
{a : α}
{b : β a} :
hash_map.find_aux a (bucket_array.read hash_fn bkts a) = option.some b ↔ ⟨a, b⟩ ∈ bkts.as_list
theorem
hash_map.valid.contains_aux_iff
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ}
(v : hash_map.valid hash_fn bkts sz)
(a : α) :
↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a)) ↔ a ∈ list.map sigma.fst bkts.as_list
theorem
hash_map.append_of_modify
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{bidx : fin ↑n}
{f : list (Σ (a : α), β a) → list (Σ (a : α), β a)}
(u v1 v2 w : list (Σ (a : α), β a)) :
theorem
hash_map.valid.modify
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{bidx : fin ↑n}
{f : list (Σ (a : α), β a) → list (Σ (a : α), β a)}
(u v1 v2 w : list (Σ (a : α), β a))
(hl : array.read bkts bidx = u ++ v1 ++ w)
(hfl : f (array.read bkts bidx) = u ++ v2 ++ w)
(hvnd : (list.map sigma.fst v2).nodup)
(hal : ∀ (a : Σ (a : α), β a), a ∈ v2 → hash_map.mk_idx n (hash_fn a.fst) = bidx)
(djuv : (list.map sigma.fst u).disjoint (list.map sigma.fst v2))
(djwv : (list.map sigma.fst w).disjoint (list.map sigma.fst v2))
{sz : ℕ} :
theorem
hash_map.valid.replace
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ}
(a : α)
(b : β a) :
↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a)) → hash_map.valid hash_fn bkts sz → hash_map.valid hash_fn (bucket_array.modify hash_fn bkts a (hash_map.replace_aux a b)) sz
theorem
hash_map.valid.insert
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ}
(a : α)
(b : β a) :
¬↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a)) → hash_map.valid hash_fn bkts sz → hash_map.valid hash_fn (hash_map.reinsert_aux hash_fn bkts a b) (sz + 1)
theorem
hash_map.valid.erase
{α : Type u}
{β : α → Type v}
(hash_fn : α → ℕ)
[decidable_eq α]
{n : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ}
(a : α) :
↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a)) → hash_map.valid hash_fn bkts sz → hash_map.valid hash_fn (bucket_array.modify hash_fn bkts a (hash_map.erase_aux a)) (sz - 1)
- hash_fn : α → ℕ
- size : ℕ
- nbuckets : ℕ+
- buckets : bucket_array α β c.nbuckets
- is_valid : hash_map.valid c.hash_fn c.buckets c.size
A hash map data structure, representing a finite key-value map
with key type α and value type β (which may depend on α).
Construct an empty hash map with buffer size nbuckets (default 8).
def
hash_map.find
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a : α) :
option (β a)
Return the value corresponding to a key, or none if not found
Equations
- m.find a = hash_map.find_aux a (bucket_array.read m.hash_fn m.buckets a)
Return tt if the key exists in the map
@[instance]
def
hash_map.fold
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{δ : Type w} :
hash_map α β → δ → (δ → Π (a : α), β a → δ) → δ
Fold a function over the key-value pairs in the map
The list of key-value pairs in the map
The list of keys in the map
theorem
hash_map.find_iff
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a : α)
(b : β a) :
theorem
hash_map.contains_iff
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a : α) :
theorem
hash_map.entries_empty
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(hash_fn : α → ℕ)
(n : ℕ := 8) :
(mk_hash_map hash_fn n).entries = list.nil
theorem
hash_map.keys_empty
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(hash_fn : α → ℕ)
(n : ℕ := 8) :
(mk_hash_map hash_fn n).keys = list.nil
theorem
hash_map.find_empty
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(hash_fn : α → ℕ)
(n : ℕ := 8)
(a : α) :
(mk_hash_map hash_fn n).find a = option.none
theorem
hash_map.not_contains_empty
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(hash_fn : α → ℕ)
(n : ℕ := 8)
(a : α) :
¬↥((mk_hash_map hash_fn n).contains a)
theorem
hash_map.insert_lemma
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(hash_fn : α → ℕ)
{n n' : ℕ+}
{bkts : bucket_array α β n}
{sz : ℕ} :
hash_map.valid hash_fn bkts sz → hash_map.valid hash_fn (bkts.foldl (mk_array ↑n' list.nil) (hash_map.reinsert_aux hash_fn)) sz
def
hash_map.insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a : α) :
β a → hash_map α β
Insert a key-value pair into the map. (Modifies m in-place when applicable)
Equations
- {hash_fn := hash_fn, size := size, nbuckets := n, buckets := buckets, is_valid := v}.insert a b = let bkt : list (Σ (a : α), β a) := bucket_array.read hash_fn buckets a in dite ↥(hash_map.contains_aux a bkt) (λ (hc : ↥(hash_map.contains_aux a bkt)), {hash_fn := hash_fn, size := size, nbuckets := n, buckets := bucket_array.modify hash_fn buckets a (hash_map.replace_aux a b), is_valid := _}) (λ (hc : ¬↥(hash_map.contains_aux a bkt)), let size' : ℕ := size + 1, buckets' : bucket_array α β n := bucket_array.modify hash_fn buckets a (λ (l : list (Σ (a : α), β a)), ⟨a, b⟩ :: l), valid' : hash_map.valid hash_fn (hash_map.reinsert_aux hash_fn buckets a b) (size + 1) := _ in ite (size' ≤ ↑n) {hash_fn := hash_fn, size := size', nbuckets := n, buckets := buckets', is_valid := valid'} (let n' : ℕ+ := ⟨↑n * 2, _⟩, buckets'' : bucket_array α β n' := buckets'.foldl (mk_array ↑n' list.nil) (hash_map.reinsert_aux hash_fn) in {hash_fn := hash_fn, size := size', nbuckets := n', buckets := buckets'', is_valid := _}))
theorem
hash_map.find_insert_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a : α)
(b : β a) :
(m.insert a b).find a = option.some b
theorem
hash_map.find_insert_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a a' : α)
(b : β a) :
theorem
hash_map.find_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a' a : α)
(b : β a) :
Insert a list of key-value pairs into the map. (Modifies m in-place when applicable)
Equations
- hash_map.insert_all l m = list.foldl (λ (m : hash_map α β) (_x : Σ (a : α), β a), hash_map.insert_all._match_1 m _x) m l
- hash_map.insert_all._match_1 m ⟨a, b⟩ = m.insert a b
Construct a hash map from a list of key-value pairs.
Equations
- hash_map.of_list l hash_fn = hash_map.insert_all l (mk_hash_map hash_fn (2 * l.length))
Remove a key from the map. (Modifies m in-place when applicable)
Equations
- m.erase a = hash_map.erase._match_1 m a m
- hash_map.erase._match_1 m a {hash_fn := hash_fn, size := size, nbuckets := n, buckets := buckets, is_valid := v} = dite ↥(hash_map.contains_aux a (bucket_array.read hash_fn buckets a)) (λ (hc : ↥(hash_map.contains_aux a (bucket_array.read hash_fn buckets a))), {hash_fn := hash_fn, size := size - 1, nbuckets := n, buckets := bucket_array.modify hash_fn buckets a (hash_map.erase_aux a), is_valid := _}) (λ (hc : ¬↥(hash_map.contains_aux a (bucket_array.read hash_fn buckets a))), m)
theorem
hash_map.find_erase_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a : α) :
(m.erase a).find a = option.none
theorem
hash_map.find_erase_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a a' : α) :
theorem
hash_map.find_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(m : hash_map α β)
(a' a : α) :
@[instance]
def
hash_map.has_to_string
{α : Type u}
{β : α → Type v}
[decidable_eq α]
[has_to_string α]
[Π (a : α), has_to_string (β a)] :
has_to_string (hash_map α β)
Equations
- hash_map.has_to_string = {to_string := to_string (λ (a : α), _inst_3 a)}
@[instance]
def
hash_map.has_to_format
{α : Type u}
{β : α → Type v}
[decidable_eq α]
[has_to_format α]
[Π (a : α), has_to_format (β a)] :
has_to_format (hash_map α β)