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.instInhabited {α : Type u} {β : Type v} [BEq α] [Hashable α] :
    Inhabited (SMap α β)
    Equations
      def Lean.SMap.empty {α : Type u} {β : Type v} [BEq α] [Hashable α] :
      SMap α β
      Equations
        Instances For
          @[inline]
          def Lean.SMap.fromHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap α β) (stage₁ : Bool := true) :
          SMap α β
          Equations
            Instances For
              @[specialize #[]]
              def Lean.SMap.insert {α : Type u} {β : Type v} [BEq α] [Hashable α] :
              SMap α βαβSMap α β
              Equations
                Instances For
                  @[specialize #[]]
                  def Lean.SMap.insert' {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                  SMap α βαβSMap α β
                  Equations
                    Instances For
                      @[specialize #[]]
                      def Lean.SMap.find? {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                      SMap α βαOption β
                      Equations
                        Instances For
                          @[inline]
                          def Lean.SMap.findD {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) (a : α) (b₀ : β) :
                          β
                          Equations
                            Instances For
                              @[inline]
                              def Lean.SMap.find! {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : SMap α β) (a : α) :
                              β
                              Equations
                                Instances For
                                  @[specialize #[]]
                                  def Lean.SMap.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                                  SMap α βαBool
                                  Equations
                                    Instances For
                                      @[specialize #[]]
                                      def Lean.SMap.find?' {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                                      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
                                        Instances For
                                          def Lean.SMap.forM {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_1} [Monad m] (s : SMap α β) (f : αβm PUnit) :
                                          Equations
                                            Instances For
                                              instance Lean.SMap.instForMProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_1} :
                                              ForM m (SMap α β) (α × β)
                                              Equations
                                                instance Lean.SMap.instForInProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type (max u_1 u_2) → Type u_1} :
                                                ForIn m (SMap α β) (α × β)
                                                Equations
                                                  def Lean.SMap.switch {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) :
                                                  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 : SMap α β) :
                                                      σ
                                                      Equations
                                                        Instances For
                                                          def Lean.SMap.foldM {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} {m : Type w → Type w} [Monad m] (f : σαβm σ) (init : σ) (map : SMap α β) :
                                                          m σ

                                                          Monadic fold over a staged map.

                                                          Equations
                                                            Instances For
                                                              def Lean.SMap.fold {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} (f : σαβσ) (init : σ) (m : SMap α β) :
                                                              σ
                                                              Equations
                                                                Instances For
                                                                  def Lean.SMap.numBuckets {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) :
                                                                  Equations
                                                                    Instances For
                                                                      def Lean.SMap.toList {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) :
                                                                      List (α × β)
                                                                      Equations
                                                                        Instances For
                                                                          def List.toSMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (es : List (α × β)) :
                                                                          Lean.SMap α β
                                                                          Equations
                                                                            Instances For
                                                                              instance Lean.instReprSMap {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Repr α] [Repr β] :
                                                                              Repr (SMap α β)
                                                                              Equations