{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
-- | A variant of "Data.Vec.Lazy" with functions written using 'N.SNatI'.
-- The hypothesis is that these (goursive) functions could be fully unrolled,
-- if the 'Vec' size @n@ is known at compile time.
--
-- The module has the same API as "Data.Vec.Lazy" (sans 'L.withDict' and 'foldl'').
-- /Note:/ instance methods aren't changed, the 'Vec' type is the same.
module Data.Vec.Lazy.Inline (
    Vec (..),
    -- * Construction
    empty,
    singleton,
    -- * Conversions
    toPull,
    fromPull,
    toList,
    toNonEmpty,
    fromList,
    fromListPrefix,
    reifyList,
    -- * Indexing
    (!),
    tabulate,
    cons,
    snoc,
    head,
    last,
    tail,
    init,
    -- * Concatenation and splitting
    (++),
    split,
    concatMap,
    concat,
    chunks,
    -- * Reverse
    reverse,
    -- * Folds
    foldMap,
    foldMap1,
    ifoldMap,
    ifoldMap1,
    foldr,
    ifoldr,
    -- * Special folds
    length,
    null,
    sum,
    product,
    -- * Mapping
    map,
    imap,
    traverse,
#ifdef MIN_VERSION_semigroupoids
    traverse1,
#endif
    itraverse,
    itraverse_,
    -- * Zipping
    zipWith,
    izipWith,
    repeat,
    -- * Monadic
    bind,
    join,
    -- * Universe
    universe,
    -- * VecEach
    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)

--- Instances

#ifdef MIN_VERSION_semigroupoids
import Data.Functor.Apply (Apply, liftF2)
#endif

-- vec siblings
import qualified Data.Fin      as F
import qualified Data.Type.Nat as N
import qualified Data.Vec.Pull as P

-- $setup
-- >>> :set -XScopedTypeVariables
-- >>> import Data.Proxy (Proxy (..))
-- >>> import Prelude (Char, not, uncurry, Bool (..), Maybe (..), ($), (<$>), id, (.), Int)
-- >>> import qualified Data.Type.Nat as N
-- >>> import Data.Fin (Fin (..))

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Convert to pull 'P.Vec'.
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 }

-- | Convert from pull 'P.Vec'.
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 }

-- | Convert 'Vec' to list.
--
-- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
-- "foo"
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 $ 1 ::: 2 ::: 3 ::: VNil
-- 1 :| [2,3]
--
-- @since 0.4
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

-- | Convert list @[a]@ to @'Vec' n a@.
-- Returns 'Nothing' if lengths don't match exactly.
--
-- >>> fromList "foo" :: Maybe (Vec N.Nat3 Char)
-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- >>> fromList "quux" :: Maybe (Vec N.Nat3 Char)
-- Nothing
--
-- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)
-- Nothing
--
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) }

-- | Convert list @[a]@ to @'Vec' n a@.
-- Returns 'Nothing' if input list is too short.
--
-- >>> fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)
-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- >>> fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)
-- Just ('q' ::: 'u' ::: 'u' ::: VNil)
--
-- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)
-- Nothing
--
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 -- different than in fromList case

    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'

-------------------------------------------------------------------------------
-- Indexing
-------------------------------------------------------------------------------

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 }

-- | Indexing.
--
-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
-- 'b'
--
(!) :: 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

-- | Tabulating, inverse of '!'.
--
-- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
-- 0 ::: 1 ::: 2 ::: VNil
--
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

-- | Add a single element at the end of a 'Vec'.
--
-- @since 0.2.1
--
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 }

-- | The last element of a 'Vec'.
--
-- @since 0.4
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 }

-- | The elements before the 'last' of a 'Vec'.
--
-- @since 0.4
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
-------------------------------------------------------------------------------

-- | Reverse 'Vec'.
--
-- >>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)
-- 'c' ::: 'b' ::: 'a' ::: VNil
--
-- @since 0.2.1
--
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 }

-------------------------------------------------------------------------------
-- Concatenation
-------------------------------------------------------------------------------

infixr 5 ++

-- | Append two 'Vec'.
--
-- >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
-- 'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
--
(++) :: 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 vector into two parts. Inverse of '++'.
--
-- >>> split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)
-- ('a' ::: VNil,'b' ::: 'c' ::: VNil)
--
-- >>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))
-- 'a' ::: 'b' ::: 'c' ::: VNil
--
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) }
-- | Map over all the elements of a 'Vec' and concatenate the resulting 'Vec's.
--
-- >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
-- 'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil
--
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 }

-- | @'concatMap' 'id'@
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

-- | Inverse of 'concat'.
--
-- >>> chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))
-- Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)
--
-- >>> let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)
-- >>> concat . idVec . chunks <$> fromListPrefix [1..]
-- Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)
--
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) }

-------------------------------------------------------------------------------
-- Mapping
-------------------------------------------------------------------------------

-- | >>> map not $ True ::: False ::: VNil
-- False ::: True ::: VNil
--
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 (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
-- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
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 }

-- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.
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
-- | Apply an action to non-empty 'Vec', yielding a 'Vec' of results.
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

-- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.
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) }

-- | Apply an action to every element of a 'Vec' and its index, ignoring the results.
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 () }

-------------------------------------------------------------------------------
-- Folding
-------------------------------------------------------------------------------

-- | See 'I.Foldable'.
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 }

-- | See 'I.Foldable1'.
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 }

-- | See 'I.FoldableWithIndex'.
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 }

-- | There is no type-class for this :(
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 }

-- | Right fold.
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)

-- | Right fold with an index.
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 }

-- | Yield the length of a 'Vec'. /O(n)/
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 }

-------------------------------------------------------------------------------
-- Special folds
-------------------------------------------------------------------------------

-- | Non-strict 'sum'.
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

-- | Non-strict 'product'.
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

-------------------------------------------------------------------------------
-- Zipping
-------------------------------------------------------------------------------

-- | Zip two 'Vec's with a function.
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 }

-- | Zip two 'Vec's. with a function that also takes the elements' indices.
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 value
--
-- >>> repeat 'x' :: Vec N.Nat3 Char
-- 'x' ::: 'x' ::: 'x' ::: VNil
--
-- @since 0.2.1
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
:::)

-------------------------------------------------------------------------------
-- Monadic
-------------------------------------------------------------------------------

-- | Monadic bind.
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 }

-- | Monadic join.
--
-- >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
-- 'a' ::: 'd' ::: VNil
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
-------------------------------------------------------------------------------

-- | Get all @'Fin' n@ in a @'Vec' n@.
--
-- >>> universe :: Vec N.Nat3 (Fin N.Nat3)
-- 0 ::: 1 ::: 2 ::: VNil
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) }