CLaSH.Sized.Vector

Documentation

data Vec where

Constructors

Nil :: Vec 0 a

(:>) :: a -> Vec n a -> Vec (n + 1) a

Instances

Functor (Vec n)

KnownNat n => Applicative (Vec n)

Foldable (Vec n)

Traversable (Vec n)

Eq a => Eq (Vec n a)

Show a => Show (Vec n a)

(KnownNat n, KnownNat (BitSize a), BitVector a) => BitVector (Vec n a)

Pack (Vec n a)

type BitSize (Vec n a) = * n (BitSize a)

type SignalP (Vec n a) = Vec n (Signal a)

(<:) :: Vec n a -> a -> Vec (n + 1) a

Add an element to the tail of the vector

(3:>4:>5:>Nil) <: 1 == (3:>4:>5:>1:>Nil)
Nil            <: 1 == (1:>Nil)

vhead :: Vec (n + 1) a -> a

Extract the first element of a vector

vhead (1:>2:>3:>Nil) == 1
vhead Nil            == TYPE ERROR

vtail :: Vec (n + 1) a -> Vec n a

Extract the elements after the head of a vector

vtail (1:>2:>3:>Nil) == (2:>3:>Nil)
vtail Nil            == TYPE ERROR

vlast :: Vec (n + 1) a -> a

Extract the last element of a vector

vlast (1:>2:>3:>Nil) == 3
vlast Nil            == TYPE ERROR

vinit :: Vec (n + 1) a -> Vec n a

Extract all the elements of a vector except the last element

vinit (1:>2:>3:>Nil) == (1:>2:>Nil)
vinit Nil            == TYPE ERROR

(+>>) :: a -> Vec n a -> Vec n a

Add an element to the head of the vector, and extract all elements of the resulting vector except the last element

1 +>> (3:>4:>5:>Nil) == (1:>3:>4:>Nil)
1 +>> Nil            == Nil

(<<+) :: Vec n a -> a -> Vec n a

Add an element to the tail of the vector, and extract all elements of the resulting vector except the first element

(3:>4:>5:>Nil) <<+ 1 == (4:>5:>1:>Nil)
Nil            <<+ 1 == Nil

(<++>) :: Vec n a -> Vec m a -> Vec (n + m) a

Append two vectors

(1:>2:>3:>Nil) <++> (7:>8:>Nil) = (1:>2:>3:>7:>8:>Nil)

vconcat :: Vec n (Vec m a) -> Vec (n * m) a

Concatenate a vector of vectors

vunconcat ((1:>2:>3:>Nil)    :>
           (4:>5:>6:>Nil)    :>
           (7:>8:>9:>Nil)    :>
           (10:>11:>12:>Nil) :>
           Nil)                  == (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)

vsplit :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)

Split a vector into two vectors at the given point

vsplit (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil)
vsplit d3               (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil)

vsplitI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)

Split a vector into two vectors where the length of the two is determined by the context

vunconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)

Split a vector of (n * m) elements into a vector of vectors with length m, where m is given

vunconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) == ((1:>2:>3:>4:>Nil)    :>
                                                              (5:>6:>7:>8:>Nil)    :>
                                                              (9:>10:>11:>12:>Nil) :>
                                                              Nil)

vunconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)

Split a vector of (n * m) elements into a vector of vectors with length m, where m is determined by the context

vmerge :: Vec n a -> Vec n a -> Vec (n + n) a

Merge two vectors, alternating their elements, i.e.,

vmerge (xn :> ... :> x2 :> x1 :> Nil)  (yn :> ... :> y2 :> y1 :> Nil) == (xn :> yn :> ... :> x2 :> y2 :> x1 :> y1 :> Nil)

vreverse :: Vec n a -> Vec n a

Returns the elements in a list in reverse order

vmap :: (a -> b) -> Vec n a -> Vec n b

vmap f xs is the list obtained by applying f to each element of xs, i.e.,

vmap f (xn :> ... :> x2 :> x1 :> Nil) == (f xn :> ... :> f x2 :> f x1 :> Nil)

vzipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c

vzipWith generalises vzip by zipping with the function given as the first argument, instead of a tupling function. For example, vzipWith (+) is applied to two vectors to produce the vector of corresponding sums.

vzipWith f (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == (f xn yn :> ... :> f x2 y2 :> f x1 y1 :> Nil)

vfoldr :: (a -> b -> b) -> b -> Vec n a -> b

vfoldr, applied to a binary operator, a starting value (typically the right-identity of the operator), and a vector, reduces the vector using the binary operator, from right to left:

vfoldr f z (xn :> ... :> x2 :> x1 :> Nil) == xn `f` (... (x2 `f` (x1 `f` z))...)
vfoldr r z Nil                            == z

vfoldl :: (b -> a -> b) -> b -> Vec n a -> b

vfoldl, applied to a binary operator, a starting value (typically the left-identity of the operator), and a vector, reduces the vector using the binary operator, from left to right:

vfoldl f z (xn :> ... :> x2 :> x1 :> Nil) == (...((z `f` xn)... `f` x2) `f` x1
vfoldl f z Nil                            == z

vfoldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a

vfoldr1 is a variant of vfoldr that has no starting value argument, and thus must be applied to non-empty vectors.

vfoldr1 f (xn :> ... :> x3 :> x2 :> x1 :> Nil) == xn `f` (... (x3 `f` (x2 `f` x1))...)
vfoldr1 f (x1 :> Nil)                          == x1
vfoldr1 f Nil                                  == TYPE ERROR

vfoldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a

vfoldl1 is a variant of vfoldl that has no starting value argument, and thus must be applied to non-empty vectors.

vfoldl f (xn :> xn1 :> ... :> x2 :> x1 :> Nil) == (...((xn `f` xn1)... `f` x2) `f` x1
vfoldl f (x1 :> Nil)                           == x1
vfoldl f Nil                                   == TYPE ERROR

vzip :: Vec n a -> Vec n b -> Vec n (a, b)

vzip takes two lists and returns a list of corresponding pairs.

vzip (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil)

vunzip :: Vec n (a, b) -> (Vec n a, Vec n b)

vunzip transforms a list of pairs into a list of first components and a list of second components.

vunzip ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil) == (xn :> ... :> x2 :> x1 :> Nil, yn :> ... :> y2 :> y1 :> Nil)

(!) :: (KnownNat n, Integral i) => Vec n a -> i -> a

Vector index (subscript) operator, descending from maxIndex, where the last element has subscript 0.

(1:>2:>3:>4:>5:>Nil) ! 4        == 1
(1:>2:>3:>4:>5:>Nil) ! maxIndex == 1
(1:>2:>3:>4:>5:>Nil) ! 1        == 4
(1:>2:>3:>4:>5:>Nil) ! 14       == RUNTIME ERROR: Out of bounds

vreplace :: (KnownNat n, Integral i) => Vec n a -> i -> a -> Vec n a

Replace an element of a vector at the given index (subscript), NB: vector elements have a descending subscript starting from maxIndex and ending at 0

vreplace (1:>2:>3:>4:>5:>Nil) 3 7 == (1:>7:>3:>4:>5:>Nil)
vreplace (1:>2:>3:>4:>5:>Nil) 0 7 == (1:>2:>3:>4:>7:>Nil)
vreplace (1:>2:>3:>4:>5:>Nil) 9 7 == RUNTIME ERROR: Out of bounds

maxIndex :: KnownNat n => Vec n a -> Integer

Index (subscript) of the head of the Vector

maxIndex (6 :> 7 :> 8 :> Nil) == 2

vlength :: KnownNat n => Vec n a -> Integer

Length of a Vector as an Integer

vlength (6 :> 7 :> 8 :> Nil) == 3

vtake :: SNat m -> Vec (m + n) a -> Vec m a

vtake n, applied to a vector xs, returns the n-length prefix of xs

vtake (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)
vtake d3               (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)
vtake d0               (1:>2:>Nil)          == Nil
vtake d4               (1:>2:>Nil)          == TYPE ERROR

vtakeI :: KnownNat m => Vec (m + n) a -> Vec m a

vtakeI xs, returns the prefix of xs as demanded by the context

vdrop :: SNat m -> Vec (m + n) a -> Vec n a

vdrop n xs returns the suffix of xs after the first n elements

vdrop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)
vdrop d3               (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)
vdrop d0               (1:>2:>Nil)          == (1:>2:>Nil)
vdrop d4               (1:>2:>Nil)          == TYPE ERROR

vdropI :: KnownNat m => Vec (m + n) a -> Vec n a

vdropI xs, returns the suffix of xs as demanded by the context

vexact :: SNat m -> Vec (m + (n + 1)) a -> a

vexact n xs returns n'th element of xs, NB: vector elements have a descending subscript starting from maxIndex and ending at 0

vexact (snat :: SNat 1) (1:>2:>3:>4:>5:>Nil) == 4
vexact d1               (1:>2:>3:>4:>5:>Nil) == 4

vselect :: ((f + (s * n)) + 1) <= i => SNat f -> SNat s -> SNat (n + 1) -> Vec i a -> Vec (n + 1) a

vselect f s n xs selects n elements with stepsize s and offset f from xs

vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil)
vselect d1 d2 d3                                           (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil)

