Red-Black Dictionary

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

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

• items : Array (α × β)
• indices : Lean.RBMap α Nat cmp

Instances For

• Lake.Toml.RBDict.instAppend
• Lake.Toml.RBDict.instBEqOfProd
• Lake.Toml.RBDict.instEmptyCollection
• Lake.Toml.RBDict.instHAppendArrayProd
• Lake.Toml.instInhabitedRBDict

instance Lake.Toml.instInhabitedRBDict : {a : Type u_1} → {a_1 : Type u_2} → {a_2 : a → a → Ordering} → Inhabited (Lake.Toml.RBDict a a_1 a_2)

Equations

• Lake.Toml.instInhabitedRBDict = { default := { items := default, indices := default } }

@[reducible, inline]

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

Equations

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

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

Equations

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

instance Lake.Toml.RBDict.instEmptyCollection {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : EmptyCollection (Lake.Toml.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) : Lake.Toml.RBDict α β cmp

Equations

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

def Lake.Toml.RBDict.ofArray {α : Type (max u_1 u_2)} {β : Type u_2} {cmp : α → α → Ordering} (items : Array (α × β)) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) (other : Lake.Toml.RBDict α β cmp) : Bool

Equations

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

instance Lake.Toml.RBDict.instBEqOfProd {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [BEq (α × β)] : BEq (Lake.Toml.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 : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Bool

Equations

• t.isEmpty = t.items.isEmpty

def Lake.Toml.RBDict.keys {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : Lake.Toml.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 : Lake.Toml.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 : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Option (Fin t.size)

Equations

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

def Lake.Toml.RBDict.findEntry? {α : Type} {β : Type} {cmp : α → α → Ordering} (k : α) (t : Lake.Toml.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} {β : Type} {cmp : α → α → Ordering} (k : α) (t : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.RBDict α β cmp

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

Equations

• Lake.Toml.RBDict.insertSome k v? t = match v? with | some v => Lake.Toml.RBDict.insert k v t | x => t

def Lake.Toml.RBDict.appendArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self : Lake.Toml.RBDict α β cmp) (other : Array (α × β)) : Lake.Toml.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 0

instance Lake.Toml.RBDict.instHAppendArrayProd {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : HAppend (Lake.Toml.RBDict α β cmp) (Array (α × β)) (Lake.Toml.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 : Lake.Toml.RBDict α β cmp) (other : Lake.Toml.RBDict α β cmp) : Lake.Toml.RBDict α β cmp

Equations

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

instance Lake.Toml.RBDict.instAppend {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : Append (Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.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 : Lake.Toml.RBDict α β cmp) : Lake.Toml.RBDict α γ cmp

Equations

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