Red-black trees #
This module implements a type RBMap α β cmp
which is a functional data structure for
storing a key-value store in a binary search tree.
It is built on the simpler RBSet α cmp
type, which stores a set of values of type α
using the function cmp : α → α → Ordering
for determining the ordering relation.
The tree will never store two elements that compare .eq
under the cmp
function,
but the function does not have to satisfy cmp x y = .eq → x = y
, and in the map case
α
is a key-value pair and the cmp
function only compares the keys.
In a red-black tree, every node has a color which is either "red" or "black" (this particular choice of colors is conventional). A nil node is considered black.
- red : RBColor
A red node is required to have black children.
- black : RBColor
Every path from the root to a leaf must pass through the same number of black nodes.
Instances For
Equations
- Batteries.instReprRBColor = { reprPrec := Batteries.reprRBColor✝ }
A red-black tree. (This is an internal implementation detail of the RBSet
type,
which includes the invariants of the tree.) This is a binary search tree augmented with
a "color" field which is either red or black for each node and used to implement
the re-balancing operations.
See: Red–black tree
- nil
{α : Type u}
: RBNode α
An empty tree.
- node {α : Type u} (c : RBColor) (l : RBNode α) (v : α) (r : RBNode α) : RBNode α
Instances For
Equations
- Batteries.instReprRBNode = { reprPrec := Batteries.reprRBNode✝ }
Equations
- Batteries.RBNode.instEmptyCollection = { emptyCollection := Batteries.RBNode.nil }
Fold a function in tree order along the nodes. v₀
is used at nil
nodes and
f
is used to combine results at branching nodes.
Equations
Instances For
Fold a function on the values from left to right (in increasing order).
Equations
Instances For
Fold a function on the values from right to left (in decreasing order).
Equations
Instances For
Equations
- Batteries.RBNode.instForIn = { forIn := fun {β : Type ?u.23} [Monad m] => Batteries.RBNode.forIn }
An auxiliary data structure (an iterator) over an RBNode
which lazily
pulls elements from the left.
- nil
{α : Type u_1}
: RBNode.Stream α
The stream is empty.
- cons
{α : Type u_1}
(v : α)
(r : RBNode α)
(tail : RBNode.Stream α)
: RBNode.Stream α
We are ready to deliver element
v
with right childr
, and wheretail
represents all the subtrees we have yet to destructure.
Instances For
O(log n)
. Turn a node into a stream, by descending along the left spine.
Equations
Instances For
O(1)
amortized, O(log n)
worst case: Get the next element from the stream.
Equations
Instances For
Fold a function on the values from left to right (in increasing order).
Equations
Instances For
Fold a function on the values from right to left (in decreasing order).
Equations
Instances For
O(n)
. Convert the stream to a list in ascending order.
Instances For
Equations
- Batteries.RBNode.instToStreamStream = { toStream := fun (x : Batteries.RBNode α) => x.toStream }
Equations
Returns true
iff every element of the tree satisfies p
.
Equations
Instances For
Returns true
iff any element of the tree satisfies p
.
Equations
Instances For
Asserts that p
holds on every element of the tree.
Equations
Instances For
Asserts that p
holds on some element of the tree.
Equations
Instances For
True if x
is an element of t
"exactly", i.e. up to equality, not the cmp
relation.
Instances For
Equations
- Batteries.RBNode.instMembership = { mem := fun (t : Batteries.RBNode α) (x : α) => Batteries.RBNode.EMem x t }
True if the specified cut
matches at least one element of of t
.
Instances For
True if x
is equivalent to an element of t
.
Instances For
Equations
- Batteries.RBNode.Slow.instDecidableEMem = inferInstanceAs (Decidable (Batteries.RBNode.Any (fun (x_1 : α) => x = x_1) t))
Instances For
Equations
- Batteries.RBNode.Slow.instDecidableMemP = inferInstanceAs (Decidable (Batteries.RBNode.Any (fun (x : α) => cut x = Ordering.eq) t))
Instances For
Equations
- Batteries.RBNode.Slow.instDecidableMem = inferInstanceAs (Decidable (Batteries.RBNode.Any (fun (x_1 : α) => cmp x x_1 = Ordering.eq) t))
Instances For
Asserts that t₁
and t₂
have the same number of elements in the same order,
and R
holds pairwise between them. The tree structure is ignored.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Batteries.RBNode.instBEq = { beq := fun (a b : Batteries.RBNode α) => Batteries.RBNode.all₂ (fun (x1 x2 : α) => x1 == x2) a b }
We say that x < y
under the comparator cmp
if cmp x y = .lt
.
- In order to avoid assuming the comparator is always lawful, we use a
local
∀ [TransCmp cmp]
binder in the relation so that the ordering properties of the tree only need to hold if the comparator is lawful. - The
Nonempty
wrapper is a no-op because this is already a proposition, but it prevents the[TransCmp cmp]
binder from being introduced when we don't want it.
Equations
Instances For
O(n)
. Verifies an ordering relation on the nodes of the tree.
Equations
- Batteries.RBNode.isOrdered cmp Batteries.RBNode.nil (some l_2) (some r_2) = decide (cmp l_2 r_2 = Ordering.lt)
- Batteries.RBNode.isOrdered cmp Batteries.RBNode.nil l r = true
- Batteries.RBNode.isOrdered cmp (Batteries.RBNode.node a a_1 a_2 a_3) l r = (Batteries.RBNode.isOrdered cmp a_1 l (some a_2) && Batteries.RBNode.isOrdered cmp a_3 (some a_2) r)
Instances For
The first half of Okasaki's balance
, concerning red-red sequences in the left child.
Equations
- One or more equations did not get rendered due to their size.
- x✝².balance1 x✝¹ x✝ = Batteries.RBNode.node Batteries.RBColor.black x✝² x✝¹ x✝
Instances For
The second half of Okasaki's balance
, concerning red-red sequences in the right child.
Equations
- One or more equations did not get rendered due to their size.
- x✝².balance2 x✝¹ x✝ = Batteries.RBNode.node Batteries.RBColor.black x✝² x✝¹ x✝
Instances For
O(n)
. Reverses the ordering of the tree without any rebalancing.
Equations
Instances For
The core of the insert
function. This adds an element x
to a balanced red-black tree.
Importantly, the result of calling ins
is not a proper red-black tree,
because it has a broken balance invariant.
(See Balanced.ins
for the balance invariant of ins
.)
The insert
function does the final fixup needed to restore the invariant.
Equations
Instances For
insert cmp t v
inserts element v
into the tree, using the provided comparator
cmp
to put it in the right place and automatically rebalancing the tree as necessary.
Equations
Instances For
Rebalancing a tree which has shrunk on the left.
Equations
- One or more equations did not get rendered due to their size.
- (Batteries.RBNode.node Batteries.RBColor.red a x b).balLeft v r = Batteries.RBNode.node Batteries.RBColor.red (Batteries.RBNode.node Batteries.RBColor.black a x b) v r
- l.balLeft v (Batteries.RBNode.node Batteries.RBColor.black a y b) = l.balance2 v (Batteries.RBNode.node Batteries.RBColor.red a y b)
- l.balLeft v r = Batteries.RBNode.node Batteries.RBColor.red l v r
Instances For
Rebalancing a tree which has shrunk on the right.
Equations
- One or more equations did not get rendered due to their size.
- l.balRight v (Batteries.RBNode.node Batteries.RBColor.red a x b) = Batteries.RBNode.node Batteries.RBColor.red l v (Batteries.RBNode.node Batteries.RBColor.black a x b)
- (Batteries.RBNode.node Batteries.RBColor.black a x_1 b).balRight v r = (Batteries.RBNode.node Batteries.RBColor.red a x_1 b).balance1 v r
- l.balRight v r = Batteries.RBNode.node Batteries.RBColor.red l v r
Instances For
Concatenate two trees with the same black-height.
Equations
Instances For
erase #
The erase cut t
function removes an element from the tree t
.
The cut
function is used to locate an element in the tree:
it returns .gt
if we go too high and .lt
if we go too low;
if it returns .eq
we will remove the element.
(The function cmp k
for some key k
is a valid cut function, but we can also use cuts that
are not of this form as long as they are suitably monotonic.)
Instances For
Finds an element in the tree satisfying the cut
function.
Equations
Instances For
upperBound? cut
retrieves the smallest entry larger than or equal to cut
, if it exists.
Equations
Instances For
lowerBound? cut
retrieves the largest entry smaller than or equal to cut
, if it exists.
Equations
Instances For
O(n)
. Map a function on every value in the tree.
This requires IsMonotone
on the function in order to preserve the order invariant.
Equations
Instances For
A RBNode.Path α
is a "cursor" into an RBNode
which represents the path
from the root to a subtree. Note that the path goes from the target subtree
up to the root, which is reversed from the normal way data is stored in the tree.
See Zipper for more information.
- root
{α : Type u}
: Path α
The root of the tree, which is the end of the path of parents.
- left
{α : Type u}
(c : RBColor)
(parent : Path α)
(v : α)
(r : RBNode α)
: Path α
A path that goes down the left subtree.
- right
{α : Type u}
(c : RBColor)
(l : RBNode α)
(v : α)
(parent : Path α)
: Path α
A path that goes down the right subtree.
Instances For
Like find?
, but instead of just returning the element, it returns the entire subtree
at the element and a path back to the root for reconstructing the tree.
Equations
Instances For
This function does the second part of RBNode.ins
,
which unwinds the stack and rebuilds the tree.
Equations
- Batteries.RBNode.Path.root.ins x✝ = x✝.setBlack
- (Batteries.RBNode.Path.left Batteries.RBColor.red parent y b).ins x✝ = parent.ins (Batteries.RBNode.node Batteries.RBColor.red x✝ y b)
- (Batteries.RBNode.Path.right Batteries.RBColor.red a y parent).ins x✝ = parent.ins (Batteries.RBNode.node Batteries.RBColor.red a y x✝)
- (Batteries.RBNode.Path.left Batteries.RBColor.black parent y b).ins x✝ = parent.ins (x✝.balance1 y b)
- (Batteries.RBNode.Path.right Batteries.RBColor.black a y parent).ins x✝ = parent.ins (a.balance2 y x✝)
Instances For
path.del t c
does the second part of RBNode.del
, which unwinds the stack
and rebuilds the tree. The c
argument is the color of the node before the deletion
(we used t₀.isBlack
for this in RBNode.del
but the original tree is no longer
available in this formulation).
Equations
- Batteries.RBNode.Path.root.del x✝¹ x✝ = x✝¹.setBlack
- (Batteries.RBNode.Path.left c parent y b).del x✝ Batteries.RBColor.red = parent.del (Batteries.RBNode.node Batteries.RBColor.red x✝ y b) c
- (Batteries.RBNode.Path.right c a y parent).del x✝ Batteries.RBColor.red = parent.del (Batteries.RBNode.node Batteries.RBColor.red a y x✝) c
- (Batteries.RBNode.Path.left c parent y b).del x✝ Batteries.RBColor.black = parent.del (x✝.balLeft y b) c
- (Batteries.RBNode.Path.right c a y parent).del x✝ Batteries.RBColor.black = parent.del (a.balRight y x✝) c
Instances For
modify cut f t
uses cut
to find an element,
then modifies the element using f
and reinserts it into the tree.
Because the tree structure is not modified,
f
must not modify the ordering properties of the element.
The element in t
is used linearly if t
is unshared.
Equations
- One or more equations did not get rendered due to their size.
Instances For
alter cut f t
simultaneously handles inserting, erasing and replacing an element
using a function f : Option α → Option α
. It is passed the result of t.find? cut
and can either return none
to remove the element or some a
to replace/insert
the element with a
(which must have the same ordering properties as the original element).
The element is used linearly if t
is unshared.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ordering invariant of a red-black tree, which is a binary search tree.
This says that every element of a left subtree is less than the root, and
every element in the right subtree is greater than the root, where the
less than relation x < y
is understood to mean cmp x y = .lt
.
Because we do not assume that cmp
is lawful when stating this property,
we write it in such a way that if cmp
is not lawful then the condition holds trivially.
That way we can prove the ordering invariants without assuming cmp
is lawful.
Equations
Instances For
Equations
Instances For
The red-black balance invariant. Balanced t c n
says that the color of the root node is c
,
and the black-height (the number of black nodes on any path from the root) of the tree is n
.
Additionally, every red node must have black children.
- nil
{α : Type u_1}
: nil.Balanced RBColor.black 0
A nil node is balanced with black-height 0, and it is considered black.
- red
{α : Type u_1}
{x : RBNode α}
{n : Nat}
{y : RBNode α}
{v : α}
: x.Balanced RBColor.black n → y.Balanced RBColor.black n → (node RBColor.red x v y).Balanced RBColor.red n
A red node is balanced with black-height
n
if its children are both black with with black-heightn
. - black
{α : Type u_1}
{x : RBNode α}
{c₁ : RBColor}
{n : Nat}
{y : RBNode α}
{c₂ : RBColor}
{v : α}
: x.Balanced c₁ n → y.Balanced c₂ n → (node RBColor.black x v y).Balanced RBColor.black (n + 1)
A black node is balanced with black-height
n + 1
if its children both have black-heightn
.
Instances For
The well-formedness invariant for a red-black tree. The first constructor is the real invariant,
and the others allow us to "cheat" in this file and define insert
and erase
,
which have more complex proofs that are delayed to Batteries.Data.RBMap.Lemmas
.
- mk
{α : Type u_1}
{cmp : α → α → Ordering}
{t : RBNode α}
{c : RBColor}
{n : Nat}
: Ordered cmp t → t.Balanced c n → WF cmp t
The actual well-formedness invariant: a red-black tree has the ordering and balance invariants.
- insert {α : Type u_1} {cmp : α → α → Ordering} {t : RBNode α} {a : α} : WF cmp t → WF cmp (RBNode.insert cmp t a)
- erase {α : Type u_1} {cmp : α → α → Ordering} {t : RBNode α} {cut : α → Ordering} : WF cmp t → WF cmp (RBNode.erase cut t)
Instances For
An RBSet
is a self-balancing binary search tree.
The cmp
function is the comparator that will be used for performing searches;
it should satisfy the requirements of TransCmp
for it to have sensible behavior.
Instances For
O(1)
. Construct a new empty tree.
Instances For
O(1)
. Construct a new empty tree.
Equations
Instances For
O(1)
. Construct a new tree with one element v
.
Equations
Instances For
O(n)
. Fold a function on the values from left to right (in increasing order).
Instances For
O(n)
. Fold a function on the values from right to left (in decreasing order).
Instances For
Equations
- Batteries.RBSet.instForIn = { forIn := fun {β : Type ?u.35} [Monad m] (t : Batteries.RBSet α cmp) => t.val.forIn }
Equations
- Batteries.RBSet.instToStreamStream = { toStream := fun (x : Batteries.RBSet α cmp) => x.val.toStream }
O(1)
. Is the tree empty?
Instances For
Equations
- Batteries.RBSet.instRepr = { reprPrec := fun (m : Batteries.RBSet α cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "RBSet.ofList " ++ repr m.toList) prec }
O(log n)
. Insert element v
into the tree.
Equations
Instances For
O(log n)
. Remove an element from the tree using a cut function.
The cut
function is used to locate an element in the tree:
it returns .gt
if we go too high and .lt
if we go too low;
if it returns .eq
we will remove the element.
(The function cmp k
for some key k
is a valid cut function, but we can also use cuts that
are not of this form as long as they are suitably monotonic.)
Equations
Instances For
O(log n)
. upperBoundP cut
retrieves the smallest entry comparing gt
or eq
under cut
,
if it exists. If multiple keys in the map return eq
under cut
, any of them may be returned.
Instances For
O(log n)
. upperBound? k
retrieves the largest entry smaller than or equal to k
,
if it exists.
Equations
Instances For
O(log n)
. lowerBoundP cut
retrieves the largest entry comparing lt
or eq
under cut
,
if it exists. If multiple keys in the map return eq
under cut
, any of them may be returned.
Instances For
O(log n)
. lowerBound? k
retrieves the largest entry smaller than or equal to k
,
if it exists.
Equations
Instances For
O(n log n)
. Build a tree from an unsorted list by inserting them one at a time.
Equations
- Batteries.RBSet.ofList l cmp = List.foldl (fun (r : Batteries.RBSet α cmp) (p : α) => r.insert p) (Batteries.mkRBSet α cmp) l
Instances For
O(n log n)
. Build a tree from an unsorted array by inserting them one at a time.
Equations
Instances For
Asserts that t₁
and t₂
have the same number of elements in the same order,
and R
holds pairwise between them. The tree structure is ignored.
Instances For
True if x
is an element of t
"exactly", i.e. up to equality, not the cmp
relation.
Instances For
True if the specified cut
matches at least one element of of t
.
Instances For
True if x
is equivalent to an element of t
.
Instances For
Equations
- Batteries.RBSet.instMembership = { mem := fun (t : Batteries.RBSet α cmp) (x : α) => Batteries.RBSet.Mem x t }
Equations
- Batteries.RBSet.Slow.instDecidableEMem = inferInstanceAs (Decidable (Batteries.RBNode.Any (fun (x_1 : α) => x = x_1) t.val))
Instances For
Equations
- Batteries.RBSet.Slow.instDecidableMemP = inferInstanceAs (Decidable (Batteries.RBNode.Any (fun (x : α) => cut x = Ordering.eq) t.val))
Instances For
Equations
- Batteries.RBSet.Slow.instDecidableMem = inferInstanceAs (Decidable (Batteries.RBNode.Any (fun (x_1 : α) => cmp x x_1 = Ordering.eq) t.val))
Instances For
Returns true if t₁
and t₂
are equal as sets (assuming cmp
and ==
are compatible),
ignoring the internal tree structure.
Equations
- Batteries.RBSet.instBEq = { beq := fun (a b : Batteries.RBSet α cmp) => Batteries.RBSet.all₂ (fun (x1 x2 : α) => x1 == x2) a b }
O(log n)
. Returns the minimum element of the tree, or panics if the tree is empty.
Equations
Instances For
O(log n)
. Returns the maximum element of the tree, or panics if the tree is empty.
Equations
Instances For
O(log n)
. Attempts to find the value with key k : α
in t
and panics if there is no such key.
Equations
- t.findP! cut = (t.findP? cut).getD (panicWithPosWithDecl "Batteries.Data.RBMap.Basic" "Batteries.RBSet.findP!" 801 23 "key is not in the tree")
Instances For
O(log n)
. Attempts to find the value with key k : α
in t
and panics if there is no such key.
Equations
Instances For
O(log n)
. In-place replace an element found by cut
.
This takes the element out of the tree while f
runs,
so it uses the element linearly if t
is unshared.
The ModifyWF
assumption is required because f
may change
the ordering properties of the element, which would break the invariants.
Equations
Instances For
O(log n)
. alterP cut f t
simultaneously handles inserting, erasing and replacing an element
using a function f : Option α → Option α
. It is passed the result of t.findP? cut
and can either return none
to remove the element or some a
to replace/insert
the element with a
(which must have the same ordering properties as the original element).
The element is used linearly if t
is unshared.
The AlterWF
assumption is required because f
may change
the ordering properties of the element, which would break the invariants.
Equations
Instances For
O(n₂ * log (n₁ + n₂))
. Merges the maps t₁
and t₂
.
If equal keys exist in both, the key from t₂
is preferred.
Instances For
Equations
- Batteries.RBSet.instUnion = { union := Batteries.RBSet.union }
O(n₂ * log (n₁ + n₂))
. Merges the maps t₁
and t₂
. If equal keys exist in both,
then use mergeFn a₁ a₂
to produce the new merged value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
O(n₁ * log (n₁ + n₂))
. Intersects the maps t₁
and t₂
using mergeFn a b
to produce the new value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
O(n * log n)
. Constructs the set of all elements satisfying p
.
Equations
- t.filter p = Batteries.RBSet.foldl (fun (acc : Batteries.RBSet α cmp) (a : α) => bif p a then acc.insert a else acc) ∅ t
Instances For
O(n * log n)
. Map a function on every value in the set.
If the function is monotone, consider using the more efficient RBSet.mapMonotone
instead.
Equations
- t.map f = Batteries.RBSet.foldl (fun (acc : Batteries.RBSet β cmpβ) (a : α) => acc.insert (f a)) ∅ t
Instances For
Equations
- Batteries.RBSet.instSDiff = { sdiff := Batteries.RBSet.sdiff }
An RBMap
is a self-balancing binary search tree, used to store a key-value map.
The cmp
function is the comparator that will be used for performing searches;
it should satisfy the requirements of TransCmp
for it to have sensible behavior.
Instances For
O(1)
. Construct a new empty map.
Instances For
O(1)
. Construct a new empty map.
Equations
- Batteries.RBMap.empty = Batteries.mkRBMap α β cmp
Instances For
O(1)
. Construct a new tree with one key-value pair k, v
.
Instances For
O(n)
. Fold a function on the values from left to right (in increasing order).
Equations
- Batteries.RBMap.foldl f x✝ ⟨t, property⟩ = Batteries.RBNode.foldl (fun (s : σ) (x : α × β) => match x with | (a, b) => f s a b) x✝ t
Instances For
O(n)
. Fold a function on the values from right to left (in decreasing order).
Equations
- Batteries.RBMap.foldr f x✝ ⟨t, property⟩ = Batteries.RBNode.foldr (fun (x : α × β) (s : σ) => match x with | (a, b) => f a b s) t x✝
Instances For
O(n)
. Fold a monadic function on the values from left to right (in increasing order).
Equations
- Batteries.RBMap.foldlM f x✝ ⟨t, property⟩ = Batteries.RBNode.foldlM (fun (s : σ) (x : α × β) => match x with | (a, b) => f s a b) x✝ t
Instances For
O(n)
. Run monadic function f
on each element of the tree (in increasing order).
Equations
- Batteries.RBMap.forM f t = Batteries.RBNode.forM (fun (x : α × β) => match x with | (a, b) => f a b) t.val
Instances For
Equations
- Batteries.RBMap.instForInProd = inferInstanceAs (ForIn m (Batteries.RBSet (α × β) (Ordering.byKey Prod.fst cmp)) (α × β))
Equations
An "iterator" over the keys of the map. This is a trivial wrapper over the underlying map,
but it comes with a small API to use it in a for
loop or convert it to an array or list.
Instances For
Equations
Equations
Equations
- Batteries.RBMap.instForMKeys = { forM := fun [Monad m] (t : Batteries.RBMap.Keys α β cmp) (f : α → m PUnit) => Batteries.RBNode.forM (fun (x : α × β) => f x.fst) t.val }
O(1)
amortized, O(log n)
worst case: Get the next element from the stream.
Equations
Instances For
Equations
- Batteries.RBMap.instToStreamKeysStream = { toStream := Batteries.RBMap.Keys.toStream }
Equations
O(n)
. Constructs the array of values of the map.
Equations
- t.valuesArray = Batteries.RBNode.foldl (fun (x1 : Array β) (x2 : α × β) => x1.push x2.snd) #[] t.val
Instances For
O(n)
. Constructs the list of values of the map.
Equations
- t.valuesList = Batteries.RBNode.foldr (fun (x1 : α × β) (x2 : List β) => x1.snd :: x2) t.val []
Instances For
An "iterator" over the values of the map. This is a trivial wrapper over the underlying map,
but it comes with a small API to use it in a for
loop or convert it to an array or list.
Instances For
Equations
Equations
Equations
- Batteries.RBMap.instForMValues = { forM := fun [Monad m] (t : Batteries.RBMap.Values α β cmp) (f : β → m PUnit) => Batteries.RBNode.forM (fun (x : α × β) => f x.snd) t.val }
O(1)
amortized, O(log n)
worst case: Get the next element from the stream.
Equations
Instances For
Equations
- Batteries.RBMap.instToStreamValuesStream = { toStream := Batteries.RBMap.Values.toStream }
Equations
O(1)
. Is the tree empty?
Instances For
O(n)
. Convert the tree to a list in ascending order.
Instances For
O(log n)
. Returns the key-value pair (a, b)
such that a ≤ k
for all keys in the RBMap.
Equations
Instances For
O(log n)
. Returns the key-value pair (a, b)
such that a ≥ k
for all keys in the RBMap.
Equations
Instances For
Equations
- Batteries.RBMap.instRepr = { reprPrec := fun (m : Batteries.RBMap α β cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "RBMap.ofList " ++ repr m.toList) prec }
O(log n)
. Find an entry in the tree with key equal to k
.
Equations
- t.findEntry? k = Batteries.RBSet.findP? t fun (x : α × β) => cmp k x.fst
Instances For
O(log n)
. Find the value corresponding to key k
.
Equations
- t.find? k = Option.map (fun (x : α × β) => x.snd) (t.findEntry? k)
Instances For
O(log n)
. lowerBound? k
retrieves the key-value pair of the largest key
smaller than or equal to k
, if it exists.
Equations
- t.lowerBound? k = Batteries.RBSet.lowerBoundP? t fun (x : α × β) => cmp k x.fst
Instances For
O(log n)
. Returns true if the given key a
is in the RBMap.
Equations
Instances For
Asserts that t₁
and t₂
have the same number of elements in the same order,
and R
holds pairwise between them. The tree structure is ignored.
Instances For
Asserts that t₁
and t₂
have the same set of keys (up to equality).
Equations
- t₁.eqKeys t₂ = Batteries.RBMap.all₂ (fun (x1 : α × β) (x2 : α × γ) => decide (cmp x1.fst x2.fst = Ordering.eq)) t₁ t₂
Instances For
Returns true if t₁
and t₂
have the same keys and values
(assuming cmp
and ==
are compatible), ignoring the internal tree structure.
Equations
- Batteries.RBMap.instBEq = inferInstanceAs (BEq (Batteries.RBSet (α × β) (Ordering.byKey Prod.fst cmp)))
O(n)
. The number of items in the RBMap.
Equations
Instances For
O(n₂ * log (n₁ + n₂))
. Merges the maps t₁
and t₂
, if a key a : α
exists in both,
then use mergeFn a b₁ b₂
to produce the new merged value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
O(n₁ * log (n₁ + n₂))
. Intersects the maps t₁
and t₂
using mergeFn a b
to produce the new value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
O(n * log n)
. Constructs the set of all elements satisfying p
.
Equations
- t.filter p = Batteries.RBSet.filter t fun (x : α × β) => match x with | (a, b) => p a b
Instances For
O(n log n)
. Build a tree from an unsorted list by inserting them one at a time.