The type DHashMap.Raw itself is defined in the module Std.Data.DHashmap.RawDef for import
structure reasons.
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.DHashMap.Raw.emptyWithCapacity capacity = (Std.DHashMap.Internal.Raw₀.emptyWithCapacity capacity).val
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.DHashMap.Raw.instEmptyCollection = { emptyCollection := Std.DHashMap.Raw.emptyWithCapacity }
Equations
- Std.DHashMap.Raw.instInhabited = { default := ∅ }
Two hash maps are equivalent in the sense of Equiv iff
all the keys and values are equal.
- impl : (Internal.toListModel m₁.buckets).Perm (Internal.toListModel m₂.buckets)
Internal implementation detail of the hash map
Two hash maps are equivalent in the sense of Equiv iff
all the keys and values are equal.
Equations
- One or more equations did not get rendered due to their size.
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
- Std.DHashMap.Raw.instInsertSigmaOfBEqOfHashable = { insert := fun (x : (a : α) × β a) (s : Std.DHashMap.Raw α β) => match x with | ⟨a, b⟩ => 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 = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, h⟩ a b).val else m
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.
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.
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
- One or more equations did not get rendered due to their size.
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.
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
- Std.DHashMap.Raw.instMembershipOfBEqOfHashable = { mem := fun (m : Std.DHashMap.Raw α β) (a : α) => m.contains a = true }
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 = Std.DHashMap.Internal.Raw₀.get ⟨m, ⋯⟩ a ⋯
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.
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.
Tries to retrieve the mapping for the given key, returning none if no such mapping is present.
Equations
- Std.DHashMap.Raw.Const.get? m a = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.Const.get? ⟨m, h⟩ a else none
Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
a ∈ m.
Equations
- Std.DHashMap.Raw.Const.get m a h = Std.DHashMap.Internal.Raw₀.Const.get ⟨m, ⋯⟩ a ⋯
Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.
Equations
- Std.DHashMap.Raw.Const.getD m a fallback = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.Const.getD ⟨m, h⟩ a fallback else fallback
Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
Equations
- Std.DHashMap.Raw.Const.get! m a = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.Const.get! ⟨m, h⟩ a else default
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.
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 = Std.DHashMap.Internal.Raw₀.getKey ⟨m, ⋯⟩ a ⋯
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.
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.
Modifies in place the value associated with a given key.
This function ensures that the value is used linearly.
Equations
- Std.DHashMap.Raw.Const.modify m a f = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.Const.modify ⟨m, h⟩ a f).val else ∅
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.
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.DHashMap.Raw.Const.alter m a f = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.Const.alter ⟨m, h⟩ a f).val else ∅
Monadically computes a value by folding the given function over the mappings in the hash map in some order.
Equations
- Std.DHashMap.Raw.foldM f init b = Array.foldlM (fun (acc : δ) (l : Std.DHashMap.Internal.AssocList α β) => Std.DHashMap.Internal.AssocList.foldlM f acc l) init b.buckets
Folds the given function over the mappings in the hash map in some order.
Equations
- Std.DHashMap.Raw.fold f init b = (Std.DHashMap.Raw.foldM f init b).run
Internal implementation detail of the hash map.
Monadically computes a value by folding the given function over the mappings in the hash
map in the reverse order used by foldM.
Equations
- One or more equations did not get rendered due to their size.
Internal implementation detail of the hash map.
Folds the given function over the mappings in the hash map in the reverse order used
by foldM.
Equations
- Std.DHashMap.Raw.Internal.foldRev f init b = (Std.DHashMap.Raw.Internal.foldRevM f init b).run
Monadically computes a value by folding the given function over the mappings in the hash
map in the reverse order used by foldM.
Equations
- One or more equations did not get rendered due to their size.
Folds the given function over the mappings in the hash map in the reverse order used
by foldM.
Equations
- Std.DHashMap.Raw.foldRev f init b = (Std.DHashMap.Raw.Internal.foldRevM f init b).run
Support for the for loop construct in do blocks.
Equations
- Std.DHashMap.Raw.forIn f init b = forIn b.buckets init fun (bucket : Std.DHashMap.Internal.AssocList α β) (acc : δ) => bucket.forInStep acc f
Equations
- Std.DHashMap.Raw.instForMSigma = { forM := fun [Monad m] (m_1 : Std.DHashMap.Raw α β) (f : (a : α) × β a → m PUnit) => Std.DHashMap.Raw.forM (fun (a : α) (b : β a) => f ⟨a, b⟩) m_1 }
We do not define ForM and ForIn instances that are specialized to constant β. Instead, we
define uncurried versions of forM and forIn that will be used in the Const lemmas and to
define the ForM and ForIn instances for HashMap.Raw.
Carries out a monadic action on each mapping in the hash map in some order.
Equations
- Std.DHashMap.Raw.Const.forMUncurried f b = Std.DHashMap.Raw.forM (fun (a : α) (b : β) => f (a, b)) b
Support for the for loop construct in do blocks.
Equations
- Std.DHashMap.Raw.Const.forInUncurried f init b = Std.DHashMap.Raw.forIn (fun (a : α) (b : β) (d : δ) => f (a, b) d) init b
We currently do not provide lemmas for the functions below.
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.DHashMap.Raw.filterMap f m = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.filterMap f ⟨m, h⟩).val else ∅
Updates the values of the hash map by applying the given function to all mappings.
Equations
- Std.DHashMap.Raw.map f m = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.map f ⟨m, h⟩).val else ∅
Removes all mappings of the hash map for which the given function returns false.
Equations
- Std.DHashMap.Raw.filter f m = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.filter f ⟨m, h⟩).val else ∅
Transforms the hash map into an array of mappings in some order.
Returns an array of all values present in the hash map in some order.
Equations
- m.valuesArray = Std.DHashMap.Raw.fold (fun (acc : Array β) (x : α) (v : β) => acc.push v) #[] m
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
- m.insertMany l = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.insertMany ⟨m, h⟩ l).val.val else m
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
- Std.DHashMap.Raw.Const.insertMany m l = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.Const.insertMany ⟨m, h⟩ l).val.val else m
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
- Std.DHashMap.Raw.Const.insertManyIfNewUnit m l = if h : 0 < m.buckets.size then (Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l).val.val else m
Computes the union of the given hash maps, by traversing m₂ and inserting its elements into m₁.
Equations
- m₁.union m₂ = Std.DHashMap.Raw.fold (fun (acc : Std.DHashMap.Raw α β) (x : α) => acc.insert x) m₁ m₂
Equations
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.
Returns the number of buckets in the internal representation of the hash map. This function may be useful for things like monitoring system health, but it should be considered an internal implementation detail.
Equations
Transforms the hash map into a list of mappings in some order.
Equations
- Std.DHashMap.Raw.instRepr = { reprPrec := fun (m : Std.DHashMap.Raw α β) (prec : Nat) => Repr.addAppParen (Std.Format.text "Std.DHashMap.Raw.ofList " ++ reprArg m.toList) prec }
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.
Well-formedness predicate for hash maps. Users of DHashMap will not need to interact with
this. Users of DHashMap.Raw will need to provide proofs of WF to lemmas and should use lemmas
like WF.empty and WF.insert (which are always named exactly like the operations they are about)
to show that map operations preserve well-formedness. The constructors of this type are internal
implementation details and should not be accessed by users.
- wf
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw α β}
: 0 < m.buckets.size → (∀ [inst : EquivBEq α] [inst : LawfulHashable α], Internal.Raw.WFImp m) → m.WF
Internal implementation detail of the hash map
- emptyWithCapacity₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{c : Nat}
: (Internal.Raw₀.emptyWithCapacity c).val.WF
Internal implementation detail of the hash map
- insert₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
{b : β a}
: m.WF → (Internal.Raw₀.insert ⟨m, h⟩ a b).val.WF
Internal implementation detail of the hash map
- containsThenInsert₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
{b : β a}
: m.WF → (Internal.Raw₀.containsThenInsert ⟨m, h⟩ a b).snd.val.WF
Internal implementation detail of the hash map
- containsThenInsertIfNew₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
{b : β a}
: m.WF → (Internal.Raw₀.containsThenInsertIfNew ⟨m, h⟩ a b).snd.val.WF
Internal implementation detail of the hash map
- erase₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
: m.WF → (Internal.Raw₀.erase ⟨m, h⟩ a).val.WF
Internal implementation detail of the hash map
- insertIfNew₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
{b : β a}
: m.WF → (Internal.Raw₀.insertIfNew ⟨m, h⟩ a b).val.WF
Internal implementation detail of the hash map
- getThenInsertIfNew?₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
{b : β a}
: m.WF → (Internal.Raw₀.getThenInsertIfNew? ⟨m, h⟩ a b).snd.val.WF
Internal implementation detail of the hash map
- filter₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{f : (a : α) → β a → Bool}
: m.WF → (Internal.Raw₀.filter f ⟨m, h⟩).val.WF
Internal implementation detail of the hash map
- constGetThenInsertIfNew?₀
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw α fun (x : α) => β}
{h : 0 < m.buckets.size}
{a : α}
{b : β}
: m.WF → (Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, h⟩ a b).snd.val.WF
Internal implementation detail of the hash map
- modify₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
{f : β a → β a}
: m.WF → (Internal.Raw₀.modify ⟨m, h⟩ a f).val.WF
Internal implementation detail of the hash map
- constModify₀
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw α fun (x : α) => β}
{h : 0 < m.buckets.size}
{a : α}
{f : β → β}
: m.WF → (Internal.Raw₀.Const.modify ⟨m, h⟩ a f).val.WF
Internal implementation detail of the hash map
- alter₀
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Raw α β}
{h : 0 < m.buckets.size}
{a : α}
{f : Option (β a) → Option (β a)}
: m.WF → (Internal.Raw₀.alter ⟨m, h⟩ a f).val.WF
Internal implementation detail of the hash map
- constAlter₀
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw α fun (x : α) => β}
{h : 0 < m.buckets.size}
{a : α}
{f : Option β → Option β}
: m.WF → (Internal.Raw₀.Const.alter ⟨m, h⟩ a f).val.WF
Internal implementation detail of the hash map