{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
-- | Spine-strict length-indexed list defined as data-family: 'Vec'.
--
-- Data family variant allows  lazy pattern matching.
-- On the other hand, the 'Vec' value doesn't "know" its length (i.e. there isn't 'Data.Vec.Lazy.withDict').
--
-- == Agda
--
-- If you happen to familiar with Agda, then the difference
-- between GADT and data-family version is maybe clearer:
--
-- @
-- module Vec where
--
-- open import Data.Nat
-- open import Relation.Binary.PropositionalEquality using (_≡_; refl)
--
-- -- \"GADT"
-- data Vec (A : Set) : ℕ → Set where
--   []  : Vec A 0
--   _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
--
-- infixr 50 _∷_
--
-- exVec : Vec ℕ 2
-- exVec = 13 ∷ 37 ∷ []
--
-- -- "data family"
-- data Unit : Set where
--   [] : Unit
--
-- data _×_ (A B : Set) : Set where
--   _∷_ : A → B → A × B
--
-- infixr 50 _×_
--
-- VecF : Set → ℕ → Set
-- VecF A zero    = Unit
-- VecF A (suc n) = A × VecF A n
--
-- exVecF : VecF ℕ 2
-- exVecF = 13 ∷ 37 ∷ []
--
-- reduction : VecF ℕ 2 ≡ ℕ × ℕ × Unit
-- reduction = refl
-- @
--
module Data.Vec.DataFamily.SpineStrict (
    Vec (..),
    -- * Construction
    empty,
    singleton,
    -- * Conversions
    toPull,
    fromPull,
    toList,
    toNonEmpty,
    fromList,
    fromListPrefix,
    reifyList,
    -- * Indexing
    (!),
    tabulate,
    cons,
    snoc,
    head,
    last,
    tail,
    init,
    -- * Reverse
    reverse,
    -- * Concatenation and splitting
    (++),
    split,
    concatMap,
    concat,
    chunks,
    -- * 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,
    -- * Extras
    ensureSpine,
    ) where

import Prelude
       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
       Ord (..), Ordering (EQ), Show (..), ShowS, const, flip, id, seq,
       showParen, showString, uncurry, ($), (&&), (.))

import Control.Applicative (Applicative (..), liftA2, (<$>))
import Control.DeepSeq     (NFData (..))
import Data.Fin            (Fin (..))
import Data.List.NonEmpty  (NonEmpty (..))
import Data.Hashable       (Hashable (..))
import Data.Monoid         (Monoid (..))
import Data.Nat            (Nat (..))
import Data.Semigroup      (Semigroup (..))

--- Instances
import qualified Data.Foldable    as I (Foldable (..))
import qualified Data.Traversable as I (Traversable (..))
import qualified Test.QuickCheck  as QC

import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))

import Data.Functor.Classes (Eq1 (..), Ord1 (..), Show1 (..))

#ifdef MIN_VERSION_adjunctions
import qualified Data.Functor.Rep as I (Representable (..))
#endif

#ifdef MIN_VERSION_distributive
import Data.Distributive (Distributive (..))
#endif

#ifdef MIN_VERSION_semigroupoids
import Data.Functor.Apply (Apply (..))

import qualified Data.Functor.Bind          as I (Bind (..))
import qualified Data.Semigroup.Foldable    as I (Foldable1 (..))
import qualified Data.Semigroup.Traversable as I (Traversable1 (..))
#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 -XDataKinds
-- >>> import Data.Proxy (Proxy (..))
-- >>> import Control.Applicative ((<$>))
-- >>> import Prelude (Char, not, uncurry, error, Eq (..), Ord (..), Bool (..), Maybe (..), ($), id, (.), Int)
-- >>> import qualified Data.Type.Nat as N
-- >>> import Data.Fin (Fin (..))
-- >>> import Data.Nat (Nat (..))

-------------------------------------------------------------------------------
-- Type
-------------------------------------------------------------------------------

infixr 5 :::

