Documentation

Std.Data.HashMap.Basic

Hash maps #

This module develops the type Std.Data.HashMap of hash maps. Dependent hash maps are defined in Std.Data.DHashMap.

The operations map and filterMap on Std.Data.HashMap are defined in the module Std.Data.HashMap.AdditionalOperations.

Lemmas about the operations on Std.Data.HashMap are available in the module Std.Data.HashMap.Lemmas.

See the module Std.Data.HashMap.Raw for a variant of this type which is safe to use in nested inductive types.

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

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, == should be an equivalence relation and a == b should 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.

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.Data.HashMap.Raw and Std.Data.HashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer HashMap over HashMap.Raw.

Dependent hash maps, in which keys may occur in their values' types, are available as Std.Data.DHashMap.

  • inner : Std.DHashMap α fun (x : α) => β

    Internal implementation detail of the hash map

Instances For
    @[inline]
    def Std.HashMap.empty {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity : optParam Nat 8) :

    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
    Instances For
      instance Std.HashMap.instEmptyCollection {α : Type u} {β : Type v} [BEq α] [Hashable α] :
      Equations
      • Std.HashMap.instEmptyCollection = { emptyCollection := Std.HashMap.empty }
      instance Std.HashMap.instInhabited {α : Type u} {β : Type v} [BEq α] [Hashable α] :
      Equations
      • Std.HashMap.instInhabited = { default := }
      @[inline]
      def Std.HashMap.insert {α : Type u} {β : Type v} :
      {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαβStd.HashMap α β

      Inserts the given mapping into the map, replacing an existing mapping for the key if there is one.

      Equations
      • m.insert a b = { inner := m.inner.insert a b }
      Instances For
        instance Std.HashMap.instSingletonProd {α : Type u} {β : Type v} :
        {x : BEq α} → {x_1 : Hashable α} → Singleton (α × β) (Std.HashMap α β)
        Equations
        • Std.HashMap.instSingletonProd = { singleton := fun (x_1 : α × β) => match x_1 with | (a, b) => Std.HashMap.empty.insert a b }
        instance Std.HashMap.instInsertProd {α : Type u} {β : Type v} :
        {x : BEq α} → {x_1 : Hashable α} → Insert (α × β) (Std.HashMap α β)
        Equations
        • Std.HashMap.instInsertProd = { insert := fun (x_1 : α × β) (s : Std.HashMap α β) => match x_1 with | (a, b) => s.insert a b }
        instance Std.HashMap.instLawfulSingletonProd {α : Type u} {β : Type v} :
        ∀ {x : BEq α} {x_1 : Hashable α}, LawfulSingleton (α × β) (Std.HashMap α β)
        Equations
        • =
        @[inline]
        def Std.HashMap.insertIfNew {α : Type u} {β : Type v} :
        {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαβStd.HashMap α β

        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 = { inner := m.inner.insertIfNew a b }
        Instances For
          @[inline]
          def Std.HashMap.containsThenInsert {α : Type u} {β : Type v} :
          {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαβBool × Std.HashMap α β

          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 = match m.inner.containsThenInsert a b with | (replaced, r) => (replaced, { inner := r })
          Instances For
            @[inline]
            def Std.HashMap.containsThenInsertIfNew {α : Type u} {β : Type v} :
            {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαβBool × Std.HashMap α β

            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 = match m.inner.containsThenInsertIfNew a b with | (replaced, r) => (replaced, { inner := r })
            Instances For
              @[inline]
              def Std.HashMap.getThenInsertIfNew? {α : Type u} {β : Type v} :
              {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαβOption β × Std.HashMap α β

              Checks whether a key is present in a map, returning the associate 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.

              Equations
              Instances For
                @[inline]
                def Std.HashMap.get? {α : Type u} {β : Type v} :
                {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαOption β

                The notation m[a]? is preferred over calling this function directly.

                Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

                Equations
                Instances For
                  @[deprecated Std.HashMap.get?]
                  def Std.HashMap.find? {α : Type u} {β : Type v} :
                  {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαOption β

                  The notation m[a]? is preferred over calling this function directly.

                  Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

                  Equations
                  • m.find? a = m.get? a
                  Instances For
                    @[inline]
                    def Std.HashMap.contains {α : Type u} {β : Type v} :
                    {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαBool

                    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 = m.inner.contains a
                    Instances For
                      instance Std.HashMap.instMembership {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                      Equations
                      • Std.HashMap.instMembership = { mem := fun (m : Std.HashMap α β) (a : α) => a m.inner }
                      instance Std.HashMap.instDecidableMem {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap α β} {a : α} :
                      Equations
                      @[inline]
                      def Std.HashMap.get {α : Type u} {β : Type v} :
                      {x : BEq α} → {x_1 : Hashable α} → (m : Std.HashMap α β) → (a : α) → a mβ

                      The notation m[a] or m[a]'h is preferred over calling this function directly.

                      Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

                      Equations
                      Instances For
                        @[inline]
                        def Std.HashMap.getD {α : Type u} {β : Type v} :
                        {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαββ

                        Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

                        Equations
                        Instances For
                          @[deprecated Std.HashMap.getD]
                          def Std.HashMap.findD {α : Type u} {β : Type v} :
                          {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαββ

                          Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

                          Equations
                          • m.findD a fallback = m.getD a fallback
                          Instances For
                            @[inline]
                            def Std.HashMap.get! {α : Type u} {β : Type v} :
                            {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Std.HashMap α βαβ

                            The notation m[a]! is preferred over calling this function directly.

                            Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

                            Equations
                            Instances For
                              @[deprecated Std.HashMap.get!]
                              def Std.HashMap.find! {α : Type u} {β : Type v} :
                              {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Std.HashMap α βαOption β

                              The notation m[a]! is preferred over calling this function directly.

                              Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

                              Equations
                              • m.find! a = some (m.get! a)
                              Instances For
                                instance Std.HashMap.instGetElem?Mem {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                                GetElem? (Std.HashMap α β) α β fun (m : Std.HashMap α β) (a : α) => a m
                                Equations
                                @[inline]
                                def Std.HashMap.getKey? {α : Type u} {β : Type v} :
                                {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαOption α

                                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 = m.inner.getKey? a
                                Instances For
                                  @[inline]
                                  def Std.HashMap.getKey {α : Type u} {β : Type v} :
                                  {x : BEq α} → {x_1 : Hashable α} → (m : Std.HashMap α β) → (a : α) → a mα

                                  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 = m.inner.getKey a h
                                  Instances For
                                    @[inline]
                                    def Std.HashMap.getKeyD {α : Type u} {β : Type v} :
                                    {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βααα

                                    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 = m.inner.getKeyD a fallback
                                    Instances For
                                      @[inline]
                                      def Std.HashMap.getKey! {α : Type u} {β : Type v} :
                                      {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited α] → Std.HashMap α βαα

                                      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 = m.inner.getKey! a
                                      Instances For
                                        @[inline]
                                        def Std.HashMap.erase {α : Type u} {β : Type v} :
                                        {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαStd.HashMap α β

                                        Removes the mapping for the given key if it exists.

                                        Equations
                                        • m.erase a = { inner := m.inner.erase a }
                                        Instances For
                                          @[inline]
                                          def Std.HashMap.size {α : Type u} {β : Type v} :
                                          {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βNat

                                          The number of mappings present in the hash map

                                          Equations
                                          • m.size = m.inner.size
                                          Instances For
                                            @[inline]
                                            def Std.HashMap.isEmpty {α : Type u} {β : Type v} :
                                            {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βBool

                                            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 = m.inner.isEmpty
                                            Instances For

                                              We currently do not provide lemmas for the functions below.

                                              @[inline]
                                              def Std.HashMap.filter {α : Type u} {β : Type v} :
                                              {x : BEq α} → {x_1 : Hashable α} → (αβBool)Std.HashMap α βStd.HashMap α β

                                              Removes all mappings of the hash map for which the given function returns false.

                                              Equations
                                              Instances For
                                                @[inline]
                                                def Std.HashMap.partition {α : Type u} {β : Type v} :
                                                {x : BEq α} → {x_1 : Hashable α} → (αβBool)Std.HashMap α βStd.HashMap α β × Std.HashMap α β

                                                Partition a hashset into two hashsets based on a predicate.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Std.HashMap.foldM {α : Type u} {β : Type v} :
                                                  {x : BEq α} → {x_1 : Hashable α} → {m : Type w → Type w} → [inst : Monad m] → {γ : Type w} → (γαβm γ)γStd.HashMap α βm γ

                                                  Monadically computes a value by folding the given function over the mappings in the hash map in some order.

                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    def Std.HashMap.fold {α : Type u} {β : Type v} :
                                                    {x : BEq α} → {x_1 : Hashable α} → {γ : Type w} → (γαβγ)γStd.HashMap α βγ

                                                    Folds the given function over the mappings in the hash map in some order.

                                                    Equations
                                                    Instances For
                                                      @[inline]
                                                      def Std.HashMap.forM {α : Type u} {β : Type v} :
                                                      {x : BEq α} → {x_1 : Hashable α} → {m : Type w → Type w} → [inst : Monad m] → (αβm PUnit)Std.HashMap α βm PUnit

                                                      Carries out a monadic action on each mapping in the hash map in some order.

                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Std.HashMap.forIn {α : Type u} {β : Type v} :
                                                        {x : BEq α} → {x_1 : Hashable α} → {m : Type w → Type w} → [inst : Monad m] → {γ : Type w} → (αβγm (ForInStep γ))γStd.HashMap α βm γ

                                                        Support for the for loop construct in do blocks.

                                                        Equations
                                                        Instances For
                                                          instance Std.HashMap.instForMProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type w → Type w} :
                                                          ForM m (Std.HashMap α β) (α × β)
                                                          Equations
                                                          instance Std.HashMap.instForInProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type w → Type w} :
                                                          ForIn m (Std.HashMap α β) (α × β)
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          @[inline]
                                                          def Std.HashMap.toList {α : Type u} {β : Type v} :
                                                          {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βList (α × β)

                                                          Transforms the hash map into a list of mappings in some order.

                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def Std.HashMap.toArray {α : Type u} {β : Type v} :
                                                            {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βArray (α × β)

                                                            Transforms the hash map into an array of mappings in some order.

                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              def Std.HashMap.keys {α : Type u} {β : Type v} :
                                                              {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βList α

                                                              Returns a list of all keys present in the hash map in some order.

                                                              Equations
                                                              • m.keys = m.inner.keys
                                                              Instances For
                                                                @[inline]
                                                                def Std.HashMap.keysArray {α : Type u} {β : Type v} :
                                                                {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βArray α

                                                                Returns an array of all keys present in the hash map in some order.

                                                                Equations
                                                                • m.keysArray = m.inner.keysArray
                                                                Instances For
                                                                  @[inline]
                                                                  def Std.HashMap.values {α : Type u} {β : Type v} :
                                                                  {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βList β

                                                                  Returns a list of all values present in the hash map in some order.

                                                                  Equations
                                                                  • m.values = m.inner.values
                                                                  Instances For
                                                                    @[inline]
                                                                    def Std.HashMap.valuesArray {α : Type u} {β : Type v} :
                                                                    {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βArray β

                                                                    Returns an array of all values present in the hash map in some order.

                                                                    Equations
                                                                    • m.valuesArray = m.inner.valuesArray
                                                                    Instances For
                                                                      @[inline]
                                                                      def Std.HashMap.insertMany {α : Type u} {β : Type v} :
                                                                      {x : BEq α} → {x_1 : Hashable α} → {ρ : Type w} → [inst : ForIn Id ρ (α × β)] → Std.HashMap α βρStd.HashMap α β

                                                                      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.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]
                                                                        def Std.HashMap.insertManyUnit {α : Type u} :
                                                                        {x : BEq α} → {x_1 : Hashable α} → {ρ : Type w} → [inst : ForIn Id ρ α] → Std.HashMap α UnitρStd.HashMap α Unit

                                                                        Inserts multiple keys with the value () 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.

                                                                        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
                                                                        Instances For
                                                                          @[inline]
                                                                          def Std.HashMap.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :

                                                                          Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            def Std.HashMap.union {α : Type u} {β : Type v} [BEq α] [Hashable α] (m₁ : Std.HashMap α β) (m₂ : Std.HashMap α β) :

                                                                            Computes the union of the given hash maps, by traversing m₂ and inserting its elements into m₁.

                                                                            Equations
                                                                            Instances For
                                                                              instance Std.HashMap.instUnion {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                                                                              Equations
                                                                              • Std.HashMap.instUnion = { union := Std.HashMap.union }
                                                                              @[inline]
                                                                              def Std.HashMap.unitOfList {α : Type u} [BEq α] [Hashable α] (l : List α) :

                                                                              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.

                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                def Std.HashMap.unitOfArray {α : Type u} [BEq α] [Hashable α] (l : Array α) :

                                                                                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.

                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Std.HashMap.Internal.numBuckets {α : Type u} {β : Type v} :
                                                                                  {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βNat

                                                                                  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
                                                                                  Instances For
                                                                                    instance Std.HashMap.instRepr {α : Type u} {β : Type v} [BEq α] [Hashable α] [Repr α] [Repr β] :
                                                                                    Equations
                                                                                    def Array.groupByKey {α : Type u} {β : Type v} [BEq α] [Hashable α] (key : βα) (xs : Array β) :

                                                                                    Groups all elements x, y in xs with key x == key y into the same array (xs.groupByKey key).find! (key x). Groups preserve the relative order of elements in xs.

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