{-# 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 :: a
impossible = [Char] -> a
forall a. HasCallStack => [Char] -> a
error "ListN: internal error: the impossible happened"
newtype ListN (n :: Nat) a = ListN { 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 a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
$c== :: forall (n :: Nat) a. Eq a => 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 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
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
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
$cp1Ord :: forall (n :: Nat) a. Ord a => Eq (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 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
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
$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 l :: [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 l :: [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 :: [a] -> Maybe (ListN n a)
toListN l :: [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 (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_ :: [a] -> ListN n a
toListN_ l :: [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 ("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
<> " 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
<> " 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 (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 :: m a -> m (ListN n a)
replicateM action :: 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 :: ListN n (m a) -> m (ListN n a)
sequence (ListN l :: [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)
M.sequence [m a]
l
sequence_ :: Monad m => ListN n (m a) -> m ()
sequence_ :: ListN n (m a) -> m ()
sequence_ (ListN l :: [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 :: (a -> m b) -> ListN n a -> m (ListN n b)
mapM f :: a -> m b
f (ListN l :: [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)
M.mapM a -> m b
f [a]
l
mapM_ :: Monad m => (a -> m b) -> ListN n a -> m ()
mapM_ :: (a -> m b) -> ListN n a -> m ()
mapM_ f :: a -> m b
f (ListN l :: [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 :: a -> ListN n a
replicate a :: 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 :: ListN n a -> (a, ListN (n - 1) a)
uncons (ListN (x :: a
x:xs :: [a]
xs)) = (a
x, [a] -> ListN (n - 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs)
uncons _ = (a, ListN (n - 1) a)
forall a. HasCallStack => a
impossible
cons :: a -> ListN n a -> ListN (n+1) a
cons :: a -> ListN n a -> ListN (n + 1) a
cons a :: a
a (ListN l :: [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 :: ListN n a -> (ListN (n - 1) a, a)
unsnoc (ListN l :: [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. [a] -> [a]
Data.List.init [a]
l, [a] -> a
forall a. [a] -> a
Data.List.last [a]
l)
snoc :: ListN n a -> a -> ListN (n+1) a
snoc :: ListN n a -> a -> ListN (n + 1) a
snoc (ListN l :: [a]
l) a :: 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 :: 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 :: ListN n a -> CountOf a
length _ = 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 :: (Natural -> a) -> ListN n a
create f :: Natural -> 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 (Natural -> a
f (Natural -> a) -> (Integer -> Natural) -> Integer -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral) [0..(Integer
lenInteger -> Integer -> Difference Integer
forall a. Subtractive a => a -> a -> Difference a
-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 :: Proxy start -> (Natural -> a) -> ListN n a
createFrom p :: Proxy start
p f :: Natural -> 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 (Natural -> a
f (Natural -> a) -> (Integer -> Natural) -> Integer -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Natural
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
-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 :: a -> ListN 1 a
singleton a :: 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 :: a -> ListN n a -> Bool
elem a :: a
a (ListN l :: [a]
l) = 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 :: ListN n a -> ListN m a -> ListN (n + m) a
append (ListN l1 :: [a]
l1) (ListN l2 :: [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 :: ListN n a -> a
maximum (ListN l :: [a]
l) = [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 :: ListN n a -> a
minimum (ListN l :: [a]
l) = [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.minimum [a]
l
head :: (1 <= n) => ListN n a -> a
head :: ListN n a -> a
head (ListN (x :: a
x:_)) = a
x
head _ = a
forall a. HasCallStack => a
impossible
tail :: (1 <= n) => ListN n a -> ListN (n-1) a
tail :: ListN n a -> ListN (n - 1) a
tail (ListN (_:xs :: [a]
xs)) = [a] -> ListN (n - 1) a
forall (n :: Nat) a. [a] -> ListN n a
ListN [a]
xs
tail _ = ListN (n - 1) a
forall a. HasCallStack => a
impossible
init :: (1 <= n) => ListN n a -> ListN (n-1) a
init :: ListN n a -> ListN (n - 1) a
init (ListN l :: [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. [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 :: ListN n a -> ListN m a
take (ListN l :: [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 :: ListN n a -> ListN m a
drop (ListN l :: [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 :: ListN n a -> (ListN m a, ListN (n - m) a)
splitAt (ListN l :: [a]
l) = let (l1 :: [a]
l1, l2 :: [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 :: ListN n a -> a
indexStatic (ListN l :: [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 :: ListN n ty -> Offset ty -> ty
index (ListN l :: [ty]
l) ofs :: 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 :: Offset a -> (a -> a) -> ListN n a -> ListN n a
updateAt o :: Offset a
o f :: a -> a
f (ListN l :: [a]
l) = [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN (Offset a -> [a] -> [a]
doUpdate 0 [a]
l)
where doUpdate :: Offset a -> [a] -> [a]
doUpdate _ [] = []
doUpdate i :: Offset a
i (x :: a
x:xs :: [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
+1) [a]
xs
map :: (a -> b) -> ListN n a -> ListN n b
map :: (a -> b) -> ListN n a -> ListN n b
map f :: a -> b
f (ListN l :: [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 :: (Natural -> a -> b) -> ListN n a -> ListN n b
mapi f :: Natural -> a -> b
f (ListN l :: [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 k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Natural -> [a] -> [b]
loop 0 ([a] -> ListN n b) -> [a] -> ListN n b
forall a b. (a -> b) -> a -> b
$ [a]
l
where loop :: Natural -> [a] -> [b]
loop _ [] = []
loop i :: Natural
i (x :: a
x:xs :: [a]
xs) = Natural -> a -> b
f Natural
i a
x b -> [b] -> [b]
forall a. a -> [a] -> [a]
: Natural -> [a] -> [b]
loop (Natural
iNatural -> Natural -> Natural
forall a. Additive a => a -> a -> a
+1) [a]
xs
foldl :: (b -> a -> b) -> b -> ListN n a -> b
foldl :: (b -> a -> b) -> b -> ListN n a -> b
foldl f :: b -> a -> b
f acc :: b
acc (ListN l :: [a]
l) = (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' :: (b -> a -> b) -> b -> ListN n a -> b
foldl' f :: b -> a -> b
f acc :: b
acc (ListN l :: [a]
l) = (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' :: (a -> a -> a) -> ListN n a -> a
foldl1' f :: a -> a -> a
f (ListN l :: [a]
l) = (a -> a -> a) -> [a] -> a
forall a. (a -> a -> a) -> [a] -> a
Data.List.foldl1' a -> a -> a
f [a]
l
foldr :: (a -> b -> b) -> b -> ListN n a -> b
foldr :: (a -> b -> b) -> b -> ListN n a -> b
foldr f :: a -> b -> b
f acc :: b
acc (ListN l :: [a]
l) = (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 :: (a -> a -> a) -> ListN n a -> a
foldr1 f :: a -> a -> a
f (ListN l :: [a]
l) = (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' :: (b -> a -> b) -> b -> ListN n a -> ListN (n + 1) b
scanl' f :: b -> a -> b
f initialAcc :: b
initialAcc (ListN start :: [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 l :: [a]
l = b
acc b -> [b] -> [b]
forall a. a -> [a] -> [a]
: case [a]
l of
[] -> []
(x :: a
x:xs :: [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' :: (a -> a -> a) -> ListN n a -> ListN n a
scanl1' f :: a -> a -> a
f (ListN l :: [a]
l) = case [a]
l of
[] -> [a] -> ListN n a
forall (n :: Nat) a. [a] -> ListN n a
ListN []
(x :: a
x:xs :: [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 :: ListN n a -> ListN n a
reverse (ListN l :: [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 :: ListN n a -> ListN n b -> ListN n (a, b)
zip (ListN l1 :: [a]
l1) (ListN l2 :: [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 :: ListN n (a, b) -> (ListN n a, ListN n b)
unzip l :: 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 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c)
zip3 (ListN x1 :: [a]
x1) (ListN x2 :: [b]
x2) (ListN x3 :: [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 (l1 :: a
l1:l1s :: [a]
l1s) (l2 :: b
l2:l2s :: [b]
l2s) (l3 :: c
l3:l3s :: [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 [] _ _ = []
loop _ _ _ = [(a, b, c)]
forall a. HasCallStack => a
impossible
zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a,b,c,d)
zip4 :: ListN n a
-> ListN n b -> ListN n c -> ListN n d -> ListN n (a, b, c, d)
zip4 (ListN x1 :: [a]
x1) (ListN x2 :: [b]
x2) (ListN x3 :: [c]
x3) (ListN x4 :: [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 (l1 :: a
l1:l1s :: [a]
l1s) (l2 :: b
l2:l2s :: [b]
l2s) (l3 :: c
l3:l3s :: [c]
l3s) (l4 :: d
l4:l4s :: [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 [] _ _ _ = []
loop _ _ _ _ = [(a, b, c, d)]
forall a. HasCallStack => a
impossible
zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a,b,c,d,e)
zip5 :: ListN n a
-> ListN n b
-> ListN n c
-> ListN n d
-> ListN n e
-> ListN n (a, b, c, d, e)
zip5 (ListN x1 :: [a]
x1) (ListN x2 :: [b]
x2) (ListN x3 :: [c]
x3) (ListN x4 :: [d]
x4) (ListN x5 :: [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 (l1 :: a
l1:l1s :: [a]
l1s) (l2 :: b
l2:l2s :: [b]
l2s) (l3 :: c
l3:l3s :: [c]
l3s) (l4 :: d
l4:l4s :: [d]
l4s) (l5 :: e
l5:l5s :: [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 [] _ _ _ _ = []
loop _ _ _ _ _ = [(a, b, c, d, e)]
forall a. HasCallStack => a
impossible
zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith f :: a -> b -> x
f (ListN (v1 :: a
v1:vs :: [a]
vs)) (ListN (w1 :: b
w1:ws :: [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 _ (ListN []) _ = [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith _ _ _ = 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 :: (a -> b -> c -> x)
-> ListN n a -> ListN n b -> ListN n c -> ListN n x
zipWith3 f :: a -> b -> c -> x
f (ListN (v1 :: a
v1:vs :: [a]
vs)) (ListN (w1 :: b
w1:ws :: [b]
ws)) (ListN (x1 :: c
x1:xs :: [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 _ (ListN []) _ _ = [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith3 _ _ _ _ = 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 :: (a -> b -> c -> d -> x)
-> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x
zipWith4 f :: a -> b -> c -> d -> x
f (ListN (v1 :: a
v1:vs :: [a]
vs)) (ListN (w1 :: b
w1:ws :: [b]
ws)) (ListN (x1 :: c
x1:xs :: [c]
xs)) (ListN (y1 :: d
y1:ys :: [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 _ (ListN []) _ _ _ = [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith4 _ _ _ _ _ = 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 :: (a -> b -> c -> d -> e -> x)
-> ListN n a
-> ListN n b
-> ListN n c
-> ListN n d
-> ListN n e
-> ListN n x
zipWith5 f :: a -> b -> c -> d -> e -> x
f (ListN (v1 :: a
v1:vs :: [a]
vs)) (ListN (w1 :: b
w1:ws :: [b]
ws)) (ListN (x1 :: c
x1:xs :: [c]
xs)) (ListN (y1 :: d
y1:ys :: [d]
ys)) (ListN (z1 :: e
z1:zs :: [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 _ (ListN []) _ _ _ _ = [x] -> ListN n x
forall (n :: Nat) a. [a] -> ListN n a
ListN []
zipWith5 _ _ _ _ _ _ = ListN n x
forall a. HasCallStack => a
impossible