Stdlib.Data.Set

Contents

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 Set (A : Type)Source #

A self-balancing AVL binary search tree.

Constructors

\| empty	An empty AVL tree.
\| node@{ element : A; height : Nat; left : Set A; right : Set A; }	A node of an AVL tree.

module InternalSource #

height {A} (set : Set A) : NatSource #

𝒪(1) Retrieves the height of an Set. The height is the distance from the root to the deepest child.

unsafeMap {A B} (f : A -> B) (set : Set A) : Set BSource #

𝒪(n). Maps a function over an Set. 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.

type BalanceFactorSource #

Constructors

\| LeanLeft	Left child is higher.
\| LeanNone	Equal heights of children.
\| LeanRight	Right child is higher.

diffFactor {A} (set : Set A) : IntSource #

balanceFactor' {A} (left right : Set A) : BalanceFactorSource #

balanceFactor {A} (set : Set 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 : Set A) (right : Set A) : Set ASource #

𝒪(1). Helper function for creating a node.

rotateLeft {A} (set : Set A) : Set ASource #

𝒪(1). Left rotation.

rotateRight {A} (set : Set A) : Set ASource #

𝒪(1). Right rotation.

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

𝒪(1). Applies local rotations if needed.

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

𝒪(𝓃). Checks the Set 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 : Set 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 : Set A) : Maybe ASource #

𝒪(log 𝓃). Queries whether `elem` is in `set`.

isMember {A} {{Ord A}} (elem : A) (set : Set A) : BoolSource #

𝒪(log 𝓃). Queries whether `elem` is in `set`.

insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (set : Set A) : Set 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 : Set A) : Set ASource #

𝒪(log 𝓃). Inserts `elem` into `set`.

deleteMin {A} {{Ord A}} : (set : Set A) -> Maybe (Pair A (Set A))Source #

𝒪(log 𝓃). Removes the minimum element from `set`.

deleteWith {A B} {{orderA : Ord A}} {{orderB : Ord B}} (fun : A -> B) (elem : B) (set : Set A) : Set 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 : Set A) : Set ASource #

𝒪(log 𝓃). Removes `elem` from `set`.

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

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

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

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

deleteMany {A} {{Ord A}} (toDelete : List A) (set : Set A) : Set ASource #

𝒪(𝒹 log 𝓃). Deletes elements from `set`.

deleteManyWith {A B} {{Ord A}} {{Ord B}} (fun : A -> B) (toDelete : List B) (set : Set A) : Set 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) : Set ASource #

𝒪(𝓃 log 𝓃). Create a set from an unsorted List.

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

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

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

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

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

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

instance polymorphicFoldableSetI : Polymorphic.Foldable SetSource #

instance foldableSetI {A} : Foldable (Set A) ASource #

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

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

intersection {A} {{Ord A}} (set1 set2 : Set A) : Set ASource #

𝒪(n log n). Returns a set containing the elements that are members of `set1` and `set2`.

difference {A} {{Ord A}} (set1 set2 : Set A) : Set 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 : Set A) : Set 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 : Set A) : Set 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 (Set Elem)}} (sets : Container) : Set 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 : Set A) : Result A (Set 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 : Set A) : BoolSource #