module Data.Vector.Sized (
Vector (..), Index,
module Data.Type.Ordinal,
replicate, replicate', singleton, uncons,
fromList, fromList', unsafeFromList, unsafeFromList', toList,
append, head, last, tail, init, null, length, sLength,
map, reverse, intersperse, transpose,
foldl, foldl', foldl1, foldl1', foldr, foldr1, ifoldl,
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,
sized, sized'
) where
import Control.Applicative ((<$>))
import Control.DeepSeq (NFData (..))
import Data.Hashable (Hashable (..))
import Data.Maybe (Maybe (..), fromMaybe, listToMaybe)
import Data.Singletons (SingI, SingInstance (..), sing)
import Data.Singletons (singInstance)
import Data.Type.Equality (sym)
import Data.Type.Monomorphic (Monomorphic (..),
Monomorphicable (..))
import Data.Type.Natural ((:*), (:+), (:-), (:-:), (:<<=),
Min)
import Data.Type.Natural (Nat (..), One, SNat, Sing (..),
Two)
import Data.Type.Natural (plusComm, plusSuccR, plusZR)
import Data.Type.Natural (sNatToInt, (%:*))
import Data.Type.Ordinal (Ordinal (..), ordToInt)
import Language.Haskell.TH
import Language.Haskell.TH.Syntax (Lift (lift))
import Prelude (Bool (..), Eq (..), Int, Num (..))
import Prelude (Show (..), error, flip, fst,
otherwise)
import Prelude (seq, snd, ($), (&&), (.), (||))
import qualified Prelude as P
import Proof.Equational (coerce, symmetry)
#if !(defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708)
import Data.Type.Natural (sS, sZ)
#else
sZ :: SNat Z
sZ = SZ
sS :: SNat n -> SNat (S n)
sS = SS
#endif
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)
deriving instance P.Ord a => P.Ord (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 (plusSuccR (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 (sym $ plusSuccR (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 (sym $ plusSuccR (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 (plusComm n (n0 %:* 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
ordinalVecs :: SNat n -> Vector (Ordinal n) n
ordinalVecs SZ = Nil
ordinalVecs (SS sn) = OZ :- map OS (ordinalVecs sn)
ifoldl :: (a -> Index n -> b -> a) -> a -> Vector b n -> a
ifoldl fun a0 vs = foldl (\a (b, c) -> fun a b c) a0 $ zipSame (ordinalVecs $ sLength vs) vs
sized :: Lift t => [t] -> ExpQ
sized = sized' . P.map lift
sized' :: [ExpQ] -> ExpQ
sized' = P.foldr (\a b -> [| $a :- $b |]) [| Nil |]