Std.Data.RBMap

source

inductive Std.Rbcolor:

Type

red: Std.Rbcolor
black: Std.Rbcolor

source

inductive Std.RBNode (α : Type u) (β : α → Type v) :

Type (max u v)

leaf: {α : Type u} → {β : α → Type v} → Std.RBNode α β
node: {α : Type u} → {β : α → Type v} → Std.Rbcolor → Std.RBNode α β → (key : α) → β key → Std.RBNode α β → Std.RBNode α β

source

def Std.RBNode.depth {α : Type u} {β : α → Type v} (f : Nat → Nat → Nat) :

Std.RBNode α β → Nat

Equations

Std.RBNode.depth f Std.RBNode.leaf = 0
Std.RBNode.depth f (Std.RBNode.node color l key val r) = Nat.succ (f (Std.RBNode.depth f l) (Std.RBNode.depth f r))

source

def Std.RBNode.min {α : Type u} {β : α → Type v} :

Std.RBNode α β → Option ((k : α) × β k)

Equations

Std.RBNode.min Std.RBNode.leaf = none
Std.RBNode.min (Std.RBNode.node color Std.RBNode.leaf k v rchild) = some { fst := k, snd := v }
Std.RBNode.min (Std.RBNode.node color l key val rchild) = Std.RBNode.min l

source

def Std.RBNode.max {α : Type u} {β : α → Type v} :

Std.RBNode α β → Option ((k : α) × β k)

Equations

Std.RBNode.max Std.RBNode.leaf = none
Std.RBNode.max (Std.RBNode.node color lchild k v Std.RBNode.leaf) = some { fst := k, snd := v }
Std.RBNode.max (Std.RBNode.node color lchild key val r) = Std.RBNode.max r

source

@[specialize]

def Std.RBNode.fold {α : Type u} {β : α → Type v} {σ : Type w} (f : σ → (k : α) → β k → σ) (init : σ) :

Std.RBNode α β → σ

Equations

Std.RBNode.fold f _fun_discr Std.RBNode.leaf = _fun_discr
Std.RBNode.fold f _fun_discr (Std.RBNode.node color l k v r) = Std.RBNode.fold f (f (Std.RBNode.fold f _fun_discr l) k v) r

source

@[specialize]

def Std.RBNode.forM {α : Type u} {β : α → Type v} {m : Type → Type u_1} [inst : Monad m] (f : (k : α) → β k → m Unit) :

Std.RBNode α β → m Unit

Equations

Std.RBNode.forM f Std.RBNode.leaf = pure ()
Std.RBNode.forM f (Std.RBNode.node color l key val r) = do Std.RBNode.forM f l f key val Std.RBNode.forM f r

source

@[specialize]

def Std.RBNode.foldM {α : Type u} {β : α → Type v} {σ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : σ → (k : α) → β k → m σ) (init : σ) :

Std.RBNode α β → m σ

Equations

Std.RBNode.foldM f _fun_discr Std.RBNode.leaf = pure _fun_discr
Std.RBNode.foldM f _fun_discr (Std.RBNode.node color l k v r) = do let b ← Std.RBNode.foldM f _fun_discr l let b ← f b k v Std.RBNode.foldM f b r

source

@[inline]

def Std.RBNode.forIn {α : Type u} {β : α → Type v} {σ : Type w} {m : Type w → Type u_1} [inst : Monad m] (as : Std.RBNode α β) (init : σ) (f : (k : α) → β k → σ → m (ForInStep σ)) :

m σ

Equations

Std.RBNode.forIn as init f = do let a ← Std.RBNode.forIn.visit f as init match a with | ForInStep.done b => pure b | ForInStep.yield b => pure b

source

@[specialize]

def Std.RBNode.forIn.visit {α : Type u} {β : α → Type v} {σ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : (k : α) → β k → σ → m (ForInStep σ)) :

Std.RBNode α β → σ → m (ForInStep σ)

Equations

One or more equations did not get rendered due to their size.
Std.RBNode.forIn.visit f Std.RBNode.leaf _fun_discr = pure (ForInStep.yield _fun_discr)

source

@[specialize]

def Std.RBNode.revFold {α : Type u} {β : α → Type v} {σ : Type w} (f : σ → (k : α) → β k → σ) (init : σ) :

Std.RBNode α β → σ

Equations

Std.RBNode.revFold f _fun_discr Std.RBNode.leaf = _fun_discr
Std.RBNode.revFold f _fun_discr (Std.RBNode.node color l k v r) = Std.RBNode.revFold f (f (Std.RBNode.revFold f _fun_discr r) k v) l

source

@[specialize]

def Std.RBNode.all {α : Type u} {β : α → Type v} (p : (k : α) → β k → Bool) :

Std.RBNode α β → Bool

Equations

