module Data.Vector.Sized (
Vector (..), Index,
module Data.Type.Ordinal,
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 Data.Type.Ordinal
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 :-
type Index = Ordinal
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
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. SingI 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' :: SingI n => [a] -> Maybe (Vector a n)
fromList' = fromList sing
unsafeFromList' :: SingI 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
init :: Vector a (S n) -> Vector a n
init (a :- as) =
case as of
Nil -> Nil
_ :- _ -> a :- init as
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 = coerce (plusZR (sLength xs0)) $ go Nil xs0
where
go :: Vector a m -> Vector a k -> Vector a (k :+ m)
go acc Nil = acc
go acc (x :- xs) = coerce (symmetry $ plusSR (sLength xs) (sLength acc)) $ go (x:- acc) xs
intersperse :: a -> Vector a n -> Vector a ((Two :* n) :- One)
intersperse _ Nil = Nil
intersperse a (x :- xs) =
coerce (plusSR (sLength xs) (sLength xs)) $ x :- prependToAll a xs
prependToAll :: a -> Vector a n -> Vector a (Two :* n)
prependToAll _ Nil = Nil
prependToAll a (x :- xs) =
x :- (coerce (plusSR (sLength xs) (sLength xs)) $ a :- prependToAll a xs)
transpose :: SingI 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 coerce (symmetry $ plusCommutative (n0 %* n) n) $ 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 OZ (x :- _) = x
sIndex (OS n) (_ :- xs) = sIndex 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 ordToInt . sFindIndices p
sFindIndices :: (a -> Bool) -> Vector a n -> [Index n]
sFindIndices _ Nil = []
sFindIndices p (x :- xs)
| p x = OZ : P.map OS (sFindIndices p xs)
| otherwise = P.map OS $ 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 `hashWithSalt` (0 :: Int)
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