Documentation

Batteries.Data.HashMap.Basic

@[inline]
def Std.HashMap.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : 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
Instances For
    def Std.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.
    Instances For

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

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

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

      Instances
        @[deprecated Std.HashMap (since := "2025-04-09")]
        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).

        Instances For
          @[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
          Instances For
            @[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
            Instances For
              @[inline]
              def Batteries.HashMap.size {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) :

              The number of elements in the hash map.

              (ofList [("one", 1), ("two", 2)]).size = 2
              
              Equations
              Instances For
                @[inline]
                def Batteries.HashMap.isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) :

                Is the map empty?

                (empty : Batteries.HashMap Int Int).isEmpty = true
                (ofList [("one", 1), ("two", 2)]).isEmpty = false
                
                Equations
                Instances For
                  @[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
                  Instances For
                    @[inline]
                    def Batteries.HashMap.insert' {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (m : HashMap α β) (a : α) (b : β) :

                    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
                    Instances For
                      @[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
                      Instances For
                        @[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
                        Instances For
                          @[inline]
                          def Batteries.HashMap.find? {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) :

                          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
                          Instances For
                            @[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
                            Instances For
                              @[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
                              Instances For
                                instance Batteries.HashMap.instGetElemOptionTrue {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} :
                                GetElem (HashMap α β) α (Option β) fun (x : HashMap α β) (x : α) => True
                                Equations
                                @[inline]
                                def Batteries.HashMap.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : 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
                                Instances For
                                  @[inline]
                                  def Batteries.HashMap.contains {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} (self : HashMap α β) (a : α) :

                                  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
                                  Instances For
                                    @[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
                                    Instances For
                                      @[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
                                      Instances For
                                        @[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
                                        Instances For
                                          @[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
                                          Instances For
                                            @[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 α β) :

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

                                                  The number of buckets in the hash map.

                                                  Equations
                                                  Instances For
                                                    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
                                                    Instances For
                                                      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
                                                      Instances For