clash-prelude-0.5.0.1: CAES Language for Synchronous Hardware - Prelude library

CLaSH.Sized.Vector

Synopsis

# `Vec`tor constructors

data Vec :: Nat -> * -> * where Source

Fixed size vectors

• Lists with their length encoded in their type
• `Vec`tor elements have a descending subscript starting from `maxIndex` (`vlength` - 1) and ending at 0
````>>> ````(3:>4:>5:>Nil)
```<3,4,5>
`>>> ````:t (3:>4:>5:>Nil)
```(3:>4:>5:>Nil) :: Num a => Vec 3 a
```

Constructors

 Nil :: Vec 0 a (:>) :: a -> Vec n a -> Vec (n + 1) a infixr 5

Instances

 Functor (Vec n) KnownNat n => Applicative (Vec n) Foldable (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) CPack (Vec n a) type CSignalP t (Vec n a) = Vec n (CSignal t 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 infixl 5 Source

Add an element to the tail of the vector

````>>> ````(3:>4:>5:>Nil) <: 1
```<3,4,5,1>
`>>> ````:t (3:>4:>5:>Nil) <: 1
```(3:>4:>5:>Nil) <: 1 :: Num a => Vec 4 a
```

# Standard `Vec`tor functions

## Extracting sub-`Vec`tors

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

Extract the first element of a vector

````>>> ````vhead (1:>2:>3:>Nil)
```1
`>>> ````vhead Nil
```  <interactive>
Couldn't match type ‘1’ with ‘0’
Expected type: Vec (0 + 1) a
Actual type: Vec 0 a
In the first argument of ‘vhead’, namely ‘Nil’
```

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

Extract the elements after the head of a vector

````>>> ````vtail (1:>2:>3:>Nil)
```<2,3>
`>>> ````vtail Nil
```  <interactive>
Couldn't match type ‘1’ with ‘0’
Expected type: Vec (0 + 1) a
Actual type: Vec 0 a
In the first argument of ‘vtail’, namely ‘Nil’
In the expression: vtail Nil
```

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

Extract the last element of a vector

````>>> ````vlast (1:>2:>3:>Nil)
```3
`>>> ````vlast Nil
```  <interactive>
Couldn't match type ‘1’ with ‘0’
Expected type: Vec (0 + 1) a
Actual type: Vec 0 a
In the first argument of ‘vlast’, namely ‘Nil’
In the expression: vlast Nil
```

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

Extract all the elements of a vector except the last element

````>>> ````vinit (1:>2:>3:>Nil)
```<1,2>
`>>> ````vinit Nil
```  <interactive>
Couldn't match type ‘1’ with ‘0’
Expected type: Vec (0 + 1) a
Actual type: Vec 0 a
In the first argument of ‘vinit’, namely ‘Nil’
In the expression: vinit Nil
```

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

`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>
`>>> ````vtake d3               (1:>2:>3:>4:>5:>Nil)
```<1,2,3>
`>>> ````vtake d0               (1:>2:>Nil)
```<>
`>>> ````vtake d4               (1:>2:>Nil)
```  <interactive>
Couldn't match type ‘4 + n0’ with ‘2’
The type variable ‘n0’ is ambiguous
Expected type: Vec (4 + n0) a
Actual type: Vec (1 + 1) a
In the second argument of ‘vtake’, namely ‘(1 :> 2 :> Nil)’
In the expression: vtake d4 (1 :> 2 :> Nil)
In an equation for ‘it’: it = vtake d4 (1 :> 2 :> Nil)
```

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

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

````>>> ````vtakeI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
```<1,2>
```

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

`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>
`>>> ````vdrop d3               (1:>2:>3:>4:>5:>Nil)
```<4,5>
`>>> ````vdrop d0               (1:>2:>Nil)
```<1,2>
`>>> ````vdrop d4               (1:>2:>Nil)
```  <interactive>
Couldn't match expected type ‘2’ with actual type ‘4 + n0’
The type variable ‘n0’ is ambiguous
In the first argument of ‘print’, namely ‘it’
In a stmt of an interactive GHCi command: print it
```

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

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

````>>> ````vdropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
```<4,5>
```

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

`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 Source

`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>
`>>> ````vselect d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
```<2,4,6>
```

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

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

````>>> ````vselectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
```<2,4>
```

## Combining `Vec`tors

(+>>) :: a -> Vec n a -> Vec n a infixr 4 Source

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>
`>>> ````1 +>> Nil
```<>
```

(<<+) :: Vec n a -> a -> Vec n a infixl 4 Source

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 <<+ 1
```<>
```

(<++>) :: Vec n a -> Vec m a -> Vec (n + m) a infixr 5 Source

Append two vectors

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

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

Concatenate a vector of vectors

````>>> ````vconcat ((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>
```

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

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

````>>> ````vzip (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil)
```<(1,4),(2,3),(3,2),(4,1)>
```

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

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

````>>> ````vunzip ((1,4):>(2,3):>(3,2):>(4,1):>Nil)
```(<1,2,3,4>,<4,3,2,1>)
```

## Splitting `Vec`tors

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

Split a vector into two vectors at the given point

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

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

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

````>>> ````vsplitI (1:>2:>3:>7:>8:>Nil) :: (Vec 2 Int, Vec 3 Int)
```(<1,2>,<3,7,8>)
```

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

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>,<5,6,7,8>,<9,10,11,12>>
```

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

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

````>>> ````vunconcatI (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) :: Vec 2 (Vec 6 Int)
```<<1,2,3,4,5,6>,<7,8,9,10,11,12>>
```

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

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

````>>> ````vmerge (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> 7 :> 8 :> Nil)
```<1,5,2,6,3,7,4,8>
```

## Applying functions to `Vec`tor elements

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

`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 Source

`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 Source

`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 Source

`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 Source

`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 Source

`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```

## Indexing `Vec`tors

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

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
```*** Exception: index out of bounds
```

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

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>
`>>> ````vreplace (1:>2:>3:>4:>5:>Nil) 0 7
```<1,2,3,4,7>
`>>> ````vreplace (1:>2:>3:>4:>5:>Nil) 9 7
```<*** Exception: index out of bounds
```

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

Index (subscript) of the head of the `Vec`tor

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

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

Length of a `Vec`tor as an Integer

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

## Generating `Vec`tors

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

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

````>>> ````vcopy (snat :: SNat 3) 6
```<6,6,6>
`>>> ````vcopy d3 6
```<6,6,6>
```

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

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

````>>> ````vcopy 6 :: Vec 5 Int
```<6,6,6,6,6>
```

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

`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 Source

`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

`viterateI f x :: Vec 3 a == (x :> f x :> f (f x) :> Nil)`

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

`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 Source

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

`vgenerateI f x :: Vec 3 a == (f x :> f (f x) :> f (f (f x)) :> Nil)`

## Misc

vreverse :: Vec n a -> Vec n a Source

Returns the elements in a list in reverse order

````>>> ````vreverse (1:>2:>3:>4:>Nil)
```<4,3,2,1>
```

toList :: Vec n a -> [a] Source

Convert a vector to a list

````>>> ````toList (1:>2:>3:>Nil)
```[1,2,3]
```

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

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)`
````>>> ````[1 :: Signed 8,2,3,4,5]
```[1,2,3,4,5]
`>>> ````\$(v [1::Signed 8,2,3,4,5])
```<1,2,3,4,5>
```

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

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 second argument:

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

In this case, adding `lazyV` on `vzipWith`s second 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:

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

asNatProxy :: Vec n a -> Proxy n Source

`Vec`tor as a `Proxy` for `Nat`

# Alternative `Vec`tor functions

vhead' :: 1 <= n => Vec n a -> a Source

Same as `vhead`, but with a "`(1 <= n)`" constraint and "`Vec n a`" argument, instead of a "`Vec (n + 1) a`" argument