Description
AVL trees are a type of self-balancing binary search tree, where the heights of the left and right subtrees of every node differ by at most 1. This ensures that the height of the tree is logarithmic in the number of nodes, which guarantees efficient insertion, deletion, and search operations (all are guaranteed to run in 𝒪(log 𝓃) time). This module defines an AVL tree data type and provides functions for constructing, modifying, and querying AVL trees.
Definitions
| empty | An empty AVL tree. |
| node@{ element : A; height : Nat; left : AVLTree A; right : AVLTree A; } | A node of an AVL tree. |
height {A} (set : AVLTree A) : NatSource#
𝒪(1) Retrieves the height of an AVLTree. The height is the distance from the root to the deepest child.
unsafeMap {A B} (f : A -> B) (set : AVLTree A) : AVLTree BSource#
𝒪(n). Maps a function over an AVLTree. Does not check if after mapping the order of the elements is preserved. It is the responsibility of the caller to ensure that `f` preserves the ordering.
| LeanLeft | Left child is higher. |
| LeanNone | Equal heights of children. |
| LeanRight | Right child is higher. |
balanceFactor {A} (set : AVLTree A) : BalanceFactorSource#
𝒪(1). Computes the balance factor, i.e., the height of the right subtree minus the height of the left subtree.
mkNode {A} (value : A) (left : AVLTree A) (right : AVLTree A) : AVLTree ASource#
𝒪(1). Helper function for creating a node.
rotateLeft {A} (set : AVLTree A) : AVLTree ASource#
𝒪(1). Left rotation.
rotateRight {A} (set : AVLTree A) : AVLTree ASource#
𝒪(1). Right rotation.
lookupWith {A K} {{order : Ord K}} (fun : A -> K) (elem : K) (set : AVLTree A) : Maybe ASource#
𝒪(log 𝓃). Lookup a member from the set using a projection function. Ord A, Ord K and fun must be compatible. i.e cmp_k (fun a1) (fun a2) == cmp_a a1 a2
lookup {A} {{Ord A}} (elem : A) (set : AVLTree A) : Maybe ASource#
𝒪(log 𝓃). Queries whether `elem` is in `set`.
isMember {A} {{Ord A}} (elem : A) (set : AVLTree A) : BoolSource#
𝒪(log 𝓃). Queries whether `elem` is in `set`.
insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (set : AVLTree A) : AVLTree ASource#
𝒪(log 𝓃). Inserts an element `elem` into `set` using a function to deduplicate entries. Assumption: If a1 == a2 then fun a1 a2 == a1 == a2 where == comes from Ord a.
insert {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree ASource#
𝒪(log 𝓃). Inserts `elem` into `set`.
deleteMin {A} {{Ord A}} : (set : AVLTree A) -> Maybe (Pair A (AVLTree A))Source#
𝒪(log 𝓃). Removes the minimum element from `set`.
deleteWith {A B} {{orderA : Ord A}} {{orderB : Ord B}} (fun : A -> B) (elem : B) (set : AVLTree A) : AVLTree ASource#
𝒪(log 𝓃). Removes an element `elem` from `set` based on a projected comparison value. Assumption Ord A and Ord B are compatible: Given a1 a2, A then (fun a1 == fun a2) == (a1 == a2)
delete {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree ASource#
𝒪(log 𝓃). Removes `elem` from `set`.
deleteMany {A} {{Ord A}} (toDelete : List A) (set : AVLTree A) : AVLTree ASource#
𝒪(𝒹 log 𝓃). Deletes elements from `set`.
deleteManyWith {A B} {{Ord A}} {{Ord B}} (fun : A -> B) (toDelete : List B) (set : AVLTree A) : AVLTree ASource#
𝒪(𝒹 log 𝓃). Deletes elements from `set` based on a projected comparison value. Assumption: Ord A and Ord B are compatible, i.e., for a1 a2 in A, we have (fun a1 == fun a2) == (a1 == a2)
fromList {A} {{Ord A}} (list : List A) : AVLTree ASource#
𝒪(𝓃 log 𝓃). Create a set from an unsorted List.
intersection {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree ASource#
𝒪(n log n). Returns a set containing the elements that are members of `set1` and `set2`.
difference {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree ASource#
𝒪(n log n). Returns a set containing the elements that are members of `set1` but not of `set2`.
unionLeft {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree ASource#
𝒪(n log (m + n)). Returns a set containing the elements that are members of `set1` or `set2`. This is a left-biased union of `set1` and `set2` which prefers `set1` when duplicate elements are encountered.
union {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree ASource#
𝒪(min(n,m) log min(n, m)). Returns a set containing the elements that are members of `set1` or `set2`.
unions {Container Elem} {{Ord Elem}} {{Foldable Container (AVLTree Elem)}} (sets : Container) : AVLTree ElemSource#
O(n log n). Returns a set containing the elements that are members of some set in `sets`.
disjointUnion {A} {{Ord A}} (set1 set2 : AVLTree A) : Result A (AVLTree A)Source#
O(n log n). If `set1` and `set2` are disjoint, then returns `ok set` where `set` is the union of `set1` and `set2`. If `set1` and `set2` are not disjoint, then returns `error x` where `x` is a common element.
all {A} (predicate : A -> Bool) (set : AVLTree A) : BoolSource#
𝒪(𝓃). Returns true if all elements of `set` satisfy `predicate`.
any {A} (predicate : A -> Bool) (set : AVLTree A) : BoolSource#
𝒪(𝓃). Returns true if some element of `set` satisfies `predicate`.
filter {A} {{Ord A}} (predicate : A -> Bool) (set : AVLTree A) : AVLTree ASource#
𝒪(n log n). Returns a set containing all elements of `set` that satisfy `predicate`.
partition {A} {{Ord A}} (predicate : A -> Bool) (set : AVLTree A) : Pair (AVLTree A) (AVLTree A)Source#
isSubset {A} {{Ord A}} (set1 set2 : AVLTree A) : BoolSource#
𝒪(n log n). Checks if all elements of `set1` are in `set2`.
prettyDebug {A} {{Show A}} (set : AVLTree A) : StringSource#
Formats the set in a debug friendly format.
pretty {A} {{Show A}} (set : AVLTree A) : StringSource#
Returns the textual representation of an AVLTree.
instance eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A)Source#
instance ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A)Source#