-- |
-- Module      : Basement.Sized.List
-- License     : BSD-style
-- Maintainer  : Vincent Hanquez <vincent@snarc.org>
-- Stability   : experimental
-- Portability : portable
--
-- A Nat-sized list abstraction
--
-- Using this module is limited to GHC 7.10 and above.
--
{-# 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
    -- * Applicative And Monadic
    , 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 = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"ListN: internal error: the impossible happened"

-- | A Typed-level sized List equivalent to [a]
newtype ListN (n :: Nat) a = ListN { forall (n :: Nat) a. ListN n a -> [a]
unListN :: [a] }
    deriving (ListN n a -> ListN n a -> Bool
(ListN n a -> ListN n a -> Bool)
-> (ListN n a -> ListN n a -> Bool) -> Eq (ListN n a)
forall (n :: Nat) a. Eq a => ListN n a -> ListN n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: ListN n a -> ListN n a -> Bool
Eq,Eq (ListN n a)
Eq (ListN n a) =>
(ListN n a -> ListN n a -> Ordering)
-> (ListN n a -> ListN n a -> Bool)
-> (ListN n a -> ListN n a -> Bool)
-> (ListN n a -> ListN n a -> Bool)
-> (ListN n a -> ListN n a -> Bool)
-> (ListN n a -> ListN n a -> ListN n a)
-> (ListN n a -> ListN n a -> ListN n a)
-> Ord (ListN n a)
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
$ccompare :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> Ordering
compare :: ListN n a -> ListN n a -> Ordering
$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
>= :: ListN n a -> ListN n a -> Bool
$cmax :: 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
$cmin :: forall (n :: Nat) a. Ord a => ListN n a -> ListN n a -> ListN n a
min :: ListN n a -> ListN n a -> ListN n a
Ord,Typeable,(forall x. ListN n a -> Rep (ListN n a) x)
-> (forall x. Rep (ListN n a) x -> ListN n a)
-> Generic (ListN n a)
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 x. Rep (ListN n a) x -> ListN n a
forall 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
$cfrom :: forall (n :: Nat) a x. ListN n a -> Rep (ListN n a) x
from :: forall x. ListN n a -> Rep (ListN n a) x
$cto :: forall (n :: Nat) a x. Rep (ListN n a) x -> ListN n a
to :: forall x. Rep (ListN n a) x -> ListN n a
Generic)

instance Show a => Show (ListN n a) where
    show :: ListN n a -> [Char]
show (ListN [a]
l) = [a] -> [Char]
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) = [a] -> ()
forall a. NormalForm a => a -> ()
toNormalForm [a]
l

-- | Try to create a ListN from a List, succeeding if the length is correct
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Int
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
Prelude.length [a]
l) = ListN n a -> Maybe (ListN n a)
forall a. a -> Maybe a
Just ([a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l)
    | Bool
otherwise                                           = Maybe (ListN n a)
forall a. Maybe a
Nothing
  where
    expected :: Int
expected = Proxy n -> Int
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)

-- | Create a ListN from a List, expecting a given length
--
-- If this list contains more or less than the expected length of the resulting type,
-- then an asynchronous error is raised. use 'toListN' for a more friendly functions
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
got = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l
    | Bool
otherwise       = [Char] -> ListN n a
forall a. HasCallStack => [Char] -> a
error ([Char]
"toListN_: expecting list of " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
expected [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" elements, got " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
got [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" elements")
  where
    expected :: Int
expected = Proxy n -> Int
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
    got :: Int
got      = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
Prelude.length [a]
l

-- | performs a monadic action n times, gathering the results in a List of size n.
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 = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN n a) -> m [a] -> m (ListN n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m a -> m [a]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
M.replicateM (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) m a
action

-- | Evaluate each monadic action in the list sequentially, and collect the results.
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) = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN n a) -> m [a] -> m (ListN n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m a] -> m [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
M.sequence [m a]
l

-- | Evaluate each monadic action in the list sequentially, and ignore the results.
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) = [m a] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
M.sequence_ [m a]
l

