ink

class Std.HashMap.LawfulHashable (α : Type u_1) [inst : BEq α] [inst : Hashable α] : Prop

• Two elements which compare equal under the BEq instance have equal hash.

  hash_eq : ∀ {a b : α}, (a == b) = true → hash a = hash b

A hash is lawful if elements which compare equal under == have equal hash.

ink

def Std.HashMap.Imp.Bucket (α : Type u) (β : Type v) : Type (max0uv)

The bucket array of a HashMap is a nonempty array of AssocLists. (This type is an internal implementation detail of HashMap.)

Equations

• Std.HashMap.Imp.Bucket α β = { b // 0 < Array.size b }

ink

def Std.HashMap.Imp.Bucket.mk {α : Type u_1} {β : Type u_2} (buckets : optParam Nat 8) (h : autoParam (0 < buckets) _auto✝) : Std.HashMap.Imp.Bucket α β

Construct a new empty bucket array with the specified capacity.

Equations

• Std.HashMap.Imp.Bucket.mk buckets = { val := mkArray buckets Std.AssocList.nil, property := (_ : 0 < Array.size (mkArray buckets Std.AssocList.nil)) }

ink

def Std.HashMap.Imp.Bucket.update {α : Type u_1} {β : Type u_2} (data : Std.HashMap.Imp.Bucket α β) (i : USize) (d : Std.AssocList α β) (h : USize.toNat i < Array.size data.val) : Std.HashMap.Imp.Bucket α β

Update one bucket in the bucket array with a new value.

Equations

• Std.HashMap.Imp.Bucket.update data i d h = { val := Array.uset data.val i d h, property := (_ : 0 < Array.size (Array.uset data.val i d h)) }

ink

noncomputable def Std.HashMap.Imp.Bucket.size {α : Type u_1} {β : Type u_2} (data : Std.HashMap.Imp.Bucket α β) : Nat

The number of elements in the bucket array. Note: this is marked noncomputable because it is only intended for specification.

Equations

• Std.HashMap.Imp.Bucket.size data = Nat.sum (List.map (fun x => List.length (Std.AssocList.toList x)) data.val.data)

ink

@[specialize #[]]

def Std.HashMap.Imp.Bucket.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (self : Std.HashMap.Imp.Bucket α β) : Std.HashMap.Imp.Bucket α γ

Map a function over the values in the map.

Equations

• Std.HashMap.Imp.Bucket.mapVal f self = { val := Array.map (Std.AssocList.mapVal f) self.val, property := (_ : 0 < Array.size (Array.map (Std.AssocList.mapVal f) self.val)) }

ink

structure Std.HashMap.Imp.Bucket.WF {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (buckets : Std.HashMap.Imp.Bucket α β) : Prop

• The elements of a bucket are all distinct according to the BEq relation.

  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)

• Every element in a bucket should hash to its location.

  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]

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).

ink

structure Std.HashMap.Imp (α : Type u) (β : Type v) : Type (maxuv)

• The number of elements stored in the HashMap. We cache this both so that we can implement .size in O(1), and also because we use the size to determine when to resize the map.

  size : Nat

• The bucket array of the HashMap.

  buckets : Std.HashMap.Imp.Bucket α β

HashMap.Imp α β is the internal implementation type of HashMap α β.

ink

@[inline]

def Std.HashMap.Imp.numBucketsForCapacity (capacity : Nat) : Nat

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.

Equations

• Std.HashMap.Imp.numBucketsForCapacity capacity = capacity * 4 / 3

ink

@[inline]

def Std.HashMap.Imp.empty' {α : Type u_1} {β : Type u_2} (buckets : optParam Nat 8) (h : autoParam (0 < buckets) _auto✝) : Std.HashMap.Imp α β

Constructs an empty hash map with the specified nonzero number of buckets.

Equations

• Std.HashMap.Imp.empty' buckets = { size := 0, buckets := Std.HashMap.Imp.Bucket.mk buckets }

ink

def Std.HashMap.Imp.empty {α : Type u_1} {β : Type u_2} (capacity : optParam Nat 0) : Std.HashMap.Imp α β

Constructs an empty hash map with the specified target capacity.

Equations

• One or more equations did not get rendered due to their size.

ink

