module Data.Vector.Sized where
import Control.Applicative
import Data.Maybe
import Data.Type.Natural
import Prelude hiding (map, foldl, foldr, head, splitAt, tail, zipWith, take)
data Vector (a :: *) (n :: Nat) where
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
infixr 5 :-
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
foldr :: (a -> b -> b) -> b -> Vector a n -> b
foldr _ b Nil = b
foldr f a (x :- xs) = f x (foldr f a xs)
foldl :: (a -> b -> a) -> a -> Vector b n -> a
foldl _ a Nil = a
foldl f a (b :- bs) = foldl f (f a b) bs
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 (:) []
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' :: Sing n => [a] -> Maybe (Vector a n)
fromList' = fromList sing
unsafeFromList' :: Sing n => [a] -> Vector a n
unsafeFromList' = unsafeFromList sing
all :: (a -> Bool) -> Vector a n -> Bool
all p = foldr ((&&) . p) False
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!"
drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)
drop n = snd . splitAt n
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!"
map :: (a -> b) -> Vector a n -> Vector b n
map _ Nil = Nil
map f (x :- xs) = f x :- map f xs
head :: Vector a (S n) -> a
head (x :- _) = x
tail :: Vector a (S n) -> Vector a n
tail (_ :- xs) = xs