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 α] :
    Equations
    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 : Std.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
        • { stage₁ := true, map₁ := m₁, map₂ := m₂ }.insert x✝ x = { stage₁ := true, map₁ := m₁.insert x✝ x, map₂ := m₂ }
        • { stage₁ := false, map₁ := m₁, map₂ := m₂ }.insert x✝ x = { stage₁ := false, map₁ := m₁, map₂ := Lean.PersistentHashMap.insert m₂ x✝ x }
        Instances For
          @[specialize #[]]
          def Lean.SMap.insert' {α : Type u} {β : Type v} [BEq α] [Hashable α] :
          Lean.SMap α βαβLean.SMap α β
          Equations
          • { stage₁ := true, map₁ := m₁, map₂ := m₂ }.insert' x✝ x = { stage₁ := true, map₁ := m₁.insert x✝ x, map₂ := m₂ }
          • { stage₁ := false, map₁ := m₁, map₂ := m₂ }.insert' x✝ x = { stage₁ := false, map₁ := m₁, map₂ := Lean.PersistentHashMap.insert m₂ x✝ x }
          Instances For
            @[specialize #[]]
            def Lean.SMap.find? {α : Type u} {β : Type v} [BEq α] [Hashable α] :
            Lean.SMap α βαOption β
            Equations
            Instances For
              @[inline]
              def Lean.SMap.findD {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) (a : α) (b₀ : β) :
              β
              Equations
              • m.findD a b₀ = (m.find? a).getD b₀
              Instances For
                @[inline]
                def Lean.SMap.find! {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : Lean.SMap α β) (a : α) :
                β
                Equations
                • m.find! a = match m.find? a with | some b => b | none => panicWithPosWithDecl "Lean.Data.SMap" "Lean.SMap.find!" 62 14 "key is not in the map"
                Instances For
                  @[specialize #[]]
                  def Lean.SMap.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                  Lean.SMap α βαBool
                  Equations
                  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
                    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
                        instance Lean.SMap.instForMProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_1} :
                        ForM m (Lean.SMap α β) (α × β)
                        Equations
                        • Lean.SMap.instForMProd = { forM := fun [Monad m] (s : Lean.SMap α β) (f : α × βm PUnit) => s.forM fun (x : α) (y : β) => f (x, y) }
                        instance Lean.SMap.instForInProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type (max u_1 u_2) → Type u_1} :
                        ForIn m (Lean.SMap α β) (α × β)
                        Equations
                        • Lean.SMap.instForInProd = { forIn := fun {β_1 : Type (max ?u.38 ?u.37)} [Monad m] => ForM.forIn }
                        def Lean.SMap.switch {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) :
                        Lean.SMap α β

                        Move from stage 1 into stage 2.

                        Equations
                        • m.switch = if m.stage₁ = true then { stage₁ := false, map₁ := m.map₁, map₂ := m.map₂ } else m
                        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.foldM {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} {m : Type w → Type w} [Monad m] (f : σαβm σ) (init : σ) (map : Lean.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 : 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 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