nspec - 0.1.3

Stdlib.Data.Set.AVL

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

type AVLTree (A : Type)Source#

A self-balancing binary search tree.

Constructors

| 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.

Constructors

| 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.

balance {A} (set : AVLTree A) : AVLTree ASource#

𝒪(1). Applies local rotations if needed.

isBalanced {A} : (set : AVLTree A) -> BoolSource#

𝒪(𝓃). Checks the AVLTree height invariant. I.e. that every two children do not differ on height by more than 1.

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`.

lookupMin {A} : (set : AVLTree A) -> Maybe ASource#

𝒪(log 𝓃). Returns the minimum element of `set`.

lookupMax {A} : (set : AVLTree A) -> Maybe ASource#

𝒪(log 𝓃). Returns the maximum element of `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.

isEmpty {A} (set : AVLTree A) : BoolSource#

𝒪(1). Checks if `set` is empty.

size {A} : (set : AVLTree A) -> NatSource#

𝒪(𝓃). Returns the number of elements of `set`.

foldr {A B} (fun : A -> B -> B) (acc : B) : (set : AVLTree A) -> BSource#

foldl {A B} (fun : B -> A -> B) (acc : B) : (set : AVLTree A) -> BSource#

toList {A} (set : AVLTree A) : List ASource#

𝒪(n). Returns the elements of `set` in ascending order.

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`.

singleton {A} (elem : A) : AVLTree ASource#

𝒪(1). Creates a set with a single element `elem`.

isSubset {A} {{Ord A}} (set1 set2 : AVLTree A) : BoolSource#

𝒪(n log n). Checks if all elements of `set1` are in `set2`.

map {A B} {{Ord B}} (fun : A -> B) (set : AVLTree A) : AVLTree BSource#

prettyDebug {A} {{Show A}} (set : AVLTree A) : StringSource#

Formats the set in a debug friendly format.

toTree {A} : (set : AVLTree A) -> Maybe (Tree A)Source#

𝒪(𝓃).

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#