def Std.HashMap.Imp.mkIdx {n : Nat} (h : 0 < n) (u : USize) : { u // USize.toNat u < n }

Calculates the bucket index from a hash value u.

Equations

• Std.HashMap.Imp.mkIdx h u = { val := u % n, property := (_ : USize.toNat (u % n) < n) }

ink

@[inline]

def Std.HashMap.Imp.reinsertAux {α : Type u_1} {β : Type u_2} [inst : Hashable α] (data : Std.HashMap.Imp.Bucket α β) (a : α) (b : β) : Std.HashMap.Imp.Bucket α β

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.

Equations

• One or more equations did not get rendered due to their size.

ink

@[inline]

def Std.HashMap.Imp.foldM {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : δ → α → β → m δ) (d : δ) (map : Std.HashMap.Imp α β) : m δ

Folds a monadic function over the elements in the map (in arbitrary order).

Equations

• Std.HashMap.Imp.foldM f d map = Array.foldlM (fun d b => Std.AssocList.foldlM f d b) d map.buckets.val 0 (Array.size map.buckets.val)

ink

@[inline]

def Std.HashMap.Imp.fold {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (d : δ) (m : Std.HashMap.Imp α β) : δ

Folds a function over the elements in the map (in arbitrary order).

Equations

• Std.HashMap.Imp.fold f d m = Id.run (Std.HashMap.Imp.foldM f d m)

ink

@[inline]

def Std.HashMap.Imp.forM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : α → β → m PUnit) (h : Std.HashMap.Imp α β) : m PUnit

Runs a monadic function over the elements in the map (in arbitrary order).

Equations

• Std.HashMap.Imp.forM f h = Array.forM (fun b => Std.AssocList.forM f b) h.buckets.val 0 (Array.size h.buckets.val)

ink

def Std.HashMap.Imp.findEntry? {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (m : Std.HashMap.Imp α β) (a : α) : Option (α × β)

Given a key a, returns a key-value pair in the map whose key compares equal to a.

Equations

• One or more equations did not get rendered due to their size.

ink

def Std.HashMap.Imp.find? {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (m : Std.HashMap.Imp α β) (a : α) : Option β

Looks up an element in the map with key a.

Equations

• One or more equations did not get rendered due to their size.

ink

def Std.HashMap.Imp.contains {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (m : Std.HashMap.Imp α β) (a : α) : Bool

Returns true if the element a is in the map.

Equations

• One or more equations did not get rendered due to their size.

ink

def Std.HashMap.Imp.expand {α : Type u_1} {β : Type u_2} [inst : Hashable α] (size : Nat) (buckets : Std.HashMap.Imp.Bucket α β) : Std.HashMap.Imp α β

Copies all the entries from buckets into a new hash map with a larger capacity.

Equations

• Std.HashMap.Imp.expand size buckets = let nbuckets := Array.size buckets.val * 2; { size := size, buckets := Std.HashMap.Imp.expand.go 0 buckets.val (Std.HashMap.Imp.Bucket.mk nbuckets) }

ink

def Std.HashMap.Imp.expand.go {α : Type u_1} {β : Type u_2} [inst : Hashable α] (i : Nat) (source : Array (Std.AssocList α β)) (target : Std.HashMap.Imp.Bucket α β) : Std.HashMap.Imp.Bucket α β

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.

ink

@[inline]

def Std.HashMap.Imp.insert {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (m : Std.HashMap.Imp α β) (a : α) (b : β) : Std.HashMap.Imp α β

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.

Equations

• One or more equations did not get rendered due to their size.

ink

def Std.HashMap.Imp.erase {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (m : Std.HashMap.Imp α β) (a : α) : Std.HashMap.Imp α β

Removes key a from the map. If it does not exist in the map, the map is returned unchanged.

Equations

• One or more equations did not get rendered due to their size.

ink

@[inline]

def Std.HashMap.Imp.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (self : Std.HashMap.Imp α β) : Std.HashMap.Imp α γ

Map a function over the values in the map.

Equations

• Std.HashMap.Imp.mapVal f self = { size := self.size, buckets := Std.HashMap.Imp.Bucket.mapVal f self.buckets }

ink

@[specialize #[]]

def Std.HashMap.Imp.filterMap {α : Type u} {β : Type v} {γ : Type w} (f : α → β → Option γ) (m : Std.HashMap.Imp α β) : Std.HashMap.Imp α γ

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.

Equations

• One or more equations did not get rendered due to their size.

ink

@[specialize #[]]

def Std.HashMap.Imp.filterMap.go {α : Type u} {β : Type v} {γ : Type w} (f : α → β → Option γ) (acc : Std.AssocList α γ) : Std.AssocList α β → ULift Nat → Std.AssocList α γ × ULift Nat

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)

ink

@[inline]

def Std.HashMap.Imp.filter {α : Type u_1} {β : Type u_2} (f : α → β → Bool) (m : Std.HashMap.Imp α β) : Std.HashMap.Imp α β

Constructs a map with the set of all pairs a, b such that f returns true.

Equations

• Std.HashMap.Imp.filter f m = Std.HashMap.Imp.filterMap (fun a b => bif f a b then some b else none) m

ink

inductive Std.HashMap.Imp.WF {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} : Std.HashMap.Imp α β → Prop

• 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.
  mk: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Std.HashMap.Imp α x}, m.size = Std.HashMap.Imp.Bucket.size m.buckets → Std.HashMap.Imp.Bucket.WF m.buckets → Std.HashMap.Imp.WF m

• The empty hash map is well formed.

  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)

• Inserting into a well formed hash map yields a well formed hash map.

  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)

• Removing an element from 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)

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.

ink

theorem Std.HashMap.Imp.WF.empty {α : Type u_1} {β : Type u_2} {n : Nat} [inst : BEq α] [inst : Hashable α] : Std.HashMap.Imp.WF (Std.HashMap.Imp.empty n)

ink

def Std.HashMap (α : Type u) (β : Type v) [inst : BEq α] [inst : Hashable α] : Type (max0uv)

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).

Equations

• Std.HashMap α β = { m // Std.HashMap.Imp.WF m }

ink

@[inline]

def Std.mkHashMap {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (capacity : optParam Nat 0) : Std.HashMap α β

Make a new hash map with the specified capacity.

Equations

• Std.mkHashMap capacity = { val := Std.HashMap.Imp.empty capacity, property := (_ : Std.HashMap.Imp.WF (Std.HashMap.Imp.empty capacity)) }

ink

instance Std.HashMap.instInhabitedHashMap {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] : Inhabited (Std.HashMap α β)

Equations

• Std.HashMap.instInhabitedHashMap = { default := Std.mkHashMap }

ink

instance Std.HashMap.instEmptyCollectionHashMap {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] : EmptyCollection (Std.HashMap α β)

Equations

• Std.HashMap.instEmptyCollectionHashMap = { emptyCollection := Std.mkHashMap }

ink

@[inline]

def Std.HashMap.empty {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] : Std.HashMap α β

Make a new empty hash map.

Equations

• Std.HashMap.empty = Std.mkHashMap

ink

@[inline]

def Std.HashMap.size {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → Nat

The number of elements in the hash map.

Equations

• Std.HashMap.size self = self.val.size

ink

@[inline]

def Std.HashMap.isEmpty {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → Bool

Is the map empty?

Equations

• Std.HashMap.isEmpty self = decide (Std.HashMap.size self = 0)

ink

def Std.HashMap.insert {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → α → β → Std.HashMap α β

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.

Equations

• Std.HashMap.insert self a b = { val := Std.HashMap.Imp.insert self.val a b, property := (_ : Std.HashMap.Imp.WF (Std.HashMap.Imp.insert self.val a b)) }

ink

@[inline]

def Std.HashMap.insert' {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → α → β → Std.HashMap α β × Bool

Similar to insert, but also returns a boolean flag indicating whether an existing entry has been replaced with a ↦ b↦ b.

Equations

• Std.HashMap.insert' m a b = let old := Std.HashMap.size m; let m' := Std.HashMap.insert m a b; let replaced := old == Std.HashMap.size m'; (m', replaced)

ink

@[inline]

def Std.HashMap.erase {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → α → Std.HashMap α β

Removes key a from the map. If it does not exist in the map, the map is returned unchanged.

Equations

• Std.HashMap.erase self a = { val := Std.HashMap.Imp.erase self.val a, property := (_ : Std.HashMap.Imp.WF (Std.HashMap.Imp.erase self.val a)) }

ink

@[inline]

def Std.HashMap.findEntry? {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → α → Option (α × β)

Given a key a, returns a key-value pair in the map whose key compares equal to a.

Equations

• Std.HashMap.findEntry? self a = Std.HashMap.Imp.findEntry? self.val a

ink

@[inline]

def Std.HashMap.find? {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → α → Option β

Looks up an element in the map with key a.

Equations

• Std.HashMap.find? self a = Std.HashMap.Imp.find? self.val a

ink

@[inline]

def Std.HashMap.findD {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → α → β → β

Looks up an element in the map with key a. Returns b₀ if the element is not found.

Equations

• Std.HashMap.findD self a b₀ = Option.getD (Std.HashMap.find? self a) b₀

ink

@[inline]

def Std.HashMap.find! {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → [inst : Inhabited β] → Std.HashMap α β → α → β

Looks up an element in the map with key a. Panics if the element is not found.

Equations

• Std.HashMap.find! self a = Option.getD (Std.HashMap.find? self a) (panicWithPosWithDecl "Std.Data.HashMap.Basic" "Std.HashMap.find!" 294 23 "key is not in the map")

ink

instance Std.HashMap.instGetElemHashMapOptionTrue {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → GetElem (Std.HashMap α β) α (Option β) fun x x => True

Equations

• Std.HashMap.instGetElemHashMapOptionTrue = { getElem := fun m k x => Std.HashMap.find? m k }

ink

@[inline]

def Std.HashMap.contains {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → α → Bool

Returns true if the element a is in the map.

Equations

• Std.HashMap.contains self a = Std.HashMap.Imp.contains self.val a

ink

@[inline]

def Std.HashMap.foldM {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {m : Type u_2 → Type u_3} → {δ : Type u_2} → {β : Type u_4} → [inst : Monad m] → (δ → α → β → m δ) → δ → Std.HashMap α β → m δ

Folds a monadic function over the elements in the map (in arbitrary order).

Equations

• Std.HashMap.foldM f init self = Std.HashMap.Imp.foldM f init self.val

ink

@[inline]

def Std.HashMap.fold {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {δ : Type u_2} → {β : Type u_3} → (δ → α → β → δ) → δ → Std.HashMap α β → δ

Folds a function over the elements in the map (in arbitrary order).

Equations

• Std.HashMap.fold f init self = Std.HashMap.Imp.fold f init self.val

ink

@[specialize #[]]

def Std.HashMap.mergeWithM {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {m : Type (maxu_2u_1) → Type u_3} → {β : Type (maxu_2u_1)} → [inst : Monad m] → (α → β → β → m β) → Std.HashMap α β → Std.HashMap α β → m (Std.HashMap α β)

Combines two hashmaps using a monadic function f to combine two values at a key.

Equations

• One or more equations did not get rendered due to their size.

ink

@[inline]

def Std.HashMap.mergeWith {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → (α → β → β → β) → Std.HashMap α β → Std.HashMap α β → Std.HashMap α β

Combines two hashmaps using function f to combine two values at a key.

Equations

• One or more equations did not get rendered due to their size.

ink

@[inline]

def Std.HashMap.forM {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {m : Type u_2 → Type u_3} → {β : Type u_4} → [inst : Monad m] → (α → β → m PUnit) → Std.HashMap α β → m PUnit

Runs a monadic function over the elements in the map (in arbitrary order).

Equations

• Std.HashMap.forM f self = Std.HashMap.Imp.forM f self.val

ink

def Std.HashMap.toList {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → List (α × β)

Converts the map into a list of key-value pairs.

Equations

• Std.HashMap.toList self = Std.HashMap.fold (fun r k v => (k, v) :: r) [] self

ink

def Std.HashMap.toArray {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → Array (α × β)

Converts the map into an array of key-value pairs.

Equations

• Std.HashMap.toArray self = Std.HashMap.fold (fun r k v => Array.push r (k, v)) #[] self

ink

def Std.HashMap.numBuckets {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Std.HashMap α β → Nat

The number of buckets in the hash map.

Equations

• Std.HashMap.numBuckets self = Array.size self.val.buckets.val

ink

def Std.HashMap.ofList {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → List (α × β) → Std.HashMap α β

Builds a HashMap from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences.

Equations

• Std.HashMap.ofList l = List.foldl (fun m x => match x with | (k, v) => Std.HashMap.insert m k v) Std.HashMap.empty l

ink

def Std.HashMap.ofListWith {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → List (α × β) → (β → β → β) → Std.HashMap α β

Variant of ofList which accepts a function that combines values of duplicated keys.

Equations

• One or more equations did not get rendered due to their size.