parameterized-utils-2.1.6.0: Classes and data structures for working with data-kind indexed types
Copyright(c) Galois Inc 2014-2019
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Parameterized.Vector

Description

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

Documentation

data Vector n a Source #

Fixed-size non-empty vectors.

Instances

Instances details
Foldable (Vector n) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

fold :: Monoid m => Vector n m -> m #

foldMap :: Monoid m => (a -> m) -> Vector n a -> 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 #

toList :: Vector n a -> [a] #

null :: Vector n a -> Bool #

length :: Vector n a -> Int #

elem :: Eq a => a -> Vector n a -> Bool #

maximum :: Ord a => Vector n a -> a #

minimum :: Ord a => Vector n a -> a #

sum :: Num a => Vector n a -> a #

product :: Num a => Vector n a -> a #

Traversable (Vector n) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

traverse :: Applicative f => (a -> f b) -> Vector n a -> f (Vector n b) #

sequenceA :: Applicative f => Vector n (f a) -> f (Vector n a) #

mapM :: Monad m => (a -> m b) -> Vector n a -> m (Vector n b) #

sequence :: Monad m => Vector n (m a) -> m (Vector n a) #

Functor (Vector n) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

fmap :: (a -> b) -> Vector n a -> Vector n b #

(<$) :: a -> Vector n b -> Vector n a #

FoldableWithIndex (Fin n) (Vector n) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vector n a -> m #

ifoldMap' :: Monoid m => (Fin n -> a -> m) -> Vector n a -> m #

ifoldr :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b #

ifoldl :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b #

ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b #

ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b #

FunctorWithIndex (Fin n) (Vector n) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

imap :: (Fin n -> a -> b) -> Vector n a -> Vector n b #

TraversableWithIndex (Fin n) (Vector n) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

itraverse :: Applicative f => (Fin n -> a -> f b) -> Vector n a -> f (Vector n b) #

Show a => Show (Vector n a) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

showsPrec :: Int -> Vector n a -> ShowS #

show :: Vector n a -> String #

showList :: [Vector n a] -> ShowS #

Eq a => Eq (Vector n a) Source # 
Instance details

Defined in Data.Parameterized.Vector

Methods

(==) :: Vector n a -> Vector n a -> Bool #

(/=) :: Vector n a -> Vector n a -> Bool #

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

toList :: Vector n a -> [a] Source #

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

Assignments

fromAssignment :: forall f ctx tp e. (forall tp'. f tp' -> e) -> Assignment f (ctx ::> tp) -> Vector (CtxSize (ctx ::> tp)) e Source #

Convert a non-empty Assignment to a fixed-size Vector.

This function uses the same ordering convention as toVector.

toAssignment :: Size ctx -> (forall tp. Index ctx tp -> e -> f tp) -> Vector (CtxSize ctx) e -> Assignment f ctx Source #

Convert a Vector into a Assignment.

This function uses the same ordering convention as toVector.

Length

length :: Vector n a -> NatRepr n Source #

Length of the vector. O(1)

nonEmpty :: Vector n a -> LeqProof 1 n Source #

Proof that the length of this vector is not 0.

lengthInt :: Vector n a -> Int Source #

The length of the vector as an Int.

Indexing

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

elemAtMaybe :: Int -> Vector n a -> Maybe a Source #

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

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)

Indexing with Fin

indicesUpTo :: NatRepr n -> Vector (n + 1) (Fin (n + 1)) Source #

indicesOf :: Vector n a -> Vector n (Fin n) Source #

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.

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

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

slice Source #

Arguments

:: ((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.

replace Source #

Arguments

:: ((i + w) <= n, 1 <= w) 
=> NatRepr i

Start index

-> Vector w a

sub-vector

-> Vector n a 
-> Vector n a 

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

mapAt Source #

Arguments

:: ((i + w) <= n, 1 <= w) 
=> NatRepr i

Start index

-> NatRepr w

Section width

-> (Vector w a -> Vector w a)

map for the sub-vector

-> Vector n a 
-> Vector n a 

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

mapAtM Source #

Arguments

:: Monad m 
=> ((i + w) <= n, 1 <= w) 
=> NatRepr i

Start index

-> NatRepr w

Section width

-> (Vector w a -> m (Vector w a))

map for the sub-vector

-> Vector n a 
-> m (Vector n a) 

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

Zipping

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

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

zipWithM :: Monad m => (a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c) Source #

zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m () Source #

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)

reverse :: forall a n. 1 <= n => Vector n a -> Vector n a Source #

Reverse the vector.

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

singleton :: forall a. a -> Vector 1 a Source #

Vector with exactly one element

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.

Unfolding

unfoldr :: forall h a b. NatRepr h -> (b -> (a, b)) -> b -> Vector (h + 1) a Source #

Construct a vector with exactly h + 1 elements by repeatedly applying a generator function to a seed value.

c.f. Data.Vector.unfoldrExactN

unfoldrM :: forall m h a b. Monad m => NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a) Source #

Monadically construct a vector with exactly h + 1 elements by repeatedly applying a generator function to a seed value.

c.f. Data.Vector.unfoldrExactNM

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

Unfold a vector, with access to the current index.

c.f. Data.Vector.unfoldrExactN

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

Monadically unfold a vector, with access to the current index.

c.f. Data.Vector.unfoldrExactNM

iterateN :: NatRepr n -> (a -> a) -> a -> Vector (n + 1) a Source #

Build a vector by repeatedly applying a function to a seed value.

Compare to iterateN

iterateNM :: Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a) Source #

Build a vector by repeatedly applying a monadic function to a seed value.

Compare to iterateNM.

Splitting and joining

General

joinWithM Source #

Arguments

:: forall m f n w. (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.

joinWith Source #

Arguments

:: forall f n w. 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.

splitWith Source #

Arguments

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

A function for slicing out a chunk of length w, starting at i

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

splitWithA Source #

Arguments

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

f function for slicing out f chunk of length w, starting at i

-> NatRepr n 
-> NatRepr w 
-> g (n * w) 
-> f (Vector n (g w)) 

An applicative version of splitWith.

Vectors

split Source #

Arguments

:: (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 ]

append :: Vector m a -> Vector n a -> Vector (m + n) a Source #

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