Red-Black Dictionary

Defines an insertion-ordered key-value mapping backed by an red-black tree. Implemented via a key-index Std.TreeMap into an Array of key-value pairs.

structure Lake.Toml.RBDict (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v)

An insertion-ordered key-value mapping backed by a red-black tree.

• items : Array (α × β)
• indices : Std.TreeMap α Nat cmp

@[instance_reducible]

instance Lake.Toml.instInhabitedRBDict {a✝ : Type u_1} {a✝¹ : Type u_2} {a✝² : a✝ → a✝ → Ordering} : Inhabited (RBDict a✝ a✝¹ a✝²)

Equations

• Lake.Toml.instInhabitedRBDict = { default := Lake.Toml.instInhabitedRBDict.default }

@[reducible, inline]

abbrev Lake.Toml.NameDict (α : Type u) : Type u

Equations

• Lake.Toml.NameDict α = Lake.Toml.RBDict Lean.Name α Lean.Name.quickCmp

def Lake.Toml.RBDict.empty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : RBDict α β cmp

Equations

• Lake.Toml.RBDict.empty = { items := #[], indices := ∅ }

@[instance_reducible]

instance Lake.Toml.RBDict.instEmptyCollection {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : EmptyCollection (RBDict α β cmp)

Equations

• Lake.Toml.RBDict.instEmptyCollection = { emptyCollection := Lake.Toml.RBDict.empty }

def Lake.Toml.RBDict.mkEmpty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (capacity : Nat) : RBDict α β cmp

Equations

• Lake.Toml.RBDict.mkEmpty capacity = { items := Array.mkEmpty capacity, indices := ∅ }

def Lake.Toml.RBDict.ofArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (items : Array (α × β)) : RBDict α β cmp

Equations

• One or more equations did not get rendered due to their size.

def Lake.Toml.RBDict.beq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [BEq (α × β)] (self other : RBDict α β cmp) : Bool

Equations

• self.beq other = (self.items == other.items)

@[instance_reducible]

instance Lake.Toml.RBDict.instBEqOfProd {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [BEq (α × β)] : BEq (RBDict α β cmp)

Equations

• Lake.Toml.RBDict.instBEqOfProd = { beq := Lake.Toml.RBDict.beq }

@[reducible, inline]

abbrev Lake.Toml.RBDict.size {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Nat

Equations

• t.size = t.items.size

@[reducible, inline]

abbrev Lake.Toml.RBDict.isEmpty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Bool

Equations

• t.isEmpty = t.items.isEmpty

def Lake.Toml.RBDict.keys {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Array α

Equations

• t.keys = Array.map (fun (x : α × β) => x.fst) t.items

def Lake.Toml.RBDict.values {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Array β

Equations

• t.values = Array.map (fun (x : α × β) => x.snd) t.items

def Lake.Toml.RBDict.contains {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Bool

Equations

• Lake.Toml.RBDict.contains k t = t.indices.contains k

def Lake.Toml.RBDict.findIdx? {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Option (Fin t.size)

Equations

• Lake.Toml.RBDict.findIdx? k t = do let i ← t.indices.get? k if h : i < t.items.size then some ⟨i, h⟩ else none

def Lake.Toml.RBDict.findEntry? {α β : Type} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Option (α × β)

Equations

• Lake.Toml.RBDict.findEntry? k t = do let __do_lift ← Lake.Toml.RBDict.findIdx? k t pure t.items[__do_lift]

@[inline]

def Lake.Toml.RBDict.find? {α β : Type} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Option β

Equations

• Lake.Toml.RBDict.find? k t = do let __do_lift ← Lake.Toml.RBDict.findEntry? k t pure __do_lift.snd

def Lake.Toml.RBDict.push {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

Equations

• Lake.Toml.RBDict.push k v t = { items := t.items.push (k, v), indices := t.indices.insert k t.items.size }

@[specialize #[]]

def Lake.Toml.RBDict.alter {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (f : Option β → β) (t : RBDict α β cmp) : RBDict α β cmp

Equations

• One or more equations did not get rendered due to their size.

def Lake.Toml.RBDict.insert {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

Equations

• One or more equations did not get rendered due to their size.

@[macro_inline]

def Lake.Toml.RBDict.insertIf {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (p : Bool) (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

Inserts the value into the dictionary if p is true.

Equations

• Lake.Toml.RBDict.insertIf p k v t = if p = true then Lake.Toml.RBDict.insert k v t else t

@[macro_inline]

def Lake.Toml.RBDict.insertUnless {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (p : Bool) (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

Inserts the value into the dictionary if p is false.

Equations

• Lake.Toml.RBDict.insertUnless p k v t = if p = true then t else Lake.Toml.RBDict.insert k v t

@[macro_inline]

def Lake.Toml.RBDict.insertSome {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (v? : Option β) (t : RBDict α β cmp) : RBDict α β cmp

Insert the value into the dictionary if it is not none.

Equations

• Lake.Toml.RBDict.insertSome k (some v) t = Lake.Toml.RBDict.insert k v t
• Lake.Toml.RBDict.insertSome k v? t = t

def Lake.Toml.RBDict.appendArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self : RBDict α β cmp) (other : Array (α × β)) : RBDict α β cmp

Equations

• self.appendArray other = Array.foldl (fun (t : Lake.Toml.RBDict α β cmp) (x : α × β) => match x with | (k, v) => Lake.Toml.RBDict.insert k v t) self other

@[instance_reducible]

instance Lake.Toml.RBDict.instHAppendArrayProd {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : HAppend (RBDict α β cmp) (Array (α × β)) (RBDict α β cmp)

Equations

• Lake.Toml.RBDict.instHAppendArrayProd = { hAppend := Lake.Toml.RBDict.appendArray }

@[inline]

def Lake.Toml.RBDict.append {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self other : RBDict α β cmp) : RBDict α β cmp

Equations

• self.append other = self.appendArray other.items

@[instance_reducible]

instance Lake.Toml.RBDict.instAppend {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : Append (RBDict α β cmp)

Equations

• Lake.Toml.RBDict.instAppend = { append := Lake.Toml.RBDict.append }

@[inline]

def Lake.Toml.RBDict.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : α → α → Ordering} (f : α → β → γ) (t : RBDict α β cmp) : RBDict α γ cmp

Equations

• Lake.Toml.RBDict.map f t = { items := Array.map (fun (x : α × β) => match x with | (k, v) => (k, f k v)) t.items, indices := t.indices }

@[inline]

def Lake.Toml.RBDict.filter {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (p : α → β → Bool) (t : RBDict α β cmp) : RBDict α β cmp

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Toml.RBDict.filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : α → α → Ordering} (f : α → β → Option γ) (t : RBDict α β cmp) : RBDict α γ cmp

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Toml.RBDict.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} [Monad m] (f : σ → α → β → m σ) (init : σ) (t : RBDict α β cmp) : m σ

Equations

• Lake.Toml.RBDict.foldM f init t = Array.foldlM (fun (s : σ) (x : α × β) => match x with | (k, v) => f s k v) init t.items

@[inline]

def Lake.Toml.RBDict.fold {σ : Type u_1} {α : Type u_2} {β : Type u_3} {cmp : α → α → Ordering} (f : σ → α → β → σ) (init : σ) (t : RBDict α β cmp) : σ

Equations

• Lake.Toml.RBDict.fold f init t = (Lake.Toml.RBDict.foldM f init t).run