Copyright | (c) Galois Inc 2014-2019 |
---|---|

Safe Haskell | None |

Language | Haskell98 |

A fixed-size vector of typed elements.

NB: This module contains an orphan instance. It will be included in GHC 8.10, see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.

## Synopsis

- data Vector n a
- fromList :: 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a)
- toList :: Vector n a -> [a]
- length :: Vector n a -> NatRepr n
- nonEmpty :: Vector n a -> LeqProof 1 n
- lengthInt :: Vector n a -> Int
- elemAt :: (i + 1) <= n => NatRepr i -> Vector n a -> a
- elemAtMaybe :: Int -> Vector n a -> Maybe a
- elemAtUnsafe :: Int -> Vector n a -> a
- insertAt :: (i + 1) <= n => NatRepr i -> a -> Vector n a -> Vector n a
- insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)
- uncons :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
- slice :: ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> Vector n a -> Vector w a
- take :: forall n x a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a
- zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
- zipWithM :: Monad m => (a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
- zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()
- interleave :: forall n a. 1 <= n => Vector n a -> Vector n a -> Vector (2 * n) a
- shuffle :: (Int -> Int) -> Vector n a -> Vector n a
- reverse :: forall a n. 1 <= n => Vector n a -> Vector n a
- rotateL :: Int -> Vector n a -> Vector n a
- rotateR :: Int -> Vector n a -> Vector n a
- shiftL :: Int -> a -> Vector n a -> Vector n a
- shiftR :: Int -> a -> Vector n a -> Vector n a
- singleton :: forall a. a -> Vector 1 a
- cons :: forall n a. a -> Vector n a -> Vector (n + 1) a
- snoc :: forall n a. Vector n a -> a -> Vector (n + 1) a
- generate :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> Vector (h + 1) a
- generateM :: forall m h a. Monad m => NatRepr h -> (forall n. n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a)
- joinWithM :: forall m f n w. (1 <= w, Monad m) => (forall l. 1 <= l => NatRepr l -> f w -> f l -> m (f (w + l))) -> NatRepr w -> Vector n (f w) -> m (f (n * w))
- joinWith :: forall f n w. 1 <= w => (forall l. 1 <= l => NatRepr l -> f w -> f l -> f (w + l)) -> NatRepr w -> Vector n (f w) -> f (n * w)
- splitWith :: forall f w n. (1 <= w, 1 <= n) => Endian -> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w) -> NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)
- splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) => Endian -> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w)) -> NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))
- split :: (1 <= w, 1 <= n) => NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)
- join :: 1 <= w => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
- append :: Vector m a -> Vector n a -> Vector (m + n) a

# Documentation

Fixed-size non-empty vectors.

## Instances

Functor (Vector n) Source # | |

Foldable (Vector n) Source # | |

Defined in Data.Parameterized.Vector fold :: Monoid m => Vector n m -> m # foldMap :: Monoid m => (a -> m) -> Vector n a -> m # foldr :: (a -> b -> b) -> b -> Vector n a -> b # foldr' :: (a -> b -> b) -> b -> Vector n a -> b # foldl :: (b -> a -> b) -> b -> Vector n a -> b # foldl' :: (b -> a -> b) -> b -> Vector n a -> b # foldr1 :: (a -> a -> a) -> Vector n a -> a # foldl1 :: (a -> a -> a) -> Vector n a -> a # elem :: Eq a => a -> Vector n a -> Bool # maximum :: Ord a => Vector n a -> a # minimum :: Ord a => Vector n a -> a # | |

Traversable (Vector n) Source # | |

Eq a => Eq (Vector n a) Source # | |

Show a => Show (Vector n a) Source # | |

# Lists

fromList :: 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a) Source #

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

.

# Length

# Indexing

elemAtUnsafe :: Int -> Vector n a -> a Source #

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

# Update

insertAt :: (i + 1) <= n => NatRepr i -> a -> Vector n a -> Vector n a Source #

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

.

insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a) Source #

Insert an element at the given index.
Return `Nothing`

if the element is outside the vector bounds.
`O(n)`

.

# Sub sequences

uncons :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a)) Source #

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

:: ((i + w) <= n, 1 <= w) | |

=> NatRepr i | Start index |

-> NatRepr w | Width of sub-vector |

-> Vector n a | |

-> Vector w a |

Extract a subvector of the given vector.

take :: forall n x a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a Source #

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

# Zipping

zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c Source #

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

interleave :: forall n a. 1 <= n => Vector n a -> Vector n a -> Vector (2 * n) a Source #

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.

# Reorder

shuffle :: (Int -> Int) -> Vector n a -> Vector n a Source #

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

rotateL :: Int -> Vector n a -> Vector n a Source #

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.

rotateR :: Int -> Vector n a -> Vector n a Source #

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.

shiftL :: Int -> a -> Vector n a -> Vector n a Source #

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

.

shiftR :: Int -> a -> Vector n a -> Vector n a Source #

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

.

# Construction

cons :: forall n a. a -> Vector n a -> Vector (n + 1) a Source #

Add an element to the head of a vector

snoc :: forall n a. Vector n a -> a -> Vector (n + 1) a Source #

Add an element to the tail of a vector

generate :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> Vector (h + 1) a Source #

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`

generateM :: forall m h a. Monad m => NatRepr h -> (forall n. n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a) Source #

Since `Vector`

is traversable, we can pretty trivially sequence
`natFromZeroVec`

inside a monad.

# Splitting and joining

## General

:: (1 <= w, Monad m) | |

=> (forall l. 1 <= l => NatRepr l -> f w -> f l -> m (f (w + l))) | A function for joining contained elements. The first argument is the size of the accumulated third term, and the second argument is the element to join to the accumulated term. The function can use any join strategy desired (prepending/BigEndian, appending/LittleEndian, etc.). |

-> NatRepr w | |

-> Vector n (f w) | |

-> m (f (n * w)) |

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.

:: 1 <= w | |

=> (forall l. 1 <= l => NatRepr l -> f w -> f l -> f (w + l)) | A function for joining contained elements. The first argument is the size of the accumulated third term, and the second argument is the element to join to the accumulated term. The function can use any join strategy desired (prepending/BigEndian, appending/LittleEndian, etc.). |

-> NatRepr w | |

-> Vector n (f w) | |

-> f (n * w) |

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

:: (1 <= w, 1 <= n) | |

=> Endian | |

-> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w) | A function for slicing out a chunk of length |

-> NatRepr n | |

-> NatRepr w | |

-> f (n * w) | |

-> Vector n (f w) |

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.

:: (Applicative f, 1 <= w, 1 <= n) | |

=> Endian | |

-> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w)) | f function for slicing out f chunk of length |

-> NatRepr n | |

-> NatRepr w | |

-> g (n * w) | |

-> f (Vector n (g w)) |

An applicative version of `splitWith`

.

## Vectors

:: (1 <= w, 1 <= n) | |

=> NatRepr n | Inner vector size |

-> NatRepr w | Outer vector size |

-> Vector (n * w) a | Input vector |

-> Vector n (Vector w a) |

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 :: 1 <= w => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a Source #

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