{-# 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 = [Char] -> a
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
(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
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)
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
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
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
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
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
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
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
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
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)
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)
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])
empty :: ListN 0 a
empty :: forall a. ListN 0 a
empty = [a] -> ListN 0 a
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
_ = 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 :: 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)
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
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]
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 :: 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)
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
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
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
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
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 :: 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 :: 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)
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)
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))
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
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 :: (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)
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
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
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
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
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
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' :: (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' :: (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 :: 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 :: 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 :: 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)
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
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
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
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 (ZonkAny 0) x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> x)
-> ListN (ZonkAny 0) a
-> ListN (ZonkAny 0) b
-> ListN (ZonkAny 0) 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 (ZonkAny 0) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN (ZonkAny 0) 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
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 (ZonkAny 1) x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> c -> x)
-> ListN (ZonkAny 1) a
-> ListN (ZonkAny 1) b
-> ListN (ZonkAny 1) c
-> ListN (ZonkAny 1) 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 (ZonkAny 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN (ZonkAny 1) b
forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) ([c] -> ListN (ZonkAny 1) 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
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 (ZonkAny 2) x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> c -> d -> x)
-> ListN (ZonkAny 2) a
-> ListN (ZonkAny 2) b
-> ListN (ZonkAny 2) c
-> ListN (ZonkAny 2) d
-> ListN (ZonkAny 2) 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 (ZonkAny 2) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN (ZonkAny 2) b
forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) ([c] -> ListN (ZonkAny 2) c
forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs) ([d] -> ListN (ZonkAny 2) 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
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 (ZonkAny 3) x -> [x]
forall (n :: Nat) a. ListN n a -> [a]
unListN ((a -> b -> c -> d -> e -> x)
-> ListN (ZonkAny 3) a
-> ListN (ZonkAny 3) b
-> ListN (ZonkAny 3) c
-> ListN (ZonkAny 3) d
-> ListN (ZonkAny 3) e
-> ListN (ZonkAny 3) 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 (ZonkAny 3) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
vs) ([b] -> ListN (ZonkAny 3) b
forall (n :: Nat) a. [a] -> ListN n a
ListN [b]
ws) ([c] -> ListN (ZonkAny 3) c
forall (n :: Nat) a. [a] -> ListN n a
ListN [c]
xs) ([d] -> ListN (ZonkAny 3) d
forall (n :: Nat) a. [a] -> ListN n a
ListN [d]
ys) ([e] -> ListN (ZonkAny 3) 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