module Data.Vector.Sized (
Vector (..)
, Index(..), succIndex, indexToInt,
replicate, replicate', singleton, uncons,
fromList, fromList', unsafeFromList, unsafeFromList', toList,
append, head, last, tail, null, length, sLength,
map, reverse, intersperse, transpose,
foldl, foldl', foldl1, foldl1', foldr, foldr1,
concat, and, or, any, all, sum, product, maximum, minimum,
take, takeAtMost, drop, splitAt, splitAtMost, stripPrefix,
elem, notElem,
find,
(!!), (%!!), index, sIndex, elemIndex, sElemIndex
, findIndex, sFindIndex, findIndices, sFindIndices
, elemIndices, sElemIndices,
zip, zipSame, zipWith, zipWithSame, unzip
) where
import Control.Applicative
import Control.DeepSeq
import Data.Hashable
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)
data Vector (a :: *) (n :: Nat) where
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
infixr 5 :-
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
data Index (n :: Nat) where
Index :: ((S m :<<= n) ~ True) => SNat m -> Index n
succIndex :: Index n -> Index (S n)
succIndex (Index n) = Index (sS n)
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!"
replicate :: SNat n -> a -> Vector a n
replicate SZ _ = Nil
replicate (SS n) a = a :- replicate n a
replicate' :: forall n a. SingRep n => a -> Vector a n
replicate' = replicate (sing :: SNat n)
singleton :: a -> Vector a (S Z)
singleton = (:- Nil)
uncons :: Vector a (S n) -> (a, Vector a n)
uncons (a :- as) = (a, as)
fromList :: SNat n -> [a] -> Maybe (Vector a n)
fromList SZ _ = Just Nil
fromList (SS n) (x:xs) = (x :-) <$> fromList n xs
fromList _ _ = Nothing
unsafeFromList :: SNat n -> [a] -> Vector a n
unsafeFromList len = fromMaybe (error "Length too short") . fromList len
fromList' :: SingRep n => [a] -> Maybe (Vector a n)
fromList' = fromList sing
unsafeFromList' :: SingRep n => [a] -> Vector a n
unsafeFromList' = unsafeFromList sing
toList :: Vector a n -> [a]
toList = foldr (:) []
append :: Vector a n -> Vector a m -> Vector a (n :+: m)
append (x :- xs) ys = x :- append xs ys
append Nil ys = ys
head :: Vector a (S n) -> a
head (x :- _) = x
last :: Vector a (S n) -> a
last (x :- Nil) = x
last (_ :- xs@(_ :- _)) = last xs
tail :: Vector a (S n) -> Vector a n
tail (_ :- xs) = xs
null :: Vector a n -> Bool
null Nil = True
null _ = False
length :: Vector a n -> Int
length = sNatToInt . sLength
sLength :: Vector a n -> SNat n
sLength Nil = sZ
sLength (_ :- xs) = sS $ sLength xs
map :: (a -> b) -> Vector a n -> Vector b n
map _ Nil = Nil
map f (x :- xs) = f x :- map f xs
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
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
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)
foldl :: (a -> b -> a) -> a -> Vector b n -> a
foldl _ a Nil = a
foldl f a (b :- bs) = foldl f (f a b) bs
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
foldl1 :: (a -> a -> a) -> Vector a (S n) -> a
foldl1 f (a :- as) = foldl f a as
foldl1' :: (a -> a -> a) -> Vector a (S n) -> a
foldl1' f (a :- as) = foldl' f a as
foldr :: (a -> b -> b) -> b -> Vector a n -> b
foldr _ b Nil = b
foldr f a (x :- xs) = f x (foldr f a xs)
foldr1 :: (a -> a -> a) -> Vector a (S n) -> a
foldr1 _ (x :- Nil) = x
foldr1 f (x :- xs@(_ :- _)) = f x (foldr1 f xs)
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 = foldr (&&) True
or = foldr (||) False
any, all :: (a -> Bool) -> Vector a n -> Bool
any p = or . map p
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
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!"
takeAtMost :: SNat n -> Vector a m -> Vector a (Min n m)
takeAtMost = (fst .) . splitAtMost
drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)
drop n = snd . splitAt n
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!"
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)
splitAtMost (SS _) Nil = (Nil, Nil)
splitAtMost (SS n) (x :- xs) =
case splitAtMost n xs of
(ys, zs) -> (x :- ys, zs)
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
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
(!!) :: ((n :<<= m) ~ True) => Vector a (S m) -> SNat n -> a
(!!) = flip index
(%!!) :: Vector a n -> Index n -> a
(%!!) = flip sIndex
index :: ((n :<<= m) ~ True) => SNat n -> Vector a (S m) -> a
index SZ (a :- _) = a
index (SS n) (_ :- (a :- as)) = index n (a :- as)
sIndex :: Index n -> Vector a n -> a
sIndex (Index SZ) (x :- _) = x
sIndex (Index (SS n)) (_ :- xs) = sIndex (Index n) xs
elemIndex :: Eq a => a -> Vector a n -> Maybe Int
elemIndex a = findIndex (== a)
sElemIndex :: Eq a => a -> Vector a n -> Maybe (Index n)
sElemIndex a = sFindIndex (== a)
elemIndices :: Eq a => a -> Vector a n -> [Int]
elemIndices a = findIndices (== a)
sElemIndices :: Eq a => a -> Vector a n -> [Index n]
sElemIndices a = sFindIndices (== a)
findIndex :: (a -> Bool) -> Vector a n -> Maybe Int
findIndex p = listToMaybe . findIndices p
sFindIndex :: (a -> Bool) -> Vector a n -> Maybe (Index n)
sFindIndex p = listToMaybe . sFindIndices p
findIndices :: (a -> Bool) -> Vector a n -> [Int]
findIndices p = P.map indexToInt . sFindIndices p
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
zip :: Vector a n -> Vector b m -> Vector (a, b) (Min n m)
zip = zipWith (,)
zipSame :: Vector a n -> Vector b n -> Vector (a, b) n
zipSame = zipWithSame (,)
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
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"
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)
instance NFData a => NFData (Vector a n) where
rnf = rnfVector
rnfVector :: NFData a => Vector a n -> ()
rnfVector Nil = Nil `seq` ()
rnfVector (x :- xs) = rnf x `seq` rnf xs `seq` ()
vecHashWithSalt :: Hashable a => Int -> Vector a n -> Int
vecHashWithSalt salt Nil = salt `combine` 0
vecHashWithSalt salt xs = foldl hashWithSalt salt xs
instance Hashable a => Hashable (Vector a n) where
hash Nil = 0
hash (a :- as) = foldl hashWithSalt (hash a) as
hashWithSalt = vecHashWithSalt