Fixed-size non-empty vectors.

Make a vector of the given length and element type. Returns Nothing if the input list does not have the right number of elements. O(n).

Get the elements of the vector as a list, lowest index first.

Length of the vector. O(1)

Proof that the length of this vector is not 0.

The length of the vector as an Int.

Get the element at the given index. O(1)

Get the element at the given index. Raises an exception if the element is not in the vector's domain. O(1)

Insert an element at the given index. O(n).

Insert an element at the given index. Return Nothing if the element is outside the vector bounds. O(n).

Remove the first element of the vector, and return the rest, if any.

Extract a subvector of the given vector.

Take the front (lower-indexes) part of the vector.

Replace a sub-section of a vector with the given sub-vector.

Scope a function to a sub-section of the given vector.

Scope a monadic function to a sub-section of the given vector.

Zip two vectors, potentially changing types. O(n)

Interleave two vectors. The elements of the first vector are at even indexes in the result, the elements of the second are at odd indexes.

Move the elements around, as specified by the given function. * Note: the reindexing function says where each of the elements in the new vector come from. * Note: it is OK for the same input element to end up in mulitple places in the result. O(n)

Reverse the vector.

Rotate "left". The first element of the vector is on the "left", so rotate left moves all elemnts toward the corresponding smaller index. Elements that fall off the beginning end up at the end.

Rotate "right". The first element of the vector is on the "left", so rotate right moves all elemnts toward the corresponding larger index. Elements that fall off the end, end up at the beginning.

Move all elements towards smaller indexes. Elements that fall off the front are ignored. Empty slots are filled in with the given element. O(n).

Move all elements towards the larger indexes. Elements that "fall" off the end are ignored. Empty slots are filled in with the given element. O(n).

Vector with exactly one element

Add an element to the head of a vector

Add an element to the tail of a vector

Apply a function to each element in a range starting at zero; return the a vector of values obtained. cf. both natFromZero and Data.Vector.generate

Since Vector is traversable, we can pretty trivially sequence natFromZeroVec inside a monad.

Monadically join a vector of values, using the given function. This functionality can sometimes be reproduced by creating a newtype wrapper and using joinWith, this implementation is provided for convenience.

Join a vector of vectors, using the given function to combine the sub-vectors.

Split a vector into a vector of vectors.

The Endian parameter determines the ordering of the inner vectors. If LittleEndian, then less significant bits go into smaller indexes. If BigEndian, then less significant bits go into larger indexes. See the documentation for split for more details.

An applicative version of splitWith.

Split a vector into a vector of vectors. The default ordering of the outer result vector is LittleEndian.

For example: let wordsize = knownNat :: NatRepr 3 vecsize = knownNat :: NatRepr 12 numwords = knownNat :: NatRepr 4 (12 / 3) Just inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ] in show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9], [10,11,12] ]" whereas a BigEndian result would have been [ [10,11,12], [7,8,9], [4,5,6], [1,2,3] ]

Join a vector of vectors into a single vector. Assumes an append/LittleEndian join strategy: the order of the inner vectors is preserved in the result vector.

  let innersize = knownNat :: NatRepr 4
      Just inner1 = fromList innersize [ 1, 2, 3, 4 ]
      Just inner2 = fromList innersize [ 5, 6, 7, 8 ]
      Just inner3 = fromList innersize [ 9, 10, 11, 12 ]
      outersize = knownNat :: NatRepr 3
      Just outer = fromList outersize [ inner1, inner2, inner3 ]
  in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]

a prepend/BigEndian join strategy would have the result: [ 9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ]

Append two vectors. The first one is at lower indexes in the result.