lastAt : IArray (S n) a -> a Read the final element of a known nonempty indexed array.
The bound proof is erased at runtime.
Totality: total
Visibility: exportrecord RelaxedIndex : Nat -> Type The result of locating an element within a relaxed RRB tree node.
`child` identifies the child subtree containing the requested logical
element. Its `Fin count` type guarantees that the child index is valid
for the corresponding node.
`offset` is the element's index relative to the beginning of that child
subtree.
Returning the child position as a bounded index allows subsequent array
access to avoid an additional `Nat`-to-`Fin` conversion.
Totality: total
Visibility: public export
Constructor: MkRelaxedIndex : Fin count -> Nat -> RelaxedIndex count
Projections:
.child : RelaxedIndex count -> Fin count.offset : RelaxedIndex count -> Nat
.child : RelaxedIndex count -> Fin count- Totality: total
Visibility: public export child : RelaxedIndex count -> Fin count- Totality: total
Visibility: public export .offset : RelaxedIndex count -> Nat- Totality: total
Visibility: public export offset : RelaxedIndex count -> Nat- Totality: total
Visibility: public export Shift : Type- Totality: total
Visibility: public export blockshift : Shift The number of bits used per level.
Totality: total
Visibility: exportblocksize : Nat The maximum size of a block.
Totality: total
Visibility: exportblockmask : Nat The mask used to extract the index into the array.
Totality: total
Visibility: exportup : Shift -> Shift- Totality: total
Visibility: export down : Shift -> Shift- Totality: total
Visibility: export radixIndex : Nat -> Shift -> Nat- Totality: total
Visibility: export data Children : Type -> Type A nonempty collection of child nodes for a balanced RRB tree node.
The number of children is existentially quantified by `n`.
The erased proofs guarantee that:
- the node contains at least one child, and
- the number of children does not exceed the RRB branching factor.
Because these invariants are carried in the type, callers can index the
underlying `IArray` using bounded indices without repeatedly recovering
these facts through `tryNatToFin` or other runtime bounds checks.
Totality: total
Visibility: public export
Constructor: MkChildren : {auto 0 _ : LT 0 n} -> {auto 0 _ : LTE n blocksize} -> IArray n (Tree a) -> Children a
data RelaxedChildren : Type -> Type A nonempty collection of child nodes for a relaxed RRB tree node,
together with its cumulative size table.
Both arrays have the same statically tracked length `n`, which guarantees
that every child has a corresponding cumulative-size entry.
The erased proofs additionally guarantee that:
- the node contains at least one child, and
- the number of children does not exceed the RRB branching factor.
Encoding these invariants directly avoids repeatedly converting raw
`Nat` indices with `tryNatToFin` when traversing relaxed nodes.
Totality: total
Visibility: public export
Constructor: MkRelaxedChildren : {auto 0 _ : LT 0 n} -> {auto 0 _ : LTE n blocksize} -> IArray n (Tree a) -> IArray n Nat -> RelaxedChildren a
data Tree : Type -> Type The internal tree representation of an RRB vector.
A tree node is one of:
- `Balanced` -> containing a nonempty bounded array of child nodes whose
positions are determined directly from the radix index.
- `Unbalanced` -> containing a nonempty bounded array of child nodes plus
a cumulative size table used for relaxed indexing.
- `Leaf` -> containing the actual vector elements.
Internal-node invariants such as nonemptiness, maximum branching factor,
and matching child/size-table lengths are encoded by `Children` and
`RelaxedChildren`. This allows traversal code to work with bounded indices
directly rather than repeatedly recovering those invariants at runtime.
Totality: total
Visibility: public export
Constructors:
Balanced : Children a -> Tree aUnbalanced : RelaxedChildren a -> Tree aLeaf : Array a -> Tree a
Hints:
Eq a => Eq (Tree a)Foldable TreeOrd a => Ord (Tree a)Show a => Show (Tree a)
childrenToArray : Children a -> Array (Tree a) Convert a bounded collection of balanced-node children back to the
existential `Array` representation.
This is primarily useful for APIs and utility functions that do not need
to retain the child-count index in their result type.
Totality: total
Visibility: exportrelaxedChildrenToArray : RelaxedChildren a -> Array (Tree a) Convert the child array of a relaxed node back to the existential
`Array` representation.
The corresponding size table has the same statically tracked length, but
is intentionally discarded by this projection.
Totality: total
Visibility: exportrelaxedSizesToArray : RelaxedChildren a -> Array Nat Convert the cumulative size table of a relaxed node back to the
existential `Array` representation.
Totality: total
Visibility: exporttoList : Tree a -> List a- Totality: total
Visibility: export showTreeRep : Show a => Show (Tree a) => Tree a -> String- Totality: total
Visibility: public export singleton : a -> Array a- Totality: total
Visibility: export treeToArray : Tree a -> Array (Tree a)- Totality: total
Visibility: export treeBalanced : Tree a -> Bool- Totality: total
Visibility: export treeSize : Shift -> Tree a -> Nat Computes the size of a tree with shift.
Totality: total
Visibility: exportrelaxedRadixIndex : {auto 0 _ : LT 0 n} -> IArray n Nat -> Nat -> Shift -> RelaxedIndex n Locate the child subtree containing a logical index in a relaxed node.
The size table contains cumulative subtree sizes and has exactly `n`
entries, one for each child in the corresponding relaxed node.
The radix-derived initial guess is a lower bound on the actual child
position. The search advances through the cumulative size table until it
finds the first entry greater than `i`.
The returned `RelaxedIndex` carries the selected child as `Fin n`, so the
caller can index the corresponding child array directly without performing
another `Nat`-to-`Fin` conversion.
For a well-formed relaxed node and a logical index belonging to that node:
- the initial radix guess is strictly smaller than the number of children
- whenever the current cumulative size does not contain `i`, another size
entry exists.
These structural invariants are supplied as erased proofs and therefore
introduce no runtime bounds checks.
Totality: total
Visibility: exportcomputeSizes : Shift -> Children a -> Tree a Turns a valid collection of child nodes into an internal tree node.
If every non-final child is a full subtree and the final child is
balanced, the resulting node is represented as `Balanced`.
Otherwise, a cumulative size table with exactly the same statically
tracked length as the child array is constructed and the node is
represented as `Unbalanced`.
Totality: total
Visibility: exportcountTrailingZeros : Nat -> Nat Count the number of consecutive zero bits beginning at the least
significant bit of a natural number.
Bit positions are traversed from least significant to most significant.
The `Ix` witness carries the current valid bit position within the fixed
width of `Int`, so no `tryNatToFin` conversion is required.
If no set bit is found, the full bit width of `Int` is returned.
Totality: total
Visibility: exportlog2 : Nat -> Nat Compute the base-2 logarithm of a natural number, rounded down.
The implementation scans the fixed-width `Int` representation from the
most significant bit toward the least significant bit and returns the
position of the first set bit.
The recursive `LTE remaining (bitSizeOf Int)` proof guarantees that every
tested bit position is valid. The proof is erased, and conversion to
`Fin (bitSizeOf Int)` therefore requires no dynamic `Nat`-to-`Fin`
bounds check.
`log2 0` is defined as `0`.
Totality: total
Visibility: exportdata RRBVector : Type -> Type A relaxed radix balanced vector (RRBVector).
It supports fast indexing, iteration, concatenation and splitting.
Totality: total
Visibility: public export
Constructors:
Root : Nat -> Shift -> Tree a -> RRBVector aEmpty : RRBVector a
Hints:
Applicative RRBVectorEq a => Eq (RRBVector a)Foldable RRBVectorFunctor RRBVectorMonad RRBVectorSemigroup (RRBVector a) => Monoid (RRBVector a)Ord a => Ord (RRBVector a)Semigroup (RRBVector a)Show {arg:11028} => Show (RRBVector {arg:11028})