-- | Vector, i.e. length-indexed list.
data family   Vec (n :: Nat) a
data instance Vec 'Z     a = VNil
data instance Vec ('S n) a = a ::: !(Vec n a)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

-- |
--
-- >>> 'a' ::: 'b' ::: VNil == 'a' ::: 'c' ::: VNil
-- False
instance (Eq a, N.SNatI n) => Eq (Vec n a) where
    == :: Vec n a -> Vec n a -> Bool
(==) = forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Equal a a 'Z
start forall (m :: Nat). Equal a a m -> Equal a a ('S m)
step) where
        start :: Equal a a 'Z
        start :: Equal a a 'Z
start = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z a
_ -> Bool
True

        step :: Equal a a m -> Equal a a ('S m)
        step :: forall (m :: Nat). Equal a a m -> Equal a a ('S m)
step (Equal Vec m a -> Vec m a -> Bool
go) = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (a
y ::: Vec m a
ys) ->
            a
x forall a. Eq a => a -> a -> Bool
== a
y Bool -> Bool -> Bool
&& Vec m a -> Vec m a -> Bool
go Vec m a
xs Vec m a
ys

newtype Equal a b n = Equal { forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual :: Vec n a -> Vec n b -> Bool }

-- |
--
-- >>> compare ('a' ::: 'b' ::: VNil) ('a' ::: 'c' ::: VNil)
-- LT
instance (Ord a, N.SNatI n) => Ord (Vec n a) where
    compare :: Vec n a -> Vec n a -> Ordering
compare = forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Compare a a 'Z
start forall (m :: Nat). Compare a a m -> Compare a a ('S m)
step) where
        start :: Compare a a 'Z
        start :: Compare a a 'Z
start = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z a
_ -> Ordering
EQ

        step :: Compare a a m -> Compare a a ('S m)
        step :: forall (m :: Nat). Compare a a m -> Compare a a ('S m)
step (Compare Vec m a -> Vec m a -> Ordering
go) = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (a
y ::: Vec m a
ys) ->
            forall a. Ord a => a -> a -> Ordering
compare a
x a
y forall a. Semigroup a => a -> a -> a
<> Vec m a -> Vec m a -> Ordering
go Vec m a
xs Vec m a
ys

newtype Compare a b n = Compare { forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare :: Vec n a -> Vec n b -> Ordering }

instance (Show a, N.SNatI n) => Show (Vec n a) where
    showsPrec :: Int -> Vec n a -> ShowS
showsPrec = forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec (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 ShowsPrec 'Z a
start forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step) where
        start :: ShowsPrec 'Z a
        start :: ShowsPrec 'Z a
start = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
_ Vec 'Z a
_ -> String -> ShowS
showString String
"VNil"

        step :: ShowsPrec m a -> ShowsPrec ('S m) a
        step :: forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step (ShowsPrec Int -> Vec m a -> ShowS
go) = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
d (a
x ::: Vec m a
xs) -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
5)
            forall a b. (a -> b) -> a -> b
$ forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 a
x
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ::: "
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Vec m a -> ShowS
go Int
5 Vec m a
xs

newtype ShowsPrec n a = ShowsPrec { forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec :: Int -> Vec n a -> ShowS }

instance N.SNatI n => Functor (Vec n) where
    fmap :: forall a b. (a -> b) -> Vec n a -> Vec n b
fmap = forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map

instance N.SNatI n => I.Foldable (Vec n) where
    foldMap :: forall m a. Monoid m => (a -> m) -> Vec n a -> m
foldMap = forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(a -> m) -> Vec n a -> m
foldMap

    foldr :: forall a b. (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
    -- foldl' = foldl'

#if MIN_VERSION_base(4,8,0)
    null :: forall a. Vec n a -> Bool
null    = forall (n :: Nat) a. SNatI n => Vec n a -> Bool
null
    length :: forall a. Vec n a -> Int
length  = forall (n :: Nat) a. SNatI n => Vec n a -> Int
length
    sum :: forall a. Num a => Vec n a -> a
sum     = forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
sum
    product :: forall a. Num a => Vec n a -> a
product = forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
product
#endif

#ifdef MIN_VERSION_semigroupoids
instance (N.SNatI m, n ~ 'S m) => I.Foldable1 (Vec n) where
    foldMap1 :: forall m a. Semigroup m => (a -> m) -> Vec n a -> m
foldMap1 = forall s a (n :: Nat).
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1

instance (N.SNatI m, n ~ 'S m) => I.Traversable1 (Vec n) where
    traverse1 :: forall (f :: * -> *) a b.
Apply f =>
(a -> f b) -> Vec n a -> f (Vec 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
#endif

instance N.SNatI n => I.Traversable (Vec n) where
    traverse :: forall (f :: * -> *) a b.
Applicative f =>
(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

-- | @since 0.4
instance N.SNatI n => WI.FunctorWithIndex (Fin n) (Vec n) where
    imap :: forall a b. (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

-- | @since 0.4
instance N.SNatI n => WI.FoldableWithIndex (Fin n) (Vec n) where
    ifoldMap :: forall m a. Monoid m => (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
    ifoldr :: forall a b. (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

-- | @since 0.4
instance N.SNatI n => WI.TraversableWithIndex (Fin n) (Vec n) where
    itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(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

instance (NFData a, N.SNatI n) => NFData (Vec n a) where
    rnf :: Vec n a -> ()
rnf = forall (n :: Nat) a. Rnf n a -> Vec n a -> ()
getRnf (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}. Rnf 'Z a
z forall {a} {n :: Nat}. NFData a => Rnf n a -> Rnf ('S n) a
s) where
        z :: Rnf 'Z a
z           = forall (n :: Nat) a. (Vec n a -> ()) -> Rnf n a
Rnf forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
R:VecZa a
VNil -> ()
        s :: Rnf n a -> Rnf ('S n) a
s (Rnf Vec n a -> ()
rec) = forall (n :: Nat) a. (Vec n a -> ()) -> Rnf n a
Rnf forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> forall a. NFData a => a -> ()
rnf a
x seq :: forall a b. a -> b -> b
`seq` Vec n a -> ()
rec Vec n a
xs

newtype Rnf n a = Rnf { forall (n :: Nat) a. Rnf n a -> Vec n a -> ()
getRnf :: Vec n a -> () }

instance (Hashable a, N.SNatI n) => Hashable (Vec n a) where
    hashWithSalt :: Int -> Vec n a -> Int
hashWithSalt = forall (n :: Nat) a. HashWithSalt n a -> Int -> Vec n a -> Int
getHashWithSalt (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}. HashWithSalt 'Z a
z forall {a} {n :: Nat}.
Hashable a =>
HashWithSalt n a -> HashWithSalt ('S n) a
s) where
        z :: HashWithSalt 'Z a
z = forall (n :: Nat) a. (Int -> Vec n a -> Int) -> HashWithSalt n a
HashWithSalt forall a b. (a -> b) -> a -> b
$ \Int
salt Vec 'Z a
R:VecZa a
VNil -> Int
salt forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)
        s :: HashWithSalt n a -> HashWithSalt ('S n) a
s (HashWithSalt Int -> Vec n a -> Int
rec) = forall (n :: Nat) a. (Int -> Vec n a -> Int) -> HashWithSalt n a
HashWithSalt forall a b. (a -> b) -> a -> b
$ \Int
salt (a
x ::: Vec n a
xs) -> Int -> Vec n a -> Int
rec (Int
salt
            forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
x) Vec n a
xs

newtype HashWithSalt n a = HashWithSalt { forall (n :: Nat) a. HashWithSalt n a -> Int -> Vec n a -> Int
getHashWithSalt :: Int -> Vec n a -> Int }

instance N.SNatI n => Applicative (Vec n) where
    pure :: forall a. a -> Vec n a
pure a
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 (a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
:::)
    <*> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
(<*>)  = forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a b. (a -> b) -> a -> b
($)
    Vec n a
_ *> :: forall a b. Vec n a -> Vec n b -> Vec n b
*> Vec n b
x = Vec n b
x
    Vec n a
x <* :: forall a b. Vec n a -> Vec n b -> Vec n a
<* Vec n b
_ = Vec n a
x
#if MIN_VERSION_base(4,10,0)
    liftA2 :: forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftA2 = forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith
#endif

instance N.SNatI n => Monad (Vec n) where
    return :: forall a. a -> Vec n a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: forall a b. Vec n a -> (a -> Vec n b) -> Vec n b
(>>=)  = forall (n :: Nat) a b.
SNatI n =>
Vec n a -> (a -> Vec n b) -> Vec n b
bind
    Vec n a
_ >> :: forall a b. Vec n a -> Vec n b -> Vec n b
>> Vec n b
x = Vec n b
x

#ifdef MIN_VERSION_distributive
instance N.SNatI n => Distributive (Vec n) where
    distribute :: forall (f :: * -> *) a. Functor f => f (Vec n a) -> Vec n (f a)
distribute f (Vec n a)
f = forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (n :: Nat) a. SNatI n => Vec n a -> Fin n -> a
! Fin n
k) f (Vec n a)
f)

#ifdef MIN_VERSION_adjunctions
instance N.SNatI n => I.Representable (Vec n) where
    type Rep (Vec n) = Fin n
    tabulate :: forall a. (Rep (Vec n) -> a) -> Vec n a
tabulate = forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate
    index :: forall a. Vec n a -> Rep (Vec n) -> a
index    = forall (n :: Nat) a. SNatI n => Vec n a -> Fin n -> a
(!)
#endif
#endif

instance (Semigroup a, N.SNatI n) => Semigroup (Vec n a) where
    <> :: Vec n a -> Vec n a -> Vec n a
(<>) = forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a. Semigroup a => a -> a -> a
(<>)

instance (Monoid a, N.SNatI n) => Monoid (Vec n a) where
    mempty :: Vec n a
mempty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
    mappend :: Vec n a -> Vec n a -> Vec n a
mappend = forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a. Monoid a => a -> a -> a
mappend

#ifdef MIN_VERSION_semigroupoids
instance N.SNatI n => Apply (Vec n) where
    <.> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
(<.>) = forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a b. (a -> b) -> a -> b
($)
    Vec n a
_ .> :: forall a b. Vec n a -> Vec n b -> Vec n b
.> Vec n b
x = Vec n b
x
    Vec n a
x <. :: forall a b. Vec n a -> Vec n b -> Vec n a
<. Vec n b
_ = Vec n a
x
    liftF2 :: forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftF2 = forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith

instance N.SNatI n => I.Bind (Vec n) where
    >>- :: forall a b. Vec n a -> (a -> Vec n b) -> Vec n b
(>>-) = forall (n :: Nat) a b.
SNatI n =>
Vec n a -> (a -> Vec n b) -> Vec n b
bind
    join :: forall a. Vec n (Vec n a) -> Vec n a
join  = forall (n :: Nat) a. SNatI n => Vec n (Vec n a) -> Vec n a
join
#endif

-------------------------------------------------------------------------------
-- Data.Functor.Classes
-------------------------------------------------------------------------------

#ifndef MIN_VERSION_transformers_compat
#define MIN_VERSION_transformers_compat(x,y,z) 0
#endif


#if MIN_VERSION_base(4,9,0)
#define LIFTED_FUNCTOR_CLASSES 1
#else
#if MIN_VERSION_transformers(0,5,0)
#define LIFTED_FUNCTOR_CLASSES 1
#else
#if MIN_VERSION_transformers_compat(0,5,0) && !MIN_VERSION_transformers(0,4,0)
#define LIFTED_FUNCTOR_CLASSES 1
#endif
#endif
#endif

#if LIFTED_FUNCTOR_CLASSES

-- | @since 0.4
instance N.SNatI n => Eq1 (Vec n) where
    liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
    liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
liftEq a -> b -> Bool
eq = forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Equal a b 'Z
start forall (m :: Nat). Equal a b m -> Equal a b ('S m)
step) where
        start :: Equal a b 'Z
        start :: Equal a b 'Z
start = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z b
_ -> Bool
True

        step :: Equal a b m -> Equal a b ('S m)
        step :: forall (m :: Nat). Equal a b m -> Equal a b ('S m)
step (Equal Vec m a -> Vec m b -> Bool
go) = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (b
y ::: Vec m b
ys) ->
            a -> b -> Bool
eq a
x b
y Bool -> Bool -> Bool
&& Vec m a -> Vec m b -> Bool
go Vec m a
xs Vec m b
ys

-- | @since 0.4
instance N.SNatI n => Ord1 (Vec n) where
    liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
    liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
liftCompare a -> b -> Ordering
cmp = forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Compare a b 'Z
start forall (m :: Nat). Compare a b m -> Compare a b ('S m)
step) where
        start :: Compare a b 'Z
        start :: Compare a b 'Z
start = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z b
_ -> Ordering
EQ

        step :: Compare a b m -> Compare a b ('S m)
        step :: forall (m :: Nat). Compare a b m -> Compare a b ('S m)
step (Compare Vec m a -> Vec m b -> Ordering
go) = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (b
y ::: Vec m b
ys) ->
            a -> b -> Ordering
cmp a
x b
y forall a. Semigroup a => a -> a -> a
<> Vec m a -> Vec m b -> Ordering
go Vec m a
xs Vec m b
ys

-- | @since 0.4
instance N.SNatI n => Show1 (Vec n) where
    liftShowsPrec :: forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
    liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
_ = forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec (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 ShowsPrec 'Z a
start forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step) where
        start :: ShowsPrec 'Z a
        start :: ShowsPrec 'Z a
start = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
_ Vec 'Z a
_ -> String -> ShowS
showString String
"VNil"

        step :: ShowsPrec m a -> ShowsPrec ('S m) a
        step :: forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step (ShowsPrec Int -> Vec m a -> ShowS
go) = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
d (a
x ::: Vec m a
xs) -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
5)
            forall a b. (a -> b) -> a -> b
$ Int -> a -> ShowS
sp Int
6 a
x
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ::: "
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Vec m a -> ShowS
go Int
5 Vec m a
xs
#else
-- | @since 0.4
instance N.SNatI n => Eq1 (Vec n) where eq1 = (==)

-- | @since 0.4
instance N.SNatI n => Ord1 (Vec n) where compare1 = compare

-- | @since 0.4
instance N.SNatI n => Show1 (Vec n) where showsPrec1 = showsPrec
#endif
-------------------------------------------------------------------------------
-- Construction
-------------------------------------------------------------------------------

-- | Empty 'Vec'.
empty :: Vec 'Z a
empty :: forall a. Vec 'Z a
empty = forall a. Vec 'Z a
VNil

-- | 'Vec' with exactly one element.
--
-- >>> singleton True
-- True ::: VNil
--
singleton :: a -> Vec ('S 'Z) a
singleton :: forall a. a -> Vec ('S 'Z) a
singleton a
x = a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil

-------------------------------------------------------------------------------
-- 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 m 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 m 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 (n :: Nat) a. 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 m a
xs) -> a
x forall a. a -> [a] -> [a]
: Vec m a -> [a]
f Vec m 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 (n :: Nat) a. 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 (n :: Nat) a. 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'

-- | Reify any list @[a]@ to @'Vec' n a@.
--
-- >>> reifyList "foo" length
-- 3
reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r
reifyList :: forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList []       forall (n :: Nat). SNatI n => Vec n a -> r
f = forall (n :: Nat). SNatI n => Vec n a -> r
f forall a. Vec 'Z a
VNil
reifyList (a
x : [a]
xs) forall (n :: Nat). SNatI n => Vec n a -> r
f = forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [a]
xs forall a b. (a -> b) -> a -> b
$ \Vec n a
xs' -> forall (n :: Nat). SNatI n => Vec n a -> r
f (a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec n 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 m 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 m 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

-- | Cons an element in front of a 'Vec'.
cons :: a -> Vec n a -> Vec ('S n) a
cons :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons = forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::)

-- | Add a single element at the end of a 'Vec'.
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 (n :: Nat) a. 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 m a
ys) -> a
y forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec ('S m) a
rec Vec m 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 first element of a 'Vec'.
head :: Vec ('S n) a -> a
head :: forall (n :: Nat) a. Vec ('S n) a -> a
head (a
x ::: Vec n a
_) = a
x

-- | The elements after the 'head' of a 'Vec'.
tail :: Vec ('S n) a -> Vec n a
tail :: forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail (a
_ ::: Vec n a
xs) = Vec n a
xs

-- | 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 'Z a
R:VecZa 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 ('S m) a
ys) -> Vec ('S m) a -> a
rec Vec ('S m) 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 ('S m) a
ys) -> a
y forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec ('S m) a -> Vec m a
rec Vec ('S m) 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 m 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 m 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 p a
xs) -> a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec p a -> Vec (Plus p m) a
f Vec p 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 (Plus n m) a
xs) -> case Vec (Plus n m) a -> (Vec n a, Vec m a)
f Vec (Plus n m) a
xs of
        (Vec n a
ys, Vec m a
zs) -> (a
x forall (n :: Nat) a. 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 p 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 p 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 (n :: Nat) a. 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 m a
xs) -> a -> b
f a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m b
go Vec m 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 m a
xs) -> Fin ('S m) -> a -> b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall (n :: Nat) a. 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 m 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 m a
xs) -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) (a -> f b
f a
x) (Vec m a -> f (Vec m b)
go Vec m a
xs)
{-# INLINE traverse #-}

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 'Z a
_) -> (forall (n :: Nat) a. 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 ('S m) a
xs) -> forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 forall (n :: Nat) a. 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 ('S m) 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 m a
xs) -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall (n :: Nat) a. 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 m a
xs)
{-# INLINE itraverse #-}

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 m 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 m 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 m a
xs) -> a -> m
f a
x forall a. Monoid a => a -> a -> a
`mappend` Vec m a -> m
go Vec m 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 'Z 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 ('S m) a
xs) -> a -> s
f a
x forall a. Semigroup a => a -> a -> a
<> Vec ('S m) a -> s
g Vec ('S m) 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 p 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 p 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 'Z 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 ('S p) 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 ('S p) 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 m a
xs) -> a -> b -> b
f a
x (Vec m a -> b
go Vec m 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 m 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 m 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 }

-- | Test whether a 'Vec' is empty. /O(1)/
null :: forall n a. N.SNatI n => Vec n a -> Bool
null :: forall (n :: Nat) a. SNatI n => Vec n a -> Bool
null Vec n a
_ = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
    SNat n
N.SZ -> Bool
True
    SNat n
N.SS -> Bool
False

-------------------------------------------------------------------------------
-- 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 m a
xs) -> a
x forall a. Num a => a -> a -> a
+ Vec m a -> a
f Vec m 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 m a
xs) -> a
x forall a. Num a => a -> a -> a
* Vec m a -> a
f Vec m 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 m a
xs) (b
y ::: Vec m b
ys) -> a -> b -> c
f a
x b
y forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m b -> Vec m c
go Vec m a
xs Vec m 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 m a
xs) (b
y ::: Vec m b
ys) -> Fin ('S m) -> a -> b -> c
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x b
y forall (n :: Nat) a. 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 m a
xs Vec m 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 (n :: Nat) a. 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 m 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 (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> (a -> Vec m b) -> Vec m b
go Vec m 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 m (Vec ('S m) a)
xs) -> forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S m) a
x forall (n :: Nat) a. 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 m (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 (n :: Nat) a. 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) }

-------------------------------------------------------------------------------
-- EnsureSpine
-------------------------------------------------------------------------------

-- | Ensure spine.
--
-- If we have an undefined 'Vec',
--
-- >>> let v = error "err" :: Vec N.Nat3 Char
--
-- And insert data into it later:
--
-- >>> let setHead :: a -> Vec ('S n) a -> Vec ('S n) a; setHead x (_ ::: xs) = x ::: xs
--
-- Then without a spine, it will fail:
--
-- >>> head $ setHead 'x' v
-- *** Exception: err
-- ...
--
-- But with the spine, it won't:
--
-- >>> head $ setHead 'x' $ ensureSpine v
-- 'x'
--
ensureSpine :: N.SNatI n => Vec n a -> Vec n a
ensureSpine :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
ensureSpine = forall (n :: Nat) a. EnsureSpine n a -> Vec n a -> Vec n a
getEnsureSpine (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. EnsureSpine 'Z a
first forall (m :: Nat) a. EnsureSpine m a -> EnsureSpine ('S m) a
step) where
    first :: EnsureSpine 'Z a
    first :: forall a. EnsureSpine 'Z a
first = forall (n :: Nat) a. (Vec n a -> Vec n a) -> EnsureSpine n a
EnsureSpine forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil

    step :: EnsureSpine m a -> EnsureSpine ('S m) a
    step :: forall (m :: Nat) a. EnsureSpine m a -> EnsureSpine ('S m) a
step (EnsureSpine Vec m a -> Vec m a
go) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> EnsureSpine n a
EnsureSpine forall a b. (a -> b) -> a -> b
$ \ ~(a
x ::: Vec m a
xs) -> a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m a
go Vec m a
xs

newtype EnsureSpine n a = EnsureSpine { forall (n :: Nat) a. EnsureSpine n a -> Vec n a -> Vec n a
getEnsureSpine :: Vec n a -> Vec n a }

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance N.SNatI n => QC.Arbitrary1 (Vec n) where
    liftArbitrary :: forall a. Gen a -> Gen (Vec n a)
liftArbitrary = forall (n :: Nat) a. SNatI n => Gen a -> Gen (Vec n a)
liftArbitrary
    liftShrink :: forall a. (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink    = forall (n :: Nat) a. SNatI n => (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink

liftArbitrary :: forall n a. N.SNatI n => QC.Gen a -> QC.Gen (Vec n a)
liftArbitrary :: forall (n :: Nat) a. SNatI n => Gen a -> Gen (Vec n a)
liftArbitrary Gen a
arb = forall (n :: Nat) a. Arb n a -> Gen (Vec n a)
getArb 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 (n :: Nat) a. Gen (Vec n a) -> Arb n a
Arb (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Vec 'Z a
VNil)) forall (m :: Nat). Arb m a -> Arb ('S m) a
step where
    step :: Arb m a -> Arb ('S m) a
    step :: forall (m :: Nat). Arb m a -> Arb ('S m) a
step (Arb Gen (Vec m a)
rec) = forall (n :: Nat) a. Gen (Vec n a) -> Arb n a
Arb forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
arb forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Vec m a)
rec

newtype Arb n a = Arb { forall (n :: Nat) a. Arb n a -> Gen (Vec n a)
getArb :: QC.Gen (Vec n a) }

liftShrink :: forall n a. N.SNatI n => (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink :: forall (n :: Nat) a. SNatI n => (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink a -> [a]
shr = forall (n :: Nat) a. Shr n a -> Vec n a -> [Vec n a]
getShr 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 (n :: Nat) a. (Vec n a -> [Vec n a]) -> Shr n a
Shr forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
R:VecZa a
VNil -> []) forall (m :: Nat). Shr m a -> Shr ('S m) a
step where
    step :: Shr m a -> Shr ('S m) a
    step :: forall (m :: Nat). Shr m a -> Shr ('S m) a
step (Shr Vec m a -> [Vec m a]
rec) = forall (n :: Nat) a. (Vec n a -> [Vec n a]) -> Shr n a
Shr forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) ->
        forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> * -> *) a b.
Arbitrary2 f =>
(a -> [a]) -> (b -> [b]) -> f a b -> [f a b]
QC.liftShrink2 a -> [a]
shr Vec m a -> [Vec m a]
rec (a
x, Vec m a
xs)

newtype Shr n a = Shr { forall (n :: Nat) a. Shr n a -> Vec n a -> [Vec n a]
getShr :: Vec n a -> [Vec n a] }

instance (N.SNatI n, QC.Arbitrary a) => QC.Arbitrary (Vec n a) where
    arbitrary :: Gen (Vec n a)
arbitrary = forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => Gen (f a)
QC.arbitrary1
    shrink :: Vec n a -> [Vec n a]
shrink    = forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => f a -> [f a]
QC.shrink1

instance (N.SNatI n, QC.CoArbitrary a) => QC.CoArbitrary (Vec n a) where
    coarbitrary :: forall b. Vec n a -> Gen b -> Gen b
coarbitrary Vec n a
v = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
        SNat n
N.SS -> forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (case Vec n a
v of (a
x ::: Vec n1 a
xs) -> forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (a
x, Vec n1 a
xs))

instance (N.SNatI n, QC.Function a) => QC.Function (Vec n a) where
    function :: forall b. (Vec n a -> b) -> Vec n a :-> b
function = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\Vec n a
R:VecZa a
VNil -> ()) (\() -> forall a. Vec 'Z a
VNil)
        SNat n
N.SS -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(a
x ::: Vec n1 a
xs) -> (a
x, Vec n1 a
xs)) (\(a
x,Vec n1 a
xs) -> a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec n1 a
xs)