-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Parameterized data library implementing lightweight dependent
types
--   
--   This library provides an implementation of parameterized types using
--   type-level computations to implement the type parameters and emulate
--   dependent types. Right now only fixed-sized vectors are provided. A
--   tutorial on how to use them can be found at
--   <a>http://www.ict.kth.se/forsyde/files/tutorial/tutorial.html#FSVec</a>
@package parameterized-data
@version 0.1.5


-- | <a>FSVec</a>: Fixed sized vectors. Vectors with numerically
--   parameterized size.
--   
--   Tutorial:
--   <a>http://www.ict.kth.se/forsyde/files/tutorial/tutorial.html#FSVec</a>
module Data.Param.FSVec

-- | Fixed-Sized Vector data type, indexed with type-level naturals, the
--   first index for all vectors is 0
data Nat s => FSVec s a
empty :: FSVec D0 a

-- | Cons operator, note it's not a constructor
(+>) :: (Nat s, Pos s', Succ s s') => a -> FSVec s a -> FSVec s' a

-- | A FSVec with a single element
singleton :: a -> FSVec D1 a

-- | Build a vector from a list (CPS style)
vectorCPS :: [a] -> (forall s. Nat s => FSVec s a -> w) -> w

-- | Build a vector from a list (using Template Haskell)
vectorTH :: Lift a => [a] -> ExpQ

-- | Build a vector from a list (unsafe version: The static/dynamic size of
--   the list is checked to match at runtime)
unsafeVector :: Nat s => s -> [a] -> FSVec s a

-- | 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!
reallyUnsafeVector :: [a] -> FSVec s a

-- | Read a vector (Note the the size of the vector string is checked to
--   match the resulting type at runtime)
readFSVec :: (Read a, Nat s) => String -> FSVec s a

-- | Read a vector, CPS version.
readFSVecCPS :: Read a => String -> (forall s. Nat s => FSVec s a -> w) -> w

-- | value-level length of a vector
length :: Nat s => FSVec s a -> Int

-- | generic value-level length of a vector
genericLength :: (Nat s, Num n) => FSVec s a -> n

-- | type-level version of length
lengthT :: Nat s => FSVec s a -> s

-- | Transform Vector to a list
fromVector :: Nat s => FSVec s a -> [a]

-- | Check if a Vector is empty
null :: FSVec D0 a -> Bool

-- | Access an element of a vector
(!) :: (Pos s, Nat i, :<: i s) => FSVec s a -> i -> a

-- | Replace an element of a vector
replace :: (Nat s, Nat i) => FSVec s a -> i -> a -> FSVec s a

-- | Take the first element of a vector
head :: Pos s => FSVec s a -> a

-- | Take the last element of a vector
last :: Pos s => FSVec s a -> a

-- | Return all but the last element of a vector
init :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a

-- | Return all but the first element of a vector
tail :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a

-- | Take the first i elements of a vector
take :: (Nat i, Nat s, Min s i s') => i -> FSVec s a -> FSVec s' a

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

-- | The function <a>select</a> 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.
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

-- | break a vector into subvectors of size n.
group :: (Pos n, Nat s, Div s n s') => n -> FSVec s a -> FSVec s' (FSVec n a)

-- | add an element at the end of a vector. (Inverse of '(+&gt;)')
(<+) :: (Nat s, Pos s', Succ s s') => FSVec s a -> a -> FSVec s' a

-- | Concatenate two vectors
(++) :: (Nat s1, Nat s2, Add s1 s2 s3) => FSVec s1 a -> FSVec s2 a -> FSVec s3 a

-- | Apply a function on all elements of a vector
map :: Nat s => (a -> b) -> FSVec s a -> FSVec s b

-- | Applies function pairwise on two vectors
zipWith :: Nat s => (a -> b -> c) -> FSVec s a -> FSVec s b -> FSVec s c

-- | Folds a function from the right to the left over a vector using an
--   initial value.
foldl :: Nat s => (a -> b -> a) -> a -> FSVec s b -> a

-- | Folds a function from the left to the right over a vector using an
--   initial value.
foldr :: Nat s => (b -> a -> a) -> a -> FSVec s b -> a

-- | zip two vectors into a vector of tuples.
zip :: Nat s => FSVec s a -> FSVec s b -> FSVec s (a, b)

-- | unzip a vector of tuples into two vectors.
unzip :: Nat s => FSVec s (a, b) -> (FSVec s a, FSVec s b)

-- | shift a value from the left into a vector.
shiftl :: Pos s => FSVec s a -> a -> FSVec s a

-- | shift a value from the left into a vector.
shiftr :: Pos s => FSVec s a -> a -> FSVec s a

-- | Rotate a vector to the left. Note that this fuctions does not change
--   the size of a vector.
rotl :: Nat s => FSVec s a -> FSVec s a

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

-- | flatten a vector of vectors to a single vector
concat :: (Nat s1, Nat s2, Nat s3, Mul s1 s2 s3) => FSVec s1 (FSVec s2 a) -> FSVec s3 a

-- | reverse a vector
reverse :: Nat s => FSVec s a -> FSVec s a

-- | generate a vector with a given number of elements starting from an
--   initial element using a supplied function for the generation of
--   elements.
--   
--   <pre>
--   FSVec&gt; iterate d5 (+1) 1
--   </pre>
--   
--   <pre>
--   &lt;1,2,3,4,5&gt; :: Num a =&gt; FSVec D5 a
--   </pre>
iterate :: Nat s => s -> (a -> a) -> a -> FSVec s a

-- | <a>generate</a> behaves in the same way as <a>iterate</a>, but starts
--   with the application of the supplied function to the supplied value.
--   
--   <pre>
--   FSVec&gt; generate d5 (+1) 1
--   </pre>
--   
--   <pre>
--   &lt;2,3,4,5,6&gt; :: Num a =&gt; FSVec  D5 a
--   </pre>
generate :: Nat s => s -> (a -> a) -> a -> FSVec s a

-- | generates a vector with a given number of copies of the same element.
--   
--   <pre>
--   FSVec&gt; copy d7 5 
--   </pre>
--   
--   <pre>
--   &lt;5,5,5,5,5,5,5&gt; :: FSVec D7 Integer
--   </pre>
copy :: Nat s => s -> a -> FSVec s a
instance Typeable2 FSVec
instance Eq a => Eq (FSVec s a)
instance (Lift a, Nat s) => Lift (FSVec s a)
instance Nat s => Traversable (FSVec s)
instance Nat s => Functor (FSVec s)
instance Nat s => Foldable (FSVec s)
instance (Read a, Nat s) => Read (FSVec s a)
instance Show a => Show (FSVec s a)
instance (Data a, Typeable s) => Data (FSVec s a)


-- | This module is a wrapper for all the publicly usable types and
--   functions of the parameterized-data library.
module Data.Param