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 #
@[implicit_reducible]
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]
Instances For
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
Instances For
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 }
Instances For
@[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.exists_bucket_of_update
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Array (AssocList α β))
(h : 0 < m.size)
(k : α)
(f : AssocList α β → AssocList α β)
:
∃ (l : List ((a : α) × β a)), (toListModel m).Perm ((bucket m h k).toList ++ l) ∧ (toListModel (updateBucket m h k f)).Perm ((f (bucket m h k)).toList ++ l) ∧ ∀ [LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → Internal.List.containsKey k' l = false
theorem
Std.DHashMap.Internal.exists_bucket
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Array (AssocList α β))
(h : 0 < m.size)
(k : α)
:
∃ (l : List ((a : α) × β a)), (toListModel m).Perm ((bucket m h k).toList ++ l) ∧ ∀ [LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → Internal.List.containsKey k' l = false
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)}, Internal.List.DistinctKeys l → l.Perm l' → g l = g l')
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, Internal.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)) → Internal.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 : Internal.List.containsKey a l = true},
Internal.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' : Internal.List.containsKey a (toListModel m.val.buckets) = true}
(hg₂ :
∀ {l l' : List ((a : α) × β a)} {a : α} {h : Internal.List.containsKey a (l ++ l') = true}
(hl' : Internal.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)}, Internal.List.DistinctKeys l → l.Perm l' → (g l).Perm (g l'))
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, Internal.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 → Internal.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 → Internal.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
Instances For
def
Std.DHashMap.Internal.Raw₀.getEntryₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(a : α)
(h : m.containsₘ a = true)
:
(a : α) × β a
Internal implementation detail of the hash map
Equations
- m.getEntryₘ a h = Std.DHashMap.Internal.AssocList.getEntry a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a) h
Instances For
def
Std.DHashMap.Internal.Raw₀.getEntryDₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(a : α)
(fallback : (a : α) × β a)
:
(a : α) × β a
Internal implementation detail of the hash map
Equations
- m.getEntryDₘ a fallback = Std.DHashMap.Internal.AssocList.getEntryD a fallback (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a)
Instances For
def
Std.DHashMap.Internal.Raw₀.getKeyₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(a : α)
(h : m.containsₘ a = true)
:
α
Internal implementation detail of the hash map
Equations
- m.getKeyₘ a h = Std.DHashMap.Internal.AssocList.getKey a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a) h
Instances For
def
Std.DHashMap.Internal.Raw₀.Const.alterₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => β)
(a : α)
(f : Option β → Option β)
:
Raw₀ α fun (x : α) => β
Internal implementation detail of the hash map
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
def
Std.DHashMap.Internal.Raw₀.insertListₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(l : List ((a : α) × β a))
:
Raw₀ α β
Internal implementation detail of the hash map
Equations
- m.insertListₘ [] = m
- m.insertListₘ (hd :: tl) = (m.insert hd.fst hd.snd).insertListₘ tl
Instances For
def
Std.DHashMap.Internal.Raw₀.eraseListₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(l : List α)
:
Raw₀ α β
Internal implementation detail of the hash map
Equations
- m.eraseListₘ [] = m
- m.eraseListₘ (hd :: tl) = (m.erase hd).eraseListₘ tl
Instances For
def
Std.DHashMap.Internal.Raw₀.insertListIfNewₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(l : List ((a : α) × β a))
:
Raw₀ α β
Internal implementation detail of the hash map
Equations
- m.insertListIfNewₘ [] = m
- m.insertListIfNewₘ (hd :: tl) = (m.insertIfNew hd.fst hd.snd).insertListIfNewₘ tl
Instances For
def
Std.DHashMap.Internal.Raw₀.unionₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m₁ m₂ : Raw₀ α β)
:
Raw₀ α β
Internal implementation detail of the hash map
Equations
- m₁.unionₘ m₂ = if m₁.val.size ≤ m₂.val.size then m₂.insertListIfNewₘ (Std.DHashMap.Internal.toListModel m₁.val.buckets) else m₁.insertListₘ (Std.DHashMap.Internal.toListModel m₂.val.buckets)
Instances For
def
Std.DHashMap.Internal.Raw₀.interSmallerFnₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m sofar : Raw₀ α β)
(k : α)
:
Raw₀ α β
Internal implementation detail of the hash map
Equations
- m.interSmallerFnₘ sofar k = match m.getEntry?ₘ k with | some kv' => sofar.insertₘ kv'.fst kv'.snd | none => sofar
Instances For
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