Documentation

Lean.Data.SMap

structure Lean.SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
Type (max u v)

Staged map for implementing the Environment. The idea is to store imported entries into a hashtable and local entries into a persistent hashtable.

Hypotheses:

  • The number of entries (i.e., declarations) coming from imported files is much bigger than the number of entries in the current file.
  • HashMap is faster than PersistentHashMap.
  • When we are reading imported files, we have exclusive access to the map, and efficient destructive updates are performed.

Remarks:

  • We never remove declarations from the Environment. In principle, we could support deletion by using (PHashMap α (Option β)) where the value none would indicate that an entry was "removed" from the hashtable.
  • We do not need additional bookkeeping for extracting the local entries.
Instances For
    instance Lean.SMap.instInhabitedSMap {α : Type u} {β : Type v} [BEq α] [Hashable α] :
    Equations
    • One or more equations did not get rendered due to their size.
    def Lean.SMap.empty {α : Type u} {β : Type v} [BEq α] [Hashable α] :
    Lean.SMap α β
    Equations
    Instances For
      @[inline]
      def Lean.SMap.fromHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMap α β) (stage₁ : optParam Bool true) :
      Lean.SMap α β
      Equations
      Instances For
        @[specialize #[]]
        def Lean.SMap.insert {α : Type u} {β : Type v} [BEq α] [Hashable α] :
        Lean.SMap α βαβLean.SMap α β
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[specialize #[]]
          def Lean.SMap.insert' {α : Type u} {β : Type v} [BEq α] [Hashable α] :
          Lean.SMap α βαβLean.SMap α β
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[specialize #[]]
            def Lean.SMap.find? {α : Type u} {β : Type v} [BEq α] [Hashable α] :
            Lean.SMap α βαOption β
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]
              def Lean.SMap.findD {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) (a : α) (b₀ : β) :
              β
              Equations
              Instances For
                @[inline]
                def Lean.SMap.find! {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : Lean.SMap α β) (a : α) :
                β
                Equations
                Instances For
                  @[specialize #[]]
                  def Lean.SMap.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                  Lean.SMap α βαBool
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[specialize #[]]
                    def Lean.SMap.find?' {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                    Lean.SMap α βαOption β

                    Similar to find?, but searches for result in the hashmap first. So, the result is correct only if we never "overwrite" map₁ entries using map₂.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Lean.SMap.forM {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_1} [Monad m] (s : Lean.SMap α β) (f : αβm PUnit) :
                      Equations
                      Instances For
                        def Lean.SMap.switch {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) :
                        Lean.SMap α β

                        Move from stage 1 into stage 2.

                        Equations
                        Instances For
                          @[inline]
                          def Lean.SMap.foldStage2 {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} (f : σαβσ) (s : σ) (m : Lean.SMap α β) :
                          σ
                          Equations
                          Instances For
                            def Lean.SMap.fold {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} (f : σαβσ) (init : σ) (m : Lean.SMap α β) :
                            σ
                            Equations
                            Instances For
                              def Lean.SMap.size {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) :
                              Equations
                              Instances For
                                def Lean.SMap.stageSizes {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) :
                                Equations
                                Instances For
                                  def Lean.SMap.numBuckets {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) :
                                  Equations
                                  Instances For
                                    def Lean.SMap.toList {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) :
                                    List (α × β)
                                    Equations
                                    Instances For
                                      def Lean.List.toSMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (es : List (α × β)) :
                                      Lean.SMap α β
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        instance Lean.instReprSMap {α : Type u_1} {β : Type u_2} :
                                        {x : BEq α} → {x_1 : Hashable α} → [inst : Repr α] → [inst : Repr β] → Repr (Lean.SMap α β)
                                        Equations