{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vec.Lazy.Inline (
Vec (..),
empty,
singleton,
toPull,
fromPull,
toList,
toNonEmpty,
fromList,
fromListPrefix,
reifyList,
(!),
tabulate,
cons,
snoc,
head,
last,
tail,
init,
(++),
split,
concatMap,
concat,
chunks,
reverse,
foldMap,
foldMap1,
ifoldMap,
ifoldMap1,
foldr,
ifoldr,
length,
null,
sum,
product,
map,
imap,
traverse,
#ifdef MIN_VERSION_semigroupoids
traverse1,
#endif
itraverse,
itraverse_,
zipWith,
izipWith,
repeat,
bind,
join,
universe,
VecEach (..)
) where
import Prelude (Int, Maybe (..), Num (..), const, flip, id, ($), (.))
import Control.Applicative (Applicative (pure, (*>)), liftA2, (<$>))
import Data.Fin (Fin (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Monoid (Monoid (..))
import Data.Nat (Nat (..))
import Data.Semigroup (Semigroup (..))
import Data.Vec.Lazy
(Vec (..), VecEach (..), cons, empty, head, null, reifyList, singleton,
tail)
#ifdef MIN_VERSION_semigroupoids
import Data.Functor.Apply (Apply, liftF2)
#endif
import qualified Data.Fin as F
import qualified Data.Type.Nat as N
import qualified Data.Vec.Pull as P
toPull :: forall n a. N.SNatI n => Vec n a -> P.Vec n a
toPull :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
toPull = forall (n :: Nat) a. ToPull n a -> Vec n a -> Vec n a
getToPull (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 ToPull 'Z a
start forall (m :: Nat). ToPull m a -> ToPull ('S m) a
step) where
start :: ToPull 'Z a
start :: ToPull 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec n a) -> ToPull n a
ToPull forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec forall b. Fin 'Z -> b
F.absurd
step :: ToPull m a -> ToPull ('S m) a
step :: forall (m :: Nat). ToPull m a -> ToPull ('S m) a
step (ToPull Vec m a -> Vec m a
f) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> ToPull n a
ToPull forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
i -> case Fin ('S m)
i of
Fin ('S m)
FZ -> a
x
FS Fin n1
i' -> forall (n :: Nat) a. Vec n a -> Fin n -> a
P.unVec (Vec m a -> Vec m a
f Vec n a
xs) Fin n1
i'
newtype ToPull n a = ToPull { forall (n :: Nat) a. ToPull n a -> Vec n a -> Vec n a
getToPull :: Vec n a -> P.Vec n a }
fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
fromPull :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull = forall (n :: Nat) a. FromPull n a -> Vec n a -> Vec n a
getFromPull (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 FromPull 'Z a
start forall (m :: Nat). FromPull m a -> FromPull ('S m) a
step) where
start :: FromPull 'Z a
start :: FromPull 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec n a) -> FromPull n a
FromPull forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Vec 'Z a
VNil
step :: FromPull m a -> FromPull ('S m) a
step :: forall (m :: Nat). FromPull m a -> FromPull ('S m) a
step (FromPull Vec m a -> Vec m a
f) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> FromPull n a
FromPull forall a b. (a -> b) -> a -> b
$ \(P.Vec Fin ('S m) -> a
v) -> Fin ('S m) -> a
v forall (n1 :: Nat). Fin ('S n1)
FZ forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m a
f (forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec (Fin ('S m) -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS))
newtype FromPull n a = FromPull { forall (n :: Nat) a. FromPull n a -> Vec n a -> Vec n a
getFromPull :: P.Vec n a -> Vec n a }
toList :: forall n a. N.SNatI n => Vec n a -> [a]
toList :: forall (n :: Nat) a. SNatI n => Vec n a -> [a]
toList = forall (n :: Nat) a. ToList n a -> Vec n a -> [a]
getToList (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 ToList 'Z a
start forall (m :: Nat). ToList m a -> ToList ('S m) a
step) where
start :: ToList 'Z a
start :: ToList 'Z a
start = forall (n :: Nat) a. (Vec n a -> [a]) -> ToList n a
ToList (forall a b. a -> b -> a
const [])
step :: ToList m a -> ToList ('S m) a
step :: forall (m :: Nat). ToList m a -> ToList ('S m) a
step (ToList Vec m a -> [a]
f) = forall (n :: Nat) a. (Vec n a -> [a]) -> ToList n a
ToList forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a
x forall a. a -> [a] -> [a]
: Vec m a -> [a]
f Vec n a
xs
newtype ToList n a = ToList { forall (n :: Nat) a. ToList n a -> Vec n a -> [a]
getToList :: Vec n a -> [a] }
toNonEmpty :: forall n a. N.SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty (a
x ::: Vec n a
xs) = a
x forall a. a -> [a] -> NonEmpty a
:| forall (n :: Nat) a. SNatI n => Vec n a -> [a]
toList Vec n a
xs
fromList :: N.SNatI n => [a] -> Maybe (Vec n a)
fromList :: forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromList = forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. FromList 'Z a
start forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
start :: FromList 'Z a
start :: forall a. FromList 'Z a
start = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> forall a. a -> Maybe a
Just forall a. Vec 'Z a
VNil
(a
_ : [a]
_) -> forall a. Maybe a
Nothing
step :: FromList n a -> FromList ('N.S n) a
step :: forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step (FromList [a] -> Maybe (Vec n a)
f) = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> forall a. Maybe a
Nothing
(a
x : [a]
xs') -> (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Vec n a)
f [a]
xs'
newtype FromList n a = FromList { forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList :: [a] -> Maybe (Vec n a) }
fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)
fromListPrefix :: forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromListPrefix = forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. FromList 'Z a
start forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
start :: FromList 'Z a
start :: forall a. FromList 'Z a
start = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
_ -> forall a. a -> Maybe a
Just forall a. Vec 'Z a
VNil
step :: FromList n a -> FromList ('N.S n) a
step :: forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step (FromList [a] -> Maybe (Vec n a)
f) = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> forall a. Maybe a
Nothing
(a
x : [a]
xs') -> (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Vec n a)
f [a]
xs'
flipIndex :: N.SNatI n => Fin n -> Vec n a -> a
flipIndex :: forall (n :: Nat) a. SNatI n => Fin n -> Vec n a -> a
flipIndex = forall (n :: Nat) a. Index n a -> Fin n -> Vec n a -> a
getIndex (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. Index 'Z a
start forall (m :: Nat) a. Index m a -> Index ('S m) a
step) where
start :: Index 'Z a
start :: forall a. Index 'Z a
start = forall (n :: Nat) a. (Fin n -> Vec n a -> a) -> Index n a
Index forall b. Fin 'Z -> b
F.absurd
step :: Index m a-> Index ('N.S m) a
step :: forall (m :: Nat) a. Index m a -> Index ('S m) a
step (Index Fin m -> Vec m a -> a
go) = forall (n :: Nat) a. (Fin n -> Vec n a -> a) -> Index n a
Index forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
n (a
x ::: Vec n a
xs) -> case Fin ('S m)
n of
Fin ('S m)
FZ -> a
x
FS Fin n1
m -> Fin m -> Vec m a -> a
go Fin n1
m Vec n a
xs
newtype Index n a = Index { forall (n :: Nat) a. Index n a -> Fin n -> Vec n a -> a
getIndex :: Fin n -> Vec n a -> a }
(!) :: N.SNatI n => Vec n a -> Fin n -> a
! :: forall (n :: Nat) a. SNatI n => Vec n a -> Fin n -> a
(!) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (n :: Nat) a. SNatI n => Fin n -> Vec n a -> a
flipIndex
tabulate :: N.SNatI n => (Fin n -> a) -> Vec n a
tabulate :: forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate = forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.tabulate
snoc :: forall n a. N.SNatI n => Vec n a -> a -> Vec ('S n) a
snoc :: forall (n :: Nat) a. SNatI n => Vec n a -> a -> Vec ('S n) a
snoc Vec n a
xs a
x = forall (n :: Nat) a. Snoc n a -> Vec n a -> Vec ('S n) a
getSnoc (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Snoc 'Z a
start forall (m :: Nat). Snoc m a -> Snoc ('S m) a
step) Vec n a
xs where
start :: Snoc 'Z a
start :: Snoc 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec ('S n) a) -> Snoc n a
Snoc forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
ys -> a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
ys
step :: Snoc m a -> Snoc ('S m) a
step :: forall (m :: Nat). Snoc m a -> Snoc ('S m) a
step (Snoc Vec m a -> Vec ('S m) a
rec) = forall (n :: Nat) a. (Vec n a -> Vec ('S n) a) -> Snoc n a
Snoc forall a b. (a -> b) -> a -> b
$ \(a
y ::: Vec n a
ys) -> a
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec ('S m) a
rec Vec n a
ys
newtype Snoc n a = Snoc { forall (n :: Nat) a. Snoc n a -> Vec n a -> Vec ('S n) a
getSnoc :: Vec n a -> Vec ('S n) a }
last :: forall n a. N.SNatI n => Vec ('S n) a -> a
last :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> a
last Vec ('S n) a
xs = forall (n :: Nat) a. Last n a -> Vec ('S n) a -> a
getLast (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Last 'Z a
start forall (m :: Nat). Last m a -> Last ('S m) a
step) Vec ('S n) a
xs where
start :: Last 'Z a
start :: Last 'Z a
start = forall (n :: Nat) a. (Vec ('S n) a -> a) -> Last n a
Last forall a b. (a -> b) -> a -> b
$ \(a
x:::Vec n a
VNil) -> a
x
step :: Last m a -> Last ('S m) a
step :: forall (m :: Nat). Last m a -> Last ('S m) a
step (Last Vec ('S m) a -> a
rec) = forall (n :: Nat) a. (Vec ('S n) a -> a) -> Last n a
Last forall a b. (a -> b) -> a -> b
$ \(a
_ ::: Vec n a
ys) -> Vec ('S m) a -> a
rec Vec n a
ys
newtype Last n a = Last { forall (n :: Nat) a. Last n a -> Vec ('S n) a -> a
getLast :: Vec ('S n) a -> a }
init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a
init :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> Vec n a
init Vec ('S n) a
xs = forall (n :: Nat) a. Init n a -> Vec ('S n) a -> Vec n a
getInit (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Init 'Z a
start forall (m :: Nat). Init m a -> Init ('S m) a
step) Vec ('S n) a
xs where
start :: Init 'Z a
start :: Init 'Z a
start = forall (n :: Nat) a. (Vec ('S n) a -> Vec n a) -> Init n a
Init (forall a b. a -> b -> a
const forall a. Vec 'Z a
VNil)
step :: Init m a -> Init ('S m) a
step :: forall (m :: Nat). Init m a -> Init ('S m) a
step (Init Vec ('S m) a -> Vec m a
rec) = forall (n :: Nat) a. (Vec ('S n) a -> Vec n a) -> Init n a
Init forall a b. (a -> b) -> a -> b
$ \(a
y ::: Vec n a
ys) -> a
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec ('S m) a -> Vec m a
rec Vec n a
ys
newtype Init n a = Init { forall (n :: Nat) a. Init n a -> Vec ('S n) a -> Vec n a
getInit :: Vec ('S n) a -> Vec n a}
reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a
reverse :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
reverse = forall (n :: Nat) a. Reverse n a -> Vec n a -> Vec n a
getReverse (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Reverse 'Z a
start forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a
step) where
start :: Reverse 'Z a
start :: Reverse 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec n a) -> Reverse n a
Reverse forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: N.SNatI m => Reverse m a -> Reverse ('S m) a
step :: forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a
step (Reverse Vec m a -> Vec m a
rec) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> Reverse n a
Reverse forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> forall (n :: Nat) a. SNatI n => Vec n a -> a -> Vec ('S n) a
snoc (Vec m a -> Vec m a
rec Vec n a
xs) a
x
newtype Reverse n a = Reverse { forall (n :: Nat) a. Reverse n a -> Vec n a -> Vec n a
getReverse :: Vec n a -> Vec n a }
infixr 5 ++
(++) :: forall n m a. N.SNatI n => Vec n a -> Vec m a -> Vec (N.Plus n m) a
Vec n a
as ++ :: forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec m a
ys = forall (m :: Nat) (n :: Nat) a.
Append m n a -> Vec n a -> Vec (Plus n m) a
getAppend (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Append m 'Z a
start forall (p :: Nat). Append m p a -> Append m ('S p) a
step) Vec n a
as where
start :: Append m 'Z a
start :: Append m 'Z a
start = forall (m :: Nat) (n :: Nat) a.
(Vec n a -> Vec (Plus n m) a) -> Append m n a
Append forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec m a
ys
step :: Append m p a -> Append m ('S p) a
step :: forall (p :: Nat). Append m p a -> Append m ('S p) a
step (Append Vec p a -> Vec (Plus p m) a
f) = forall (m :: Nat) (n :: Nat) a.
(Vec n a -> Vec (Plus n m) a) -> Append m n a
Append forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec p a -> Vec (Plus p m) a
f Vec n a
xs
newtype Append m n a = Append { forall (m :: Nat) (n :: Nat) a.
Append m n a -> Vec n a -> Vec (Plus n m) a
getAppend :: Vec n a -> Vec (N.Plus n m) a }
split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)
split :: forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec (Plus n m) a -> (Vec n a, Vec m a)
split = forall (m :: Nat) (n :: Nat) a.
Split m n a -> Vec (Plus n m) a -> (Vec n a, Vec m a)
appSplit (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall (m :: Nat) a. Split m 'Z a
start forall (m :: Nat) (n :: Nat) a. Split m n a -> Split m ('S n) a
step) where
start :: Split m 'Z a
start :: forall (m :: Nat) a. Split m 'Z a
start = forall (m :: Nat) (n :: Nat) a.
(Vec (Plus n m) a -> (Vec n a, Vec m a)) -> Split m n a
Split forall a b. (a -> b) -> a -> b
$ \Vec (Plus 'Z m) a
xs -> (forall a. Vec 'Z a
VNil, Vec (Plus 'Z m) a
xs)
step :: Split m n a -> Split m ('S n) a
step :: forall (m :: Nat) (n :: Nat) a. Split m n a -> Split m ('S n) a
step (Split Vec (Plus n m) a -> (Vec n a, Vec m a)
f) = forall (m :: Nat) (n :: Nat) a.
(Vec (Plus n m) a -> (Vec n a, Vec m a)) -> Split m n a
Split forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> case Vec (Plus n m) a -> (Vec n a, Vec m a)
f Vec n a
xs of
(Vec n a
ys, Vec m a
zs) -> (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
ys, Vec m a
zs)
newtype Split m n a = Split { forall (m :: Nat) (n :: Nat) a.
Split m n a -> Vec (Plus n m) a -> (Vec n a, Vec m a)
appSplit :: Vec (N.Plus n m) a -> (Vec n a, Vec m a) }
concatMap :: forall a b n m. (N.SNatI m, N.SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
concatMap :: forall a b (n :: Nat) (m :: Nat).
(SNatI m, SNatI n) =>
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap a -> Vec m b
f = forall (m :: Nat) a (n :: Nat) b.
ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b
getConcatMap forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 ConcatMap m a 'Z b
start forall (p :: Nat). ConcatMap m a p b -> ConcatMap m a ('S p) b
step where
start :: ConcatMap m a 'Z b
start :: ConcatMap m a 'Z b
start = forall (m :: Nat) a (n :: Nat) b.
(Vec n a -> Vec (Mult n m) b) -> ConcatMap m a n b
ConcatMap forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: ConcatMap m a p b -> ConcatMap m a ('S p) b
step :: forall (p :: Nat). ConcatMap m a p b -> ConcatMap m a ('S p) b
step (ConcatMap Vec p a -> Vec (Mult p m) b
g) = forall (m :: Nat) a (n :: Nat) b.
(Vec n a -> Vec (Mult n m) b) -> ConcatMap m a n b
ConcatMap forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a -> Vec m b
f a
x forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec p a -> Vec (Mult p m) b
g Vec n a
xs
newtype ConcatMap m a n b = ConcatMap { forall (m :: Nat) a (n :: Nat) b.
ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b
getConcatMap :: Vec n a -> Vec (N.Mult n m) b }
concat :: (N.SNatI m, N.SNatI n) => Vec n (Vec m a) -> Vec (N.Mult n m) a
concat :: forall (m :: Nat) (n :: Nat) a.
(SNatI m, SNatI n) =>
Vec n (Vec m a) -> Vec (Mult n m) a
concat = forall a b (n :: Nat) (m :: Nat).
(SNatI m, SNatI n) =>
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap forall a. a -> a
id
chunks :: (N.SNatI n, N.SNatI m) => Vec (N.Mult n m) a -> Vec n (Vec m a)
chunks :: forall (n :: Nat) (m :: Nat) a.
(SNatI n, SNatI m) =>
Vec (Mult n m) a -> Vec n (Vec m a)
chunks = forall (m :: Nat) (n :: Nat) a.
Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
getChunks forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall (m :: Nat) a. Chunks m 'Z a
start forall (m :: Nat) (n :: Nat) a.
SNatI m =>
Chunks m n a -> Chunks m ('S n) a
step where
start :: Chunks m 'Z a
start :: forall (m :: Nat) a. Chunks m 'Z a
start = forall (m :: Nat) (n :: Nat) a.
(Vec (Mult n m) a -> Vec n (Vec m a)) -> Chunks m n a
Chunks forall a b. (a -> b) -> a -> b
$ \Vec (Mult 'Z m) a
_ -> forall a. Vec 'Z a
VNil
step :: forall m n a. N.SNatI m => Chunks m n a -> Chunks m ('S n) a
step :: forall (m :: Nat) (n :: Nat) a.
SNatI m =>
Chunks m n a -> Chunks m ('S n) a
step (Chunks Vec (Mult n m) a -> Vec n (Vec m a)
go) = forall (m :: Nat) (n :: Nat) a.
(Vec (Mult n m) a -> Vec n (Vec m a)) -> Chunks m n a
Chunks forall a b. (a -> b) -> a -> b
$ \Vec (Mult ('S n) m) a
xs ->
let (Vec m a
ys, Vec (Mult n m) a
zs) = forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec (Plus n m) a -> (Vec n a, Vec m a)
split Vec (Mult ('S n) m) a
xs :: (Vec m a, Vec (N.Mult n m) a)
in Vec m a
ys forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec (Mult n m) a -> Vec n (Vec m a)
go Vec (Mult n m) a
zs
newtype Chunks m n a = Chunks { forall (m :: Nat) (n :: Nat) a.
Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
getChunks :: Vec (N.Mult n m) a -> Vec n (Vec m a) }
map :: forall a b n. N.SNatI n => (a -> b) -> Vec n a -> Vec n b
map :: forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map a -> b
f = forall a (n :: Nat) b. Map a n b -> Vec n a -> Vec n b
getMap forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Map a 'Z b
start forall (m :: Nat). Map a m b -> Map a ('S m) b
step where
start :: Map a 'Z b
start :: Map a 'Z b
start = forall a (n :: Nat) b. (Vec n a -> Vec n b) -> Map a n b
Map forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: Map a m b -> Map a ('S m) b
step :: forall (m :: Nat). Map a m b -> Map a ('S m) b
step (Map Vec m a -> Vec m b
go) = forall a (n :: Nat) b. (Vec n a -> Vec n b) -> Map a n b
Map forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a -> b
f a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m b
go Vec n a
xs
newtype Map a n b = Map { forall a (n :: Nat) b. Map a n b -> Vec n a -> Vec n b
getMap :: Vec n a -> Vec n b }
imap :: N.SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b
imap :: forall (n :: Nat) a b.
SNatI n =>
(Fin n -> a -> b) -> Vec n a -> Vec n b
imap = forall a (n :: Nat) b.
IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b
getIMap forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a b. IMap a 'Z b
start forall a (m :: Nat) b. IMap a m b -> IMap a ('S m) b
step where
start :: IMap a 'Z b
start :: forall a b. IMap a 'Z b
start = forall a (n :: Nat) b.
((Fin n -> a -> b) -> Vec n a -> Vec n b) -> IMap a n b
IMap forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b
_ Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: IMap a m b -> IMap a ('S m) b
step :: forall a (m :: Nat) b. IMap a m b -> IMap a ('S m) b
step (IMap (Fin m -> a -> b) -> Vec m a -> Vec m b
go) = forall a (n :: Nat) b.
((Fin n -> a -> b) -> Vec n a -> Vec n b) -> IMap a n b
IMap forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b
f (a
x ::: Vec n a
xs) -> Fin ('S m) -> a -> b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: (Fin m -> a -> b) -> Vec m a -> Vec m b
go (Fin ('S m) -> a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
newtype IMap a n b = IMap { forall a (n :: Nat) b.
IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b
getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }
traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)
traverse :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse a -> f b
f = forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Vec n a -> f (Vec n b)
getTraverse forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Traverse f a 'Z b
start forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step where
start :: Traverse f a 'Z b
start :: Traverse f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
(Vec n a -> f (Vec n b)) -> Traverse f a n b
Traverse forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Vec 'Z a
VNil
step :: Traverse f a m b -> Traverse f a ('S m) b
step :: forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step (Traverse Vec m a -> f (Vec m b)
go) = forall (f :: * -> *) a (n :: Nat) b.
(Vec n a -> f (Vec n b)) -> Traverse f a n b
Traverse forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) (a -> f b
f a
x) (Vec m a -> f (Vec m b)
go Vec n a
xs)
newtype Traverse f a n b = Traverse { forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Vec n a -> f (Vec n b)
getTraverse :: Vec n a -> f (Vec n b) }
#ifdef MIN_VERSION_semigroupoids
traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 :: forall (n :: Nat) (f :: * -> *) a b.
(Apply f, SNatI n) =>
(a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 a -> f b
f = forall (f :: * -> *) a (n :: Nat) b.
Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b)
getTraverse1 forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Traverse1 f a 'Z b
start forall (m :: Nat). Traverse1 f a m b -> Traverse1 f a ('S m) b
step where
start :: Traverse1 f a 'Z b
start :: Traverse1 f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
(Vec ('S n) a -> f (Vec ('S n) b)) -> Traverse1 f a n b
Traverse1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
_) -> (forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
step :: Traverse1 f a m b -> Traverse1 f a ('S m) b
step :: forall (m :: Nat). Traverse1 f a m b -> Traverse1 f a ('S m) b
step (Traverse1 Vec ('S m) a -> f (Vec ('S m) b)
go) = forall (f :: * -> *) a (n :: Nat) b.
(Vec ('S n) a -> f (Vec ('S n) b)) -> Traverse1 f a n b
Traverse1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) (a -> f b
f a
x) (Vec ('S m) a -> f (Vec ('S m) b)
go Vec n a
xs)
newtype Traverse1 f a n b = Traverse1 { forall (f :: * -> *) a (n :: Nat) b.
Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b)
getTraverse1 :: Vec ('S n) a -> f (Vec ('S n) b) }
#endif
itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse = forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b -> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
getITraverse forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 ITraverse f a 'Z b
start forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step where
start :: ITraverse f a 'Z b
start :: ITraverse f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f (Vec n b))
-> ITraverse f a n b
ITraverse forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> f b
_ Vec 'Z a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Vec 'Z a
VNil
step :: ITraverse f a m b -> ITraverse f a ('S m) b
step :: forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step (ITraverse (Fin m -> a -> f b) -> Vec m a -> f (Vec m b)
go) = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f (Vec n b))
-> ITraverse f a n b
ITraverse forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> f b
f (a
x ::: Vec n a
xs) -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) (Fin ('S m) -> a -> f b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x) ((Fin m -> a -> f b) -> Vec m a -> f (Vec m b)
go (Fin ('S m) -> a -> f b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs)
newtype ITraverse f a n b = ITraverse { forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b -> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }
itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ = forall (f :: * -> *) a (n :: Nat) b.
ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ()
getITraverse_ forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 ITraverse_ f a 'Z b
start forall (m :: Nat). ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step where
start :: ITraverse_ f a 'Z b
start :: ITraverse_ f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f ()) -> ITraverse_ f a n b
ITraverse_ forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> f b
_ Vec 'Z a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step :: forall (m :: Nat). ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step (ITraverse_ (Fin m -> a -> f b) -> Vec m a -> f ()
go) = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f ()) -> ITraverse_ f a n b
ITraverse_ forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> f b
f (a
x ::: Vec n a
xs) -> Fin ('S m) -> a -> f b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Fin m -> a -> f b) -> Vec m a -> f ()
go (Fin ('S m) -> a -> f b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
newtype ITraverse_ f a n b = ITraverse_ { forall (f :: * -> *) a (n :: Nat) b.
ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ()
getITraverse_ :: (Fin n -> a -> f b) -> Vec n a -> f () }
foldMap :: (Monoid m, N.SNatI n) => (a -> m) -> Vec n a -> m
foldMap :: forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(a -> m) -> Vec n a -> m
foldMap a -> m
f = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 (forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty)) forall a b. (a -> b) -> a -> b
$ \(Fold Vec m a -> m
go) ->
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a -> m
f a
x forall a. Monoid a => a -> a -> a
`mappend` Vec m a -> m
go Vec n a
xs
newtype Fold a n b = Fold { forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold :: Vec n a -> b }
foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s
foldMap1 :: forall s a (n :: Nat).
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f = forall a (n :: Nat) b. Fold1 a n b -> Vec ('S n) a -> b
getFold1 forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Fold1 a 'Z s
start forall (m :: Nat). Fold1 a m s -> Fold1 a ('S m) s
step where
start :: Fold1 a 'Z s
start :: Fold1 a 'Z s
start = forall a (n :: Nat) b. (Vec ('S n) a -> b) -> Fold1 a n b
Fold1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
_) -> a -> s
f a
x
step :: Fold1 a m s -> Fold1 a ('S m) s
step :: forall (m :: Nat). Fold1 a m s -> Fold1 a ('S m) s
step (Fold1 Vec ('S m) a -> s
g) = forall a (n :: Nat) b. (Vec ('S n) a -> b) -> Fold1 a n b
Fold1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a -> s
f a
x forall a. Semigroup a => a -> a -> a
<> Vec ('S m) a -> s
g Vec n a
xs
newtype Fold1 a n b = Fold1 { forall a (n :: Nat) b. Fold1 a n b -> Vec ('S n) a -> b
getFold1 :: Vec ('S n) a -> b }
ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap :: forall a (n :: Nat) m.
(Monoid m, SNatI n) =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap = forall a (n :: Nat) m.
IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m
getIFoldMap forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 IFoldMap a 'Z m
start forall (p :: Nat). IFoldMap a p m -> IFoldMap a ('S p) m
step where
start :: IFoldMap a 'Z m
start :: IFoldMap a 'Z m
start = forall a (n :: Nat) m.
((Fin n -> a -> m) -> Vec n a -> m) -> IFoldMap a n m
IFoldMap forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> m
_ Vec 'Z a
_ -> forall a. Monoid a => a
mempty
step :: IFoldMap a p m -> IFoldMap a ('S p) m
step :: forall (p :: Nat). IFoldMap a p m -> IFoldMap a ('S p) m
step (IFoldMap (Fin p -> a -> m) -> Vec p a -> m
go) = forall a (n :: Nat) m.
((Fin n -> a -> m) -> Vec n a -> m) -> IFoldMap a n m
IFoldMap forall a b. (a -> b) -> a -> b
$ \Fin ('S p) -> a -> m
f (a
x ::: Vec n a
xs) -> Fin ('S p) -> a -> m
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall a. Monoid a => a -> a -> a
`mappend` (Fin p -> a -> m) -> Vec p a -> m
go (Fin ('S p) -> a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
newtype IFoldMap a n m = IFoldMap { forall a (n :: Nat) m.
IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m
getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }
ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 :: forall a (n :: Nat) s.
(Semigroup s, SNatI n) =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 = forall a (n :: Nat) m.
IFoldMap1 a n m -> (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m
getIFoldMap1 forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 IFoldMap1 a 'Z s
start forall (p :: Nat). IFoldMap1 a p s -> IFoldMap1 a ('S p) s
step where
start :: IFoldMap1 a 'Z s
start :: IFoldMap1 a 'Z s
start = forall a (n :: Nat) m.
((Fin ('S n) -> a -> m) -> Vec ('S n) a -> m) -> IFoldMap1 a n m
IFoldMap1 forall a b. (a -> b) -> a -> b
$ \Fin ('S 'Z) -> a -> s
f (a
x ::: Vec n a
_) -> Fin ('S 'Z) -> a -> s
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x
step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s
step :: forall (p :: Nat). IFoldMap1 a p s -> IFoldMap1 a ('S p) s
step (IFoldMap1 (Fin ('S p) -> a -> s) -> Vec ('S p) a -> s
go) = forall a (n :: Nat) m.
((Fin ('S n) -> a -> m) -> Vec ('S n) a -> m) -> IFoldMap1 a n m
IFoldMap1 forall a b. (a -> b) -> a -> b
$ \Fin ('S ('S p)) -> a -> s
f (a
x ::: Vec n a
xs) -> Fin ('S ('S p)) -> a -> s
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall a. Semigroup a => a -> a -> a
<> (Fin ('S p) -> a -> s) -> Vec ('S p) a -> s
go (Fin ('S ('S p)) -> a -> s
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
newtype IFoldMap1 a n m = IFoldMap1 { forall a (n :: Nat) m.
IFoldMap1 a n m -> (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m
getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }
foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b
foldr :: forall a b (n :: Nat).
SNatI n =>
(a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 Fold a 'Z b
start forall (m :: Nat). Fold a m b -> Fold a ('S m) b
step where
start :: Fold a 'Z b
start :: Fold a 'Z b
start = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> b
z
step :: Fold a m b -> Fold a ('S m) b
step :: forall (m :: Nat). Fold a m b -> Fold a ('S m) b
step (Fold Vec m a -> b
go) = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a -> b -> b
f a
x (Vec m a -> b
go Vec n a
xs)
ifoldr :: forall a b n. N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr :: forall a b (n :: Nat).
SNatI n =>
(Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr = forall a (n :: Nat) b.
IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b
getIFoldr forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 IFoldr a 'Z b
start forall (m :: Nat). IFoldr a m b -> IFoldr a ('S m) b
step where
start :: IFoldr a 'Z b
start :: IFoldr a 'Z b
start = forall a (n :: Nat) b.
((Fin n -> a -> b -> b) -> b -> Vec n a -> b) -> IFoldr a n b
IFoldr forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b -> b
_ b
z Vec 'Z a
_ -> b
z
step :: IFoldr a m b -> IFoldr a ('S m) b
step :: forall (m :: Nat). IFoldr a m b -> IFoldr a ('S m) b
step (IFoldr (Fin m -> a -> b -> b) -> b -> Vec m a -> b
go) = forall a (n :: Nat) b.
((Fin n -> a -> b -> b) -> b -> Vec n a -> b) -> IFoldr a n b
IFoldr forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b -> b
f b
z (a
x ::: Vec n a
xs) -> Fin ('S m) -> a -> b -> b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x ((Fin m -> a -> b -> b) -> b -> Vec m a -> b
go (Fin ('S m) -> a -> b -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) b
z Vec n a
xs)
newtype IFoldr a n b = IFoldr { forall a (n :: Nat) b.
IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b
getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }
length :: forall n a. N.SNatI n => Vec n a -> Int
length :: forall (n :: Nat) a. SNatI n => Vec n a -> Int
length Vec n a
_ = forall (n :: Nat). Length n -> Int
getLength Length n
l where
l :: Length n
l :: Length n
l = forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). Int -> Length n
Length Int
0) forall a b. (a -> b) -> a -> b
$ \(Length Int
n) -> forall (n :: Nat). Int -> Length n
Length (Int
1 forall a. Num a => a -> a -> a
+ Int
n)
newtype Length (n :: Nat) = Length { forall (n :: Nat). Length n -> Int
getLength :: Int }
sum :: (Num a, N.SNatI n) => Vec n a -> a
sum :: forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
sum = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. Num a => Fold a 'Z a
start forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step where
start :: Num a => Fold a 'Z a
start :: forall a. Num a => Fold a 'Z a
start = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> a
0
step :: Num a => Fold a m a -> Fold a ('S m) a
step :: forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step (Fold Vec m a -> a
f) = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a
x forall a. Num a => a -> a -> a
+ Vec m a -> a
f Vec n a
xs
product :: (Num a, N.SNatI n) => Vec n a -> a
product :: forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
product = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. Num a => Fold a 'Z a
start forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step where
start :: Num a => Fold a 'Z a
start :: forall a. Num a => Fold a 'Z a
start = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> a
1
step :: Num a => Fold a m a -> Fold a ('S m) a
step :: forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step (Fold Vec m a -> a
f) = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> a
x forall a. Num a => a -> a -> a
* Vec m a -> a
f Vec n a
xs
zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith :: forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
f = forall a b c (n :: Nat).
ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c
getZipWith forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction ZipWith a b c 'Z
start forall (m :: Nat). ZipWith a b c m -> ZipWith a b c ('S m)
step where
start :: ZipWith a b c 'Z
start :: ZipWith a b c 'Z
start = forall a b c (n :: Nat).
(Vec n a -> Vec n b -> Vec n c) -> ZipWith a b c n
ZipWith forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z b
_ -> forall a. Vec 'Z a
VNil
step :: ZipWith a b c m -> ZipWith a b c ('S m)
step :: forall (m :: Nat). ZipWith a b c m -> ZipWith a b c ('S m)
step (ZipWith Vec m a -> Vec m b -> Vec m c
go) = forall a b c (n :: Nat).
(Vec n a -> Vec n b -> Vec n c) -> ZipWith a b c n
ZipWith forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) -> a -> b -> c
f a
x b
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m b -> Vec m c
go Vec n a
xs Vec n b
ys
newtype ZipWith a b c n = ZipWith { forall a b c (n :: Nat).
ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c
getZipWith :: Vec n a -> Vec n b -> Vec n c }
izipWith :: N.SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith :: forall (n :: Nat) a b c.
SNatI n =>
(Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith = forall a b c (n :: Nat).
IZipWith a b c n
-> (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
getIZipWith forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction forall a b c. IZipWith a b c 'Z
start forall a b c (m :: Nat). IZipWith a b c m -> IZipWith a b c ('S m)
step where
start :: IZipWith a b c 'Z
start :: forall a b c. IZipWith a b c 'Z
start = forall a b c (n :: Nat).
((Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c)
-> IZipWith a b c n
IZipWith forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b -> c
_ Vec 'Z a
_ Vec 'Z b
_ -> forall a. Vec 'Z a
VNil
step :: IZipWith a b c m -> IZipWith a b c ('S m)
step :: forall a b c (m :: Nat). IZipWith a b c m -> IZipWith a b c ('S m)
step (IZipWith (Fin m -> a -> b -> c) -> Vec m a -> Vec m b -> Vec m c
go) = forall a b c (n :: Nat).
((Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c)
-> IZipWith a b c n
IZipWith forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b -> c
f (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) -> Fin ('S m) -> a -> b -> c
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x b
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: (Fin m -> a -> b -> c) -> Vec m a -> Vec m b -> Vec m c
go (Fin ('S m) -> a -> b -> c
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs Vec n b
ys
newtype IZipWith a b c n = IZipWith { forall a b c (n :: Nat).
IZipWith a b c n
-> (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
getIZipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c }
repeat :: N.SNatI n => x -> Vec n x
repeat :: forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat x
x = forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. Vec 'Z a
VNil (x
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
:::)
bind :: N.SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b
bind :: forall (n :: Nat) a b.
SNatI n =>
Vec n a -> (a -> Vec n b) -> Vec n b
bind = forall a (n :: Nat) b.
Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b
getBind forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a b. Bind a 'Z b
start forall a (m :: Nat) b. Bind a m b -> Bind a ('S m) b
step where
start :: Bind a 'Z b
start :: forall a b. Bind a 'Z b
start = forall a (n :: Nat) b.
(Vec n a -> (a -> Vec n b) -> Vec n b) -> Bind a n b
Bind forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ a -> Vec 'Z b
_ -> forall a. Vec 'Z a
VNil
step :: Bind a m b -> Bind a ('S m) b
step :: forall a (m :: Nat) b. Bind a m b -> Bind a ('S m) b
step (Bind Vec m a -> (a -> Vec m b) -> Vec m b
go) = forall a (n :: Nat) b.
(Vec n a -> (a -> Vec n b) -> Vec n b) -> Bind a n b
Bind forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) a -> Vec ('S m) b
f -> forall (n :: Nat) a. Vec ('S n) a -> a
head (a -> Vec ('S m) b
f a
x) forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec m a -> (a -> Vec m b) -> Vec m b
go Vec n a
xs (forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vec ('S m) b
f)
newtype Bind a n b = Bind { forall a (n :: Nat) b.
Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b
getBind :: Vec n a -> (a -> Vec n b) -> Vec n b }
join :: N.SNatI n => Vec n (Vec n a) -> Vec n a
join :: forall (n :: Nat) a. SNatI n => Vec n (Vec n a) -> Vec n a
join = forall (n :: Nat) a. Join n a -> Vec n (Vec n a) -> Vec n a
getJoin forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. Join 'Z a
start forall (m :: Nat) a. SNatI m => Join m a -> Join ('S m) a
step where
start :: Join 'Z a
start :: forall a. Join 'Z a
start = forall (n :: Nat) a. (Vec n (Vec n a) -> Vec n a) -> Join n a
Join forall a b. (a -> b) -> a -> b
$ \Vec 'Z (Vec 'Z a)
_ -> forall a. Vec 'Z a
VNil
step :: N.SNatI m => Join m a -> Join ('S m) a
step :: forall (m :: Nat) a. SNatI m => Join m a -> Join ('S m) a
step (Join Vec m (Vec m a) -> Vec m a
go) = forall (n :: Nat) a. (Vec n (Vec n a) -> Vec n a) -> Join n a
Join forall a b. (a -> b) -> a -> b
$ \(Vec ('S m) a
x ::: Vec n (Vec ('S m) a)
xs) -> forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S m) a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec m (Vec m a) -> Vec m a
go (forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail Vec n (Vec ('S m) a)
xs)
newtype Join n a = Join { forall (n :: Nat) a. Join n a -> Vec n (Vec n a) -> Vec n a
getJoin :: Vec n (Vec n a) -> Vec n a }
universe :: N.SNatI n => Vec n (Fin n)
universe :: forall (n :: Nat). SNatI n => Vec n (Fin n)
universe = forall (n :: Nat). Universe n -> Vec n (Fin n)
getUniverse (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Universe 'Z
first forall (m :: Nat). SNatI m => Universe m -> Universe ('S m)
step) where
first :: Universe 'Z
first :: Universe 'Z
first = forall (n :: Nat). Vec n (Fin n) -> Universe n
Universe forall a. Vec 'Z a
VNil
step :: N.SNatI m => Universe m -> Universe ('S m)
step :: forall (m :: Nat). SNatI m => Universe m -> Universe ('S m)
step (Universe Vec m (Fin m)
go) = forall (n :: Nat). Vec n (Fin n) -> Universe n
Universe (forall (n1 :: Nat). Fin ('S n1)
FZ forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS Vec m (Fin m)
go)
newtype Universe n = Universe { forall (n :: Nat). Universe n -> Vec n (Fin n)
getUniverse :: Vec n (Fin n) }