Lean.Data.SMap

source

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

Type (max u v)

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

source

instance Lean.SMap.instInhabitedSMap {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] :

Inhabited (Lean.SMap α β)

Equations

Lean.SMap.instInhabitedSMap = { default := { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }

source

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

Lean.SMap α β

Equations

Lean.SMap.empty = { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }

source

@[inline]

def Lean.SMap.fromHashMap {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMap α β) (stage₁ : optParam Bool true) :

Lean.SMap α β

Equations

Lean.SMap.fromHashMap m stage₁ = { stage₁ := stage₁, map₁ := m, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }

source

@[specialize]

def Lean.SMap.insert {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] :

Lean.SMap α β → α → β → Lean.SMap α β

Equations

Lean.SMap.insert x x x = match x, x, x with | { stage₁ := true, map₁ := m₁, map₂ := m₂ }, k, v => { stage₁ := true, map₁ := Std.HashMap.insert m₁ k v, map₂ := m₂ } | { stage₁ := false, map₁ := m₁, map₂ := m₂ }, k, v => { stage₁ := false, map₁ := m₁, map₂ := Std.PersistentHashMap.insert m₂ k v }

source

@[specialize]

def Lean.SMap.insert' {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] :

Lean.SMap α β → α → β → Lean.SMap α β

Equations

Lean.SMap.insert' x x x = match x, x, x with | { stage₁ := true, map₁ := m₁, map₂ := m₂ }, k, v => { stage₁ := true, map₁ := Std.HashMap.insert m₁ k v, map₂ := m₂ } | { stage₁ := false, map₁ := m₁, map₂ := m₂ }, k, v => { stage₁ := false, map₁ := m₁, map₂ := Std.PersistentHashMap.insert m₂ k v }

source

@[specialize]

def Lean.SMap.find? {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] :

Lean.SMap α β → α → Option β

Equations

Lean.SMap.find? x x = match x, x with | { stage₁ := true, map₁ := m₁, map₂ := x }, k => Std.HashMap.find? m₁ k | { stage₁ := false, map₁ := m₁, map₂ := m₂ }, k => Option.orElse (Std.PersistentHashMap.find? m₂ k) fun x => Std.HashMap.find? m₁ k

source

@[inline]

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

β

Equations

Lean.SMap.findD m a b₀ = Option.getD (Lean.SMap.find? m a) b₀

source

@[inline]

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

β

Equations

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

source

@[specialize]

def Lean.SMap.contains {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] :

Lean.SMap α β → α → Bool

Equations

Lean.SMap.contains x x = match x, x with | { stage₁ := true, map₁ := m₁, map₂ := x }, k => Std.HashMap.contains m₁ k | { stage₁ := false, map₁ := m₁, map₂ := m₂ }, k => Std.HashMap.contains m₁ k || Std.PersistentHashMap.contains m₂ k

source

@[specialize]

def Lean.SMap.find?' {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] :

Lean.SMap α β → α → Option β

Equations

Lean.SMap.find?' x x = match x, x with | { stage₁ := true, map₁ := m₁, map₂ := x }, k => Std.HashMap.find? m₁ k | { stage₁ := false, map₁ := m₁, map₂ := m₂ }, k => Option.orElse (Std.HashMap.find? m₁ k) fun x => Std.PersistentHashMap.find? m₂ k

source

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

m PUnit

Equations

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

source

def Lean.SMap.switch {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Lean.SMap α β) :

Lean.SMap α β

Equations

Lean.SMap.switch m = if m.stage₁ = true then { stage₁ := false, map₁ := m.map₁, map₂ := m.map₂ } else m

source

@[inline]

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

σ

Equations

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

source

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

σ

Equations

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

source

def Lean.SMap.size {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Lean.SMap α β) :

Nat

Equations

Lean.SMap.size m = Std.HashMap.size m.map₁ + m.map₂.size

source

def Lean.SMap.stageSizes {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Lean.SMap α β) :

Nat × Nat

Equations

Lean.SMap.stageSizes m = (Std.HashMap.size m.map₁, m.map₂.size)

source

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

Nat

Equations

Lean.SMap.numBuckets m = Std.HashMap.numBuckets m.map₁

source

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

List (α × β)

Equations

Lean.SMap.toList m = Lean.SMap.fold (fun es a b => (a, b) :: es) [] m

source

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

Lean.SMap α β

Equations

Lean.List.toSMap es = List.foldl (fun s x => match x with | (a, b) => Lean.SMap.insert s a b) { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } es

source

instance Lean.instReprSMap {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → [inst : Repr α] → [inst : Repr β] → Repr (Lean.SMap α β)

Equations

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