sized-vector 0.0.2.5 → 1.0.0.0

raw patch · 2 files changed

+363/−72 lines, 2 filesdep +equational-reasoning

Dependencies added: equational-reasoning

Files

• Data/Vector/Sized.hs +357/−67
• sized-vector.cabal +6/−5

@@ -1,102 +1,295 @@-{-# LANGUAGE DataKinds, GADTs, MultiParamTypeClasses, PolyKinds #-}-{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators    #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds, GADTs, MultiParamTypeClasses, PolyKinds    #-}+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies #-}+{-# LANGUAGE TypeOperators, NoImplicitPrelude                      #-} -- | Size-parameterized vector types and functions.-module Data.Vector.Sized ( Vector (..), sLength, length, append, foldr-                         , foldl, singleton, zipWith, zipWithSame, toList, fromList-                         , unsafeFromList, fromList', unsafeFromList'-                         , all, splitAt, takeAtMost, splitAtMost-                         , drop, take, map, head, tail, index) where-import Control.Applicative-import Data.Maybe-import Data.Singletons       hiding (promote)-import Data.Type.Monomorphic-import Data.Type.Natural     hiding (promote)-import Prelude               hiding (all, drop, foldl, foldr, head, length, map,-                              splitAt, tail, take, zipWith)+module Data.Vector.Sized ( -- * Vectors and indices+                           Vector (..)+                         , Index(..), succIndex, indexToInt,+                           -- * Conversion & Construction+                           replicate, replicate', singleton, uncons,+                           -- ** List+                           fromList, fromList', unsafeFromList, unsafeFromList', toList,+                           -- * Basic functions+                           append, head, last, tail, null, length, sLength,+                           -- * Vector transformations+                           map, reverse, intersperse, transpose,+                           -- * Reducing vectors (folds)+                           foldl, foldl', foldl1, foldl1', foldr, foldr1,+                           -- ** Special folds+                           concat, and, or, any, all, sum, product, maximum, minimum,+                           -- * Subvectors+                           -- ** Extracting subvectors+                           take, takeAtMost, drop, splitAt, splitAtMost, stripPrefix,+                           -- * Searching vectors+                           -- ** Searching by equality+                           elem, notElem,+                           -- ** Searching with a predicate+                           find,+                           -- * Indexing vectors+                           (!!), (%!!), index, sIndex, elemIndex, sElemIndex+                         , findIndex, sFindIndex, findIndices, sFindIndices+                         , elemIndices, sElemIndices,+                           -- * Zipping vectors+                           zip, zipSame, zipWith, zipWithSame, unzip+                         ) where+import           Control.Applicative+import           Data.Maybe+import           Data.Type.Monomorphic+import           Data.Type.Natural     hiding (promote)+import qualified Prelude               as P+import           Prelude               (Eq(..), Bool(..), Int, Show(..), (&&), Num(..)+                                       , (||), not, error, ($), (.), seq, fst, snd+                                       , flip, otherwise)+import           Proof.Equational      hiding (promote) +-- | Fixed-length list. data Vector (a :: *) (n :: Nat)  where   Nil  :: Vector a Z   (:-) :: a -> Vector a n -> Vector a (S n)  infixr 5 :- +-- | Monomorphic representation of 'Vector' @a n@ is @[a]@.+instance Monomorphicable (Vector a) where+  type MonomorphicRep (Vector a) = [a]+  demote (Monomorphic vec) = toList vec+  promote [] = Monomorphic Nil+  promote (x:xs) =+    case promote xs of+      Monomorphic vec -> Monomorphic $ x :- vec++-- | Index type for list.+data Index (n :: Nat) where+  Index :: ((S m :<<= n) ~ True) => SNat m -> Index n++-- | Succ index number.+succIndex :: Index n -> Index (S n)+succIndex (Index n) = Index (sS n)++-- | Convert index into integer.+indexToInt :: Index n -> Int+indexToInt (Index n) = sNatToInt n++deriving instance Show (Index n)+ deriving instance Show a => Show (Vector a n) instance (Eq a) => Eq (Vector a n) where   Nil == Nil = True   (x :- xs) == (y :- ys) = x == y && xs == ys   _ == _ = error "impossible!" -sLength :: Vector a n -> SNat n-sLength Nil       = sZ-sLength (_ :- xs) = sS $ sLength xs--length :: Vector a n -> Int-length = sNatToInt . sLength--append :: Vector a n -> Vector a m -> Vector a (n :+: m)-append (x :- xs) ys = x :- append xs ys-append Nil       ys = ys+--------------------------------------------------+-- Conversion & Construction+-------------------------------------------------- -foldr :: (a -> b -> b) -> b -> Vector a n -> b-foldr _ b Nil       = b-foldr f a (x :- xs) = f x (foldr f a xs)+-- | 'replicate' @n x@ is a vector of length @n@ with @x@ the value of every element.+replicate :: SNat n -> a -> Vector a n+replicate SZ _ = Nil+replicate (SS n) a = a :- replicate n a -foldl :: (a -> b -> a) -> a -> Vector b n -> a-foldl _ a Nil       = a-foldl f a (b :- bs) = foldl f (f a b) bs+-- | 'replicate', with the length inferred.+replicate' :: forall n a. SingRep n => a -> Vector a n+replicate' = replicate (sing :: SNat n) +-- | Construct a singleton vector. singleton :: a -> Vector a (S Z) singleton = (:- Nil) -zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n-zipWithSame _ Nil Nil = Nil-zipWithSame f (x :- xs) (y :- ys) = f x y :- zipWithSame f xs ys-zipWithSame _ _ _ = error "cannot happen"--zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)-zipWith _ Nil Nil             = Nil-zipWith _ Nil (_ :- _)        = Nil-zipWith _ (_ :- _) Nil        = Nil-zipWith f (x :- xs) (y :- ys) = f x y :- zipWith f xs ys--toList :: Vector a n -> [a]-toList = foldr (:) []+-- | Uncons the non-empty list.+uncons :: Vector a (S n) -> (a, Vector a n)+uncons (a :- as) = (a, as) +-- | Convert a list into a vector.+-- If a given list is shorter than the length, it returns @Nothing@. fromList :: SNat n -> [a] -> Maybe (Vector a n) fromList SZ     _      = Just Nil fromList (SS n) (x:xs) = (x :-) <$> fromList n xs fromList _      _      = Nothing +-- | Unsafe version of 'fromList'.+-- If a given list is shorter than the length, it aborts. unsafeFromList :: SNat n -> [a] -> Vector a n unsafeFromList len = fromMaybe (error "Length too short") . fromList len +-- | Convert a list into vector, with length inferred. fromList' :: SingRep n => [a] -> Maybe (Vector a n) fromList' = fromList sing +-- | Unsafe version of 'unsafeFromList'. unsafeFromList' :: SingRep n => [a] -> Vector a n unsafeFromList' = unsafeFromList sing -all :: (a -> Bool) -> Vector a n -> Bool-all p = foldr ((&&) . p) False+-- | Convert a vector into a list.+toList :: Vector a n -> [a]+toList = foldr (:) [] -splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))-splitAt SZ     xs        = (Nil, xs)-splitAt (SS n) (x :- xs) =-  case splitAt n xs of-    (xs', ys') -> (x :- xs', ys')-splitAt _ _ = error "could not happen!"+--------------------------------------------------+-- Basic Functions+-------------------------------------------------- -drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)-drop n = snd . splitAt n+-- | Append two @Vector@s.+append :: Vector a n -> Vector a m -> Vector a (n :+: m)+append (x :- xs) ys = x :- append xs ys+append Nil       ys = ys +-- | Extract the first element of a non-empty vector.+head :: Vector a (S n) -> a+head (x :- _) = x++-- | Extract the last element of a non-empty vector.+last :: Vector a (S n) -> a+last (x :- Nil) = x+last (_ :- xs@(_ :- _)) = last xs++-- | Extract the elements after the head of a non-empty list.+tail :: Vector a (S n) -> Vector a n+tail (_ :- xs) = xs++-- | Test whether a @Vector@ is empty, though it's clear from the type parameter.+null :: Vector a n -> Bool+null Nil = True+null _   = False++-- | 'length' returns the length of a finite list as an 'Int'.+length :: Vector a n -> Int+length = sNatToInt . sLength++-- | 'sLength' returns the length of a finite list as a 'SNat' @n@.+sLength :: Vector a n -> SNat n+sLength Nil       = sZ+sLength (_ :- xs) = sS $ sLength xs++--------------------------------------------------+-- Vector transformations+--------------------------------------------------++-- | 'map' @f xs@ is the vector obtained by applying @f@ to each element of xs.+map :: (a -> b) -> Vector a n -> Vector b n+map _ Nil       = Nil+map f (x :- xs) = f x :- map f xs++-- | 'reverse' @xs@ returns the elements of xs in reverse order. @xs@ must be finite.+reverse :: forall a n. Vector a n -> Vector a n+reverse xs0 = case plusZR (sLength xs0) of Refl -> go Nil xs0+  where+    go :: Vector a m -> Vector a k -> Vector a (k :+ m)+    go acc Nil = acc+    go acc (x :- xs) = case plusSR (sLength xs) (sLength acc) of Refl -> go (x:- acc) xs+         +-- | The 'intersperse' function takes an element and a vector and+-- \`intersperses\' that element between the elements of the vector.+intersperse :: a -> Vector a n -> Vector a ((Two :* n) :- One)+intersperse _ Nil = Nil+intersperse a (x :- xs) = case plusSR (sLength xs) (sLength xs) of Refl -> x :- prependToAll a xs++prependToAll :: a -> Vector a n -> Vector a (Two :* n)+prependToAll _ Nil = Nil+prependToAll a (x :- xs) = case plusSR (sLength xs) (sLength xs) of Refl -> x :- a :- prependToAll a xs++-- | The 'transpose' function transposes the rows and columns of its argument.+transpose :: SingRep n => Vector (Vector a n) m -> Vector (Vector a m) n+transpose Nil = replicate' Nil+transpose (Nil :- _) = Nil+transpose ((x :- xs) :- xss) =+    case singInstance (sLength xs) of+      SingInstance -> (x :- map head xss) :- transpose (xs :- map tail xss)++--------------------------------------------------+-- Reducing vectors (folds)+--------------------------------------------------++-- | Left fold.+foldl :: (a -> b -> a) -> a -> Vector b n -> a+foldl _ a Nil       = a+foldl f a (b :- bs) = foldl f (f a b) bs++-- | A strict version of 'foldl'.+foldl' :: forall a b n. (a -> b -> a) -> a -> Vector b n -> a+foldl' f z0 xs0 = lgo z0 xs0+  where+    lgo :: a -> Vector b m -> a+    lgo z Nil = z+    lgo z (x :- xs) = let z' = f z x in z' `seq` lgo z' xs++-- | Left fold for non-empty vector.+foldl1 :: (a -> a -> a) -> Vector a (S n) -> a+foldl1 f (a :- as) = foldl f a as++-- | A strict version of 'foldl1'.+foldl1' :: (a -> a -> a) -> Vector a (S n) -> a+foldl1' f (a :- as) = foldl' f a as++-- | Right fold.+foldr :: (a -> b -> b) -> b -> Vector a n -> b+foldr _ b Nil       = b+foldr f a (x :- xs) = f x (foldr f a xs)++-- | Right fold for non-empty vector.+foldr1 :: (a -> a -> a) -> Vector a (S n) -> a+foldr1 _ (x :- Nil) = x+foldr1 f (x :- xs@(_ :- _)) = f x (foldr1 f xs)++-- | The function 'concat' concatenates all vectors in th vector.+concat :: Vector (Vector a n) m -> Vector a (m :*: n)+concat Nil = Nil+concat (xs :- xss) =+  let n = sLength xs+      n0 = sLength xss+  in case plusCommutative (n0 %* n) n of+       Refl -> xs `append` concat xss++and, or :: Vector Bool m -> Bool+-- | 'and' returns the conjunction of a Boolean vector.+and = foldr (&&) True++-- | 'or' returns the disjunction of a Boolean vector.+or  = foldr (||) False++any, all :: (a -> Bool) -> Vector a n -> Bool+-- | Applied to a predicate and a list, 'any' determines if any element of the vector satisfies the predicate. +any p = or . map p+-- | Applied to a predicate and a list, 'all' determines if all element of the vector satisfies the predicate. +all p = and . map p++sum, product :: P.Num a => Vector a n -> a+sum = foldr (+) 0+product = foldr (*) 1++maximum, minimum :: P.Ord a => Vector a (S n) -> a+maximum = foldr1 P.max+minimum = foldr1 P.min++--------------------------------------------------+-- Subvectors+--------------------------------------------------++-- | 'take' @n xs@ returns the prefix of @xs@ of length @n@,+-- with @n@ less than or equal to the length of @xs@. take :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n take SZ     _         = Nil take (SS n) (x :- xs) = x :- take n xs take _ _ = error "imposible!" +-- | A variant of @take@ which returns entire @xs@ if @n@ is greater than the length of @xs@. takeAtMost :: SNat n -> Vector a m -> Vector a (Min n m) takeAtMost = (fst .) . splitAtMost +-- | 'drop' @n xs@ returns the suffix of @xs@ after the first @n@ elements,+-- with @n@ less than or equal to the length of @xs@.+drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)+drop n = snd . splitAt n++-- | 'splitAt' @n xs@ returns a tuple where first element is @xs@ prefix of length @n@+-- and second element is the remainder of the list. @n@ should be less than or equal to the length of @xs@.+splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))+splitAt SZ     xs        = (Nil, xs)+splitAt (SS n) (x :- xs) =+  case splitAt n xs of+    (xs', ys') -> (x :- xs', ys')+splitAt _ _ = error "could not happen!"++-- | A varian of 'splitAt' which allows @n@ to be greater than the length of @xs@. splitAtMost :: SNat n -> Vector a m -> (Vector a (Min n m), Vector a (m :-: n)) splitAtMost SZ Nil = (Nil, Nil) splitAtMost SZ (x :- xs) = (Nil, x :- xs)@@ -105,24 +298,121 @@   case splitAtMost n xs of     (ys, zs) -> (x :- ys, zs) -map :: (a -> b) -> Vector a n -> Vector b n-map _ Nil       = Nil-map f (x :- xs) = f x :- map f xs+-- | The 'stripPrefix' function drops the given prefix from a vector.+-- It returns @Nothing@ if the vector did not start with the prefix given or shorter than the prefix,+-- or Just the vector after the prefix, if it does.+stripPrefix :: Eq a => Vector a n -> Vector a m -> Maybe (Vector a (m :- n))+stripPrefix Nil ys = Just ys+stripPrefix (_ :- _) Nil = Nothing+stripPrefix (x :- xs) (y :- ys)+    | x == y    = stripPrefix xs ys+    | otherwise = Nothing -head :: Vector a (S n) -> a-head (x :- _) = x+--------------------------------------------------+-- Searching vectors+-------------------------------------------------- -tail :: Vector a (S n) -> Vector a n-tail (_ :- xs) = xs+elem, notElem :: Eq a => a -> Vector a n -> Bool+elem a = any (== a)+notElem a = all (/= a) +find :: (a -> Bool) -> Vector a n -> Maybe a+find _ Nil = Nothing+find p (x :- xs)+    | p x       = Just x+    | otherwise = find p xs++--------------------------------------------------+-- Indexing vectors+--------------------------------------------------++-- | List index (subscript) operator, starting from @sZero@.+(!!) ::  ((n :<<= m) ~ True) => Vector a (S m) -> SNat n -> a+(!!) = flip index++-- | A 'Index' version of '!!'.+(%!!) :: Vector a n -> Index n -> a+(%!!) = flip sIndex++-- | Flipped version of '!!'. index :: ((n :<<= m) ~ True) => SNat n -> Vector a (S m) -> a index SZ     (a :- _)  = a index (SS n) (_ :- (a :- as)) = index n (a :- as) -instance Monomorphicable (Vector a) where-  type MonomorphicRep (Vector a) = [a]-  demote (Monomorphic vec) = toList vec-  promote [] = Monomorphic Nil-  promote (x:xs) =-    case promote xs of-      Monomorphic vec -> Monomorphic $ x :- vec+-- | A 'Index' version of 'index'.+sIndex :: Index n -> Vector a n -> a+sIndex (Index SZ) (x :- _) = x+sIndex (Index (SS n)) (_ :- xs) = sIndex (Index n) xs++-- | The 'elemIndex' function returns the index (as 'Int') of the first element in the given list+-- which is equal (by '==') to the query element, or Nothing if there is no such element.+elemIndex :: Eq a => a -> Vector a n -> Maybe Int+elemIndex a = findIndex (== a)++-- | 'Index' version of 'elemIndex'.+sElemIndex :: Eq a => a -> Vector a n -> Maybe (Index n)+sElemIndex a = sFindIndex (== a)++-- | The 'elemIndices' function extends 'elemIndex', by returning the indices of all elements equal to the query element,+-- in ascending order.+elemIndices :: Eq a => a -> Vector a n -> [Int]+elemIndices a = findIndices (== a)++-- | 'Index' version of 'elemIndices'.+sElemIndices :: Eq a => a -> Vector a n -> [Index n]+sElemIndices a = sFindIndices (== a)++-- | The findIndex function takes a predicate and a vector+-- and returns the index of the first element in the vector+-- satisfying the predicate, or Nothing if there is no such element.+findIndex :: (a -> Bool) -> Vector a n -> Maybe Int+findIndex p = listToMaybe . findIndices p++-- | 'Index' version of 'findIndex'.+sFindIndex :: (a -> Bool) -> Vector a n -> Maybe (Index n)+sFindIndex p = listToMaybe . sFindIndices p++-- | The 'findIndices' function extends 'findIndex', by returning the indices of all elements satisfying the predicate,+--  in ascending order.+findIndices :: (a -> Bool) -> Vector a n -> [Int]+findIndices p = P.map indexToInt . sFindIndices p++-- | 'Index' version of 'findIndices'.+sFindIndices :: (a -> Bool) -> Vector a n -> [Index n]+sFindIndices _ Nil = []+sFindIndices p (x :- xs)+            | p x       = Index sZero : P.map succIndex (sFindIndices p xs)+            | otherwise =  P.map succIndex $ sFindIndices p xs++--------------------------------------------------+-- Zipping vectors+--------------------------------------------------++-- | 'zip' takes two vectors and returns a vector of corresponding pairs.+--  If one input list is short, excess elements of the longer list are discarded.+zip :: Vector a n -> Vector b m  -> Vector (a, b) (Min n m)+zip = zipWith (,)++-- | Same as 'zip', but the given vectors must have the same length.+zipSame :: Vector a n -> Vector b n -> Vector (a, b) n+zipSame = zipWithSame (,)++-- | 'zipWith' generalises 'zip' by zipping with the function given as the first argument, instead of a tupling function.+zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)+zipWith _ Nil Nil             = Nil+zipWith _ Nil (_ :- _)        = Nil+zipWith _ (_ :- _) Nil        = Nil+zipWith f (x :- xs) (y :- ys) = f x y :- zipWith f xs ys++-- | Same as 'zipWith', but the given vectors must have the same length.+zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n+zipWithSame _ Nil Nil = Nil+zipWithSame f (x :- xs) (y :- ys) = f x y :- zipWithSame f xs ys+zipWithSame _ _ _ = error "cannot happen"++-- | Inverse of 'zipSame'.+unzip :: Vector (a, b) n -> (Vector a n, Vector b n)+unzip Nil = (Nil, Nil)+unzip ((a, b) :- ps) =+  let (as, bs) = unzip ps+  in (a :- as, b :- bs)

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                sized-vector-version:             0.0.2.5+version:             1.0.0.0 synopsis:            Size-parameterized vector types and functions. description:         Size-parameterized vector types and functions using a data-type promotion. homepage:            https://github.com/konn/sized-vector@@ -21,7 +21,8 @@  library   exposed-modules:     Data.Vector.Sized-  build-depends:       base >= 2.0 && < 5-               ,       singletons     == 0.8.*-               ,       type-natural   >= 0.0.2.0-               ,       monomorphic    == 0.0.*+  build-depends:       base                     >= 2.0 && < 5+               ,       singletons               == 0.8.*+               ,       type-natural             >= 0.0.2.0+               ,       monomorphic              == 0.0.*+               ,       equational-reasoning     == 0.0.*