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

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

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

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

structure Batteries.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

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

• inner : Std.HashMap α β

  The inner Std.HashMap powering the Batteries.HashMap.

@[inline]

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

Make a new hash map with the specified capacity.

Equations

• Batteries.mkHashMap capacity = { inner := { inner := ⟨Std.DHashMap.Raw.emptyWithCapacity capacity, ⋯⟩ } }

instance Batteries.HashMap.instInhabited {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : Inhabited (HashMap α β)

Equations

• Batteries.HashMap.instInhabited = { default := Batteries.mkHashMap }

instance Batteries.HashMap.instEmptyCollection {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : EmptyCollection (HashMap α β)

Equations

• Batteries.HashMap.instEmptyCollection = { emptyCollection := Batteries.mkHashMap }

@[inline]

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

Make a new empty hash map.

(empty : Batteries.HashMap Int Int).toList = []

Equations

• Batteries.HashMap.empty = Batteries.mkHashMap

@[inline]

def Batteries.HashMap.size {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Nat

The number of elements in the hash map.

(ofList [("one", 1), ("two", 2)]).size = 2

Equations

• self.size = self.inner.size

@[inline]

def Batteries.HashMap.isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Bool

Is the map empty?

(empty : Batteries.HashMap Int Int).isEmpty = true
(ofList [("one", 1), ("two", 2)]).isEmpty = false

Equations

• self.isEmpty = self.inner.isEmpty

@[inline]

def Batteries.HashMap.insert {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) (b : β) : 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.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.insert "three" 3 = {"one" => 1, "two" => 2, "three" => 3}
hashMap.insert "two" 0 = {"one" => 1, "two" => 0}

Equations

• self.insert a b = { inner := self.inner.insert a b }

@[inline]

def Batteries.HashMap.insert' {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool

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

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.insert' "three" 3 = ({"one" => 1, "two" => 2, "three" => 3}, false)
hashMap.insert' "two" 0 = ({"one" => 1, "two" => 0}, true)

Equations

• m.insert' a b = match m.inner.containsThenInsert a b with | (contains, insert) => ({ inner := insert }, contains)

@[inline]

def Batteries.HashMap.erase {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) : HashMap α β

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

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.erase "one" = {"two" => 2}
hashMap.erase "three" = {"one" => 1, "two" => 2}

Equations

• self.erase a = { inner := self.inner.erase a }

@[inline]

def Batteries.HashMap.modify {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) (f : α → β → β) : HashMap α β

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.

(ofList [("one", 1), ("two", 2)]).modify "one" (fun _ v => v + 1) = {"one" => 2, "two" => 2}
(ofList [("one", 1), ("two", 2)]).modify "three" (fun _ v => v + 1) = {"one" => 1, "two" => 2}

Equations

• self.modify a f = { inner := self.inner.modify a (f a) }

@[inline]

def Batteries.HashMap.find? {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) : Option β

Looks up an element in the map with key a.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.find? "one" = some 1
hashMap.find? "three" = none

Equations

• self.find? a = self.inner[a]?

@[inline]

def Batteries.HashMap.findD {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) (b₀ : β) : β

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

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findD "one" 0 = 1
hashMap.findD "three" 0 = 0

Equations

• self.findD a b₀ = self.inner.getD a b₀

@[inline]

def Batteries.HashMap.find! {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} [Inhabited β] (self : HashMap α β) (a : α) : β

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

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.find! "one" = 1
hashMap.find! "three" => panic!

Equations

• self.find! a = self.inner.getD a (panicWithPosWithDecl "Batteries.Data.HashMap.Basic" "Batteries.HashMap.find!" 137 21 "key is not in the map")

instance Batteries.HashMap.instGetElemOptionTrue {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} : GetElem (HashMap α β) α (Option β) fun (x : HashMap α β) (x : α) => True

Equations

• Batteries.HashMap.instGetElemOptionTrue = { getElem := fun (m : Batteries.HashMap α β) (k : α) (x : True) => m.inner[k]? }

@[inline]

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

Given a key a, returns a key-value pair in the map whose key compares equal to a. Note that the returned key may not be identical to the input, if == ignores some part of the value.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findEntry? "one" = some ("one", 1)
hashMap.findEntry? "three" = none

Equations

• Batteries.HashMap.findEntry? m k = if h : k ∈ m then some (m.getKey k h, m.get k h) else none

@[inline]

def Batteries.HashMap.contains {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) : Bool

Returns true if the element a is in the map.

def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.contains "one" = true
hashMap.contains "three" = false

Equations

• self.contains a = self.inner.contains a

@[inline]

def Batteries.HashMap.foldM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type u_2 → Type u_2} {δ : Type u_2} {β : Type u_3} [Monad m] (f : δ → α → β → m δ) (init : δ) (self : HashMap α β) : m δ

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

def sumEven (sum: Nat) (k : String) (v : Nat) : Except String Nat :=
  if v % 2 == 0 then pure (sum + v) else throw s!"value {v} at key {k} is not even"

foldM sumEven 0 (ofList [("one", 1), ("three", 3)]) =
  Except.error "value 3 at key three is not even"
foldM sumEven 0 (ofList [("two", 2), ("four", 4)]) = Except.ok 6

Equations

• Batteries.HashMap.foldM f init self = Std.HashMap.foldM f init self.inner

@[inline]

def Batteries.HashMap.fold {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {δ : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (self : HashMap α β) : δ

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

fold (fun sum _ v => sum + v) 0 (ofList [("one", 1), ("two", 2)]) = 3

Equations

• Batteries.HashMap.fold f init self = Std.HashMap.fold f init self.inner

@[specialize #[]]

def Batteries.HashMap.mergeWithM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type (max u_2 u_1) → Type (max u_1 u_2)} {β : Type (max u_2 u_1)} [Monad m] (f : α → β → β → m β) (self other : HashMap α β) : m (HashMap α β)

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

def map1 := ofList [("one", 1), ("two", 2)]
def map2 := ofList [("two", 2), ("three", 3)]
def map3 := ofList [("two", 3), ("three", 3)]
def mergeIfNoConflict? (_ : String) (v₁ v₂ : Nat) : Option Nat :=
  if v₁ != v₂ then none else some v₁


mergeWithM mergeIfNoConflict? map1 map2 = some {"one" => 1, "two" => 2, "three" => 3}
mergeWithM mergeIfNoConflict? map1 map3 = none

Equations

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

@[inline]

def Batteries.HashMap.mergeWith {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (f : α → β → β → β) (self other : HashMap α β) : HashMap α β

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

mergeWith (fun _ v₁ v₂ => v₁ + v₂ )
  (ofList [("one", 1), ("two", 2)]) (ofList [("two", 2), ("three", 3)]) =
    {"one" => 1, "two" => 4, "three" => 3}

Equations

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

@[inline]

def Batteries.HashMap.forM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type u_2 → Type u_2} {β : Type u_3} [Monad m] (f : α → β → m PUnit) (self : HashMap α β) : m PUnit

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

def checkEven (k : String) (v : Nat) : Except String Unit :=
  if v % 2 == 0 then pure () else throw s!"value {v} at key {k} is not even"

forM checkEven (ofList [("one", 1), ("three", 3)]) = Except.error "value 3 at key three is not even"
forM checkEven (ofList [("two", 2), ("four", 4)]) = Except.ok ()

Equations

• Batteries.HashMap.forM f self = Std.HashMap.forM f self.inner

def Batteries.HashMap.toList {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : List (α × β)

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

open List
(ofList [("one", 1), ("two", 2)]).toList ~ [("one", 1), ("two", 2)]

Equations

• self.toList = Batteries.HashMap.fold (fun (r : List (α × β)) (k : α) (v : β) => (k, v) :: r) [] self

def Batteries.HashMap.toArray {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Array (α × β)

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

open List
(ofList [("one", 1), ("two", 2)]).toArray.data ~ #[("one", 1), ("two", 2)].data

Equations

• self.toArray = Batteries.HashMap.fold (fun (r : Array (α × β)) (k : α) (v : β) => r.push (k, v)) #[] self

def Batteries.HashMap.numBuckets {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) : Nat

The number of buckets in the hash map.

Equations

• self.numBuckets = Std.HashMap.Internal.numBuckets self.inner

def Batteries.HashMap.ofList {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (l : List (α × β)) : HashMap α β

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

ofList [("one", 1), ("one", 2)] = {"one" => 2}

Equations

• Batteries.HashMap.ofList l = List.foldl (fun (m : Batteries.HashMap α β) (x : α × β) => match x with | (k, v) => m.insert k v) Batteries.HashMap.empty l

def Batteries.HashMap.ofListWith {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (l : List (α × β)) (f : β → β → β) : HashMap α β

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

ofListWith [("one", 1), ("one", 2)] (fun v₁ v₂ => v₁ + v₂) = {"one" => 3}

Equations

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