-- | Map each element of a List to a monadic action, evaluate these
-- actions sequentially and collect the results
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) = [b] -> ListN n b
forall (n :: Nat) a. [a] -> ListN n a
ListN ([b] -> ListN n b) -> m [b] -> m (ListN n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> m b) -> [a] -> m [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
M.mapM a -> m b
f [a]
l

-- | Map each element of a List to a monadic action, evaluate these
-- actions sequentially and ignore the results
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) = (a -> m b) -> [a] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
M.mapM_ a -> m b
f [a]
l

-- | Create a list of n elements where each element is the element in argument
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 = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN n a) -> [a] -> ListN n a
forall a b. (a -> b) -> a -> b
$ Int -> a -> [a]
forall a. Int -> a -> [a]
Prelude.replicate (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) a
a

-- | Decompose a list into its head and tail.
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, [a] -> ListN (n - 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs)
uncons ListN n a
_ = (a, ListN (n - 1) a)
forall a. HasCallStack => a
impossible

-- | prepend an element to the list
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) = [a] -> ListN (n + 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
l)

-- | Decompose a list into its first elements and the last.
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) = ([a] -> ListN (n - 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN (n - 1) a) -> [a] -> ListN (n - 1) a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. HasCallStack => [a] -> [a]
Data.List.init [a]
l, [a] -> a
forall a. HasCallStack => [a] -> a
Data.List.last [a]
l)

-- | append an element to the list
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 = [a] -> ListN (n + 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a]
l [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
Prelude.++ [a
a])

-- | Create an empty list of a
empty :: ListN 0 a
empty :: forall a. ListN 0 a
empty = [a] -> ListN 0 a
forall (n :: Nat) a. [a] -> ListN n a
ListN []

-- | Get the length of a list
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
_ = Int -> CountOf a
forall ty. Int -> CountOf ty
CountOf (Int -> CountOf a) -> Int -> CountOf a
forall a b. (a -> b) -> a -> b
$ Proxy n -> Int
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)

-- | Create a new list of size n, repeately calling f from 0 to n-1
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 = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN n a) -> [a] -> ListN n a
forall a b. (a -> b) -> a -> b
$ (Integer -> a) -> [Integer] -> [a]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (Nat -> a
f (Nat -> a) -> (Integer -> Nat) -> Integer -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Nat
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral) [Integer
0..(Integer
lenInteger -> Integer -> Difference Integer
forall a. Subtractive a => a -> a -> Difference a
-Integer
1)]
  where
    len :: Integer
len = Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)

-- | Same as create but apply an offset
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 = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN n a) -> [a] -> ListN n a
forall a b. (a -> b) -> a -> b
$ (Integer -> a) -> [Integer] -> [a]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (Nat -> a
f (Nat -> a) -> (Integer -> Nat) -> Integer -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Nat
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral) [Integer
idx..(Integer
idxInteger -> Integer -> Integer
forall a. Additive a => a -> a -> a
+Integer
lenInteger -> Integer -> Difference Integer
forall a. Subtractive a => a -> a -> Difference a
-Integer
1)]
  where
    len :: Integer
len = Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
    idx :: Integer
idx = Proxy start -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Proxy start
p

-- | create a list of 1 element
singleton :: a -> ListN 1 a
singleton :: forall a. a -> ListN 1 a
singleton a
a = [a] -> ListN 1 a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a
a]

-- | Check if a list contains the element 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) = a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
Prelude.elem a
a [a]
l

-- | Append 2 list together returning the new list
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) = [a] -> ListN (n + m) a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a]
l1 [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
l2)

-- | Get the maximum element of a list
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) = [a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum [a]
l

-- | Get the minimum element of a list
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) = [a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.minimum [a]
l

-- | Get the head element of a list
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
_ = a
forall a. HasCallStack => a
impossible

-- | Get the tail of a list
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)) = [a] -> ListN (n - 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs
tail ListN n a
_ = ListN (n - 1) a
forall a. HasCallStack => a
impossible

-- | Get the list with the last element missing
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) = [a] -> ListN (n - 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN (n - 1) a) -> [a] -> ListN (n - 1) a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. HasCallStack => [a] -> [a]
Data.List.init [a]
l

-- | Take m elements from the beggining of the list.
--
-- The number of elements need to be less or equal to the list in argument
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) = [a] -> ListN m a
forall (n :: Nat) a. [a] -> ListN n a
ListN (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
Prelude.take Int
n [a]
l)
  where n :: Int
n = Proxy m -> Int
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)

