module Basement.Sized.List
( ListN
, toListN
, toListN_
, unListN
, length
, create
, createFrom
, empty
, singleton
, uncons
, cons
, unsnoc
, snoc
, index
, indexStatic
, updateAt
, map
, mapi
, elem
, foldl
, foldl'
, foldl1'
, scanl'
, scanl1'
, foldr
, foldr1
, reverse
, append
, minimum
, maximum
, head
, tail
, init
, take
, drop
, splitAt
, zip, zip3, zip4, zip5
, unzip
, zipWith, zipWith3, zipWith4, zipWith5
, replicate
, replicateM
, sequence
, sequence_
, mapM
, mapM_
) where
import Data.Proxy
import qualified Data.List
import Basement.Compat.Base
import Basement.Compat.CallStack
import Basement.Compat.Natural
import Basement.Nat
import Basement.NormalForm
import Basement.Numerical.Additive
import Basement.Numerical.Subtractive
import Basement.Types.OffsetSize
import Basement.Compat.ExtList ((!!))
import qualified Prelude
import qualified Control.Monad as M (replicateM, mapM, mapM_, sequence, sequence_)
impossible :: HasCallStack => a
impossible = error "ListN: internal error: the impossible happened"
newtype ListN (n :: Nat) a = ListN { unListN :: [a] }
deriving (Eq,Ord,Typeable,Generic)
instance Show a => Show (ListN n a) where
show (ListN l) = show l
instance NormalForm a => NormalForm (ListN n a) where
toNormalForm (ListN l) = toNormalForm l
toListN :: forall (n :: Nat) a . (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a)
toListN l
| expected == Prelude.fromIntegral (Prelude.length l) = Just (ListN l)
| otherwise = Nothing
where
expected = natValInt (Proxy :: Proxy n)
toListN_ :: forall n a . (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a
toListN_ l
| expected == got = ListN l
| otherwise = error ("toListN_: expecting list of " <> show expected <> " elements, got " <> show got <> " elements")
where
expected = natValInt (Proxy :: Proxy n)
got = Prelude.length l
replicateM :: forall (n :: Nat) m a . (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a)
replicateM action = ListN <$> M.replicateM (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) action
sequence :: Monad m => ListN n (m a) -> m (ListN n a)
sequence (ListN l) = ListN <$> M.sequence l
sequence_ :: Monad m => ListN n (m a) -> m ()
sequence_ (ListN l) = M.sequence_ l
mapM :: Monad m => (a -> m b) -> ListN n a -> m (ListN n b)
mapM f (ListN l) = ListN <$> M.mapM f l
mapM_ :: Monad m => (a -> m b) -> ListN n a -> m ()
mapM_ f (ListN l) = M.mapM_ f l
replicate :: forall (n :: Nat) a . (NatWithinBound Int n, KnownNat n) => a -> ListN n a
replicate a = ListN $ Prelude.replicate (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) a
uncons :: (1 <= n) => ListN n a -> (a, ListN (n1) a)
uncons (ListN (x:xs)) = (x, ListN xs)
uncons _ = impossible
cons :: a -> ListN n a -> ListN (n+1) a
cons a (ListN l) = ListN (a : l)
unsnoc :: (1 <= n) => ListN n a -> (ListN (n1) a, a)
unsnoc (ListN l) = (ListN $ Data.List.init l, Data.List.last l)
snoc :: ListN n a -> a -> ListN (n+1) a
snoc (ListN l) a = ListN (l Prelude.++ [a])
empty :: ListN 0 a
empty = ListN []
length :: forall a (n :: Nat) . (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a
length _ = CountOf $ natValInt (Proxy :: Proxy n)
create :: forall a (n :: Nat) . KnownNat n => (Natural -> a) -> ListN n a
create f = ListN $ Prelude.map (f . Prelude.fromIntegral) [0..(len1)]
where
len = natVal (Proxy :: Proxy n)
createFrom :: forall a (n :: Nat) (start :: Nat) . (KnownNat n, KnownNat start)
=> Proxy start -> (Natural -> a) -> ListN n a
createFrom p f = ListN $ Prelude.map (f . Prelude.fromIntegral) [idx..(idx+len1)]
where
len = natVal (Proxy :: Proxy n)
idx = natVal p
singleton :: a -> ListN 1 a
singleton a = ListN [a]
elem :: Eq a => a -> ListN n a -> Bool
elem a (ListN l) = Prelude.elem a l
append :: ListN n a -> ListN m a -> ListN (n+m) a
append (ListN l1) (ListN l2) = ListN (l1 <> l2)
maximum :: (Ord a, 1 <= n) => ListN n a -> a
maximum (ListN l) = Prelude.maximum l
minimum :: (Ord a, 1 <= n) => ListN n a -> a
minimum (ListN l) = Prelude.minimum l
head :: (1 <= n) => ListN n a -> a
head (ListN (x:_)) = x
head _ = impossible
tail :: (1 <= n) => ListN n a -> ListN (n1) a
tail (ListN (_:xs)) = ListN xs
tail _ = impossible
init :: (1 <= n) => ListN n a -> ListN (n1) a
init (ListN l) = ListN $ Data.List.init l
take :: forall a (m :: Nat) (n :: Nat) . (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a
take (ListN l) = ListN (Prelude.take n l)
where n = natValInt (Proxy :: Proxy m)
drop :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n m) ~ d, m <= n) => ListN n a -> ListN m a
drop (ListN l) = ListN (Prelude.drop n l)
where n = natValInt (Proxy :: Proxy d)
splitAt :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n m) ~ d, m <= n) => ListN n a -> (ListN m a, ListN (nm) a)
splitAt (ListN l) = let (l1, l2) = Prelude.splitAt n l in (ListN l1, ListN l2)
where n = natValInt (Proxy :: Proxy d)
indexStatic :: forall i n a . (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a
indexStatic (ListN l) = l !! (natValOffset (Proxy :: Proxy i))
index :: ListN n ty -> Offset ty -> ty
index (ListN l) ofs = l !! ofs
updateAt :: forall n a
. Offset a
-> (a -> a)
-> ListN n a
-> ListN n a
updateAt o f (ListN l) = ListN (doUpdate 0 l)
where doUpdate _ [] = []
doUpdate i (x:xs)
| i == o = f x : xs
| otherwise = x : doUpdate (i+1) xs
map :: (a -> b) -> ListN n a -> ListN n b
map f (ListN l) = ListN (Prelude.map f l)
mapi :: (Natural -> a -> b) -> ListN n a -> ListN n b
mapi f (ListN l) = ListN . loop 0 $ l
where loop _ [] = []
loop i (x:xs) = f i x : loop (i+1) xs
foldl :: (b -> a -> b) -> b -> ListN n a -> b
foldl f acc (ListN l) = Prelude.foldl f acc l
foldl' :: (b -> a -> b) -> b -> ListN n a -> b
foldl' f acc (ListN l) = Data.List.foldl' f acc l
foldl1' :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldl1' f (ListN l) = Data.List.foldl1' f l
foldr :: (a -> b -> b) -> b -> ListN n a -> b
foldr f acc (ListN l) = Prelude.foldr f acc l
foldr1 :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldr1 f (ListN l) = Prelude.foldr1 f l
scanl' :: (b -> a -> b) -> b -> ListN n a -> ListN (n+1) b
scanl' f initialAcc (ListN start) = ListN (go initialAcc start)
where
go !acc l = acc : case l of
[] -> []
(x:xs) -> go (f acc x) xs
scanl1' :: (a -> a -> a) -> ListN n a -> ListN n a
scanl1' f (ListN l) = case l of
[] -> ListN []
(x:xs) -> ListN $ Data.List.scanl' f x xs
reverse :: ListN n a -> ListN n a
reverse (ListN l) = ListN (Prelude.reverse l)
zip :: ListN n a -> ListN n b -> ListN n (a,b)
zip (ListN l1) (ListN l2) = ListN (Prelude.zip l1 l2)
unzip :: ListN n (a,b) -> (ListN n a, ListN n b)
unzip l = (map fst l, map snd l)
zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a,b,c)
zip3 (ListN x1) (ListN x2) (ListN x3) = ListN (loop x1 x2 x3)
where loop (l1:l1s) (l2:l2s) (l3:l3s) = (l1,l2,l3) : loop l1s l2s l3s
loop [] _ _ = []
loop _ _ _ = impossible
zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a,b,c,d)
zip4 (ListN x1) (ListN x2) (ListN x3) (ListN x4) = ListN (loop x1 x2 x3 x4)
where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) = (l1,l2,l3,l4) : loop l1s l2s l3s l4s
loop [] _ _ _ = []
loop _ _ _ _ = impossible
zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a,b,c,d,e)
zip5 (ListN x1) (ListN x2) (ListN x3) (ListN x4) (ListN x5) = ListN (loop x1 x2 x3 x4 x5)
where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) (l5:l5s) = (l1,l2,l3,l4,l5) : loop l1s l2s l3s l4s l5s
loop [] _ _ _ _ = []
loop _ _ _ _ _ = impossible
zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith f (ListN (v1:vs)) (ListN (w1:ws)) = ListN (f v1 w1 : unListN (zipWith f (ListN vs) (ListN ws)))
zipWith _ (ListN []) _ = ListN []
zipWith _ _ _ = impossible
zipWith3 :: (a -> b -> c -> x)
-> ListN n a
-> ListN n b
-> ListN n c
-> ListN n x
zipWith3 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) =
ListN (f v1 w1 x1 : unListN (zipWith3 f (ListN vs) (ListN ws) (ListN xs)))
zipWith3 _ (ListN []) _ _ = ListN []
zipWith3 _ _ _ _ = impossible
zipWith4 :: (a -> b -> c -> d -> x)
-> ListN n a
-> ListN n b
-> ListN n c
-> ListN n d
-> ListN n x
zipWith4 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) =
ListN (f v1 w1 x1 y1 : unListN (zipWith4 f (ListN vs) (ListN ws) (ListN xs) (ListN ys)))
zipWith4 _ (ListN []) _ _ _ = ListN []
zipWith4 _ _ _ _ _ = impossible
zipWith5 :: (a -> b -> c -> d -> e -> x)
-> ListN n a
-> ListN n b
-> ListN n c
-> ListN n d
-> ListN n e
-> ListN n x
zipWith5 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) (ListN (z1:zs)) =
ListN (f v1 w1 x1 y1 z1 : unListN (zipWith5 f (ListN vs) (ListN ws) (ListN xs) (ListN ys) (ListN zs)))
zipWith5 _ (ListN []) _ _ _ _ = ListN []
zipWith5 _ _ _ _ _ _ = impossible