Data.RRBVector1.Unsized.Internal

Linear RRB Vector Internals

Definitions

Shift : Type

Totality: total
Visibility: public export

blockshift : Shift

  The number of bits used per level.

Totality: total
Visibility: export

blocksize : Nat

  The maximum size of a block.

Totality: total
Visibility: export

blockmask : Nat

  The mask used to extract the index into the array.

Totality: total
Visibility: export

up : Shift -> Shift

Totality: total
Visibility: export

down : Shift -> Shift

Totality: total
Visibility: export

radixIndex : Nat -> Shift -> Nat

Totality: total
Visibility: export

relaxedRadixIndex : IArray n Nat -> Nat -> Shift -> (Nat, Nat)

Totality: total
Visibility: export

data Tree1 : Type -> Type -> Type

  A linear internal tree representation.

Totality: total
Visibility: public export
Constructors:

Balanced : (bsize : Nat ** MArray s bsize (Tree1 s a)) -> Tree1 s a

Unbalanced : (usize : Nat ** MArray s usize (Tree1 s a)) -> IArray usize Nat -> Tree1 s a

Leaf : (lsize : Nat ** MArray s lsize a) -> Tree1 s a

singleton : a -> F1 s (MArray s 1 a)

Totality: total
Visibility: export

singleton' : Tree1 s a -> F1 s (MArray s 1 (Tree1 s a))

Totality: total
Visibility: export

treeToArray : Tree1 s a -> Either (bsize : Nat ** MArray s bsize (Tree1 s a)) (usize : Nat ** MArray s usize (Tree1 s a))

Totality: total
Visibility: export

treeToArray' : Tree1 s a -> (lsize : Nat ** MArray s lsize a)

Totality: total
Visibility: export

treeBalanced : Tree1 s a -> Bool

Totality: total
Visibility: export

treeSize : Shift -> Tree1 s a -> F1 s Nat

  Computes the size of a tree with shift.

Totality: total
Visibility: export

computeSizes : Shift -> MArray s n (Tree1 s a) -> F1 s (Tree1 s a)

  Turns an array into a tree node by computing the sizes of its subtrees.
  sh is the shift of the resulting tree.

Totality: total
Visibility: export

countTrailingZeros : Nat -> Nat

Totality: total
Visibility: export

log2 : Nat -> Nat

  Nat log base 2.

Totality: total
Visibility: export

data RRBVector1 : Type -> Type -> Type

  A linear relaxed radix balanced vector (RRBVector1).
  It supports fast indexing, iteration, concatenation and splitting.

Totality: total
Visibility: public export
Constructors:

Root : Nat -> Shift -> Tree1 s a -> RRBVector1 s a

Empty : RRBVector1 s a