This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.
In this file we define functions for manipulating a hash map based on operations defined in terms of their buckets. Then we give "model implementations" of the hash map operations in terms of these basic building blocks and show that the actual operations are equal to the model implementations T his means that later we will be able to prove properties of the operations by proving general facts about the basic building blocks.
Setting up the infrastructure #
def
Std.DHashMap.Internal.bucket
{α : Type u}
{β : α → Type v}
[Hashable α]
(self : Array (AssocList α β))
(h : 0 < self.size)
(k : α)
:
AssocList α β
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.bucket self h k = match Std.DHashMap.Internal.mkIdx self.size h (hash k) with | ⟨i, h⟩ => self[i]
def
Std.DHashMap.Internal.updateBucket
{α : Type u}
{β : α → Type v}
[Hashable α]
(self : Array (AssocList α β))
(h : 0 < self.size)
(k : α)
(f : AssocList α β → AssocList α β)
:
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.updateBucket self h k f = match Std.DHashMap.Internal.mkIdx self.size h (hash k) with | ⟨i, h⟩ => self.uset i (f self[i]) h
def
Std.DHashMap.Internal.withComputedSize
{α : Type u}
{β : α → Type v}
(self : Array (AssocList α β))
:
Raw α β
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.withComputedSize self = { size := Std.DHashMap.Internal.computeSize self, buckets := self }
@[simp]
theorem
Std.DHashMap.Internal.size_withComputedSize
{α : Type u}
{β : α → Type v}
{self : Array (AssocList α β)}
:
@[simp]
theorem
Std.DHashMap.Internal.buckets_withComputedSize
{α : Type u}
{β : α → Type v}
{self : Array (AssocList α β)}
:
theorem
Std.DHashMap.Internal.apply_bucket
{α : Type u}
{β : α → Type v}
{γ : Type w}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Raw₀ α β}
(hm : Raw.WFImp m.val)
{a : α}
{f : AssocList α β → γ}
{g : List ((a : α) × β a) → γ}
(hfg : ∀ {l : AssocList α β}, f l = g l.toList)
(hg₁ : ∀ {l l' : List ((a : α) × β a)}, List.DistinctKeys l → l.Perm l' → g l = g l')
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, List.containsKey a l' = false → g (l ++ l') = g l)
:
This is the general theorem used to show that access operations are correct.
theorem
Std.DHashMap.Internal.apply_bucket_with_proof
{α : Type u}
{β : α → Type v}
{γ : α → Type w}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Raw₀ α β}
(hm : Raw.WFImp m.val)
(a : α)
(f : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a)
(g : (a : α) → (l : List ((a : α) × β a)) → List.containsKey a l = true → γ a)
(hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯)
(hg₁ :
∀ {l l' : List ((a : α) × β a)} {a : α} {h : List.containsKey a l = true},
List.DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯)
{h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true}
{h' : List.containsKey a (toListModel m.val.buckets) = true}
(hg₂ :
∀ {l l' : List ((a : α) × β a)} {a : α} {h : List.containsKey a (l ++ l') = true}
(hl' : List.containsKey a l' = false), g a (l ++ l') h = g a l ⋯)
:
This is the general theorem used to show that access operations involving a proof (like get)
are correct.
theorem
Std.DHashMap.Internal.toListModel_updateBucket
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Raw₀ α β}
(hm : Raw.WFImp m.val)
{a : α}
{f : AssocList α β → AssocList α β}
{g : List ((a : α) × β a) → List ((a : α) × β a)}
(hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList))
(hg₁ : ∀ {l l' : List ((a : α) × β a)}, List.DistinctKeys l → l.Perm l' → (g l).Perm (g l'))
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, List.containsKey a l' = false → g (l ++ l') = g l ++ l')
:
(toListModel (updateBucket m.val.buckets ⋯ a f)).Perm (g (toListModel m.val.buckets))
This is the general theorem to show that modification operations are correct.
theorem
Std.DHashMap.Internal.toListModel_updateAllBuckets
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
{m : Raw₀ α β}
{f : AssocList α β → AssocList α δ}
{g : List ((a : α) × β a) → List ((a : α) × δ a)}
(hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList))
(hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l'))
:
(toListModel (updateAllBuckets m.val.buckets f)).Perm (g (toListModel m.val.buckets))
This is the general theorem to show that mapping operations (like map and filter) are
correct.
IsHashSelf #
theorem
Std.DHashMap.Internal.IsHashSelf.uset
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Array (AssocList α β)}
{i : USize}
{h : i.toNat < m.size}
{d : AssocList α β}
(hd : List.HashesTo m[i].toList i.toNat m.size → List.HashesTo d.toList i.toNat m.size)
(hm : IsHashSelf m)
:
IsHashSelf (m.uset i d h)
theorem
Std.DHashMap.Internal.IsHashSelf.updateBucket
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Array (AssocList α β)}
{h : 0 < m.size}
{a : α}
{f : AssocList α β → AssocList α β}
(hf :
∀ (l : AssocList α β) (p : (a : α) × β a),
p ∈ (f l).toList → List.containsKey p.fst l.toList = true ∨ hash p.fst = hash a)
(hm : IsHashSelf m)
:
IsHashSelf (Internal.updateBucket m h a f)
This is the general theorem to show that modification operations preserve well-formedness of buckets.
theorem
Std.DHashMap.Internal.IsHashSelf.updateAllBuckets
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[LawfulHashable α]
{m : Array (AssocList α β)}
{f : AssocList α β → AssocList α δ}
(hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → List.containsKey p.fst l.toList = true)
(hm : IsHashSelf m)
:
Definition of model functions #
def
Std.DHashMap.Internal.Raw₀.getₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[LawfulBEq α]
[Hashable α]
(m : Raw₀ α β)
(a : α)
(h : m.containsₘ a = true)
:
β a
Internal implementation detail of the hash map
Equations
- m.getₘ a h = Std.DHashMap.Internal.AssocList.getCast a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a) h
def
Std.DHashMap.Internal.Raw₀.Const.modifyₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => β)
(a : α)
(f : β → β)
:
Raw₀ α fun (x : α) => β
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.Raw₀.Const.modifyₘ m a f = Std.DHashMap.Internal.Raw₀.Const.alterₘ m a fun (option : Option β) => Option.map f option
def
Std.DHashMap.Internal.Raw₀.mapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
(m : Raw₀ α β)
(f : (a : α) → β a → δ a)
:
Raw₀ α δ
Internal implementation detail of the hash map
Equations
- m.mapₘ f = ⟨{ size := m.val.size, buckets := Std.DHashMap.Internal.updateAllBuckets m.val.buckets (Std.DHashMap.Internal.AssocList.map f) }, ⋯⟩
def
Std.DHashMap.Internal.Raw₀.Const.getDₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => β)
(a : α)
(fallback : β)
:
β
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback = (Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a).getD fallback