-- | Drop elements from a list keeping the m remaining elements
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) = [a] -> ListN m a
forall (n :: Nat) a. [a] -> ListN n a
ListN (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
Prelude.drop Int
n [a]
l)
  where n :: Int
n = Proxy d -> Int
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (Proxy d
forall {k} (t :: k). Proxy t
Proxy :: Proxy d)

-- | Split a list into two, returning 2 lists
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) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
Prelude.splitAt Int
n [a]
l in ([a] -> ListN m a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l1, [a] -> ListN d a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
l2)
  where n :: Int
n = Proxy d -> Int
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Int n) =>
proxy n -> Int
natValInt (Proxy d
forall {k} (t :: k). Proxy t
Proxy :: Proxy d)

-- | Get the i'th elements
--
-- This only works with TypeApplication:
--
-- > indexStatic @1 (toListN_ [1,2,3] :: ListN 3 Int)
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 [a] -> Offset a -> a
forall a. [a] -> Offset a -> a
!! (Proxy i -> Offset a
forall (n :: Nat) ty (proxy :: Nat -> *).
(KnownNat n, NatWithinBound (Offset ty) n) =>
proxy n -> Offset ty
natValOffset (Proxy i
forall {k} (t :: k). Proxy t
Proxy :: Proxy i))

-- | Get the i'the element
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 [ty] -> Offset ty -> ty
forall a. [a] -> Offset a -> a
!! Offset ty
ofs

-- | Update the value in a list at a specific location
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) = [a] -> ListN n a
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 Offset a -> Offset a -> Bool
forall a. Eq a => a -> a -> Bool
== Offset a
o      = a -> a
f a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs
            | Bool
otherwise   = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Offset a -> [a] -> [a]
doUpdate (Offset a
iOffset a -> Offset a -> Offset a
forall a. Additive a => a -> a -> a
+Offset a
1) [a]
xs

-- | Map all elements in a list
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) = [b] -> ListN n b
forall (n :: Nat) a. [a] -> ListN n a
ListN ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map a -> b
f [a]
l)

-- | Map all elements in a list with an additional index
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) = [b] -> ListN n b
forall (n :: Nat) a. [a] -> ListN n a
ListN ([b] -> ListN n b) -> ([a] -> [b]) -> [a] -> ListN n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 ([a] -> ListN n b) -> [a] -> ListN n b
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 b -> [b] -> [b]
forall a. a -> [a] -> [a]
: Nat -> [a] -> [b]
loop (Nat
iNat -> Nat -> Nat
forall a. Additive a => a -> a -> a
+Nat
1) [a]
xs

-- | Fold all elements from left
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) = (b -> a -> b) -> b -> [a] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Prelude.foldl b -> a -> b
f b
acc [a]
l

-- | Fold all elements from left strictly
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) = (b -> a -> b) -> b -> [a] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Data.List.foldl' b -> a -> b
f b
acc [a]
l

-- | Fold all elements from left strictly with a first element
-- as the accumulator
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) = (a -> a -> a) -> [a] -> a
forall a. HasCallStack => (a -> a -> a) -> [a] -> a
Data.List.foldl1' a -> a -> a
f [a]
l

-- | Fold all elements from right
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) = (a -> b -> b) -> b -> [a] -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Prelude.foldr a -> b -> b
f b
acc [a]
l

-- | Fold all elements from right assuming at least one element is in the list.
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) = (a -> a -> a) -> [a] -> a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Prelude.foldr1 a -> a -> a
f [a]
l

-- | 'scanl' is similar to 'foldl', but returns a list of successive
-- reduced values from the left
--
-- > scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]
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) = [b] -> ListN (n + 1) b
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 b -> [b] -> [b]
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' is a variant of 'scanl' that has no starting value argument:
--
-- > scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]
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
                        []     -> [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN []
                        (a
x:[a]
xs) -> [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> ListN n a) -> [a] -> ListN n a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> a -> [a] -> [a]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
Data.List.scanl' a -> a -> a
f a
x [a]
xs

-- | Reverse a list
reverse :: ListN n a -> ListN n a
reverse :: forall (n :: Nat) a. ListN n a -> ListN n a
reverse (ListN [a]
l) = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> [a]
forall a. [a] -> [a]
Prelude.reverse [a]
l)

