-- |
-- 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 = 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
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

-- | 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 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)

-- | 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 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

-- | 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 = 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

-- | 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) = 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

-- | 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) = 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) = 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

-- | 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) = 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 = 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

-- | 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, forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs)
uncons ListN n 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) = forall (n :: Nat) a. [a] -> ListN n a
ListN (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) = (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)

-- | 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 = forall (n :: Nat) a. [a] -> ListN n a
ListN ([a]
l 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 = 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
_ = 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 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 = 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)

-- | 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 = 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

-- | create a list of 1 element
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]

-- | 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) = 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) = forall (n :: Nat) a. [a] -> ListN n a
ListN ([a]
l1 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) = 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) = 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
_ = 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)) = forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs
tail ListN n 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) = 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 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) = 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 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) = 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)

-- | 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) = 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)

-- | 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 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))

-- | 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 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) = 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 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) = forall (n :: Nat) a. [a] -> ListN n a
ListN (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) = 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

-- | 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) = 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) = 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) = forall a. (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) = 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) = 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) = 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' 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
                        []     -> 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 a list
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 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) = forall (n :: Nat) a. [a] -> ListN n a
ListN (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 = (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)

-- | 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) = 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

-- | 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) = 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

-- | 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) = 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

-- | 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)) = 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

-- | 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)) =
    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

-- | 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)) =
    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

-- | 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)) =
    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