{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
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 :: forall a. HasCallStack => a
impossible = forall a. HasCallStack => [Char] -> a
error [Char]
"ListN: internal error: the impossible happened"
newtype ListN (n :: Nat) a = ListN { forall (n :: Nat) a. ListN n a -> [a]
unListN :: [a] }
deriving (ListN n a -> ListN n a -> Bool
forall (n :: Nat) a. Eq a => ListN n a -> ListN n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ListN n a -> ListN n a -> Bool
$c/= :: forall (n :: Nat) a. Eq a => ListN n a -> ListN n a -> Bool
== :: ListN n a -> ListN n a -> Bool
$c== :: forall (n :: Nat) a. Eq a => ListN n a -> ListN n a -> Bool
Eq,ListN n a -> ListN n a -> Bool
ListN n a -> ListN n a -> Ordering
ListN n a -> ListN n a -> ListN n a
forall {n :: Nat} {a}. Ord a => Eq (ListN n a)
forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Ordering
forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> ListN n a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ListN n a -> ListN n a -> ListN n a
$cmin :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> ListN n a
max :: ListN n a -> ListN n a -> ListN n a
$cmax :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> ListN n a
>= :: ListN n a -> ListN n a -> Bool
$c>= :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
> :: ListN n a -> ListN n a -> Bool
$c> :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
<= :: ListN n a -> ListN n a -> Bool
$c<= :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
< :: ListN n a -> ListN n a -> Bool
$c< :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Bool
compare :: ListN n a -> ListN n a -> Ordering
$ccompare :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Ordering
Ord,Typeable,forall (n :: Nat) a x. Rep (ListN n a) x -> ListN n a
forall (n :: Nat) a x. ListN n a -> Rep (ListN n a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) a x. Rep (ListN n a) x -> ListN n a
$cfrom :: forall (n :: Nat) a x. ListN n a -> Rep (ListN n a) x
Generic)
instance Show a => Show (ListN n a) where
show :: ListN n a -> [Char]
show (ListN [a]
l) = forall a. Show a => a -> [Char]
show [a]
l
instance NormalForm a => NormalForm (ListN n a) where
toNormalForm :: ListN n a -> ()
toNormalForm (ListN [a]
l) = forall a. NormalForm a => a -> ()
toNormalForm [a]
l
toListN :: forall (n :: Nat) a . (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a)
toListN :: forall (n :: Nat) a.
(KnownNat n, NatWithinBound Int n) =>
[a] -> Maybe (ListN n a)
toListN [a]
l
| Int
expected forall a. Eq a => a -> a -> Bool
== forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (forall (t :: * -> *) a. Foldable t => t a -> Int
Prelude.length [a]
l) = forall a. a -> Maybe a
Just (forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l)
| Bool
otherwise = forall a. Maybe a
Nothing
where
expected :: Int
expected = forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
toListN_ :: forall n a . (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a
toListN_ :: forall (n :: Nat) a.
(HasCallStack, NatWithinBound Int n, KnownNat n) =>
[a] -> ListN n a
toListN_ [a]
l
| Int
expected forall a. Eq a => a -> a -> Bool
== Int
got = forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l
| Bool
otherwise = forall a. HasCallStack => [Char] -> a
error ([Char]
"toListN_: expecting list of " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Int
expected forall a. Semigroup a => a -> a -> a
<> [Char]
" elements, got " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Int
got forall a. Semigroup a => a -> a -> a
<> [Char]
" elements")
where
expected :: Int
expected = forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
got :: Int
got = forall (t :: * -> *) a. Foldable t => t a -> Int
Prelude.length [a]
l
replicateM :: forall (n :: Nat) m a . (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a)
replicateM :: forall (n :: Nat) (m :: * -> *) a.
(NatWithinBound Int n, Monad m, KnownNat n) =>
m a -> m (ListN n a)
replicateM m a
action = forall (n :: Nat) a. [a] -> ListN n a
ListN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
M.replicateM (forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) m a
action
sequence :: Monad m => ListN n (m a) -> m (ListN n a)
sequence :: forall (m :: * -> *) (n :: Nat) a.
Monad m =>
ListN n (m a) -> m (ListN n a)
sequence (ListN [m a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
M.sequence [m a]
l
sequence_ :: Monad m => ListN n (m a) -> m ()
sequence_ :: forall (m :: * -> *) (n :: Nat) a. Monad m => ListN n (m a) -> m ()
sequence_ (ListN [m a]
l) = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
M.sequence_ [m a]
l
mapM :: Monad m => (a -> m b) -> ListN n a -> m (ListN n b)
mapM :: forall (m :: * -> *) a b (n :: Nat).
Monad m =>
(a -> m b) -> ListN n a -> m (ListN n b)
mapM a -> m b
f (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
M.mapM a -> m b
f [a]
l
mapM_ :: Monad m => (a -> m b) -> ListN n a -> m ()
mapM_ :: forall (m :: * -> *) a b (n :: Nat).
Monad m =>
(a -> m b) -> ListN n a -> m ()
mapM_ a -> m b
f (ListN [a]
l) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
M.mapM_ a -> m b
f [a]
l
replicate :: forall (n :: Nat) a . (NatWithinBound Int n, KnownNat n) => a -> ListN n a
replicate :: forall (n :: Nat) a.
(NatWithinBound Int n, KnownNat n) =>
a -> ListN n a
replicate a
a = forall (n :: Nat) a. [a] -> ListN n a
ListN forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
Prelude.replicate (forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) a
a
uncons :: (1 <= n) => ListN n a -> (a, ListN (n-1) a)
uncons :: forall (n :: Nat) a. (1 <= n) => ListN n a -> (a, ListN (n - 1) a)
uncons (ListN (a
x:[a]
xs)) = (a
x, forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs)
uncons ListN n a
_ = forall a. HasCallStack => a
impossible
cons :: a -> ListN n a -> ListN (n+1) a
cons :: forall a (n :: Nat). a -> ListN n a -> ListN (n + 1) a
cons a
a (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN (a
a forall a. a -> [a] -> [a]
: [a]
l)
unsnoc :: (1 <= n) => ListN n a -> (ListN (n-1) a, a)
unsnoc :: forall (n :: Nat) a. (1 <= n) => ListN n a -> (ListN (n - 1) a, a)
unsnoc (ListN [a]
l) = (forall (n :: Nat) a. [a] -> ListN n a
ListN forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
Data.List.init [a]
l, forall a. [a] -> a
Data.List.last [a]
l)
snoc :: ListN n a -> a -> ListN (n+1) a
snoc :: forall (n :: Nat) a. ListN n a -> a -> ListN (n + 1) a
snoc (ListN [a]
l) a
a = forall (n :: Nat) a. [a] -> ListN n a
ListN ([a]
l forall a. [a] -> [a] -> [a]
Prelude.++ [a
a])
empty :: ListN 0 a
empty :: forall a. ListN 0 a
empty = forall (n :: Nat) a. [a] -> ListN n a
ListN []
length :: forall a (n :: Nat) . (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a
length :: forall a (n :: Nat).
(KnownNat n, NatWithinBound Int n) =>
ListN n a -> CountOf a
length ListN n a
_ = forall ty. Int -> CountOf ty
CountOf forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
create :: forall a (n :: Nat) . KnownNat n => (Natural -> a) -> ListN n a
create :: forall a (n :: Nat). KnownNat n => (Nat -> a) -> ListN n a
create Nat -> a
f = forall (n :: Nat) a. [a] -> ListN n a
ListN forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
Prelude.map (Nat -> a
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral) [Integer
0..(Integer
lenforall a. Subtractive a => a -> a -> Difference a
-Integer
1)]
where
len :: Integer
len = forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
createFrom :: forall a (n :: Nat) (start :: Nat) . (KnownNat n, KnownNat start)
=> Proxy start -> (Natural -> a) -> ListN n a
createFrom :: forall a (n :: Nat) (start :: Nat).
(KnownNat n, KnownNat start) =>
Proxy start -> (Nat -> a) -> ListN n a
createFrom Proxy start
p Nat -> a
f = forall (n :: Nat) a. [a] -> ListN n a
ListN forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
Prelude.map (Nat -> a
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral) [Integer
idx..(Integer
idxforall a. Additive a => a -> a -> a
+Integer
lenforall a. Subtractive a => a -> a -> Difference a
-Integer
1)]
where
len :: Integer
len = forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
idx :: Integer
idx = forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Proxy start
p
singleton :: a -> ListN 1 a
singleton :: forall a. a -> ListN 1 a
singleton a
a = forall (n :: Nat) a. [a] -> ListN n a
ListN [a
a]
elem :: Eq a => a -> ListN n a -> Bool
elem :: forall a (n :: Nat). Eq a => a -> ListN n a -> Bool
elem a
a (ListN [a]
l) = forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
Prelude.elem a
a [a]
l
append :: ListN n a -> ListN m a -> ListN (n+m) a
append :: forall (n :: Nat) a (m :: Nat).
ListN n a -> ListN m a -> ListN (n + m) a
append (ListN [a]
l1) (ListN [a]
l2) = forall (n :: Nat) a. [a] -> ListN n a
ListN ([a]
l1 forall a. Semigroup a => a -> a -> a
<> [a]
l2)
maximum :: (Ord a, 1 <= n) => ListN n a -> a
maximum :: forall a (n :: Nat). (Ord a, 1 <= n) => ListN n a -> a
maximum (ListN [a]
l) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum [a]
l
minimum :: (Ord a, 1 <= n) => ListN n a -> a
minimum :: forall a (n :: Nat). (Ord a, 1 <= n) => ListN n a -> a
minimum (ListN [a]
l) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.minimum [a]
l
head :: (1 <= n) => ListN n a -> a
head :: forall (n :: Nat) a. (1 <= n) => ListN n a -> a
head (ListN (a
x:[a]
_)) = a
x
head ListN n a
_ = forall a. HasCallStack => a
impossible
tail :: (1 <= n) => ListN n a -> ListN (n-1) a
tail :: forall (n :: Nat) a. (1 <= n) => ListN n a -> ListN (n - 1) a
tail (ListN (a
_:[a]
xs)) = forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs
tail ListN n a
_ = forall a. HasCallStack => a
impossible
init :: (1 <= n) => ListN n a -> ListN (n-1) a
init :: forall (n :: Nat) a. (1 <= n) => ListN n a -> ListN (n - 1) a
init (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
Data.List.init [a]
l
take :: forall a (m :: Nat) (n :: Nat) . (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a
take :: forall a (m :: Nat) (n :: Nat).
(KnownNat m, NatWithinBound Int m, m <= n) =>
ListN n a -> ListN m a
take (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall a. Int -> [a] -> [a]
Prelude.take Int
n [a]
l)
where n :: Int
n = forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (forall {k} (t :: k). Proxy t
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 :: forall a (d :: Nat) (m :: Nat) (n :: Nat).
(KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) =>
ListN n a -> ListN m a
drop (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall a. Int -> [a] -> [a]
Prelude.drop Int
n [a]
l)
where n :: Int
n = forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (forall {k} (t :: k). Proxy t
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 (n-m) a)
splitAt :: forall a (d :: Nat) (m :: Nat) (n :: Nat).
(KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) =>
ListN n a -> (ListN m a, ListN (n - m) a)
splitAt (ListN [a]
l) = let ([a]
l1, [a]
l2) = forall a. Int -> [a] -> ([a], [a])
Prelude.splitAt Int
n [a]
l in (forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l1, forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l2)
where n :: Int
n = forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (forall {k} (t :: k). Proxy t
Proxy :: Proxy d)
indexStatic :: forall i n a . (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a
indexStatic :: forall (i :: Nat) (n :: Nat) a.
(KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) =>
ListN n a -> a
indexStatic (ListN [a]
l) = [a]
l forall a. [a] -> Offset a -> a
!! (forall (n :: Nat) ty (proxy :: Nat -> *).
(KnownNat n, NatWithinBound (Offset ty) n) =>
proxy n -> Offset ty
natValOffset (forall {k} (t :: k). Proxy t
Proxy :: Proxy i))
index :: ListN n ty -> Offset ty -> ty
index :: forall (n :: Nat) ty. ListN n ty -> Offset ty -> ty
index (ListN [ty]
l) Offset ty
ofs = [ty]
l forall a. [a] -> Offset a -> a
!! Offset ty
ofs
updateAt :: forall n a
. Offset a
-> (a -> a)
-> ListN n a
-> ListN n a
updateAt :: forall (n :: Nat) a. Offset a -> (a -> a) -> ListN n a -> ListN n a
updateAt Offset a
o a -> a
f (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN (Offset a -> [a] -> [a]
doUpdate Offset a
0 [a]
l)
where doUpdate :: Offset a -> [a] -> [a]
doUpdate Offset a
_ [] = []
doUpdate Offset a
i (a
x:[a]
xs)
| Offset a
i forall a. Eq a => a -> a -> Bool
== Offset a
o = a -> a
f a
x forall a. a -> [a] -> [a]
: [a]
xs
| Bool
otherwise = a
x forall a. a -> [a] -> [a]
: Offset a -> [a] -> [a]
doUpdate (Offset a
iforall a. Additive a => a -> a -> a
+Offset a
1) [a]
xs
map :: (a -> b) -> ListN n a -> ListN n b
map :: forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
map a -> b
f (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall a b. (a -> b) -> [a] -> [b]
Prelude.map a -> b
f [a]
l)
mapi :: (Natural -> a -> b) -> ListN n a -> ListN n b
mapi :: forall a b (n :: Nat). (Nat -> a -> b) -> ListN n a -> ListN n b
mapi Nat -> a -> b
f (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Nat -> [a] -> [b]
loop Nat
0 forall a b. (a -> b) -> a -> b
$ [a]
l
where loop :: Nat -> [a] -> [b]
loop Nat
_ [] = []
loop Nat
i (a
x:[a]
xs) = Nat -> a -> b
f Nat
i a
x forall a. a -> [a] -> [a]
: Nat -> [a] -> [b]
loop (Nat
iforall a. Additive a => a -> a -> a
+Nat
1) [a]
xs
foldl :: (b -> a -> b) -> b -> ListN n a -> b
foldl :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b
foldl b -> a -> b
f b
acc (ListN [a]
l) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Prelude.foldl b -> a -> b
f b
acc [a]
l
foldl' :: (b -> a -> b) -> b -> ListN n a -> b
foldl' :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b
foldl' b -> a -> b
f b
acc (ListN [a]
l) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Data.List.foldl' b -> a -> b
f b
acc [a]
l
foldl1' :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldl1' :: forall (n :: Nat) a. (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldl1' a -> a -> a
f (ListN [a]
l) = forall a. (a -> a -> a) -> [a] -> a
Data.List.foldl1' a -> a -> a
f [a]
l
foldr :: (a -> b -> b) -> b -> ListN n a -> b
foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> ListN n a -> b
foldr a -> b -> b
f b
acc (ListN [a]
l) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Prelude.foldr a -> b -> b
f b
acc [a]
l
foldr1 :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldr1 :: forall (n :: Nat) a. (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldr1 a -> a -> a
f (ListN [a]
l) = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Prelude.foldr1 a -> a -> a
f [a]
l
scanl' :: (b -> a -> b) -> b -> ListN n a -> ListN (n+1) b
scanl' :: forall b a (n :: Nat).
(b -> a -> b) -> b -> ListN n a -> ListN (n + 1) b
scanl' b -> a -> b
f b
initialAcc (ListN [a]
start) = forall (n :: Nat) a. [a] -> ListN n a
ListN (b -> [a] -> [b]
go b
initialAcc [a]
start)
where
go :: b -> [a] -> [b]
go !b
acc [a]
l = b
acc forall a. a -> [a] -> [a]
: case [a]
l of
[] -> []
(a
x:[a]
xs) -> b -> [a] -> [b]
go (b -> a -> b
f b
acc a
x) [a]
xs
scanl1' :: (a -> a -> a) -> ListN n a -> ListN n a
scanl1' :: forall a (n :: Nat). (a -> a -> a) -> ListN n a -> ListN n a
scanl1' a -> a -> a
f (ListN [a]
l) = case [a]
l of
[] -> forall (n :: Nat) a. [a] -> ListN n a
ListN []
(a
x:[a]
xs) -> forall (n :: Nat) a. [a] -> ListN n a
ListN forall a b. (a -> b) -> a -> b
$ forall b a. (b -> a -> b) -> b -> [a] -> [b]
Data.List.scanl' a -> a -> a
f a
x [a]
xs
reverse :: ListN n a -> ListN n a
reverse :: forall (n :: Nat) a. ListN n a -> ListN n a
reverse (ListN [a]
l) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall a. [a] -> [a]
Prelude.reverse [a]
l)
zip :: ListN n a -> ListN n b -> ListN n (a,b)
zip :: forall (n :: Nat) a b. ListN n a -> ListN n b -> ListN n (a, b)
zip (ListN [a]
l1) (ListN [b]
l2) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall a b. [a] -> [b] -> [(a, b)]
Prelude.zip [a]
l1 [b]
l2)
unzip :: ListN n (a,b) -> (ListN n a, ListN n b)
unzip :: forall (n :: Nat) a b. ListN n (a, b) -> (ListN n a, ListN n b)
unzip ListN n (a, b)
l = (forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
map forall a b. (a, b) -> a
fst ListN n (a, b)
l, forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
map forall a b. (a, b) -> b
snd ListN n (a, b)
l)
zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a,b,c)
zip3 :: forall (n :: Nat) a b c.
ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c)
zip3 (ListN [a]
x1) (ListN [b]
x2) (ListN [c]
x3) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall {a} {b} {c}. [a] -> [b] -> [c] -> [(a, b, c)]
loop [a]
x1 [b]
x2 [c]
x3)
where loop :: [a] -> [b] -> [c] -> [(a, b, c)]
loop (a
l1:[a]
l1s) (b
l2:[b]
l2s) (c
l3:[c]
l3s) = (a
l1,b
l2,c
l3) forall a. a -> [a] -> [a]
: [a] -> [b] -> [c] -> [(a, b, c)]
loop [a]
l1s [b]
l2s [c]
l3s
loop [] [b]
_ [c]
_ = []
loop [a]
_ [b]
_ [c]
_ = forall a. HasCallStack => a
impossible
zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a,b,c,d)
zip4 :: forall (n :: Nat) a b c d.
ListN n a
-> ListN n b -> ListN n c -> ListN n d -> ListN n (a, b, c, d)
zip4 (ListN [a]
x1) (ListN [b]
x2) (ListN [c]
x3) (ListN [d]
x4) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall {a} {b} {c} {d}. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
loop [a]
x1 [b]
x2 [c]
x3 [d]
x4)
where loop :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
loop (a
l1:[a]
l1s) (b
l2:[b]
l2s) (c
l3:[c]
l3s) (d
l4:[d]
l4s) = (a
l1,b
l2,c
l3,d
l4) forall a. a -> [a] -> [a]
: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
loop [a]
l1s [b]
l2s [c]
l3s [d]
l4s
loop [] [b]
_ [c]
_ [d]
_ = []
loop [a]
_ [b]
_ [c]
_ [d]
_ = forall a. HasCallStack => a
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 :: forall (n :: Nat) a b c d e.
ListN n a
-> ListN n b
-> ListN n c
-> ListN n d
-> ListN n e
-> ListN n (a, b, c, d, e)
zip5 (ListN [a]
x1) (ListN [b]
x2) (ListN [c]
x3) (ListN [d]
x4) (ListN [e]
x5) = forall (n :: Nat) a. [a] -> ListN n a
ListN (forall {a} {b} {c} {d} {e}.
[a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
loop [a]
x1 [b]
x2 [c]
x3 [d]
x4 [e]
x5)
where loop :: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
loop (a
l1:[a]
l1s) (b
l2:[b]
l2s) (c
l3:[c]
l3s) (d
l4:[d]
l4s) (e
l5:[e]
l5s) = (a
l1,b
l2,c
l3,d
l4,e
l5) forall a. a -> [a] -> [a]
: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
loop [a]
l1s [b]
l2s [c]
l3s [d]
l4s [e]
l5s
loop [] [b]
_ [c]
_ [d]
_ [e]
_ = []
loop [a]
_ [b]
_ [c]
_ [d]
_ [e]
_ = forall a. HasCallStack => a
impossible
zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith :: forall a b x (n :: Nat).
(a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith a -> b -> x
f (ListN (a
v1:[a]
vs)) (ListN (b
w1:[b]
ws)) = forall (n :: Nat) a. [a] -> ListN n a
ListN (a -> b -> x
f a
v1 b
w1 forall a. a -> [a] -> [a]
: forall (n :: Nat) a. ListN n a -> [a]
unListN (forall a b x (n :: Nat).
(a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith a -> b -> x
f (forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) (forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws)))
zipWith a -> b -> x
_ (ListN []) ListN n b
_ = forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith a -> b -> x
_ ListN n a
_ ListN n b
_ = forall a. HasCallStack => a
impossible
zipWith3 :: (a -> b -> c -> x)
-> ListN n a
-> ListN n b
-> ListN n c
-> ListN n x
zipWith3 :: forall a b c x (n :: Nat).
(a -> b -> c -> x)
-> ListN n a -> ListN n b -> ListN n c -> ListN n x
zipWith3 a -> b -> c -> x
f (ListN (a
v1:[a]
vs)) (ListN (b
w1:[b]
ws)) (ListN (c
x1:[c]
xs)) =
forall (n :: Nat) a. [a] -> ListN n a
ListN (a -> b -> c -> x
f a
v1 b
w1 c
x1 forall a. a -> [a] -> [a]
: forall (n :: Nat) a. ListN n a -> [a]
unListN (forall a b c x (n :: Nat).
(a -> b -> c -> x)
-> ListN n a -> ListN n b -> ListN n c -> ListN n x
zipWith3 a -> b -> c -> x
f (forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) (forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) (forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs)))
zipWith3 a -> b -> c -> x
_ (ListN []) ListN n b
_ ListN n c
_ = forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith3 a -> b -> c -> x
_ ListN n a
_ ListN n b
_ ListN n c
_ = forall a. HasCallStack => a
impossible
zipWith4 :: (a -> b -> c -> d -> x)
-> ListN n a
-> ListN n b
-> ListN n c
-> ListN n d
-> ListN n x
zipWith4 :: forall a b c d x (n :: Nat).
(a -> b -> c -> d -> x)
-> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x
zipWith4 a -> b -> c -> d -> x
f (ListN (a
v1:[a]
vs)) (ListN (b
w1:[b]
ws)) (ListN (c
x1:[c]
xs)) (ListN (d
y1:[d]
ys)) =
forall (n :: Nat) a. [a] -> ListN n a
ListN (a -> b -> c -> d -> x
f a
v1 b
w1 c
x1 d
y1 forall a. a -> [a] -> [a]
: forall (n :: Nat) a. ListN n a -> [a]
unListN (forall a b c d x (n :: Nat).
(a -> b -> c -> d -> x)
-> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x
zipWith4 a -> b -> c -> d -> x
f (forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) (forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) (forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs) (forall (n :: Nat) a. [a] -> ListN n a
ListN [d]
ys)))
zipWith4 a -> b -> c -> d -> x
_ (ListN []) ListN n b
_ ListN n c
_ ListN n d
_ = forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith4 a -> b -> c -> d -> x
_ ListN n a
_ ListN n b
_ ListN n c
_ ListN n d
_ = forall a. HasCallStack => a
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 :: forall a b c d e x (n :: Nat).
(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 a -> b -> c -> d -> e -> x
f (ListN (a
v1:[a]
vs)) (ListN (b
w1:[b]
ws)) (ListN (c
x1:[c]
xs)) (ListN (d
y1:[d]
ys)) (ListN (e
z1:[e]
zs)) =
forall (n :: Nat) a. [a] -> ListN n a
ListN (a -> b -> c -> d -> e -> x
f a
v1 b
w1 c
x1 d
y1 e
z1 forall a. a -> [a] -> [a]
: forall (n :: Nat) a. ListN n a -> [a]
unListN (forall a b c d e x (n :: Nat).
(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 a -> b -> c -> d -> e -> x
f (forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) (forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) (forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs) (forall (n :: Nat) a. [a] -> ListN n a
ListN [d]
ys) (forall (n :: Nat) a. [a] -> ListN n a
ListN [e]
zs)))
zipWith5 a -> b -> c -> d -> e -> x
_ (ListN []) ListN n b
_ ListN n c
_ ListN n d
_ ListN n e
_ = forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith5 a -> b -> c -> d -> e -> x
_ ListN n a
_ ListN n b
_ ListN n c
_ ListN n d
_ ListN n e
_ = forall a. HasCallStack => a
impossible