-- | Zip 2 lists of the same size, returning a new list of
-- the tuple of each elements
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) = [(a, b)] -> ListN n (a, b)
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
Prelude.zip [a]
l1 [b]
l2)

-- | Unzip a list of tuple, to 2 List of the deconstructed tuples
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 = (((a, b) -> a) -> ListN n (a, b) -> ListN n a
forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
map (a, b) -> a
forall a b. (a, b) -> a
fst ListN n (a, b)
l, ((a, b) -> b) -> ListN n (a, b) -> ListN n b
forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
map (a, b) -> b
forall a b. (a, b) -> b
snd ListN n (a, b)
l)

-- | Zip 3 lists of the same size
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) = [(a, b, c)] -> ListN n (a, b, c)
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> [b] -> [c] -> [(a, b, c)]
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) (a, b, c) -> [(a, b, c)] -> [(a, b, c)]
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]
_        = [(a, b, c)]
forall a. HasCallStack => a
impossible

-- | Zip 4 lists of the same size
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) = [(a, b, c, d)] -> ListN n (a, b, c, d)
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
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) (a, b, c, d) -> [(a, b, c, d)] -> [(a, b, c, d)]
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]
_        = [(a, b, c, d)]
forall a. HasCallStack => a
impossible

-- | Zip 5 lists of the same size
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) = [(a, b, c, d, e)] -> ListN n (a, b, c, d, e)
forall (n :: Nat) a. [a] -> ListN n a
ListN ([a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
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) (a, b, c, d, e) -> [(a, b, c, d, e)] -> [(a, b, c, d, e)]
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]
_        = [(a, b, c, d, e)]
forall a. HasCallStack => a
impossible

-- | Zip 2 lists using a function
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)) = [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN (a -> b -> x
f a
v1 b
w1 x -> [x] -> [x]
forall a. a -> [a] -> [a]
: ListN Any x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> x) -> ListN Any a -> ListN Any b -> ListN Any x
forall a b x (n :: Nat).
(a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith a -> b -> x
f ([a] -> ListN Any a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN Any b
forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws)))
zipWith a -> b -> x
_ (ListN [])       ListN n b
_ = [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith a -> b -> x
_ ListN n a
_                ListN n b
_ = ListN n x
forall a. HasCallStack => a
impossible

-- | Zip 3 lists using a function
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)) =
    [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN (a -> b -> c -> x
f a
v1 b
w1 c
x1 x -> [x] -> [x]
forall a. a -> [a] -> [a]
: ListN Any x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> c -> x)
-> ListN Any a -> ListN Any b -> ListN Any c -> ListN Any x
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 ([a] -> ListN Any a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN Any b
forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) ([c] -> ListN Any c
forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs)))
zipWith3 a -> b -> c -> x
_ (ListN []) ListN n b
_       ListN n c
_ = [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith3 a -> b -> c -> x
_ ListN n a
_          ListN n b
_       ListN n c
_ = ListN n x
forall a. HasCallStack => a
impossible

-- | Zip 4 lists using a function
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)) =
    [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN (a -> b -> c -> d -> x
f a
v1 b
w1 c
x1 d
y1 x -> [x] -> [x]
forall a. a -> [a] -> [a]
: ListN Any x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> c -> d -> x)
-> ListN Any a
-> ListN Any b
-> ListN Any c
-> ListN Any d
-> ListN Any x
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 ([a] -> ListN Any a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN Any b
forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) ([c] -> ListN Any c
forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs) ([d] -> ListN Any d
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
_ = [x] -> ListN n x
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
_ = ListN n x
forall a. HasCallStack => a
impossible

-- | Zip 5 lists using a function
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)) =
    [x] -> ListN n x
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 x -> [x] -> [x]
forall a. a -> [a] -> [a]
: ListN Any x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> c -> d -> e -> x)
-> ListN Any a
-> ListN Any b
-> ListN Any c
-> ListN Any d
-> ListN Any e
-> ListN Any x
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 ([a] -> ListN Any a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN Any b
forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) ([c] -> ListN Any c
forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs) ([d] -> ListN Any d
forall (n :: Nat) a. [a] -> ListN n a
ListN [d]
ys) ([e] -> ListN Any e
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
_ = [x] -> ListN n x
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
_ = ListN n x
forall a. HasCallStack => a
impossible