vselectI :: (((f + (s * n)) + 1) <= i, KnownNat (n + 1)) => SNat f -> SNat s -> Vec i a -> Vec (n + 1) a

vselectI f s xs selects as many elements as demanded by the context with stepsize s and offset f from xs

vcopy :: SNat n -> a -> Vec n a

vcopy n a returns a vector that has n copies of a

vcopy (snat :: SNat 3) 6 == (6:>6:>6:>Nil)
vcopy d3 6               == (6:>6:>6:>Nil)

vcopyI :: KnownNat n => a -> Vec n a

vcopyI a creates a vector with as many copies of a as demanded by the context

viterate :: SNat n -> (a -> a) -> a -> Vec n a

viterate n f x returns a vector starting with x followed by n repeated applications of f to x

viterate (snat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
viterate d4 f x               == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)

viterateI :: KnownNat n => (a -> a) -> a -> Vec n a

viterate f x returns a vector starting with x followed by n repeated applications of f to x, where n is determined by the context

vgenerate :: SNat n -> (a -> a) -> a -> Vec n a

vgenerate n f x returns a vector with n repeated applications of f to x

vgenerate (snat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
vgenerate d4 f x               == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)

vgenerateI :: KnownNat n => (a -> a) -> a -> Vec n a

vgenerate f x returns a vector with n repeated applications of f to x, where n is determined by the context

toList :: Vec n a -> [a]

Convert a vector to a list

v :: Lift a => [a] -> ExpQ

Create a vector literal from a list literal

$(v [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)

lazyV :: KnownNat n => Vec n a -> Vec n a

For when your vector functions are too strict in their arguments

For example:

-- Bubble sort for 1 iteration
sortV xs = vmap fst sorted <: (snd (vlast sorted))
 where
   lefts  = vhead xs :> vmap snd (vinit sorted)
   rights = vtail xs
   sorted = vzipWith compareSwapL lefts rights

-- Compare and swap
compareSwapL a b = if a < b then (a,b)
                            else (b,a)

Will not terminate because vzipWith is too strict in its left argument:

*Main> sortV (4 :> 1 :> 2 :> 3 :> Nil)
<*** Exception: <<loop>>

In this case, adding lazyV on vzipWiths left argument:

sortVL xs = vmap fst sorted <: (snd (vlast sorted))
 where
   lefts  = vhead xs :> vmap snd (vinit sorted)
   rights = vtail xs
   sorted = vzipWith compareSwapL (lazyV lefts) rights

Results in a successful computation:

*Main> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
<1,2,3,4>

asNatProxy :: Vec n a -> Proxy n

Vector as a Proxy for Nat