{-# 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
(==) = Equal a a n -> Vec n a -> Vec n a -> Bool
forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual (Equal a a 'Z
-> (forall (m :: Nat). SNatI m => Equal a a m -> Equal a a ('S m))
-> Equal a a n
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). SNatI m => Equal a a m -> Equal a a ('S m)
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 = (Vec 'Z a -> Vec 'Z a -> Bool) -> Equal a a 'Z
forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal ((Vec 'Z a -> Vec 'Z a -> Bool) -> Equal a a 'Z)
-> (Vec 'Z a -> Vec 'Z a -> Bool) -> Equal a a 'Z
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 :: Equal a a m -> Equal a a ('S m)
step (Equal Vec m a -> Vec m a -> Bool
go) = (Vec ('S m) a -> Vec ('S m) a -> Bool) -> Equal a a ('S m)
forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal ((Vec ('S m) a -> Vec ('S m) a -> Bool) -> Equal a a ('S m))
-> (Vec ('S m) a -> Vec ('S m) a -> Bool) -> Equal a a ('S m)
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) (y ::: ys) ->
            a
x a -> a -> Bool
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 { 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 = Compare a a n -> Vec n a -> Vec n a -> Ordering
forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare (Compare a a 'Z
-> (forall (m :: Nat).
    SNatI m =>
    Compare a a m -> Compare a a ('S m))
-> Compare a a n
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). SNatI m => Compare a a m -> Compare a a ('S m)
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 = (Vec 'Z a -> Vec 'Z a -> Ordering) -> Compare a a 'Z
forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare ((Vec 'Z a -> Vec 'Z a -> Ordering) -> Compare a a 'Z)
-> (Vec 'Z a -> Vec 'Z a -> Ordering) -> Compare a a 'Z
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 :: Compare a a m -> Compare a a ('S m)
step (Compare Vec m a -> Vec m a -> Ordering
go) = (Vec ('S m) a -> Vec ('S m) a -> Ordering) -> Compare a a ('S m)
forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare ((Vec ('S m) a -> Vec ('S m) a -> Ordering) -> Compare a a ('S m))
-> (Vec ('S m) a -> Vec ('S m) a -> Ordering) -> Compare a a ('S m)
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) (y ::: ys) ->
            a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y Ordering -> Ordering -> Ordering
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 { 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 = ShowsPrec n a -> Int -> Vec n a -> ShowS
forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec (ShowsPrec 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    ShowsPrec m a -> ShowsPrec ('S m) a)
-> ShowsPrec n a
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). SNatI m => ShowsPrec m a -> ShowsPrec ('S m) a
forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step) where
        start :: ShowsPrec 'Z a
        start :: ShowsPrec 'Z a
start = (Int -> Vec 'Z a -> ShowS) -> ShowsPrec 'Z a
forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec ((Int -> Vec 'Z a -> ShowS) -> ShowsPrec 'Z a)
-> (Int -> Vec 'Z a -> ShowS) -> ShowsPrec 'Z a
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 :: ShowsPrec m a -> ShowsPrec ('S m) a
step (ShowsPrec Int -> Vec m a -> ShowS
go) = (Int -> Vec ('S m) a -> ShowS) -> ShowsPrec ('S m) a
forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec ((Int -> Vec ('S m) a -> ShowS) -> ShowsPrec ('S m) a)
-> (Int -> Vec ('S m) a -> ShowS) -> ShowsPrec ('S m) a
forall a b. (a -> b) -> a -> b
$ \Int
d (x ::: xs) -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5)
            (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 a
x
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ::: "
            ShowS -> ShowS -> ShowS
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 { ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec :: Int -> Vec n a -> ShowS }

instance N.SNatI n => Functor (Vec n) where
    fmap :: (a -> b) -> Vec n a -> Vec n b
fmap = (a -> b) -> Vec n a -> Vec n b
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 :: (a -> m) -> Vec n a -> m
foldMap = (a -> m) -> Vec n a -> m
forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(a -> m) -> Vec n a -> m
foldMap

    foldr :: (a -> b -> b) -> b -> Vec n a -> b
foldr  = (a -> b -> b) -> b -> Vec n a -> b
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 :: Vec n a -> Bool
null    = Vec n a -> Bool
forall (n :: Nat) a. SNatI n => Vec n a -> Bool
null
    length :: Vec n a -> Int
length  = Vec n a -> Int
forall (n :: Nat) a. SNatI n => Vec n a -> Int
length
    sum :: Vec n a -> a
sum     = Vec n a -> a
forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
sum
    product :: Vec n a -> a
product = Vec n a -> a
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 :: (a -> m) -> Vec n a -> m
foldMap1 = (a -> m) -> Vec n a -> m
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 :: (a -> f b) -> Vec n a -> f (Vec n b)
traverse1 = (a -> f b) -> Vec n a -> f (Vec n b)
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 :: (a -> f b) -> Vec n a -> f (Vec n b)
traverse = (a -> f b) -> Vec n a -> f (Vec n b)
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 :: (Fin n -> a -> b) -> Vec n a -> Vec n b
imap = (Fin n -> a -> b) -> Vec n a -> Vec n b
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 :: (Fin n -> a -> m) -> Vec n a -> m
ifoldMap = (Fin n -> a -> m) -> Vec n a -> m
forall a (n :: Nat) m.
(Monoid m, SNatI n) =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap
    ifoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr   = (Fin n -> a -> b -> b) -> b -> Vec n a -> b
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 :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse = (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
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 = Rnf n a -> Vec n a -> ()
forall (n :: Nat) a. Rnf n a -> Vec n a -> ()
getRnf (Rnf 'Z a
-> (forall (m :: Nat). SNatI m => Rnf m a -> Rnf ('S m) a)
-> Rnf n a
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 Rnf 'Z a
forall a. Rnf 'Z a
z forall a (n :: Nat). NFData a => Rnf n a -> Rnf ('S n) a
forall (m :: Nat). SNatI m => Rnf m a -> Rnf ('S m) a
s) where
        z :: Rnf 'Z a
z           = (Vec 'Z a -> ()) -> Rnf 'Z a
forall (n :: Nat) a. (Vec n a -> ()) -> Rnf n a
Rnf ((Vec 'Z a -> ()) -> Rnf 'Z a) -> (Vec 'Z a -> ()) -> Rnf 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
VNil -> ()
        s :: Rnf n a -> Rnf ('S n) a
s (Rnf Vec n a -> ()
rec) = (Vec ('S n) a -> ()) -> Rnf ('S n) a
forall (n :: Nat) a. (Vec n a -> ()) -> Rnf n a
Rnf ((Vec ('S n) a -> ()) -> Rnf ('S n) a)
-> (Vec ('S n) a -> ()) -> Rnf ('S n) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a -> ()
forall a. NFData a => a -> ()
rnf a
x () -> () -> ()
`seq` Vec n a -> ()
rec Vec n a
xs

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

newtype HashWithSalt n a = HashWithSalt { HashWithSalt n a -> Int -> Vec n a -> Int
getHashWithSalt :: Int -> Vec n a -> Int }

instance N.SNatI n => Applicative (Vec n) where
    pure :: a -> Vec n a
pure a
x = Vec 'Z a
-> (forall (m :: Nat). SNatI m => Vec m a -> Vec ('S m) a)
-> Vec n a
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 Vec 'Z a
forall a. Vec 'Z a
VNil (a
x a -> Vec m a -> Vec ('S m) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
:::)
    <*> :: Vec n (a -> b) -> Vec n a -> Vec n b
(<*>)  = ((a -> b) -> 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 (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    Vec n a
_ *> :: Vec n a -> Vec n b -> Vec n b
*> Vec n b
x = Vec n b
x
    Vec n a
x <* :: Vec n a -> Vec n b -> Vec n a
<* Vec n b
_ = Vec n a
x
#if MIN_VERSION_base(4,10,0)
    liftA2 :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftA2 = (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
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 :: a -> Vec n a
return = a -> Vec n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: Vec n a -> (a -> Vec n b) -> Vec n 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
_ >> :: 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 :: f (Vec n a) -> Vec n (f a)
distribute f (Vec n a)
f = (Fin n -> f a) -> Vec n (f a)
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
k -> (Vec n a -> a) -> f (Vec n a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Vec n a -> Fin n -> a
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 :: (Rep (Vec n) -> a) -> Vec n a
tabulate = (Rep (Vec n) -> a) -> Vec n a
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate
    index :: Vec n a -> Rep (Vec n) -> a
index    = (!)
#endif
#endif

instance (Semigroup a, N.SNatI n) => Semigroup (Vec n a) where
    <> :: Vec n a -> Vec n a -> Vec n a
(<>) = (a -> a -> a) -> 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 a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)

instance (Monoid a, N.SNatI n) => Monoid (Vec n a) where
    mempty :: Vec n a
mempty = a -> Vec n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall a. Monoid a => a
mempty
    mappend :: Vec n a -> Vec n a -> Vec n a
mappend = (a -> a -> a) -> 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 a -> a -> a
forall a. Monoid a => a -> a -> a
mappend

#ifdef MIN_VERSION_semigroupoids
instance N.SNatI n => Apply (Vec n) where
    <.> :: Vec n (a -> b) -> Vec n a -> Vec n b
(<.>) = ((a -> b) -> 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 (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    Vec n a
_ .> :: Vec n a -> Vec n b -> Vec n b
.> Vec n b
x = Vec n b
x
    Vec n a
x <. :: Vec n a -> Vec n b -> Vec n a
<. Vec n b
_ = Vec n a
x
    liftF2 :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftF2 = (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
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
    >>- :: Vec n a -> (a -> Vec n b) -> Vec n 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 :: Vec n (Vec n a) -> Vec n a
join  = Vec n (Vec n a) -> Vec n a
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 :: (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
liftEq a -> b -> Bool
eq = Equal a b n -> Vec n a -> Vec n b -> Bool
forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual (Equal a b 'Z
-> (forall (m :: Nat). SNatI m => Equal a b m -> Equal a b ('S m))
-> Equal a b n
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). SNatI m => Equal a b m -> Equal a b ('S m)
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 = (Vec 'Z a -> Vec 'Z b -> Bool) -> Equal a b 'Z
forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal ((Vec 'Z a -> Vec 'Z b -> Bool) -> Equal a b 'Z)
-> (Vec 'Z a -> Vec 'Z b -> Bool) -> Equal a b 'Z
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 :: Equal a b m -> Equal a b ('S m)
step (Equal Vec m a -> Vec m b -> Bool
go) = (Vec ('S m) a -> Vec ('S m) b -> Bool) -> Equal a b ('S m)
forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal ((Vec ('S m) a -> Vec ('S m) b -> Bool) -> Equal a b ('S m))
-> (Vec ('S m) a -> Vec ('S m) b -> Bool) -> Equal a b ('S m)
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) (y ::: 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 :: (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
liftCompare a -> b -> Ordering
cmp = Compare a b n -> Vec n a -> Vec n b -> Ordering
forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare (Compare a b 'Z
-> (forall (m :: Nat).
    SNatI m =>
    Compare a b m -> Compare a b ('S m))
-> Compare a b n
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). SNatI m => Compare a b m -> Compare a b ('S m)
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 = (Vec 'Z a -> Vec 'Z b -> Ordering) -> Compare a b 'Z
forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare ((Vec 'Z a -> Vec 'Z b -> Ordering) -> Compare a b 'Z)
-> (Vec 'Z a -> Vec 'Z b -> Ordering) -> Compare a b 'Z
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 :: Compare a b m -> Compare a b ('S m)
step (Compare Vec m a -> Vec m b -> Ordering
go) = (Vec ('S m) a -> Vec ('S m) b -> Ordering) -> Compare a b ('S m)
forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare ((Vec ('S m) a -> Vec ('S m) b -> Ordering) -> Compare a b ('S m))
-> (Vec ('S m) a -> Vec ('S m) b -> Ordering) -> Compare a b ('S m)
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) (y ::: ys) ->
            a -> b -> Ordering
cmp a
x b
y Ordering -> Ordering -> Ordering
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 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
_ = ShowsPrec n a -> Int -> Vec n a -> ShowS
forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec (ShowsPrec 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    ShowsPrec m a -> ShowsPrec ('S m) a)
-> ShowsPrec n a
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). SNatI m => ShowsPrec m a -> ShowsPrec ('S m) a
forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step) where
        start :: ShowsPrec 'Z a
        start :: ShowsPrec 'Z a
start = (Int -> Vec 'Z a -> ShowS) -> ShowsPrec 'Z a
forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec ((Int -> Vec 'Z a -> ShowS) -> ShowsPrec 'Z a)
-> (Int -> Vec 'Z a -> ShowS) -> ShowsPrec 'Z a
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 :: ShowsPrec m a -> ShowsPrec ('S m) a
step (ShowsPrec Int -> Vec m a -> ShowS
go) = (Int -> Vec ('S m) a -> ShowS) -> ShowsPrec ('S m) a
forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec ((Int -> Vec ('S m) a -> ShowS) -> ShowsPrec ('S m) a)
-> (Int -> Vec ('S m) a -> ShowS) -> ShowsPrec ('S m) a
forall a b. (a -> b) -> a -> b
$ \Int
d (x ::: xs) -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5)
            (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> a -> ShowS
sp Int
6 a
x
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ::: "
            ShowS -> ShowS -> ShowS
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 :: Vec 'Z a
empty = Vec 'Z a
forall a. Vec 'Z a
VNil

-- | 'Vec' with exactly one element.
--
-- >>> singleton True
-- True ::: VNil
--
singleton :: a -> Vec ('S 'Z) a
singleton :: a -> Vec ('S 'Z) a
singleton a
x = a
x a -> Vec 'Z a -> Vec ('S 'Z) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec 'Z 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 :: Vec n a -> Vec n a
toPull = ToPull n a -> Vec n a -> Vec n a
forall (n :: Nat) a. ToPull n a -> Vec n a -> Vec n a
getToPull (ToPull 'Z a
-> (forall (m :: Nat). SNatI m => ToPull m a -> ToPull ('S m) a)
-> ToPull n a
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). SNatI m => ToPull m a -> ToPull ('S m) a
forall (m :: Nat). ToPull m a -> ToPull ('S m) a
step) where
    start :: ToPull 'Z a
    start :: ToPull 'Z a
start = (Vec 'Z a -> Vec 'Z a) -> ToPull 'Z a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> ToPull n a
ToPull ((Vec 'Z a -> Vec 'Z a) -> ToPull 'Z a)
-> (Vec 'Z a -> Vec 'Z a) -> ToPull 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> (Fin 'Z -> a) -> Vec 'Z a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec Fin 'Z -> a
forall b. Fin 'Z -> b
F.absurd

    step :: ToPull m a -> ToPull ('S m) a
    step :: ToPull m a -> ToPull ('S m) a
step (ToPull Vec m a -> Vec m a
f) = (Vec ('S m) a -> Vec ('S m) a) -> ToPull ('S m) a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> ToPull n a
ToPull ((Vec ('S m) a -> Vec ('S m) a) -> ToPull ('S m) a)
-> (Vec ('S m) a -> Vec ('S m) a) -> ToPull ('S m) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> (Fin ('S m) -> a) -> Vec ('S m) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec ((Fin ('S m) -> a) -> Vec ('S m) a)
-> (Fin ('S m) -> a) -> Vec ('S m) a
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' -> Vec m a -> Fin m -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
P.unVec (Vec m a -> Vec m a
f Vec m a
xs) Fin m
Fin n1
i'

newtype ToPull n a = ToPull { 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 :: Vec n a -> Vec n a
fromPull = FromPull n a -> Vec n a -> Vec n a
forall (n :: Nat) a. FromPull n a -> Vec n a -> Vec n a
getFromPull (FromPull 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    FromPull m a -> FromPull ('S m) a)
-> FromPull n a
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). SNatI m => FromPull m a -> FromPull ('S m) a
forall (m :: Nat). FromPull m a -> FromPull ('S m) a
step) where
    start :: FromPull 'Z a
    start :: FromPull 'Z a
start = (Vec 'Z a -> Vec 'Z a) -> FromPull 'Z a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> FromPull n a
FromPull ((Vec 'Z a -> Vec 'Z a) -> FromPull 'Z a)
-> (Vec 'Z a -> Vec 'Z a) -> FromPull 'Z a
forall a b. (a -> b) -> a -> b
$ Vec 'Z a -> Vec 'Z a -> Vec 'Z a
forall a b. a -> b -> a
const Vec 'Z a
forall a. Vec 'Z a
VNil

    step :: FromPull m a -> FromPull ('S m) a
    step :: FromPull m a -> FromPull ('S m) a
step (FromPull Vec m a -> Vec m a
f) = (Vec ('S m) a -> Vec ('S m) a) -> FromPull ('S m) a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> FromPull n a
FromPull ((Vec ('S m) a -> Vec ('S m) a) -> FromPull ('S m) a)
-> (Vec ('S m) a -> Vec ('S m) a) -> FromPull ('S m) a
forall a b. (a -> b) -> a -> b
$ \(P.Vec Fin ('S m) -> a
v) -> Fin ('S m) -> a
v Fin ('S m)
forall (n1 :: Nat). Fin ('S n1)
FZ a -> Vec m a -> Vec ('S m) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m a
f ((Fin m -> a) -> Vec m a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec (Fin ('S m) -> a
v (Fin ('S m) -> a) -> (Fin m -> Fin ('S m)) -> Fin m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> Fin ('S m)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS))

newtype FromPull n a = FromPull { 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 :: Vec n a -> [a]
toList = ToList n a -> Vec n a -> [a]
forall (n :: Nat) a. ToList n a -> Vec n a -> [a]
getToList (ToList 'Z a
-> (forall (m :: Nat). SNatI m => ToList m a -> ToList ('S m) a)
-> ToList n a
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). SNatI m => ToList m a -> ToList ('S m) a
forall (m :: Nat). ToList m a -> ToList ('S m) a
step) where
    start :: ToList 'Z a
    start :: ToList 'Z a
start = (Vec 'Z a -> [a]) -> ToList 'Z a
forall (n :: Nat) a. (Vec n a -> [a]) -> ToList n a
ToList ([a] -> Vec 'Z a -> [a]
forall a b. a -> b -> a
const [])

    step :: ToList m a -> ToList ('S m) a
    step :: ToList m a -> ToList ('S m) a
step (ToList Vec m a -> [a]
f) = (Vec ('S m) a -> [a]) -> ToList ('S m) a
forall (n :: Nat) a. (Vec n a -> [a]) -> ToList n a
ToList ((Vec ('S m) a -> [a]) -> ToList ('S m) a)
-> (Vec ('S m) a -> [a]) -> ToList ('S m) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Vec m a -> [a]
f Vec m a
xs

newtype ToList n a = ToList { 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 :: Vec ('S n) a -> NonEmpty a
toNonEmpty (x ::: xs) = a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| Vec n a -> [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 :: [a] -> Maybe (Vec n a)
fromList = FromList n a -> [a] -> Maybe (Vec n a)
forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (FromList 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    FromList m a -> FromList ('S m) a)
-> FromList n a
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 FromList 'Z a
forall a. FromList 'Z a
start forall (m :: Nat). SNatI m => FromList m a -> FromList ('S m) a
forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
    start :: FromList 'Z a
    start :: FromList 'Z a
start = ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a)
-> ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
        []      -> Vec 'Z a -> Maybe (Vec 'Z a)
forall a. a -> Maybe a
Just Vec 'Z a
forall a. Vec 'Z a
VNil
        (a
_ : [a]
_) -> Maybe (Vec 'Z a)
forall a. Maybe a
Nothing

    step :: FromList n a -> FromList ('N.S n) a
    step :: FromList n a -> FromList ('S n) a
step (FromList [a] -> Maybe (Vec n a)
f) = ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a)
-> ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
        []       -> Maybe (Vec ('S n) a)
forall a. Maybe a
Nothing
        (a
x : [a]
xs') -> (a
x a -> Vec n a -> Vec ('S n) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
:::) (Vec n a -> Vec ('S n) a)
-> Maybe (Vec n a) -> Maybe (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 { 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 :: [a] -> Maybe (Vec n a)
fromListPrefix = FromList n a -> [a] -> Maybe (Vec n a)
forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (FromList 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    FromList m a -> FromList ('S m) a)
-> FromList n a
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 FromList 'Z a
forall a. FromList 'Z a
start forall (m :: Nat). SNatI m => FromList m a -> FromList ('S m) a
forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
    start :: FromList 'Z a
    start :: FromList 'Z a
start = ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a)
-> ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall a b. (a -> b) -> a -> b
$ \[a]
_ -> Vec 'Z a -> Maybe (Vec 'Z a)
forall a. a -> Maybe a
Just Vec 'Z a
forall a. Vec 'Z a
VNil -- different than in fromList case

    step :: FromList n a -> FromList ('N.S n) a
    step :: FromList n a -> FromList ('S n) a
step (FromList [a] -> Maybe (Vec n a)
f) = ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a)
-> ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
        []       -> Maybe (Vec ('S n) a)
forall a. Maybe a
Nothing
        (a
x : [a]
xs') -> (a
x a -> Vec n a -> Vec ('S n) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
:::) (Vec n a -> Vec ('S n) a)
-> Maybe (Vec n a) -> Maybe (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 :: [a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList []       forall (n :: Nat). SNatI n => Vec n a -> r
f = Vec 'Z a -> r
forall (n :: Nat). SNatI n => Vec n a -> r
f Vec 'Z a
forall a. Vec 'Z a
VNil
reifyList (a
x : [a]
xs) forall (n :: Nat). SNatI n => Vec n a -> r
f = [a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [a]
xs ((forall (n :: Nat). SNatI n => Vec n a -> r) -> r)
-> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Vec n a
xs' -> Vec ('S n) a -> r
forall (n :: Nat). SNatI n => Vec n a -> r
f (a
x a -> Vec n a -> Vec ('S n) a
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 :: Fin n -> Vec n a -> a
flipIndex = Index n a -> Fin n -> Vec n a -> a
forall (n :: Nat) a. Index n a -> Fin n -> Vec n a -> a
getIndex (Index 'Z a
-> (forall (m :: Nat). SNatI m => Index m a -> Index ('S m) a)
-> Index n a
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 Index 'Z a
forall a. Index 'Z a
start forall (m :: Nat). SNatI m => Index m a -> Index ('S m) a
forall (m :: Nat) a. Index m a -> Index ('S m) a
step) where
    start :: Index 'Z a
    start :: Index 'Z a
start = (Fin 'Z -> Vec 'Z a -> a) -> Index 'Z a
forall (n :: Nat) a. (Fin n -> Vec n a -> a) -> Index n a
Index Fin 'Z -> Vec 'Z a -> a
forall b. Fin 'Z -> b
F.absurd

    step :: Index m a-> Index ('N.S m) a
    step :: Index m a -> Index ('S m) a
step (Index Fin m -> Vec m a -> a
go) = (Fin ('S m) -> Vec ('S m) a -> a) -> Index ('S m) a
forall (n :: Nat) a. (Fin n -> Vec n a -> a) -> Index n a
Index ((Fin ('S m) -> Vec ('S m) a -> a) -> Index ('S m) a)
-> (Fin ('S m) -> Vec ('S m) a -> a) -> Index ('S m) a
forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
n (x ::: 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 m
Fin n1
m Vec m a
xs

newtype Index n a = Index { 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
(!) = (Fin n -> Vec n a -> a) -> Vec n a -> Fin n -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Fin n -> Vec n a -> a
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 :: (Fin n -> a) -> Vec n a
tabulate = Vec n a -> Vec n a
forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull (Vec n a -> Vec n a)
-> ((Fin n -> a) -> Vec n a) -> (Fin n -> a) -> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Fin n -> a) -> Vec n a
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 :: a -> Vec n a -> Vec ('S n) a
cons = a -> Vec n a -> Vec ('S n) a
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 :: Vec n a -> a -> Vec ('S n) a
snoc Vec n a
xs a
x = Snoc n a -> Vec n a -> Vec ('S n) a
forall (n :: Nat) a. Snoc n a -> Vec n a -> Vec ('S n) a
getSnoc (Snoc 'Z a
-> (forall (m :: Nat). SNatI m => Snoc m a -> Snoc ('S m) a)
-> Snoc n a
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). SNatI m => Snoc m a -> Snoc ('S m) a
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 = (Vec 'Z a -> Vec ('S 'Z) a) -> Snoc 'Z a
forall (n :: Nat) a. (Vec n a -> Vec ('S n) a) -> Snoc n a
Snoc ((Vec 'Z a -> Vec ('S 'Z) a) -> Snoc 'Z a)
-> (Vec 'Z a -> Vec ('S 'Z) a) -> Snoc 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
ys -> a
x a -> Vec 'Z a -> Vec ('S 'Z) a
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 :: Snoc m a -> Snoc ('S m) a
step (Snoc Vec m a -> Vec ('S m) a
rec) = (Vec ('S m) a -> Vec ('S ('S m)) a) -> Snoc ('S m) a
forall (n :: Nat) a. (Vec n a -> Vec ('S n) a) -> Snoc n a
Snoc ((Vec ('S m) a -> Vec ('S ('S m)) a) -> Snoc ('S m) a)
-> (Vec ('S m) a -> Vec ('S ('S m)) a) -> Snoc ('S m) a
forall a b. (a -> b) -> a -> b
$ \(y ::: ys) -> a
y a -> Vec ('S m) a -> Vec ('S ('S m)) a
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 { 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 :: Vec ('S n) a -> a
head (x ::: _) = a
x

-- | The elements after the 'head' of a 'Vec'.
tail :: Vec ('S n) a -> Vec n a
tail :: Vec ('S n) a -> Vec n a
tail (_ ::: 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 :: Vec ('S n) a -> a
last Vec ('S n) a
xs = Last n a -> Vec ('S n) a -> a
forall (n :: Nat) a. Last n a -> Vec ('S n) a -> a
getLast (Last 'Z a
-> (forall (m :: Nat). SNatI m => Last m a -> Last ('S m) a)
-> Last n a
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). SNatI m => Last m a -> Last ('S m) a
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 = (Vec ('S 'Z) a -> a) -> Last 'Z a
forall (n :: Nat) a. (Vec ('S n) a -> a) -> Last n a
Last ((Vec ('S 'Z) a -> a) -> Last 'Z a)
-> (Vec ('S 'Z) a -> a) -> Last 'Z a
forall a b. (a -> b) -> a -> b
$ \(x:::VNil) -> a
x
    
    step :: Last m a -> Last ('S m) a
    step :: Last m a -> Last ('S m) a
step (Last Vec ('S m) a -> a
rec) = (Vec ('S ('S m)) a -> a) -> Last ('S m) a
forall (n :: Nat) a. (Vec ('S n) a -> a) -> Last n a
Last ((Vec ('S ('S m)) a -> a) -> Last ('S m) a)
-> (Vec ('S ('S m)) a -> a) -> Last ('S m) a
forall a b. (a -> b) -> a -> b
$ \(_ ::: ys) -> Vec ('S m) a -> a
rec Vec ('S m) a
ys
    

newtype Last n a = Last { 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 :: Vec ('S n) a -> Vec n a
init Vec ('S n) a
xs = Init n a -> Vec ('S n) a -> Vec n a
forall (n :: Nat) a. Init n a -> Vec ('S n) a -> Vec n a
getInit (Init 'Z a
-> (forall (m :: Nat). SNatI m => Init m a -> Init ('S m) a)
-> Init n a
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). SNatI m => Init m a -> Init ('S m) a
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 = (Vec ('S 'Z) a -> Vec 'Z a) -> Init 'Z a
forall (n :: Nat) a. (Vec ('S n) a -> Vec n a) -> Init n a
Init (Vec 'Z a -> Vec ('S 'Z) a -> Vec 'Z a
forall a b. a -> b -> a
const Vec 'Z a
forall a. Vec 'Z a
VNil)
    
    step :: Init m a -> Init ('S m) a
    step :: Init m a -> Init ('S m) a
step (Init Vec ('S m) a -> Vec m a
rec) = (Vec ('S ('S m)) a -> Vec ('S m) a) -> Init ('S m) a
forall (n :: Nat) a. (Vec ('S n) a -> Vec n a) -> Init n a
Init ((Vec ('S ('S m)) a -> Vec ('S m) a) -> Init ('S m) a)
-> (Vec ('S ('S m)) a -> Vec ('S m) a) -> Init ('S m) a
forall a b. (a -> b) -> a -> b
$ \(y ::: ys) -> a
y a -> Vec m a -> Vec ('S m) a
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 { 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 :: Vec n a -> Vec n a
reverse = Reverse n a -> Vec n a -> Vec n a
forall (n :: Nat) a. Reverse n a -> Vec n a -> Vec n a
getReverse (Reverse 'Z a
-> (forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a)
-> Reverse n a
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 = (Vec 'Z a -> Vec 'Z a) -> Reverse 'Z a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> Reverse n a
Reverse ((Vec 'Z a -> Vec 'Z a) -> Reverse 'Z a)
-> (Vec 'Z a -> Vec 'Z a) -> Reverse 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec 'Z a
forall a. Vec 'Z a
VNil

    step :: N.SNatI m => Reverse m a -> Reverse ('S m) a
    step :: Reverse m a -> Reverse ('S m) a
step (Reverse Vec m a -> Vec m a
rec) = (Vec ('S m) a -> Vec ('S m) a) -> Reverse ('S m) a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> Reverse n a
Reverse ((Vec ('S m) a -> Vec ('S m) a) -> Reverse ('S m) a)
-> (Vec ('S m) a -> Vec ('S m) a) -> Reverse ('S m) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> Vec m a -> a -> Vec ('S m) a
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 { 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 ++ :: Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec m a
ys = Append m n a -> Vec n a -> Vec (Plus n m) a
forall (m :: Nat) (n :: Nat) a.
Append m n a -> Vec n a -> Vec (Plus n m) a
getAppend (Append m 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    Append m m a -> Append m ('S m) a)
-> Append m n a
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 (m :: Nat). SNatI m => Append m m a -> Append m ('S m) a
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 = (Vec 'Z a -> Vec (Plus 'Z m) a) -> Append m 'Z a
forall (m :: Nat) (n :: Nat) a.
(Vec n a -> Vec (Plus n m) a) -> Append m n a
Append ((Vec 'Z a -> Vec (Plus 'Z m) a) -> Append m 'Z a)
-> (Vec 'Z a -> Vec (Plus 'Z m) a) -> Append m 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec m a
Vec (Plus 'Z m) a
ys

    step :: Append m p a -> Append m ('S p) a
    step :: Append m p a -> Append m ('S p) a
step (Append Vec p a -> Vec (Plus p m) a
f) = (Vec ('S p) a -> Vec (Plus ('S p) m) a) -> Append m ('S p) a
forall (m :: Nat) (n :: Nat) a.
(Vec n a -> Vec (Plus n m) a) -> Append m n a
Append ((Vec ('S p) a -> Vec (Plus ('S p) m) a) -> Append m ('S p) a)
-> (Vec ('S p) a -> Vec (Plus ('S p) m) a) -> Append m ('S p) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a
x a -> Vec (Plus p m) a -> Vec ('S (Plus p m)) a
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 { 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 :: Vec (Plus n m) a -> (Vec n a, Vec m a)
split = Split m n a -> Vec (Plus n m) a -> (Vec n a, Vec m a)
forall (m :: Nat) (n :: Nat) a.
Split m n a -> Vec (Plus n m) a -> (Vec n a, Vec m a)
appSplit (Split m 'Z a
-> (forall (m :: Nat). SNatI m => Split m m a -> Split m ('S m) a)
-> Split m n a
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 Split m 'Z a
forall (m :: Nat) a. Split m 'Z a
start forall (m :: Nat). SNatI m => Split m m a -> Split m ('S m) a
forall (m :: Nat) (n :: Nat) a. Split m n a -> Split m ('S n) a
step) where
    start :: Split m 'Z a
    start :: Split m 'Z a
start = (Vec (Plus 'Z m) a -> (Vec 'Z a, Vec m a)) -> Split m 'Z a
forall (m :: Nat) (n :: Nat) a.
(Vec (Plus n m) a -> (Vec n a, Vec m a)) -> Split m n a
Split ((Vec (Plus 'Z m) a -> (Vec 'Z a, Vec m a)) -> Split m 'Z a)
-> (Vec (Plus 'Z m) a -> (Vec 'Z a, Vec m a)) -> Split m 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec (Plus 'Z m) a
xs -> (Vec 'Z a
forall a. Vec 'Z a
VNil, Vec m a
Vec (Plus 'Z m) a
xs)

    step :: Split m n a -> Split m ('S n) a
    step :: Split m n a -> Split m ('S n) a
step (Split Vec (Plus n m) a -> (Vec n a, Vec m a)
f) = (Vec (Plus ('S n) m) a -> (Vec ('S n) a, Vec m a))
-> Split m ('S n) a
forall (m :: Nat) (n :: Nat) a.
(Vec (Plus n m) a -> (Vec n a, Vec m a)) -> Split m n a
Split ((Vec (Plus ('S n) m) a -> (Vec ('S n) a, Vec m a))
 -> Split m ('S n) a)
-> (Vec (Plus ('S n) m) a -> (Vec ('S n) a, Vec m a))
-> Split m ('S n) a
forall a b. (a -> b) -> a -> b
$ \(x ::: 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 a -> Vec n a -> Vec ('S n) a
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 { 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 :: (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap a -> Vec m b
f = ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b
forall (m :: Nat) a (n :: Nat) b.
ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b
getConcatMap (ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b)
-> ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b
forall a b. (a -> b) -> a -> b
$ ConcatMap m a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    ConcatMap m a m b -> ConcatMap m a ('S m) b)
-> ConcatMap m a n 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 (m :: Nat).
SNatI m =>
ConcatMap m a m b -> ConcatMap m a ('S m) b
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 = (Vec 'Z a -> Vec (Mult 'Z m) b) -> ConcatMap m a 'Z b
forall (m :: Nat) a (n :: Nat) b.
(Vec n a -> Vec (Mult n m) b) -> ConcatMap m a n b
ConcatMap ((Vec 'Z a -> Vec (Mult 'Z m) b) -> ConcatMap m a 'Z b)
-> (Vec 'Z a -> Vec (Mult 'Z m) b) -> ConcatMap m a 'Z b
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec (Mult 'Z m) b
forall a. Vec 'Z a
VNil

    step :: ConcatMap m a p b -> ConcatMap m a ('S p) b
    step :: ConcatMap m a p b -> ConcatMap m a ('S p) b
step (ConcatMap Vec p a -> Vec (Mult p m) b
g) = (Vec ('S p) a -> Vec (Mult ('S p) m) b) -> ConcatMap m a ('S p) b
forall (m :: Nat) a (n :: Nat) b.
(Vec n a -> Vec (Mult n m) b) -> ConcatMap m a n b
ConcatMap ((Vec ('S p) a -> Vec (Mult ('S p) m) b) -> ConcatMap m a ('S p) b)
-> (Vec ('S p) a -> Vec (Mult ('S p) m) b)
-> ConcatMap m a ('S p) b
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a -> Vec m b
f a
x Vec m b -> Vec (Mult p m) b -> Vec (Plus m (Mult p m)) b
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 { 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 :: Vec n (Vec m a) -> Vec (Mult n m) a
concat = (Vec m a -> Vec m a) -> Vec n (Vec m a) -> Vec (Mult n m) a
forall a b (n :: Nat) (m :: Nat).
(SNatI m, SNatI n) =>
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap Vec m a -> Vec m a
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 :: Vec (Mult n m) a -> Vec n (Vec m a)
chunks = Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
forall (m :: Nat) (n :: Nat) a.
Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
getChunks (Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a))
-> Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
forall a b. (a -> b) -> a -> b
$ Chunks m 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    Chunks m m a -> Chunks m ('S m) a)
-> Chunks m n a
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 Chunks m 'Z a
forall (m :: Nat) a. Chunks m 'Z a
start forall (m :: Nat). SNatI m => Chunks m m a -> Chunks m ('S m) a
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 :: Chunks m 'Z a
start = (Vec (Mult 'Z m) a -> Vec 'Z (Vec m a)) -> Chunks m 'Z a
forall (m :: Nat) (n :: Nat) a.
(Vec (Mult n m) a -> Vec n (Vec m a)) -> Chunks m n a
Chunks ((Vec (Mult 'Z m) a -> Vec 'Z (Vec m a)) -> Chunks m 'Z a)
-> (Vec (Mult 'Z m) a -> Vec 'Z (Vec m a)) -> Chunks m 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec (Mult 'Z m) a
_ -> Vec 'Z (Vec 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 :: Chunks m n a -> Chunks m ('S n) a
step (Chunks Vec (Mult n m) a -> Vec n (Vec m a)
go) = (Vec (Mult ('S n) m) a -> Vec ('S n) (Vec m a))
-> Chunks m ('S n) a
forall (m :: Nat) (n :: Nat) a.
(Vec (Mult n m) a -> Vec n (Vec m a)) -> Chunks m n a
Chunks ((Vec (Mult ('S n) m) a -> Vec ('S n) (Vec m a))
 -> Chunks m ('S n) a)
-> (Vec (Mult ('S n) m) a -> Vec ('S n) (Vec m a))
-> Chunks m ('S n) a
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) = Vec (Plus m (Mult n m)) a -> (Vec m a, Vec (Mult n m) a)
forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec (Plus n m) a -> (Vec n a, Vec m a)
split Vec (Plus m (Mult n m)) a
Vec (Mult ('S n) m) a
xs :: (Vec m a, Vec (N.Mult n m) a)
        in Vec m a
ys Vec m a -> Vec n (Vec m a) -> Vec ('S n) (Vec m a)
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  { 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 :: (a -> b) -> Vec n a -> Vec n b
map a -> b
f = Map a n b -> Vec n a -> Vec n b
forall a (n :: Nat) b. Map a n b -> Vec n a -> Vec n b
getMap (Map a n b -> Vec n a -> Vec n b)
-> Map a n b -> Vec n a -> Vec n b
forall a b. (a -> b) -> a -> b
$ Map a 'Z b
-> (forall (m :: Nat). SNatI m => Map a m b -> Map a ('S m) b)
-> Map a n 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). SNatI m => Map a m b -> Map a ('S m) b
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 = (Vec 'Z a -> Vec 'Z b) -> Map a 'Z b
forall a (n :: Nat) b. (Vec n a -> Vec n b) -> Map a n b
Map ((Vec 'Z a -> Vec 'Z b) -> Map a 'Z b)
-> (Vec 'Z a -> Vec 'Z b) -> Map a 'Z b
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec 'Z b
forall a. Vec 'Z a
VNil

    step :: Map a m b -> Map a ('S m) b
    step :: Map a m b -> Map a ('S m) b
step (Map Vec m a -> Vec m b
go) = (Vec ('S m) a -> Vec ('S m) b) -> Map a ('S m) b
forall a (n :: Nat) b. (Vec n a -> Vec n b) -> Map a n b
Map ((Vec ('S m) a -> Vec ('S m) b) -> Map a ('S m) b)
-> (Vec ('S m) a -> Vec ('S m) b) -> Map a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a -> b
f a
x b -> Vec m b -> Vec ('S m) b
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 { 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 :: (Fin n -> a -> b) -> Vec n a -> Vec n b
imap = IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b
forall a (n :: Nat) b.
IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b
getIMap (IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b)
-> IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b
forall a b. (a -> b) -> a -> b
$ IMap a 'Z b
-> (forall (m :: Nat). SNatI m => IMap a m b -> IMap a ('S m) b)
-> IMap a n 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 IMap a 'Z b
forall a b. IMap a 'Z b
start forall a (m :: Nat) b. IMap a m b -> IMap a ('S m) b
forall (m :: Nat). SNatI m => IMap a m b -> IMap a ('S m) b
step where
    start :: IMap a 'Z b
    start :: IMap a 'Z b
start = ((Fin 'Z -> a -> b) -> Vec 'Z a -> Vec 'Z b) -> IMap a 'Z b
forall a (n :: Nat) b.
((Fin n -> a -> b) -> Vec n a -> Vec n b) -> IMap a n b
IMap (((Fin 'Z -> a -> b) -> Vec 'Z a -> Vec 'Z b) -> IMap a 'Z b)
-> ((Fin 'Z -> a -> b) -> Vec 'Z a -> Vec 'Z b) -> IMap a 'Z b
forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b
_ Vec 'Z a
_ -> Vec 'Z b
forall a. Vec 'Z a
VNil

    step :: IMap a m b -> IMap a ('S m) b
    step :: IMap a m b -> IMap a ('S m) b
step (IMap (Fin m -> a -> b) -> Vec m a -> Vec m b
go) = ((Fin ('S m) -> a -> b) -> Vec ('S m) a -> Vec ('S m) b)
-> IMap a ('S m) b
forall a (n :: Nat) b.
((Fin n -> a -> b) -> Vec n a -> Vec n b) -> IMap a n b
IMap (((Fin ('S m) -> a -> b) -> Vec ('S m) a -> Vec ('S m) b)
 -> IMap a ('S m) b)
-> ((Fin ('S m) -> a -> b) -> Vec ('S m) a -> Vec ('S m) b)
-> IMap a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b
f (x ::: xs) -> Fin ('S m) -> a -> b
f Fin ('S m)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x b -> Vec m b -> Vec ('S m) b
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 (Fin ('S m) -> a -> b) -> (Fin m -> Fin ('S m)) -> Fin m -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> Fin ('S m)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs

newtype IMap a n b = IMap { 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 :: (a -> f b) -> Vec n a -> f (Vec n b)
traverse a -> f b
f =  Traverse f a n b -> Vec n a -> f (Vec n b)
forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Vec n a -> f (Vec n b)
getTraverse (Traverse f a n b -> Vec n a -> f (Vec n b))
-> Traverse f a n b -> Vec n a -> f (Vec n b)
forall a b. (a -> b) -> a -> b
$ Traverse f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    Traverse f a m b -> Traverse f a ('S m) b)
-> Traverse f a n 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).
SNatI m =>
Traverse f a m b -> Traverse f a ('S m) b
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 = (Vec 'Z a -> f (Vec 'Z b)) -> Traverse f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
(Vec n a -> f (Vec n b)) -> Traverse f a n b
Traverse ((Vec 'Z a -> f (Vec 'Z b)) -> Traverse f a 'Z b)
-> (Vec 'Z a -> f (Vec 'Z b)) -> Traverse f a 'Z b
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec 'Z b -> f (Vec 'Z b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vec 'Z b
forall a. Vec 'Z a
VNil

    step :: Traverse f a m b -> Traverse f a ('S m) b
    step :: Traverse f a m b -> Traverse f a ('S m) b
step (Traverse Vec m a -> f (Vec m b)
go) = (Vec ('S m) a -> f (Vec ('S m) b)) -> Traverse f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
(Vec n a -> f (Vec n b)) -> Traverse f a n b
Traverse ((Vec ('S m) a -> f (Vec ('S m) b)) -> Traverse f a ('S m) b)
-> (Vec ('S m) a -> f (Vec ('S m) b)) -> Traverse f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> (b -> Vec m b -> Vec ('S m) b)
-> f b -> f (Vec m b) -> f (Vec ('S m) b)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> Vec m b -> Vec ('S m) b
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 { 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 :: (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 a -> f b
f = Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b)
forall (f :: * -> *) a (n :: Nat) b.
Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b)
getTraverse1 (Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b))
-> Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b)
forall a b. (a -> b) -> a -> b
$ Traverse1 f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    Traverse1 f a m b -> Traverse1 f a ('S m) b)
-> Traverse1 f a n 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).
SNatI m =>
Traverse1 f a m b -> Traverse1 f a ('S m) b
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 = (Vec ('S 'Z) a -> f (Vec ('S 'Z) b)) -> Traverse1 f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
(Vec ('S n) a -> f (Vec ('S n) b)) -> Traverse1 f a n b
Traverse1 ((Vec ('S 'Z) a -> f (Vec ('S 'Z) b)) -> Traverse1 f a 'Z b)
-> (Vec ('S 'Z) a -> f (Vec ('S 'Z) b)) -> Traverse1 f a 'Z b
forall a b. (a -> b) -> a -> b
$ \(x ::: _) -> (b -> Vec 'Z b -> Vec ('S 'Z) b
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec 'Z b
forall a. Vec 'Z a
VNil) (b -> Vec ('S 'Z) b) -> f b -> f (Vec ('S 'Z) b)
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 :: Traverse1 f a m b -> Traverse1 f a ('S m) b
step (Traverse1 Vec ('S m) a -> f (Vec ('S m) b)
go) = (Vec ('S ('S m)) a -> f (Vec ('S ('S m)) b))
-> Traverse1 f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
(Vec ('S n) a -> f (Vec ('S n) b)) -> Traverse1 f a n b
Traverse1 ((Vec ('S ('S m)) a -> f (Vec ('S ('S m)) b))
 -> Traverse1 f a ('S m) b)
-> (Vec ('S ('S m)) a -> f (Vec ('S ('S m)) b))
-> Traverse1 f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> (b -> Vec ('S m) b -> Vec ('S ('S m)) b)
-> f b -> f (Vec ('S m) b) -> f (Vec ('S ('S m)) b)
forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 b -> Vec ('S m) b -> Vec ('S ('S m)) b
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 { 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 :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse = ITraverse f a n b -> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b -> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
getITraverse (ITraverse f a n b
 -> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b))
-> ITraverse f a n b
-> (Fin n -> a -> f b)
-> Vec n a
-> f (Vec n b)
forall a b. (a -> b) -> a -> b
$ ITraverse f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    ITraverse f a m b -> ITraverse f a ('S m) b)
-> ITraverse f a n 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).
SNatI m =>
ITraverse f a m b -> ITraverse f a ('S m) b
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 = ((Fin 'Z -> a -> f b) -> Vec 'Z a -> f (Vec 'Z b))
-> ITraverse f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f (Vec n b))
-> ITraverse f a n b
ITraverse (((Fin 'Z -> a -> f b) -> Vec 'Z a -> f (Vec 'Z b))
 -> ITraverse f a 'Z b)
-> ((Fin 'Z -> a -> f b) -> Vec 'Z a -> f (Vec 'Z b))
-> ITraverse f a 'Z b
forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> f b
_ Vec 'Z a
_ -> Vec 'Z b -> f (Vec 'Z b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vec 'Z b
forall a. Vec 'Z a
VNil

    step :: ITraverse f a m b -> ITraverse f a ('S m) b
    step :: 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) = ((Fin ('S m) -> a -> f b) -> Vec ('S m) a -> f (Vec ('S m) b))
-> ITraverse f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f (Vec n b))
-> ITraverse f a n b
ITraverse (((Fin ('S m) -> a -> f b) -> Vec ('S m) a -> f (Vec ('S m) b))
 -> ITraverse f a ('S m) b)
-> ((Fin ('S m) -> a -> f b) -> Vec ('S m) a -> f (Vec ('S m) b))
-> ITraverse f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> f b
f (x ::: xs) -> (b -> Vec m b -> Vec ('S m) b)
-> f b -> f (Vec m b) -> f (Vec ('S m) b)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> Vec m b -> Vec ('S m) b
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) (Fin ('S m) -> a -> f b
f Fin ('S m)
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 (Fin ('S m) -> a -> f b)
-> (Fin m -> Fin ('S m)) -> Fin m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> Fin ('S m)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs)
{-# INLINE itraverse #-}

newtype ITraverse f a n b = ITraverse { 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_ :: (Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ = ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ()
forall (f :: * -> *) a (n :: Nat) b.
ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ()
getITraverse_ (ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ())
-> ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ()
forall a b. (a -> b) -> a -> b
$ ITraverse_ f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    ITraverse_ f a m b -> ITraverse_ f a ('S m) b)
-> ITraverse_ f a n 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).
SNatI m =>
ITraverse_ f a m b -> ITraverse_ f a ('S m) b
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 = ((Fin 'Z -> a -> f b) -> Vec 'Z a -> f ()) -> ITraverse_ f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f ()) -> ITraverse_ f a n b
ITraverse_ (((Fin 'Z -> a -> f b) -> Vec 'Z a -> f ()) -> ITraverse_ f a 'Z b)
-> ((Fin 'Z -> a -> f b) -> Vec 'Z a -> f ())
-> ITraverse_ f a 'Z b
forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> f b
_ Vec 'Z a
_ -> () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
    step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step (ITraverse_ (Fin m -> a -> f b) -> Vec m a -> f ()
go) = ((Fin ('S m) -> a -> f b) -> Vec ('S m) a -> f ())
-> ITraverse_ f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f ()) -> ITraverse_ f a n b
ITraverse_ (((Fin ('S m) -> a -> f b) -> Vec ('S m) a -> f ())
 -> ITraverse_ f a ('S m) b)
-> ((Fin ('S m) -> a -> f b) -> Vec ('S m) a -> f ())
-> ITraverse_ f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> f b
f (x ::: xs) -> Fin ('S m) -> a -> f b
f Fin ('S m)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x f b -> f () -> f ()
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 (Fin ('S m) -> a -> f b)
-> (Fin m -> Fin ('S m)) -> Fin m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> Fin ('S m)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs

newtype ITraverse_ f a n b = ITraverse_ { 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 :: (a -> m) -> Vec n a -> m
foldMap a -> m
f = Fold a n m -> Vec n a -> m
forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold (Fold a n m -> Vec n a -> m) -> Fold a n m -> Vec n a -> m
forall a b. (a -> b) -> a -> b
$ Fold a 'Z m
-> (forall (m :: Nat). SNatI m => Fold a m m -> Fold a ('S m) m)
-> Fold a n m
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 ((Vec 'Z a -> m) -> Fold a 'Z m
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold (m -> Vec 'Z a -> m
forall a b. a -> b -> a
const m
forall a. Monoid a => a
mempty)) ((forall (m :: Nat). SNatI m => Fold a m m -> Fold a ('S m) m)
 -> Fold a n m)
-> (forall (m :: Nat). SNatI m => Fold a m m -> Fold a ('S m) m)
-> Fold a n m
forall a b. (a -> b) -> a -> b
$ \(Fold Vec m a -> m
go) ->
    (Vec ('S m) a -> m) -> Fold a ('S m) m
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold ((Vec ('S m) a -> m) -> Fold a ('S m) m)
-> (Vec ('S m) a -> m) -> Fold a ('S m) m
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a -> m
f a
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Vec m a -> m
go Vec m a
xs

newtype Fold  a n b = Fold  { 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 :: (a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f = Fold1 a n s -> Vec ('S n) a -> s
forall a (n :: Nat) b. Fold1 a n b -> Vec ('S n) a -> b
getFold1 (Fold1 a n s -> Vec ('S n) a -> s)
-> Fold1 a n s -> Vec ('S n) a -> s
forall a b. (a -> b) -> a -> b
$ Fold1 a 'Z s
-> (forall (m :: Nat). SNatI m => Fold1 a m s -> Fold1 a ('S m) s)
-> Fold1 a n s
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). SNatI m => Fold1 a m s -> Fold1 a ('S m) s
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 = (Vec ('S 'Z) a -> s) -> Fold1 a 'Z s
forall a (n :: Nat) b. (Vec ('S n) a -> b) -> Fold1 a n b
Fold1 ((Vec ('S 'Z) a -> s) -> Fold1 a 'Z s)
-> (Vec ('S 'Z) a -> s) -> Fold1 a 'Z s
forall a b. (a -> b) -> a -> b
$ \(x ::: _) -> a -> s
f a
x

    step :: Fold1 a m s -> Fold1 a ('S m) s
    step :: Fold1 a m s -> Fold1 a ('S m) s
step (Fold1 Vec ('S m) a -> s
g) = (Vec ('S ('S m)) a -> s) -> Fold1 a ('S m) s
forall a (n :: Nat) b. (Vec ('S n) a -> b) -> Fold1 a n b
Fold1 ((Vec ('S ('S m)) a -> s) -> Fold1 a ('S m) s)
-> (Vec ('S ('S m)) a -> s) -> Fold1 a ('S m) s
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a -> s
f a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> Vec ('S m) a -> s
g Vec ('S m) a
xs

newtype Fold1 a n b = Fold1 { 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 :: (Fin n -> a -> m) -> Vec n a -> m
ifoldMap = IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m
forall a (n :: Nat) m.
IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m
getIFoldMap (IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m)
-> IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m
forall a b. (a -> b) -> a -> b
$ IFoldMap a 'Z m
-> (forall (m :: Nat).
    SNatI m =>
    IFoldMap a m m -> IFoldMap a ('S m) m)
-> IFoldMap a n m
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 (m :: Nat). SNatI m => IFoldMap a m m -> IFoldMap a ('S m) m
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 = ((Fin 'Z -> a -> m) -> Vec 'Z a -> m) -> IFoldMap a 'Z m
forall a (n :: Nat) m.
((Fin n -> a -> m) -> Vec n a -> m) -> IFoldMap a n m
IFoldMap (((Fin 'Z -> a -> m) -> Vec 'Z a -> m) -> IFoldMap a 'Z m)
-> ((Fin 'Z -> a -> m) -> Vec 'Z a -> m) -> IFoldMap a 'Z m
forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> m
_ Vec 'Z a
_ -> m
forall a. Monoid a => a
mempty

    step :: IFoldMap a p m -> IFoldMap a ('S p) m
    step :: IFoldMap a p m -> IFoldMap a ('S p) m
step (IFoldMap (Fin p -> a -> m) -> Vec p a -> m
go) = ((Fin ('S p) -> a -> m) -> Vec ('S p) a -> m)
-> IFoldMap a ('S p) m
forall a (n :: Nat) m.
((Fin n -> a -> m) -> Vec n a -> m) -> IFoldMap a n m
IFoldMap (((Fin ('S p) -> a -> m) -> Vec ('S p) a -> m)
 -> IFoldMap a ('S p) m)
-> ((Fin ('S p) -> a -> m) -> Vec ('S p) a -> m)
-> IFoldMap a ('S p) m
forall a b. (a -> b) -> a -> b
$ \Fin ('S p) -> a -> m
f (x ::: xs) -> Fin ('S p) -> a -> m
f Fin ('S p)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Fin p -> a -> m) -> Vec p a -> m
go (Fin ('S p) -> a -> m
f (Fin ('S p) -> a -> m) -> (Fin p -> Fin ('S p)) -> Fin p -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin p -> Fin ('S p)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec p a
xs

newtype IFoldMap a n m = IFoldMap { 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 :: (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 = IFoldMap1 a n s -> (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
forall a (n :: Nat) m.
IFoldMap1 a n m -> (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m
getIFoldMap1 (IFoldMap1 a n s -> (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s)
-> IFoldMap1 a n s -> (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
forall a b. (a -> b) -> a -> b
$ IFoldMap1 a 'Z s
-> (forall (m :: Nat).
    SNatI m =>
    IFoldMap1 a m s -> IFoldMap1 a ('S m) s)
-> IFoldMap1 a n s
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 (m :: Nat).
SNatI m =>
IFoldMap1 a m s -> IFoldMap1 a ('S m) s
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 = ((Fin ('S 'Z) -> a -> s) -> Vec ('S 'Z) a -> s) -> IFoldMap1 a 'Z s
forall a (n :: Nat) m.
((Fin ('S n) -> a -> m) -> Vec ('S n) a -> m) -> IFoldMap1 a n m
IFoldMap1 (((Fin ('S 'Z) -> a -> s) -> Vec ('S 'Z) a -> s)
 -> IFoldMap1 a 'Z s)
-> ((Fin ('S 'Z) -> a -> s) -> Vec ('S 'Z) a -> s)
-> IFoldMap1 a 'Z s
forall a b. (a -> b) -> a -> b
$ \Fin ('S 'Z) -> a -> s
f (x ::: _) -> Fin ('S 'Z) -> a -> s
f Fin ('S 'Z)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x

    step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s
    step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s
step (IFoldMap1 (Fin ('S p) -> a -> s) -> Vec ('S p) a -> s
go) = ((Fin ('S ('S p)) -> a -> s) -> Vec ('S ('S p)) a -> s)
-> IFoldMap1 a ('S p) s
forall a (n :: Nat) m.
((Fin ('S n) -> a -> m) -> Vec ('S n) a -> m) -> IFoldMap1 a n m
IFoldMap1 (((Fin ('S ('S p)) -> a -> s) -> Vec ('S ('S p)) a -> s)
 -> IFoldMap1 a ('S p) s)
-> ((Fin ('S ('S p)) -> a -> s) -> Vec ('S ('S p)) a -> s)
-> IFoldMap1 a ('S p) s
forall a b. (a -> b) -> a -> b
$ \Fin ('S ('S p)) -> a -> s
f (x ::: xs) -> Fin ('S ('S p)) -> a -> s
f Fin ('S ('S p))
forall (n1 :: Nat). Fin ('S n1)
FZ a
x s -> s -> s
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 (Fin ('S ('S p)) -> a -> s)
-> (Fin ('S p) -> Fin ('S ('S p))) -> Fin ('S p) -> a -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S p) -> Fin ('S ('S p))
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec ('S p) a
xs

newtype IFoldMap1 a n m = IFoldMap1 { 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 :: (a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z = Fold a n b -> Vec n a -> b
forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold (Fold a n b -> Vec n a -> b) -> Fold a n b -> Vec n a -> b
forall a b. (a -> b) -> a -> b
$ Fold a 'Z b
-> (forall (m :: Nat). SNatI m => Fold a m b -> Fold a ('S m) b)
-> Fold a n 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). SNatI m => Fold a m b -> Fold a ('S m) b
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 = (Vec 'Z a -> b) -> Fold a 'Z b
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold ((Vec 'Z a -> b) -> Fold a 'Z b) -> (Vec 'Z a -> b) -> Fold a 'Z b
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> b
z

    step :: Fold a m b -> Fold a ('S m) b
    step :: Fold a m b -> Fold a ('S m) b
step (Fold Vec m a -> b
go) = (Vec ('S m) a -> b) -> Fold a ('S m) b
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold ((Vec ('S m) a -> b) -> Fold a ('S m) b)
-> (Vec ('S m) a -> b) -> Fold a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(x ::: 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 :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr = IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b
forall a (n :: Nat) b.
IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b
getIFoldr (IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b)
-> IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b
forall a b. (a -> b) -> a -> b
$ IFoldr a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    IFoldr a m b -> IFoldr a ('S m) b)
-> IFoldr a n 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). SNatI m => IFoldr a m b -> IFoldr a ('S m) b
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 = ((Fin 'Z -> a -> b -> b) -> b -> Vec 'Z a -> b) -> IFoldr a 'Z b
forall a (n :: Nat) b.
((Fin n -> a -> b -> b) -> b -> Vec n a -> b) -> IFoldr a n b
IFoldr (((Fin 'Z -> a -> b -> b) -> b -> Vec 'Z a -> b) -> IFoldr a 'Z b)
-> ((Fin 'Z -> a -> b -> b) -> b -> Vec 'Z a -> b) -> IFoldr a 'Z b
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 :: IFoldr a m b -> IFoldr a ('S m) b
step (IFoldr (Fin m -> a -> b -> b) -> b -> Vec m a -> b
go) = ((Fin ('S m) -> a -> b -> b) -> b -> Vec ('S m) a -> b)
-> IFoldr a ('S m) b
forall a (n :: Nat) b.
((Fin n -> a -> b -> b) -> b -> Vec n a -> b) -> IFoldr a n b
IFoldr (((Fin ('S m) -> a -> b -> b) -> b -> Vec ('S m) a -> b)
 -> IFoldr a ('S m) b)
-> ((Fin ('S m) -> a -> b -> b) -> b -> Vec ('S m) a -> b)
-> IFoldr a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b -> b
f b
z (x ::: xs) -> Fin ('S m) -> a -> b -> b
f Fin ('S m)
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 (Fin ('S m) -> a -> b -> b)
-> (Fin m -> Fin ('S m)) -> Fin m -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> Fin ('S m)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) b
z Vec m a
xs)

newtype IFoldr a n b = IFoldr { 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 :: Vec n a -> Int
length Vec n a
_ = Length n -> Int
forall (n :: Nat). Length n -> Int
getLength Length n
l where
    l :: Length n
    l :: Length n
l = Length 'Z
-> (forall (m :: Nat). SNatI m => Length m -> Length ('S m))
-> Length n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (Int -> Length 'Z
forall (n :: Nat). Int -> Length n
Length Int
0) ((forall (m :: Nat). SNatI m => Length m -> Length ('S m))
 -> Length n)
-> (forall (m :: Nat). SNatI m => Length m -> Length ('S m))
-> Length n
forall a b. (a -> b) -> a -> b
$ \(Length Int
n) -> Int -> Length ('S m)
forall (n :: Nat). Int -> Length n
Length (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)

newtype Length (n :: Nat) = Length { 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 :: Vec n a -> Bool
null Vec n a
_ = case SNat n
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 :: Vec n a -> a
sum = Fold a n a -> Vec n a -> a
forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold (Fold a n a -> Vec n a -> a) -> Fold a n a -> Vec n a -> a
forall a b. (a -> b) -> a -> b
$ Fold a 'Z a
-> (forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a)
-> Fold a n a
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 a
forall a. Num a => Fold a 'Z a
start forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a
step where
    start :: Num a => Fold a 'Z a
    start :: Fold a 'Z a
start = (Vec 'Z a -> a) -> Fold a 'Z a
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold ((Vec 'Z a -> a) -> Fold a 'Z a) -> (Vec 'Z a -> a) -> Fold a 'Z a
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 :: Fold a m a -> Fold a ('S m) a
step (Fold Vec m a -> a
f) = (Vec ('S m) a -> a) -> Fold a ('S m) a
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold ((Vec ('S m) a -> a) -> Fold a ('S m) a)
-> (Vec ('S m) a -> a) -> Fold a ('S m) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a
x a -> a -> a
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 :: Vec n a -> a
product = Fold a n a -> Vec n a -> a
forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold (Fold a n a -> Vec n a -> a) -> Fold a n a -> Vec n a -> a
forall a b. (a -> b) -> a -> b
$ Fold a 'Z a
-> (forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a)
-> Fold a n a
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 a
forall a. Num a => Fold a 'Z a
start forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a
step where
    start :: Num a => Fold a 'Z a
    start :: Fold a 'Z a
start = (Vec 'Z a -> a) -> Fold a 'Z a
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold ((Vec 'Z a -> a) -> Fold a 'Z a) -> (Vec 'Z a -> a) -> Fold a 'Z a
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 :: Fold a m a -> Fold a ('S m) a
step (Fold Vec m a -> a
f) = (Vec ('S m) a -> a) -> Fold a ('S m) a
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold ((Vec ('S m) a -> a) -> Fold a ('S m) a)
-> (Vec ('S m) a -> a) -> Fold a ('S m) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> a
x a -> a -> a
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 :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
f = ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c
forall a b c (n :: Nat).
ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c
getZipWith (ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c)
-> ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c
forall a b. (a -> b) -> a -> b
$ ZipWith a b c 'Z
-> (forall (m :: Nat).
    SNatI m =>
    ZipWith a b c m -> ZipWith a b c ('S m))
-> ZipWith a b c n
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).
SNatI m =>
ZipWith a b c m -> ZipWith a b c ('S m)
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 = (Vec 'Z a -> Vec 'Z b -> Vec 'Z c) -> ZipWith a b c 'Z
forall a b c (n :: Nat).
(Vec n a -> Vec n b -> Vec n c) -> ZipWith a b c n
ZipWith ((Vec 'Z a -> Vec 'Z b -> Vec 'Z c) -> ZipWith a b c 'Z)
-> (Vec 'Z a -> Vec 'Z b -> Vec 'Z c) -> ZipWith a b c 'Z
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z b
_ -> Vec 'Z c
forall a. Vec 'Z a
VNil

    step :: ZipWith a b c m -> ZipWith a b c ('S m)
    step :: ZipWith a b c m -> ZipWith a b c ('S m)
step (ZipWith Vec m a -> Vec m b -> Vec m c
go) = (Vec ('S m) a -> Vec ('S m) b -> Vec ('S m) c)
-> ZipWith a b c ('S m)
forall a b c (n :: Nat).
(Vec n a -> Vec n b -> Vec n c) -> ZipWith a b c n
ZipWith ((Vec ('S m) a -> Vec ('S m) b -> Vec ('S m) c)
 -> ZipWith a b c ('S m))
-> (Vec ('S m) a -> Vec ('S m) b -> Vec ('S m) c)
-> ZipWith a b c ('S m)
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) (y ::: ys) -> a -> b -> c
f a
x b
y c -> Vec m c -> Vec ('S m) c
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 { 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 :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith = IZipWith a b c n
-> (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
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 (IZipWith a b c n
 -> (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c)
-> IZipWith a b c n
-> (Fin n -> a -> b -> c)
-> Vec n a
-> Vec n b
-> Vec n c
forall a b. (a -> b) -> a -> b
$ IZipWith a b c 'Z
-> (forall (m :: Nat).
    SNatI m =>
    IZipWith a b c m -> IZipWith a b c ('S m))
-> IZipWith a b c n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction IZipWith a b c 'Z
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)
forall (m :: Nat).
SNatI m =>
IZipWith a b c m -> IZipWith a b c ('S m)
step where
    start :: IZipWith a b c 'Z
    start :: IZipWith a b c 'Z
start = ((Fin 'Z -> a -> b -> c) -> Vec 'Z a -> Vec 'Z b -> Vec 'Z c)
-> IZipWith a b c 'Z
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 (((Fin 'Z -> a -> b -> c) -> Vec 'Z a -> Vec 'Z b -> Vec 'Z c)
 -> IZipWith a b c 'Z)
-> ((Fin 'Z -> a -> b -> c) -> Vec 'Z a -> Vec 'Z b -> Vec 'Z c)
-> IZipWith a b c 'Z
forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b -> c
_ Vec 'Z a
_ Vec 'Z b
_ -> Vec 'Z c
forall a. Vec 'Z a
VNil

    step :: IZipWith a b c m -> IZipWith a b c ('S m)
    step :: 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) = ((Fin ('S m) -> a -> b -> c)
 -> Vec ('S m) a -> Vec ('S m) b -> Vec ('S m) c)
-> IZipWith a b c ('S m)
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 (((Fin ('S m) -> a -> b -> c)
  -> Vec ('S m) a -> Vec ('S m) b -> Vec ('S m) c)
 -> IZipWith a b c ('S m))
-> ((Fin ('S m) -> a -> b -> c)
    -> Vec ('S m) a -> Vec ('S m) b -> Vec ('S m) c)
-> IZipWith a b c ('S m)
forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b -> c
f (x ::: xs) (y ::: ys) -> Fin ('S m) -> a -> b -> c
f Fin ('S m)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x b
y c -> Vec m c -> Vec ('S m) c
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 (Fin ('S m) -> a -> b -> c)
-> (Fin m -> Fin ('S m)) -> Fin m -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> Fin ('S m)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs Vec m b
ys

newtype IZipWith a b c n = IZipWith { 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 :: x -> Vec n x
repeat x
x = Vec 'Z x
-> (forall (m :: Nat). SNatI m => Vec m x -> Vec ('S m) x)
-> Vec n 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 Vec 'Z x
forall a. Vec 'Z a
VNil (x
x x -> Vec m x -> Vec ('S m) 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 :: Vec n a -> (a -> Vec n b) -> Vec n b
bind = Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b
forall a (n :: Nat) b.
Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b
getBind (Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b)
-> Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b
forall a b. (a -> b) -> a -> b
$ Bind a 'Z b
-> (forall (m :: Nat). SNatI m => Bind a m b -> Bind a ('S m) b)
-> Bind a n 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 Bind a 'Z b
forall a b. Bind a 'Z b
start forall a (m :: Nat) b. Bind a m b -> Bind a ('S m) b
forall (m :: Nat). SNatI m => Bind a m b -> Bind a ('S m) b
step where
    start :: Bind a 'Z b
    start :: Bind a 'Z b
start = (Vec 'Z a -> (a -> Vec 'Z b) -> Vec 'Z b) -> Bind a 'Z b
forall a (n :: Nat) b.
(Vec n a -> (a -> Vec n b) -> Vec n b) -> Bind a n b
Bind ((Vec 'Z a -> (a -> Vec 'Z b) -> Vec 'Z b) -> Bind a 'Z b)
-> (Vec 'Z a -> (a -> Vec 'Z b) -> Vec 'Z b) -> Bind a 'Z b
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ a -> Vec 'Z b
_ -> Vec 'Z b
forall a. Vec 'Z a
VNil

    step :: Bind a m b -> Bind a ('S m) b
    step :: Bind a m b -> Bind a ('S m) b
step (Bind Vec m a -> (a -> Vec m b) -> Vec m b
go) = (Vec ('S m) a -> (a -> Vec ('S m) b) -> Vec ('S m) b)
-> Bind a ('S m) b
forall a (n :: Nat) b.
(Vec n a -> (a -> Vec n b) -> Vec n b) -> Bind a n b
Bind ((Vec ('S m) a -> (a -> Vec ('S m) b) -> Vec ('S m) b)
 -> Bind a ('S m) b)
-> (Vec ('S m) a -> (a -> Vec ('S m) b) -> Vec ('S m) b)
-> Bind a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) a -> Vec ('S m) b
f -> Vec ('S m) b -> b
forall (n :: Nat) a. Vec ('S n) a -> a
head (a -> Vec ('S m) b
f a
x) b -> Vec m b -> Vec ('S m) b
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 (Vec ('S m) b -> Vec m b
forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail (Vec ('S m) b -> Vec m b) -> (a -> Vec ('S m) b) -> a -> Vec m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vec ('S m) b
f)

newtype Bind a n b = Bind { 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 :: Vec n (Vec n a) -> Vec n a
join = Join n a -> Vec n (Vec n a) -> Vec n a
forall (n :: Nat) a. Join n a -> Vec n (Vec n a) -> Vec n a
getJoin (Join n a -> Vec n (Vec n a) -> Vec n a)
-> Join n a -> Vec n (Vec n a) -> Vec n a
forall a b. (a -> b) -> a -> b
$ Join 'Z a
-> (forall (m :: Nat). SNatI m => Join m a -> Join ('S m) a)
-> Join n a
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 Join 'Z a
forall a. Join 'Z a
start forall (m :: Nat). SNatI m => Join m a -> Join ('S m) a
forall (m :: Nat) a. SNatI m => Join m a -> Join ('S m) a
step where
    start :: Join 'Z a
    start :: Join 'Z a
start = (Vec 'Z (Vec 'Z a) -> Vec 'Z a) -> Join 'Z a
forall (n :: Nat) a. (Vec n (Vec n a) -> Vec n a) -> Join n a
Join ((Vec 'Z (Vec 'Z a) -> Vec 'Z a) -> Join 'Z a)
-> (Vec 'Z (Vec 'Z a) -> Vec 'Z a) -> Join 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z (Vec 'Z a)
_ -> Vec 'Z a
forall a. Vec 'Z a
VNil

    step :: N.SNatI m => Join m a -> Join ('S m) a
    step :: Join m a -> Join ('S m) a
step (Join Vec m (Vec m a) -> Vec m a
go) = (Vec ('S m) (Vec ('S m) a) -> Vec ('S m) a) -> Join ('S m) a
forall (n :: Nat) a. (Vec n (Vec n a) -> Vec n a) -> Join n a
Join ((Vec ('S m) (Vec ('S m) a) -> Vec ('S m) a) -> Join ('S m) a)
-> (Vec ('S m) (Vec ('S m) a) -> Vec ('S m) a) -> Join ('S m) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) -> Vec ('S m) a -> a
forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S m) a
x a -> Vec m a -> Vec ('S m) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m (Vec m a) -> Vec m a
go ((Vec ('S m) a -> Vec m a)
-> Vec m (Vec ('S m) a) -> Vec m (Vec m a)
forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map Vec ('S m) a -> Vec m a
forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail Vec m (Vec ('S m) a)
xs)

newtype Join n a = Join { 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 :: Vec n (Fin n)
universe = Universe n -> Vec n (Fin n)
forall (n :: Nat). Universe n -> Vec n (Fin n)
getUniverse (Universe 'Z
-> (forall (m :: Nat). SNatI m => Universe m -> Universe ('S m))
-> Universe n
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 = Vec 'Z (Fin 'Z) -> Universe 'Z
forall (n :: Nat). Vec n (Fin n) -> Universe n
Universe Vec 'Z (Fin 'Z)
forall a. Vec 'Z a
VNil

    step :: N.SNatI m => Universe m -> Universe ('S m)
    step :: Universe m -> Universe ('S m)
step (Universe Vec m (Fin m)
go) = Vec ('S m) (Fin ('S m)) -> Universe ('S m)
forall (n :: Nat). Vec n (Fin n) -> Universe n
Universe (Fin ('S m)
forall (n1 :: Nat). Fin ('S n1)
FZ Fin ('S m) -> Vec m (Fin ('S m)) -> Vec ('S m) (Fin ('S m))
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: (Fin m -> Fin ('S m)) -> Vec m (Fin m) -> Vec m (Fin ('S m))
forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map Fin m -> Fin ('S m)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS Vec m (Fin m)
go)

newtype Universe n = Universe { 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 :: Vec n a -> Vec n a
ensureSpine = EnsureSpine n a -> Vec n a -> Vec n a
forall (n :: Nat) a. EnsureSpine n a -> Vec n a -> Vec n a
getEnsureSpine (EnsureSpine 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    EnsureSpine m a -> EnsureSpine ('S m) a)
-> EnsureSpine n a
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 EnsureSpine 'Z a
forall a. EnsureSpine 'Z a
first forall (m :: Nat).
SNatI m =>
EnsureSpine m a -> EnsureSpine ('S m) a
forall (m :: Nat) a. EnsureSpine m a -> EnsureSpine ('S m) a
step) where
    first :: EnsureSpine 'Z a
    first :: EnsureSpine 'Z a
first = (Vec 'Z a -> Vec 'Z a) -> EnsureSpine 'Z a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> EnsureSpine n a
EnsureSpine ((Vec 'Z a -> Vec 'Z a) -> EnsureSpine 'Z a)
-> (Vec 'Z a -> Vec 'Z a) -> EnsureSpine 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec 'Z a
forall a. Vec 'Z a
VNil

    step :: EnsureSpine m a -> EnsureSpine ('S m) a
    step :: EnsureSpine m a -> EnsureSpine ('S m) a
step (EnsureSpine Vec m a -> Vec m a
go) = (Vec ('S m) a -> Vec ('S m) a) -> EnsureSpine ('S m) a
forall (n :: Nat) a. (Vec n a -> Vec n a) -> EnsureSpine n a
EnsureSpine ((Vec ('S m) a -> Vec ('S m) a) -> EnsureSpine ('S m) a)
-> (Vec ('S m) a -> Vec ('S m) a) -> EnsureSpine ('S m) a
forall a b. (a -> b) -> a -> b
$ \ ~(x ::: xs) -> a
x a -> Vec m a -> Vec ('S m) a
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 { 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 :: Gen a -> Gen (Vec n a)
liftArbitrary = Gen a -> Gen (Vec n a)
forall (n :: Nat) a. SNatI n => Gen a -> Gen (Vec n a)
liftArbitrary
    liftShrink :: (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink    = (a -> [a]) -> Vec n a -> [Vec n a]
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 :: Gen a -> Gen (Vec n a)
liftArbitrary Gen a
arb = Arb n a -> Gen (Vec n a)
forall (n :: Nat) a. Arb n a -> Gen (Vec n a)
getArb (Arb n a -> Gen (Vec n a)) -> Arb n a -> Gen (Vec n a)
forall a b. (a -> b) -> a -> b
$ Arb 'Z a
-> (forall (m :: Nat). SNatI m => Arb m a -> Arb ('S m) a)
-> Arb n a
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 (Gen (Vec 'Z a) -> Arb 'Z a
forall (n :: Nat) a. Gen (Vec n a) -> Arb n a
Arb (Vec 'Z a -> Gen (Vec 'Z a)
forall (m :: * -> *) a. Monad m => a -> m a
return Vec 'Z a
forall a. Vec 'Z a
VNil)) forall (m :: Nat). SNatI m => Arb m a -> Arb ('S m) a
forall (m :: Nat). Arb m a -> Arb ('S m) a
step where
    step :: Arb m a -> Arb ('S m) a
    step :: Arb m a -> Arb ('S m) a
step (Arb Gen (Vec m a)
rec) = Gen (Vec ('S m) a) -> Arb ('S m) a
forall (n :: Nat) a. Gen (Vec n a) -> Arb n a
Arb (Gen (Vec ('S m) a) -> Arb ('S m) a)
-> Gen (Vec ('S m) a) -> Arb ('S m) a
forall a b. (a -> b) -> a -> b
$ a -> Vec m a -> Vec ('S m) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) (a -> Vec m a -> Vec ('S m) a)
-> Gen a -> Gen (Vec m a -> Vec ('S m) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
arb Gen (Vec m a -> Vec ('S m) a)
-> Gen (Vec m a) -> Gen (Vec ('S m) a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Vec m a)
rec

newtype Arb n a = Arb { 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 :: (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink a -> [a]
shr = Shr n a -> Vec n a -> [Vec n a]
forall (n :: Nat) a. Shr n a -> Vec n a -> [Vec n a]
getShr (Shr n a -> Vec n a -> [Vec n a])
-> Shr n a -> Vec n a -> [Vec n a]
forall a b. (a -> b) -> a -> b
$ Shr 'Z a
-> (forall (m :: Nat). SNatI m => Shr m a -> Shr ('S m) a)
-> Shr n a
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 ((Vec 'Z a -> [Vec 'Z a]) -> Shr 'Z a
forall (n :: Nat) a. (Vec n a -> [Vec n a]) -> Shr n a
Shr ((Vec 'Z a -> [Vec 'Z a]) -> Shr 'Z a)
-> (Vec 'Z a -> [Vec 'Z a]) -> Shr 'Z a
forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
VNil -> []) forall (m :: Nat). SNatI m => Shr m a -> Shr ('S m) a
forall (m :: Nat). Shr m a -> Shr ('S m) a
step where
    step :: Shr m a -> Shr ('S m) a
    step :: Shr m a -> Shr ('S m) a
step (Shr Vec m a -> [Vec m a]
rec) = (Vec ('S m) a -> [Vec ('S m) a]) -> Shr ('S m) a
forall (n :: Nat) a. (Vec n a -> [Vec n a]) -> Shr n a
Shr ((Vec ('S m) a -> [Vec ('S m) a]) -> Shr ('S m) a)
-> (Vec ('S m) a -> [Vec ('S m) a]) -> Shr ('S m) a
forall a b. (a -> b) -> a -> b
$ \(x ::: xs) ->
        (a -> Vec m a -> Vec ('S m) a) -> (a, Vec m a) -> Vec ('S m) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> Vec m a -> Vec ('S m) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) ((a, Vec m a) -> Vec ('S m) a) -> [(a, Vec m a)] -> [Vec ('S m) a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> [a])
-> (Vec m a -> [Vec m a]) -> (a, Vec m a) -> [(a, Vec m a)]
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 { 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 = Gen (Vec n a)
forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => Gen (f a)
QC.arbitrary1
    shrink :: Vec n a -> [Vec n a]
shrink    = Vec n a -> [Vec n a]
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 :: Vec n a -> Gen b -> Gen b
coarbitrary Vec n a
v = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
        SNat n
N.SS -> Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (case Vec n a
v of (x ::: xs) -> (a, Vec n1 a) -> Gen b -> Gen b
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 :: (Vec n a -> b) -> Vec n a :-> b
function = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> (Vec 'Z a -> ())
-> (() -> Vec 'Z a) -> (Vec 'Z a -> b) -> Vec 'Z a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\Vec 'Z a
VNil -> ()) (\() -> Vec 'Z a
forall a. Vec 'Z a
VNil)
        SNat n
N.SS -> (Vec ('S n1) a -> (a, Vec n1 a))
-> ((a, Vec n1 a) -> Vec ('S n1) a)
-> (Vec ('S n1) a -> b)
-> Vec ('S n1) a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(x ::: xs) -> (a
x, Vec n1 a
xs)) (\(a
x,Vec n1 a
xs) -> a
x a -> Vec n1 a -> Vec ('S n1) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec n1 a
xs)