Extensional dependent hash maps #
This file develops the type Std.ExtDHashMap
of extensional dependent hash maps.
Lemmas about the operations on Std.ExtDHashMap
are available in the
module Std.Data.ExtDHashMap.Lemmas
.
Extensional dependent hash maps.
This is a simple separate-chaining hash table. The data of the hash map consists of a cached size and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets is always a power of two. The hash map doubles its size upon inserting an element such that the number of elements is more than 75% of the number of buckets.
The hash table is backed by an Array
. Users should make sure that the hash map is used linearly to
avoid expensive copies.
The hash map uses ==
(provided by the BEq
typeclass) to compare keys and hash
(provided by
the Hashable
typeclass) to hash them. To ensure that the operations behave as expected, ==
must be an equivalence relation and a == b
must imply hash a = hash b
(see also the
EquivBEq
and LawfulHashable
typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if a == b
implies a = b
.
In contrast to regular dependent hash maps, Std.ExtDHashMap
offers several extensionality lemmas
and therefore has more lemmas about equality of hash maps. This however also makes it lose the
ability to iterate freely over the hash map.
These hash maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, Std.DHashMap.Raw
and
Std.DHashMap.Raw.WF
unbundle the invariant from the hash map. When in doubt, prefer
DHashMap
over DHashMap.Raw
.
Equations
- Std.ExtDHashMap α β = Quotient (Std.DHashMap.isSetoid α β)
Instances For
Creates a new empty hash map. The optional parameter capacity
can be supplied to presize the
map so that it can hold the given number of mappings without reallocating. It is also possible to
use the empty collection notations ∅
and {}
to create an empty hash map with the default
capacity.
Equations
- Std.ExtDHashMap.emptyWithCapacity capacity = Quotient.mk' (Std.DHashMap.emptyWithCapacity capacity)
Instances For
Equations
- Std.ExtDHashMap.instEmptyCollection = { emptyCollection := Std.ExtDHashMap.emptyWithCapacity }
Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.
Note: this replacement behavior is true for HashMap
, DHashMap
, HashMap.Raw
and DHashMap.Raw
.
The insert
function on HashSet
and HashSet.Raw
behaves differently: it will return the set
unchanged if a matching key is already present.
Equations
- m.insert a b = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (m.insert a b)) ⋯ m
Instances For
Equations
- Std.ExtDHashMap.instInsertSigmaOfEquivBEqOfLawfulHashable = { insert := fun (x : (a : α) × β a) (x_1 : Std.ExtDHashMap α β) => match x, x_1 with | ⟨a, b⟩, s => s.insert a b }
If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.
Equations
- m.insertIfNew a b = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (m.insertIfNew a b)) ⋯ m
Instances For
Checks whether a key is present in a map, and unconditionally inserts a value for the key.
Equivalent to (but potentially faster than) calling contains
followed by insert
.
Equations
- m.containsThenInsert a b = Quotient.lift (fun (m : Std.DHashMap α β) => let m' := m.containsThenInsert a b; (m'.fst, Quotient.mk' m'.snd)) ⋯ m
Instances For
Checks whether a key is present in a map and inserts a value for the key if it was not found.
If the returned Bool
is true
, then the returned map is unaltered. If the Bool
is false
, then
the returned map has a new value inserted.
Equivalent to (but potentially faster than) calling contains
followed by insertIfNew
.
Equations
- m.containsThenInsertIfNew a b = Quotient.lift (fun (m : Std.DHashMap α β) => let m' := m.containsThenInsertIfNew a b; (m'.fst, Quotient.mk' m'.snd)) ⋯ m
Instances For
Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.
If the returned value is some v
, then the returned map is unaltered. If it is none
, then the
returned map has a new value inserted.
Equivalent to (but potentially faster than) calling get?
followed by insertIfNew
.
Uses the LawfulBEq
instance to cast the retrieved value to the correct type.
Equations
- m.getThenInsertIfNew? a b = Quotient.lift (fun (m : Std.DHashMap α β) => let m' := m.getThenInsertIfNew? a b; (m'.fst, Quotient.mk' m'.snd)) ⋯ m
Instances For
Tries to retrieve the mapping for the given key, returning none
if no such mapping is present.
Uses the LawfulBEq
instance to cast the retrieved value to the correct type.
Equations
- m.get? a = Quotient.lift (fun (m : Std.DHashMap α β) => m.get? a) ⋯ m
Instances For
Returns true
if there is a mapping for the given key. There is also a Prop
-valued version
of this: a ∈ m
is equivalent to m.contains a = true
.
Observe that this is different behavior than for lists: for lists, ∈
uses =
and contains
uses
==
for comparisons, while for hash maps, both use ==
.
Equations
- m.contains a = Quotient.lift (fun (m : Std.DHashMap α β) => m.contains a) ⋯ m
Instances For
Equations
- Std.ExtDHashMap.instMembershipOfEquivBEqOfLawfulHashable = { mem := fun (m : Std.ExtDHashMap α β) (a : α) => m.contains a = true }
Equations
Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof
of a ∈ m
.
Uses the LawfulBEq
instance to cast the retrieved value to the correct type.
Equations
- m.get a h = Quotient.pliftOn m (fun (m_1 : Std.DHashMap α β) (h' : m = Quotient.mk (Std.DHashMap.isSetoid α β) m_1) => m_1.get a ⋯) ⋯
Instances For
Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
Uses the LawfulBEq
instance to cast the retrieved value to the correct type.
Equations
- m.get! a = Quotient.lift (fun (m : Std.DHashMap α β) => m.get! a) ⋯ m
Instances For
Tries to retrieve the mapping for the given key, returning fallback
if no such mapping is present.
Uses the LawfulBEq
instance to cast the retrieved value to the correct type.
Equations
- m.getD a fallback = Quotient.lift (fun (m : Std.DHashMap α β) => m.getD a fallback) ⋯ m
Instances For
Removes the mapping for the given key if it exists.
Equations
- m.erase a = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (m.erase a)) ⋯ m
Instances For
Tries to retrieve the mapping for the given key, returning none
if no such mapping is present.
Equations
- Std.ExtDHashMap.Const.get? m a = Quotient.lift (fun (m : Std.DHashMap α fun (x : α) => β) => Std.DHashMap.Const.get? m a) ⋯ m
Instances For
Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
a ∈ m
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tries to retrieve the mapping for the given key, returning fallback
if no such mapping is present.
Equations
- Std.ExtDHashMap.Const.getD m a fallback = Quotient.lift (fun (m : Std.DHashMap α fun (x : α) => β) => Std.DHashMap.Const.getD m a fallback) ⋯ m
Instances For
Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
Equations
- Std.ExtDHashMap.Const.get! m a = Quotient.lift (fun (m : Std.DHashMap α fun (x : α) => β) => Std.DHashMap.Const.get! m a) ⋯ m
Instances For
Equivalent to (but potentially faster than) calling Const.get?
followed by insertIfNew
.
Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.
If the returned value is some v
, then the returned map is unaltered. If it is none
, then the
returned map has a new value inserted.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Checks if a mapping for the given key exists and returns the key if it does, otherwise none
.
The result in the some
case is guaranteed to be pointer equal to the key in the map.
Equations
- m.getKey? a = Quotient.lift (fun (m : Std.DHashMap α β) => m.getKey? a) ⋯ m
Instances For
Retrieves the key from the mapping that matches a
. Ensures that such a mapping exists by
requiring a proof of a ∈ m
. The result is guaranteed to be pointer equal to the key in the map.
Equations
- m.getKey a h = Quotient.pliftOn m (fun (m_1 : Std.DHashMap α β) (h' : m = Quotient.mk (Std.DHashMap.isSetoid α β) m_1) => m_1.getKey a ⋯) ⋯
Instances For
Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
Equations
- m.getKey! a = Quotient.lift (fun (m : Std.DHashMap α β) => m.getKey! a) ⋯ m
Instances For
Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback
.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
Equations
- m.getKeyD a fallback = Quotient.lift (fun (m : Std.DHashMap α β) => m.getKeyD a fallback) ⋯ m
Instances For
The number of mappings present in the hash map
Equations
- m.size = Quotient.lift (fun (m : Std.DHashMap α β) => m.size) ⋯ m
Instances For
Returns true
if the hash map contains no mappings.
Note that if your BEq
instance is not reflexive or your Hashable
instance is not
lawful, then it is possible that this function returns false
even though is not possible
to get anything out of the hash map.
Equations
- m.isEmpty = Quotient.lift (fun (m : Std.DHashMap α β) => m.isEmpty) ⋯ m
Instances For
Removes all mappings of the hash map for which the given function returns false
.
Equations
- Std.ExtDHashMap.filter f m = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (Std.DHashMap.filter f m)) ⋯ m
Instances For
Updates the values of the hash map by applying the given function to all mappings.
Equations
- Std.ExtDHashMap.map f m = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (Std.DHashMap.map f m)) ⋯ m
Instances For
Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns some
value.
Equations
- Std.ExtDHashMap.filterMap f m = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (Std.DHashMap.filterMap f m)) ⋯ m
Instances For
Modifies in place the value associated with a given key.
This function ensures that the value is used linearly.
Equations
- m.modify a f = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (m.modify a f)) ⋯ m
Instances For
Modifies in place the value associated with a given key.
This function ensures that the value is used linearly.
Equations
- Std.ExtDHashMap.Const.modify m a f = Quotient.lift (fun (m : Std.DHashMap α fun (x : α) => β) => Quotient.mk' (Std.DHashMap.Const.modify m a f)) ⋯ m
Instances For
Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an Option
valued replacement function.
This function ensures that the value is used linearly.
Equations
- m.alter a f = Quotient.lift (fun (m : Std.DHashMap α β) => Quotient.mk' (m.alter a f)) ⋯ m
Instances For
Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an Option
valued replacement function.
This function ensures that the value is used linearly.
Equations
- Std.ExtDHashMap.Const.alter m a f = Quotient.lift (fun (m : Std.DHashMap α fun (x : α) => β) => Quotient.mk' (Std.DHashMap.Const.alter m a f)) ⋯ m
Instances For
Inserts multiple mappings into the hash map by iterating over the given collection and calling
insert
. If the same key appears multiple times, the last occurrence takes precedence.
Note: this precedence behavior is true for HashMap
, DHashMap
, HashMap.Raw
and DHashMap.Raw
.
The insertMany
function on HashSet
and HashSet.Raw
behaves differently: it will prefer the first
appearance.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inserts multiple mappings into the hash map by iterating over the given collection and calling
insert
. If the same key appears multiple times, the last occurrence takes precedence.
Note: this precedence behavior is true for HashMap
, DHashMap
, HashMap.Raw
and DHashMap.Raw
.
The insertMany
function on HashSet
and HashSet.Raw
behaves differently: it will prefer the first
appearance.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inserts multiple keys with the value ()
into the hash map by iterating over the given collection
and calling insertIfNew
. If the same key appears multiple times, the first occurrence takes
precedence.
This is mainly useful to implement HashSet.insertMany
, so if you are considering using this,
HashSet
or HashSet.Raw
might be a better fit for you.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Creates a hash map from an array of keys, associating the value ()
with each key.
This is mainly useful to implement HashSet.ofArray
, so if you are considering using this,
HashSet
or HashSet.Raw
might be a better fit for you.
Instances For
Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.
Equations
Instances For
Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.
Equations
Instances For
Creates a hash map from a list of keys, associating the value ()
with each key.
This is mainly useful to implement HashSet.ofList
, so if you are considering using this,
HashSet
or HashSet.Raw
might be a better fit for you.