map

Map

data Map (K : Type) (V : Type)

An ordered finite map: a leaf, or a branch with its subtree’s size, an entry and the smaller and larger keys’ subtrees.

Split

data Split (K : Type) (V : Type)

An entry taken out of a tree (its smallest or largest) and the tree that is left.

Map.Entry

def Entry (K : Type) (V : Type) : Type

An entry: a key and its value.

Map.empty

def empty {K : Type} {V : Type} : Map K V

The empty map.

Map.size

def size {K : Type} {V : Type} (m : Map K V) : Nat

The number of entries, in constant time.

Map.singleton

def singleton {K : Type} {V : Type} (k : K) (v : V) : Map K V

The map with one entry.

Map.build

def build {K : Type} {V : Type} (k : K) (v : V) (l : Map K V) (r : Map K V) : Map K V

A branch whose size is computed from its subtrees.

Map.rotateLeft

def rotateLeft {K : Type} {V : Type} (k : K) (v : V) (l : Map K V) (r : Map K V) : Map K V

The branch of k over l and r turned left, when r is too heavy: once if r’s outer side is the heavier one, twice (through r’s inner side) otherwise.

Map.rotateRight

def rotateRight {K : Type} {V : Type} (k : K) (v : V) (l : Map K V) (r : Map K V) : Map K V

The branch of k over l and r turned right, when l is too heavy (the mirror of rotateLeft).

Map.balance

def balance {K : Type} {V : Type} (k : K) (v : V) (l : Map K V) (r : Map K V) : Map K V

The branch of k over l and r after one insertion or deletion, turned when one side outweighs the other three times.

Map.lookup

def lookup {K : Type} {V : Type} {{o : Ord K}} (k : K) (m : Map K V) : Option V

The value at a key, if the key is there.

Map.contains

def contains {K : Type} {V : Type} {{o : Ord K}} (k : K) (m : Map K V) : Bool

Whether a key is there.

Map.getOr

def getOr {K : Type} {V : Type} {{o : Ord K}} (d : V) (k : K) (m : Map K V) : V

The value at a key, or d when the key is not there.

Map.insertWith

def insertWith {K : Type} {V : Type} {{o : Ord K}} (f : V -> V -> V) (k : K) (v : V) (m : Map K V) : Map K V

The map with an entry inserted; when the key is already there, its value becomes f new old.

Map.insert

def insert {K : Type} {V : Type} {{o : Ord K}} (k : K) (v : V) (m : Map K V) : Map K V

The map with an entry inserted, replacing the key’s value if it is already there.

Map.splitMin

def splitMin {K : Type} {V : Type} (k : K) (v : V) (l : Map K V) (r : Map K V) : Split K V

The smallest entry of the branch of k over l and r, and the branch rebalanced without it.

Map.splitMax

def splitMax {K : Type} {V : Type} (k : K) (v : V) (l : Map K V) (r : Map K V) : Split K V

The largest entry of the branch of k over l and r, and the branch rebalanced without it.

Map.join

def join {K : Type} {V : Type} (l : Map K V) (r : Map K V) : Map K V

Two trees joined, every key of l smaller than every key of r: the new root is taken from the larger side.

Map.delete

def delete {K : Type} {V : Type} {{o : Ord K}} (k : K) (m : Map K V) : Map K V

The map without a key (unchanged when the key is not there).

Map.adjust

def adjust {K : Type} {V : Type} {{o : Ord K}} (f : V -> V) (k : K) (m : Map K V) : Map K V

The map with f applied to the value at a key (unchanged when the key is not there).

Map.foldRight

def foldRight {K : Type} {V : Type} {B : Type} (f : K -> V -> B -> B) (z : B) (m : Map K V) : B

The entries folded from the largest key to the smallest: f key value rest.

Map.toList

def toList {K : Type} {V : Type} (m : Map K V) : List (Entry K V)

The entries as key-value pairs, by ascending key.

Map.keys

def keys {K : Type} {V : Type} (m : Map K V) : List K

The keys, ascending.

Map.values

def values {K : Type} {V : Type} (m : Map K V) : List V

The values, by ascending key.

Map.fromList

def fromList {K : Type} {V : Type} {{o : Ord K}} (xs : List (Entry K V)) : Map K V

The map of key-value pairs; of pairs with the same key, the first one wins.

Map.mapValues

def mapValues {K : Type} {V : Type} {W : Type} (f : V -> W) (m : Map K V) : Map K W

The map with f applied to every value; the keys and the shape stay.

Map.unionWith

def unionWith {K : Type} {V : Type} {{o : Ord K}} (f : V -> V -> V) (a : Map K V) (b : Map K V) : Map K V

The entries of both maps; a key in both gets f left right.

Map.depth

def depth {K : Type} {V : Type} (m : Map K V) : Nat

The height of the tree (for tests of the balance).

Map.before

def before {K : Type} {{o : Ord K}} (a : K) (b : K) : Bool

Whether a comes strictly before b.

Map.aboveLow

def aboveLow {K : Type} {{o : Ord K}} (lo : Option K) (k : K) : Bool

Whether a key comes strictly after a lower bound, if there is one.

Map.belowHigh

def belowHigh {K : Type} {{o : Ord K}} (k : K) (hi : Option K) : Bool

Whether a key comes strictly before an upper bound, if there is one.

Map.withinBounds

def withinBounds {K : Type} {{o : Ord K}} (lo : Option K) (k : K) (hi : Option K) : Bool

Whether a key lies strictly between the bounds that are given.

Map.balancedBranch

def balancedBranch {K : Type} {V : Type} (s : Nat) (l : Map K V) (r : Map K V) : Bool

Whether every branch records its size and is balanced (neither side outweighs the other three times).

Map.validWithin

def validWithin {K : Type} {V : Type} {{o : Ord K}} (lo : Option K) (hi : Option K) (m : Map K V) : Bool

Whether a tree is a valid weight-balanced search tree with every key strictly between the bounds that are given.

Map.valid

def valid {K : Type} {V : Type} {{o : Ord K}} (m : Map K V) : Bool

Whether a tree is a valid weight-balanced search tree: sizes recorded, keys ordered, branches balanced (for tests).