parameterized-data-0.1.6: Parameterized data library implementing lightweight dependent types

Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and KTH's SAM group BSD-style (see the file LICENSE) alfonso.acosta@gmail.com experimental non-portable None Haskell98

Data.Param.FSVec

Description

FSVec: Fixed sized vectors. Vectors with numerically parameterized size.

Synopsis

# Documentation

data Nat s => FSVec s a Source #

Fixed-Sized Vector data type, indexed with type-level naturals, the first index for all vectors is 0

Instances

(+>) :: (Nat s, Pos s', Succ s s') => a -> FSVec s a -> FSVec s' a infixr 5 Source #

Cons operator, note it's not a constructor

singleton :: a -> FSVec D1 a Source #

A FSVec with a single element

vectorCPS :: [a] -> (forall s. Nat s => FSVec s a -> w) -> w Source #

Build a vector from a list (CPS style)

vectorTH :: Lift a => [a] -> ExpQ Source #

Build a vector from a list (using Template Haskell)

unsafeVector :: Nat s => s -> [a] -> FSVec s a Source #

Build a vector from a list (unsafe version: The static/dynamic size of the list is checked to match at runtime)

reallyUnsafeVector :: [a] -> FSVec s a Source #

Build a vector from a list.

Unlike unsafeVector, reallyunsafeVector doesn't have access to the static size of the list and thus cannot not check it against its dynamic size (which saves traversing the list at runtime to obtain the dynamic length).

Therefore, reallyUnsafeVector (the name is that long on purspose) can be used to gain some performance but may break the consistency of the size parameter if not handled with care (i.e. the size parameter can nolonger be checked statically and the fullfilment of function constraints is left to the programmers judgement).

Do not use reallyUnsafeVector unless you know what you're doing!

readFSVec :: (Read a, Nat s) => String -> FSVec s a Source #

Read a vector (Note the the size of the vector string is checked to match the resulting type at runtime)

readFSVecCPS :: Read a => String -> (forall s. Nat s => FSVec s a -> w) -> w Source #

length :: forall s a. Nat s => FSVec s a -> Int Source #

value-level length of a vector

genericLength :: forall s a n. (Nat s, Num n) => FSVec s a -> n Source #

generic value-level length of a vector

lengthT :: Nat s => FSVec s a -> s Source #

type-level version of length

fromVector :: Nat s => FSVec s a -> [a] Source #

Transform Vector to a list

null :: FSVec D0 a -> Bool Source #

Check if a Vector is empty

(!) :: (Pos s, Nat i, i :<: s) => FSVec s a -> i -> a Source #

Access an element of a vector

replace :: (Nat s, Nat i) => FSVec s a -> i -> a -> FSVec s a Source #

Replace an element of a vector

head :: Pos s => FSVec s a -> a Source #

Take the first element of a vector

last :: Pos s => FSVec s a -> a Source #

Take the last element of a vector

init :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a Source #

Return all but the last element of a vector

tail :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a Source #

Return all but the first element of a vector

take :: (Nat i, Nat s, Min s i s') => i -> FSVec s a -> FSVec s' a Source #

Take the first i elements of a vector

drop :: (Nat i, Nat s, Min s i sm, Sub s sm s') => i -> FSVec s a -> FSVec s' a Source #

Drop the first i elements of a vector

select :: (Nat f, Nat s, Nat n, f :<: i, Mul s n smn, Add f smn fasmn, fasmn :<=: i) => f -> s -> n -> FSVec i a -> FSVec n a Source #

The function select selects elements in the vector. The first argument gives the initial element, starting from zero, the second argument gives the stepsize between elements and the last argument gives the number of elements.

group :: (Pos n, Nat s, Div s n s') => n -> FSVec s a -> FSVec s' (FSVec n a) Source #

break a vector into subvectors of size n.

(<+) :: (Nat s, Pos s', Succ s s') => FSVec s a -> a -> FSVec s' a infixl 5 Source #

add an element at the end of a vector. (Inverse of '(+>)')

(++) :: (Nat s1, Nat s2, Add s1 s2 s3) => FSVec s1 a -> FSVec s2 a -> FSVec s3 a infixr 5 Source #

Concatenate two vectors

map :: Nat s => (a -> b) -> FSVec s a -> FSVec s b Source #

Apply a function on all elements of a vector

zipWith :: Nat s => (a -> b -> c) -> FSVec s a -> FSVec s b -> FSVec s c Source #

Applies function pairwise on two vectors

zipWith3 :: Nat s => (a -> b -> c -> d) -> FSVec s a -> FSVec s b -> FSVec s c -> FSVec s d Source #

Applies function pairwise on two vectors

foldl :: Nat s => (a -> b -> a) -> a -> FSVec s b -> a Source #

Folds a function from the right to the left over a vector using an initial value.

foldr :: Nat s => (b -> a -> a) -> a -> FSVec s b -> a Source #

Folds a function from the left to the right over a vector using an initial value.

zip :: Nat s => FSVec s a -> FSVec s b -> FSVec s (a, b) Source #

zip two vectors into a vector of tuples.

unzip :: Nat s => FSVec s (a, b) -> (FSVec s a, FSVec s b) Source #

unzip a vector of tuples into two vectors.

shiftl :: Pos s => FSVec s a -> a -> FSVec s a Source #

shift a value from the left into a vector.

shiftr :: Pos s => FSVec s a -> a -> FSVec s a Source #

shift a value from the left into a vector.

rotl :: forall s a. Nat s => FSVec s a -> FSVec s a Source #

Rotate a vector to the left. Note that this fuctions does not change the size of a vector.

rotr :: Nat s => FSVec s a -> FSVec s a Source #

Rotate a vector to the left. Note that this fuctions does not change the size of a vector.

concat :: (Nat s1, Nat s2, Nat s3, Mul s1 s2 s3) => FSVec s1 (FSVec s2 a) -> FSVec s3 a Source #

flatten a vector of vectors to a single vector

reverse :: Nat s => FSVec s a -> FSVec s a Source #

reverse a vector

iterate :: Nat s => s -> (a -> a) -> a -> FSVec s a Source #

generate a vector with a given number of elements starting from an initial element using a supplied function for the generation of elements.

FSVec> iterate d5 (+1) 1
<1,2,3,4,5> :: Num a => FSVec D5 a

generate :: Nat s => s -> (a -> a) -> a -> FSVec s a Source #

generate behaves in the same way as iterate, but starts with the application of the supplied function to the supplied value.

FSVec> generate d5 (+1) 1
<2,3,4,5,6> :: Num a => FSVec  D5 a

copy :: Nat s => s -> a -> FSVec s a Source #

generates a vector with a given number of copies of the same element.

FSVec> copy d7 5
<5,5,5,5,5,5,5> :: FSVec D7 Integer