Std.RBNode.all p Std.RBNode.leaf = true
Std.RBNode.all p (Std.RBNode.node color l key val r) = (p key val && Std.RBNode.all p l && Std.RBNode.all p r)

source

@[specialize]

def Std.RBNode.any {α : Type u} {β : α → Type v} (p : (k : α) → β k → Bool) :

Std.RBNode α β → Bool

Equations

Std.RBNode.any p Std.RBNode.leaf = false
Std.RBNode.any p (Std.RBNode.node color l key val r) = (p key val || Std.RBNode.any p l || Std.RBNode.any p r)

source

def Std.RBNode.singleton {α : Type u} {β : α → Type v} (k : α) (v : β k) :

Std.RBNode α β

Equations

Std.RBNode.singleton k v = Std.RBNode.node Std.Rbcolor.red Std.RBNode.leaf k v Std.RBNode.leaf

source

@[inline]

def Std.RBNode.balance1 {α : Type u} {β : α → Type v} (a : α) :

β a → Std.RBNode α β → Std.RBNode α β → Std.RBNode α β

Equations

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

source

@[inline]

def Std.RBNode.balance2 {α : Type u} {β : α → Type v} :

(a : Std.RBNode α β) → (a : α) → β a → Std.RBNode α β → Std.RBNode α β

Equations

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

source

def Std.RBNode.isRed {α : Type u} {β : α → Type v} :

Std.RBNode α β → Bool

Equations

Std.RBNode.isRed _fun_discr = match _fun_discr with | Std.RBNode.node Std.Rbcolor.red lchild key val rchild => true | x => false

source

def Std.RBNode.isBlack {α : Type u} {β : α → Type v} :

Std.RBNode α β → Bool

Equations

Std.RBNode.isBlack _fun_discr = match _fun_discr with | Std.RBNode.node Std.Rbcolor.black lchild key val rchild => true | x => false

source

@[specialize]

def Std.RBNode.ins {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) :

Std.RBNode α β → (k : α) → β k → Std.RBNode α β

Equations

One or more equations did not get rendered due to their size.
Std.RBNode.ins cmp Std.RBNode.leaf _fun_discr _fun_discr = Std.RBNode.node Std.Rbcolor.red Std.RBNode.leaf _fun_discr _fun_discr Std.RBNode.leaf

source

def Std.RBNode.setBlack {α : Type u} {β : α → Type v} :

Std.RBNode α β → Std.RBNode α β

Equations

Std.RBNode.setBlack _fun_discr = match _fun_discr with | Std.RBNode.node color l k v r => Std.RBNode.node Std.Rbcolor.black l k v r | e => e

source

@[specialize]

def Std.RBNode.insert {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) (t : Std.RBNode α β) (k : α) (v : β k) :

Std.RBNode α β

Equations

Std.RBNode.insert cmp t k v = if Std.RBNode.isRed t = true then Std.RBNode.setBlack (Std.RBNode.ins cmp t k v) else Std.RBNode.ins cmp t k v

source

def Std.RBNode.balance₃ {α : Type u} {β : α → Type v} (a : Std.RBNode α β) (k : α) (v : β k) (d : Std.RBNode α β) :

Std.RBNode α β

Equations

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

source

def Std.RBNode.setRed {α : Type u} {β : α → Type v} :

Std.RBNode α β → Std.RBNode α β

Equations

Std.RBNode.setRed _fun_discr = match _fun_discr with | Std.RBNode.node color a k v b => Std.RBNode.node Std.Rbcolor.red a k v b | e => e

source

def Std.RBNode.balLeft {α : Type u} {β : α → Type v} :

Std.RBNode α β → (k : α) → β k → Std.RBNode α β → Std.RBNode α β

Equations

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

source

def Std.RBNode.balRight {α : Type u} {β : α → Type v} (l : Std.RBNode α β) (k : α) (v : β k) (r : Std.RBNode α β) :

Std.RBNode α β

Equations

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

source

partial def Std.RBNode.appendTrees {α : Type u} {β : α → Type v} :

Std.RBNode α β → Std.RBNode α β → Std.RBNode α β

source

@[specialize]

def Std.RBNode.del {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) (x : α) :

Std.RBNode α β → Std.RBNode α β

Equations

One or more equations did not get rendered due to their size.
Std.RBNode.del cmp x Std.RBNode.leaf = Std.RBNode.leaf

source

@[specialize]

def Std.RBNode.erase {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) (x : α) (t : Std.RBNode α β) :

Std.RBNode α β

Equations

Std.RBNode.erase cmp x t = let t := Std.RBNode.del cmp x t; Std.RBNode.setBlack t

source

@[specialize]

def Std.RBNode.findCore {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) :

Std.RBNode α β → (k : α) → Option ((k : α) × β k)

Equations

