source
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.

- stage₁ : Bool
- map₁ : Std.HashMap α β
- map₂ : PHashMap α β

Instances For

source
instance Lean.SMap.instInhabited {α : Type u} {β : Type v} [BEq α] [Hashable α] :
Inhabited (SMap α β)
Equations

- Lean.SMap.instInhabited = { default := { } }

source
def Lean.SMap.empty {α : Type u} {β : Type v} [BEq α] [Hashable α] :
SMap α β
Equations

- Lean.SMap.empty = { }

Instances For

source
@[inline]
def Lean.SMap.fromHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap α β) (stage₁ : Bool := true) :
SMap α β
Equations

- Lean.SMap.fromHashMap m stage₁ = { stage₁ := stage₁, map₁ := m }

Instances For

source
@[specialize #[]]
def Lean.SMap.insert {α : Type u} {β : Type v} [BEq α] [Hashable α] :
SMap α β → α → β → SMap α β
Equations

- { map₁ := m₁, map₂ := m₂ }.insert x✝¹ x✝ = { 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

source
@[specialize #[]]
def Lean.SMap.insert' {α : Type u} {β : Type v} [BEq α] [Hashable α] :
SMap α β → α → β → SMap α β
Equations

- { map₁ := m₁, map₂ := m₂ }.insert' x✝¹ x✝ = { 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

source
@[specialize #[]]
def Lean.SMap.find? {α : Type u} {β : Type v} [BEq α] [Hashable α] :
SMap α β → α → Option β
Equations

- { map₁ := m₁, map₂ := map₂ }.find? x✝ = m₁[x✝]?
- { stage₁ := false, map₁ := m₁, map₂ := m₂ }.find? x✝ = (Lean.PersistentHashMap.find? m₂ x✝).orElse fun (x : Unit) => m₁[x✝]?

Instances For

source
@[inline]
def Lean.SMap.findD {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) (a : α) (b₀ : β) :
β
Equations

- m.findD a b₀ = (m.find? a).getD b₀

Instances For

source
@[inline]
def Lean.SMap.find! {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : SMap α β) (a : α) :
β
Equations

- m.find! a = match m.find? a with | some b => b | none => panicWithPosWithDecl "Lean.Data.SMap" "Lean.SMap.find!" 65 14 "key is not in the map"

Instances For

source
@[specialize #[]]
def Lean.SMap.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] :
SMap α β → α → Bool
Equations

- { map₁ := m₁, map₂ := map₂ }.contains x✝ = m₁.contains x✝
- { stage₁ := false, map₁ := m₁, map₂ := m₂ }.contains x✝ = (m₁.contains x✝ || Lean.PersistentHashMap.contains m₂ x✝)

Instances For

source
@[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

- { map₁ := m₁, map₂ := map₂ }.find?' x✝ = m₁[x✝]?
- { stage₁ := false, map₁ := m₁, map₂ := m₂ }.find?' x✝ = m₁[x✝]?.orElse fun (x : Unit) => Lean.PersistentHashMap.find? m₂ x✝

Instances For

source
def Lean.SMap.forM {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_2} [Monad m] (s : SMap α β) (f : α → β → m PUnit) :
m PUnit
Equations

- s.forM f = do Std.HashMap.forM f s.map₁ Lean.PersistentHashMap.forM s.map₂ f

Instances For

source
instance Lean.SMap.instForMProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_2} :
ForM m (SMap α β) (α × β)
Equations

- Lean.SMap.instForMProd = { forM := fun [Monad m] (s : Lean.SMap α β) (f : α × β → m PUnit) => s.forM fun (x : α) (y : β) => f (x, y) }

source
instance Lean.SMap.instForInProd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_2} :
ForIn m (SMap α β) (α × β)
Equations

- Lean.SMap.instForInProd = { forIn := fun {β_1 : Type ?u.30} [Monad m] => ForM.forIn }

source
def Lean.SMap.switch {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) :
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

source
@[inline]
def Lean.SMap.foldStage2 {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} (f : σ → α → β → σ) (s : σ) (m : SMap α β) :
σ
Equations

- Lean.SMap.foldStage2 f s m = Lean.PersistentHashMap.foldl m.map₂ f s

Instances For

source
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

- Lean.SMap.foldM f init map = do let __do_lift ← Std.HashMap.foldM f init map.map₁ Lean.PersistentHashMap.foldlM map.map₂ f __do_lift

Instances For

source
def Lean.SMap.fold {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} (f : σ → α → β → σ) (init : σ) (m : SMap α β) :
σ
Equations

- Lean.SMap.fold f init m = Lean.PersistentHashMap.foldl m.map₂ f (Std.HashMap.fold f init m.map₁)

Instances For

source
def Lean.SMap.numBuckets {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) :
Nat
Equations

- m.numBuckets = Std.HashMap.Internal.numBuckets m.map₁

Instances For

source
def Lean.SMap.toList {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : SMap α β) :
List (α × β)
Equations

- m.toList = Lean.SMap.fold (fun (es : List (α × β)) (a : α) (b : β) => (a, b) :: es) [] m

Instances For

source
def List.toSMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (es : List (α × β)) :
Lean.SMap α β
Equations

- es.toSMap = List.foldl (fun (s : Lean.SMap α β) (x : α × β) => match x with | (a, b) => s.insert a b) { } es

Instances For

source
instance Lean.instReprSMap {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Repr α] [Repr β] :
Repr (SMap α β)
Equations

- Lean.instReprSMap = { reprPrec := fun (v : Lean.SMap α β) (prec : Nat) => Repr.addAppParen (reprArg v.toList ++ Std.Format.text ".toSMap") prec }