Update one bucket in the bucket array with a new value.
Instances For
The number of elements in the bucket array.
Note: this is marked noncomputable
because it is only intended for specification.
Instances For
Map a function over the values in the map.
Instances For
- distinct : ∀ [inst : Std.HashMap.LawfulHashable α] [inst : PartialEquivBEq α] (bucket : Std.AssocList α β), bucket ∈ buckets.val.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (Std.AssocList.toList bucket)
The elements of a bucket are all distinct according to the
BEq
relation. - hash_self : ∀ (i : Nat) (h : i < Array.size buckets.val), Std.AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size buckets.val) = i) buckets.val[i]
Every element in a bucket should hash to its location.
The well-formedness invariant for the bucket array says that every element hashes to its index (assuming the hash is lawful - otherwise there are no promises about where elements are located).
Instances For
- size : Nat
- buckets : Std.HashMap.Imp.Buckets α β
The bucket array of the
HashMap
.
HashMap.Imp α β
is the internal implementation type of HashMap α β
.
Instances For
Given a desired capacity, this returns the number of buckets we should reserve.
A "load factor" of 0.75 is the usual standard for hash maps, so we return capacity * 4 / 3
.
Instances For
Constructs an empty hash map with the specified nonzero number of buckets.
Instances For
Constructs an empty hash map with the specified target capacity.
Instances For
Calculates the bucket index from a hash value u
.
Instances For
Inserts a key-value pair into the bucket array. This function assumes that the data is not already in the array, which is appropriate when reinserting elements into the array after a resize.
Instances For
Folds a monadic function over the elements in the map (in arbitrary order).
Instances For
Folds a function over the elements in the map (in arbitrary order).
Instances For
Runs a monadic function over the elements in the map (in arbitrary order).
Instances For
Given a key a
, returns a key-value pair in the map whose key compares equal to a
.
Instances For
Looks up an element in the map with key a
.
Instances For
Returns true if the element a
is in the map.
Instances For
Copies all the entries from buckets
into a new hash map with a larger capacity.
Instances For
Inner loop of expand
. Copies elements source[i:]
into target
,
destroying source
in the process.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inserts key-value pair a, b
into the map.
If an element equal to a
is already in the map, it is replaced by b
.
Instances For
Removes key a
from the map. If it does not exist in the map, the map is returned unchanged.
Instances For
Map a function over the values in the map.
Instances For
Performs an in-place edit of the value, ensuring that the value is used linearly.
Instances For
Applies f
to each key-value pair a, b
in the map. If it returns some c
then
a, c
is pushed into the new map; else the key is removed from the map.
Instances For
Inner loop of filterMap
. Note that this reverses the bucket lists,
but this is fine since bucket lists are unordered.
Equations
- One or more equations did not get rendered due to their size.
- Std.HashMap.Imp.filterMap.go f acc Std.AssocList.nil x = (acc, x)
Instances For
Constructs a map with the set of all pairs a, b
such that f
returns true.
Instances For
- mk: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Std.HashMap.Imp α x},
m.size = Std.HashMap.Imp.Buckets.size m.buckets → Std.HashMap.Imp.Buckets.WF m.buckets → Std.HashMap.Imp.WF m
The real well-formedness invariant:
- The
size
field should match the actual number of elements in the map - The bucket array should be well-formed, meaning that if the hashable instance is lawful then every element hashes to its index.
- The
- empty': ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {n : Nat} {h : 0 < n},
Std.HashMap.Imp.WF (Std.HashMap.Imp.empty' n)
The empty hash map is well formed.
- insert: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Std.HashMap.Imp α x} {a : α} {b : x},
Std.HashMap.Imp.WF m → Std.HashMap.Imp.WF (Std.HashMap.Imp.insert m a b)
Inserting into a well formed hash map yields a well formed hash map.
- erase: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Std.HashMap.Imp α x} {a : α},
Std.HashMap.Imp.WF m → Std.HashMap.Imp.WF (Std.HashMap.Imp.erase m a)
Removing an element from a well formed hash map yields a well formed hash map.
- modify: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Std.HashMap.Imp α x} {a : α} {f : α → x → x},
Std.HashMap.Imp.WF m → Std.HashMap.Imp.WF (Std.HashMap.Imp.modify m a f)
Replacing an element in a well formed hash map yields a well formed hash map.
The well-formedness invariant for a hash map. The first constructor is the real invariant,
and the others allow us to "cheat" in this file and define insert
and erase
,
which have more complex proofs that are delayed to Std.Data.HashMap.Lemmas
.
Instances For
HashMap α β
is a key-value map which stores elements in an array using a hash function
to find the values. This allows it to have very good performance for lookups
(average O(1)
for a perfectly random hash function), but it is not a persistent data structure,
meaning that one should take care to use the map linearly when performing updates.
Copies are O(n)
.
Instances For
Make a new hash map with the specified capacity.
Instances For
Make a new empty hash map.
Instances For
The number of elements in the hash map.
Instances For
Is the map empty?
Instances For
Inserts key-value pair a, b
into the map.
If an element equal to a
is already in the map, it is replaced by b
.
Instances For
Similar to insert
, but also returns a boolean flag indicating whether an existing entry has been
replaced with a => b
.
Instances For
Removes key a
from the map. If it does not exist in the map, the map is returned unchanged.
Instances For
Performs an in-place edit of the value, ensuring that the value is used linearly.
The function f
is passed the original key of the entry, along with the value in the map.
Instances For
Given a key a
, returns a key-value pair in the map whose key compares equal to a
.
Instances For
Looks up an element in the map with key a
.
Instances For
Looks up an element in the map with key a
. Returns b₀
if the element is not found.
Instances For
Looks up an element in the map with key a
. Panics if the element is not found.
Instances For
Returns true if the element a
is in the map.
Instances For
Folds a monadic function over the elements in the map (in arbitrary order).
Instances For
Folds a function over the elements in the map (in arbitrary order).
Instances For
Combines two hashmaps using a monadic function f
to combine two values at a key.
Instances For
Combines two hashmaps using function f
to combine two values at a key.
Instances For
Converts the map into a list of key-value pairs.
Instances For
Converts the map into an array of key-value pairs.
Instances For
The number of buckets in the hash map.
Instances For
Builds a HashMap
from a list of key-value pairs.
Values of duplicated keys are replaced by their respective last occurrences.
Instances For
Variant of ofList
which accepts a function that combines values of duplicated keys.