One or more equations did not get rendered due to their size.
Std.RBNode.findCore cmp Std.RBNode.leaf _fun_discr = none

source

@[specialize]

def Std.RBNode.find {α : Type u} (cmp : α → α → Ordering) {β : Type v} :

(Std.RBNode α fun x => β) → α → Option β

Equations

One or more equations did not get rendered due to their size.
Std.RBNode.find cmp Std.RBNode.leaf _fun_discr = none

source

@[specialize]

def Std.RBNode.lowerBound {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) :

Std.RBNode α β → α → Option (Sigma β) → Option (Sigma β)

Equations

One or more equations did not get rendered due to their size.
Std.RBNode.lowerBound cmp Std.RBNode.leaf _fun_discr _fun_discr = _fun_discr

source

inductive Std.RBNode.WellFormed {α : Type u} {β : α → Type v} (cmp : α → α → Ordering) :

Std.RBNode α β → Prop

leafWff: ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.RBNode.WellFormed cmp Std.RBNode.leaf
insertWff: ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {n n' : Std.RBNode α β} {k : α} {v : β k}, Std.RBNode.WellFormed cmp n → n' = Std.RBNode.insert cmp n k v → Std.RBNode.WellFormed cmp n'
eraseWff: ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {n n' : Std.RBNode α β} {k : α}, Std.RBNode.WellFormed cmp n → n' = Std.RBNode.erase cmp k n → Std.RBNode.WellFormed cmp n'

source

def Std.RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) :

Type (max u v)

source

@[inline]

def Std.mkRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) :

Std.RBMap α β cmp

Equations

Std.mkRBMap α β cmp = { val := Std.RBNode.leaf, property := (_ : Std.RBNode.WellFormed cmp Std.RBNode.leaf) }

source

@[inline]

def Std.RBMap.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp

Equations

Std.RBMap.empty = Std.mkRBMap α β cmp

source

instance Std.instEmptyCollectionRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) :

EmptyCollection (Std.RBMap α β cmp)

Equations

Std.instEmptyCollectionRBMap α β cmp = { emptyCollection := Std.RBMap.empty }

source

def Std.RBMap.depth {α : Type u} {β : Type v} {cmp : α → α → Ordering} (f : Nat → Nat → Nat) (t : Std.RBMap α β cmp) :

Nat

Equations

Std.RBMap.depth f t = Std.RBNode.depth f t.val

source

@[inline]

def Std.RBMap.fold {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} (f : σ → α → β → σ) (init : σ) :

Std.RBMap α β cmp → σ

Equations

Std.RBMap.fold f _fun_discr _fun_discr = match _fun_discr, _fun_discr with | b, { val := t, property := property } => Std.RBNode.fold f b t

source

@[inline]

def Std.RBMap.revFold {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} (f : σ → α → β → σ) (init : σ) :

Std.RBMap α β cmp → σ

Equations

Std.RBMap.revFold f _fun_discr _fun_discr = match _fun_discr, _fun_discr with | b, { val := t, property := property } => Std.RBNode.revFold f b t

source

@[inline]

def Std.RBMap.foldM {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} {m : Type w → Type u_1} [inst : Monad m] (f : σ → α → β → m σ) (init : σ) :

Std.RBMap α β cmp → m σ

Equations

Std.RBMap.foldM f _fun_discr _fun_discr = match _fun_discr, _fun_discr with | b, { val := t, property := property } => Std.RBNode.foldM f b t

source

@[inline]

def Std.RBMap.forM {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} [inst : Monad m] (f : α → β → m PUnit) (t : Std.RBMap α β cmp) :

m PUnit

Equations

Std.RBMap.forM f t = Std.RBMap.foldM (fun x k v => f k v) PUnit.unit t

source

@[inline]

def Std.RBMap.forIn {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} {m : Type w → Type u_1} [inst : Monad m] (t : Std.RBMap α β cmp) (init : σ) (f : α × β → σ → m (ForInStep σ)) :

m σ

Equations

Std.RBMap.forIn t init f = Std.RBNode.forIn t.val init fun a b acc => f (a, b) acc

source

instance Std.RBMap.instForInRBMapProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} :

ForIn m (Std.RBMap α β cmp) (α × β)

Equations

Std.RBMap.instForInRBMapProd = { forIn := fun {β} [Monad m] => Std.RBMap.forIn }

source

@[inline]

def Std.RBMap.isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → Bool

Equations

Std.RBMap.isEmpty _fun_discr = match _fun_discr with | { val := Std.RBNode.leaf, property := property } => true | x => false

source

@[specialize]

def Std.RBMap.toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → List (α × β)

Equations

Std.RBMap.toList _fun_discr = match _fun_discr with | { val := t, property := property } => Std.RBNode.revFold (fun ps k v => (k, v) :: ps) [] t

source

@[inline]

def Std.RBMap.min {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → Option (α × β)

Equations

Std.RBMap.min _fun_discr = match _fun_discr with | { val := t, property := property } => match Std.RBNode.min t with | some { fst := k, snd := v } => some (k, v) | none => none

source

@[inline]

def Std.RBMap.max {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → Option (α × β)

Equations

Std.RBMap.max _fun_discr = match _fun_discr with | { val := t, property := property } => match Std.RBNode.max t with | some { fst := k, snd := v } => some (k, v) | none => none

source

instance Std.RBMap.instReprRBMap {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Repr α] [inst : Repr β] :

Repr (Std.RBMap α β cmp)

Equations

Std.RBMap.instReprRBMap = { reprPrec := fun m prec => Repr.addAppParen (Std.Format.text "Std.rbmapOf " ++ repr (Std.RBMap.toList m)) prec }

source

@[inline]

def Std.RBMap.insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → α → β → Std.RBMap α β cmp

Equations

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

source

@[inline]

def Std.RBMap.erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → α → Std.RBMap α β cmp

Equations

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

source

@[specialize]

def Std.RBMap.ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

List (α × β) → Std.RBMap α β cmp

Equations

Std.RBMap.ofList [] = Std.mkRBMap α β cmp
Std.RBMap.ofList ((k, v) :: xs) = Std.RBMap.insert (Std.RBMap.ofList xs) k v

source

@[inline]

def Std.RBMap.findCore? {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → α → Option ((_ : α) × β)

Equations

Std.RBMap.findCore? _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := t, property := property }, x => Std.RBNode.findCore cmp t x

source

@[inline]

def Std.RBMap.find? {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → α → Option β

Equations

Std.RBMap.find? _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := t, property := property }, x => Std.RBNode.find cmp t x

source

@[inline]

def Std.RBMap.findD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (k : α) (v₀ : β) :

Equations

Std.RBMap.findD t k v₀ = Option.getD (Std.RBMap.find? t k) v₀

source

@[inline]

def Std.RBMap.lowerBound {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → α → Option ((_ : α) × β)

(lowerBound k) retrieves the kv pair of the largest key smaller than or equal to k, if it exists.

Equations

Std.RBMap.lowerBound _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := t, property := property }, x => Std.RBNode.lowerBound cmp t x none

source

@[inline]

def Std.RBMap.contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (a : α) :

Bool

Equations

Std.RBMap.contains t a = Option.isSome (Std.RBMap.find? t a)

source

@[inline]

def Std.RBMap.fromList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) :

Std.RBMap α β cmp

Equations

Std.RBMap.fromList l cmp = List.foldl (fun r p => Std.RBMap.insert r p.fst p.snd) (Std.mkRBMap α β cmp) l

source

@[inline]

def Std.RBMap.all {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → (α → β → Bool) → Bool

Equations

Std.RBMap.all _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := t, property := property }, p => Std.RBNode.all p t

source

@[inline]

def Std.RBMap.any {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

Std.RBMap α β cmp → (α → β → Bool) → Bool

Equations

Std.RBMap.any _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := t, property := property }, p => Std.RBNode.any p t

source

def Std.RBMap.size {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : Std.RBMap α β cmp) :

Nat

Equations

Std.RBMap.size m = Std.RBMap.fold (fun sz x x => sz + 1) 0 m

source

def Std.RBMap.maxDepth {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) :

Nat

Equations

Std.RBMap.maxDepth t = Std.RBNode.depth Nat.max t.val

source

@[inline]

def Std.RBMap.min! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Inhabited α] [inst : Inhabited β] (t : Std.RBMap α β cmp) :

α × β

Equations

Std.RBMap.min! t = match Std.RBMap.min t with | some p => p | none => panicWithPosWithDecl "Std.Data.RBMap" "Std.RBMap.min!" 337 14 "map is empty"

source

@[inline]

def Std.RBMap.max! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Inhabited α] [inst : Inhabited β] (t : Std.RBMap α β cmp) :

α × β

Equations

Std.RBMap.max! t = match Std.RBMap.max t with | some p => p | none => panicWithPosWithDecl "Std.Data.RBMap" "Std.RBMap.max!" 342 14 "map is empty"

source

@[inline]

def Std.RBMap.find! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Inhabited β] (t : Std.RBMap α β cmp) (k : α) :

Equations

Std.RBMap.find! t k = match Std.RBMap.find? t k with | some b => b | none => panicWithPosWithDecl "Std.Data.RBMap" "Std.RBMap.find!" 347 14 "key is not in the map"

source

def Std.rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) :

Std.RBMap α β cmp

Equations

Std.rbmapOf l cmp = Std.RBMap.fromList l cmp