{-# LANGUAGE BangPatterns           #-}
{-# LANGUAGE CPP                    #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE DeriveDataTypeable     #-}
{-# LANGUAGE EmptyCase              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE Safe                   #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE StandaloneDeriving     #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE UndecidableInstances   #-}
-- | Lazy (in elements and spine) length-indexed list: 'Vec'.
module Data.Vec.Lazy (
    Vec (..),
    -- * Construction
    empty,
    singleton,
    withDict,
    -- * Conversions
    toPull,
    fromPull,
    toList,
    toNonEmpty,
    fromList,
    fromListPrefix,
    reifyList,
    -- * Indexing
    (!),
    tabulate,
    cons,
    snoc,
    head,
    last,
    tail,
    init,
    -- * Reverse
    reverse,
    -- * Dependent folds
    dfoldr,
    dfoldl,
    dfoldl',
    -- * Concatenation and splitting
    (++),
    split,
    concatMap,
    concat,
    chunks,
    -- * Take and drop
    take,
    drop,
    -- * Folds
    foldMap,
    foldMap1,
    ifoldMap,
    ifoldMap1,
    foldr,
    ifoldr,
    foldl',
    -- * Special folds
    length,
    null,
    sum,
    product,
    -- * Mapping
    map,
    imap,
    traverse,
#ifdef MIN_VERSION_semigroupoids
    traverse1,
#endif
    itraverse,
    itraverse_,
    -- * Zipping
    zipWith,
    izipWith,
    repeat,
    -- * Monadic
    bind,
    join,
    -- * Universe
    universe,
    -- * VecEach
    VecEach (..),
    )  where

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

import Control.Applicative (Applicative (..), (<$>))
import Control.DeepSeq     (NFData (..))
import Control.Lens.Yocto  ((<&>))
import Data.Boring         (Boring (..))
import Data.Fin            (Fin (..))
import Data.Hashable       (Hashable (..))
import Data.List.NonEmpty  (NonEmpty (..))
import Data.Monoid         (Monoid (..))
import Data.Nat            (Nat (..))
import Data.Semigroup      (Semigroup (..))
import Data.Typeable       (Typeable)

import SafeCompat (coerce)

--- 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

import qualified Data.Type.Nat.LE          as LE.ZS
import qualified Data.Type.Nat.LE.ReflStep as LE.RS


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

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

infixr 5 :::

-- | Vector, i.e. length-indexed list.
data Vec (n :: Nat) a where
    VNil  :: Vec 'Z a
    (:::) :: a -> Vec n a -> Vec ('S n) a
  deriving (Typeable)

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

deriving instance Eq a => Eq (Vec n a)
deriving instance Ord a => Ord (Vec n a)

instance Show a => Show (Vec n a) where
    showsPrec :: Int -> Vec n a -> ShowS
showsPrec Int
_ Vec n a
VNil       = String -> ShowS
showString String
"VNil"
    showsPrec Int
d (a
x ::: Vec n a
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 n a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 Vec n a
xs

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

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

    foldr :: forall a b. (a -> b -> b) -> b -> Vec n a -> b
foldr  = (a -> b -> b) -> b -> Vec n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr
    foldl' :: forall b a. (b -> a -> b) -> b -> Vec n a -> b
foldl' = (b -> a -> b) -> b -> Vec n a -> b
forall a b (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl'

    null :: forall a. Vec n a -> Bool
null    = Vec n a -> Bool
forall (n :: Nat) a. Vec n a -> Bool
null
    length :: forall a. Vec n a -> Int
length  = Vec n a -> Int
forall (n :: Nat) a. Vec n a -> Int
length
    sum :: forall a. Num a => Vec n a -> a
sum     = Vec n a -> a
forall a (n :: Nat). Num a => Vec n a -> a
sum
    product :: forall a. Num a => Vec n a -> a
product = Vec n a -> a
forall a (n :: Nat). Num a => Vec n a -> a
product

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

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

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

-- | @since 0.4
instance WI.TraversableWithIndex (Fin n) (Vec n) where
    itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse = (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse

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

instance n ~ 'S m => I.Traversable1 (Vec n) where
    traverse1 :: forall (f :: * -> *) a b.
Apply f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse1 = (a -> f b) -> Vec n a -> f (Vec n b)
(a -> f b) -> Vec ('S m) a -> f (Vec ('S m) b)
forall (n :: Nat) (f :: * -> *) a b.
Apply f =>
(a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1
#endif

instance NFData a => NFData (Vec n a) where
    rnf :: Vec n a -> ()
rnf Vec n a
VNil       = ()
    rnf (a
x ::: Vec n a
xs) = a -> ()
forall a. NFData a => a -> ()
rnf a
x () -> () -> ()
forall a b. a -> b -> b
`seq` Vec n a -> ()
forall a. NFData a => a -> ()
rnf Vec n a
xs

instance Hashable a => Hashable (Vec n a) where
    hashWithSalt :: Int -> Vec n a -> Int
hashWithSalt Int
salt Vec n a
VNil = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (Int
0 :: Int)
    hashWithSalt Int
salt (a
x ::: Vec n a
xs) = Int
salt
        Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
x
        Int -> Vec n a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Vec n a
xs

instance N.SNatI n => Applicative (Vec n) where
    pure :: forall a. a -> Vec n a
pure   = a -> Vec n a
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat
    <*> :: forall a b. 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).
(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
_ *> :: forall a b. Vec n a -> Vec n b -> Vec n b
*> Vec n b
x = Vec n b
x
    Vec n a
x <* :: forall a b. Vec n a -> Vec n b -> Vec n a
<* Vec n b
_ = Vec n a
x
    liftA2 :: forall a b c. (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).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith

instance N.SNatI n => Monad (Vec n) where
    return :: forall a. a -> Vec n a
return = a -> Vec n a
forall a. a -> Vec n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: forall a b. 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. Vec n a -> (a -> Vec n b) -> Vec n b
bind
    Vec n a
_ >> :: forall a b. Vec n a -> Vec n b -> Vec n b
>> Vec n b
x = Vec n b
x

#ifdef MIN_VERSION_distributive
instance N.SNatI n => Distributive (Vec n) where
    distribute :: forall (f :: * -> *) a. Functor f => f (Vec n a) -> Vec n (f a)
distribute f (Vec n a)
f = (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 a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
k) f (Vec n a)
f)

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

instance Semigroup a => 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).
(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 a. 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).
(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 Apply (Vec n) where
    <.> :: forall a b. 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).
(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
_ .> :: forall a b. Vec n a -> Vec n b -> Vec n b
.> Vec n b
x = Vec n b
x
    Vec n a
x <. :: forall a b. Vec n a -> Vec n b -> Vec n a
<. Vec n b
_ = Vec n a
x
    liftF2 :: forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftF2 = (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith

instance I.Bind (Vec n) where
    >>- :: forall a b. 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. Vec n a -> (a -> Vec n b) -> Vec n b
bind
    join :: forall a. Vec n (Vec n a) -> Vec n a
join  = Vec n (Vec n a) -> Vec n a
forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join
#endif

-- | @since 0.4.1
instance n ~ 'N.Z => Boring (Vec n a) where
    boring :: Vec n a
boring = Vec n a
Vec 'Z a
forall a. Vec 'Z a
empty

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

-- | @since 0.4
instance Eq1 (Vec n) where
    liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
liftEq a -> b -> Bool
_eq Vec n a
VNil       Vec n b
VNil       = Bool
True
    liftEq  a -> b -> Bool
eq (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = a -> b -> Bool
eq a
x b
y Bool -> Bool -> Bool
&& (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
eq Vec n a
xs Vec n b
Vec n b
ys

-- | @since 0.4
instance Ord1 (Vec n) where
    liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
liftCompare a -> b -> Ordering
_cmp Vec n a
VNil       Vec n b
VNil       = Ordering
EQ
    liftCompare  a -> b -> Ordering
cmp (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = a -> b -> Ordering
cmp a
x b
y Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
cmp Vec n a
xs Vec n b
Vec n b
ys

-- | @since 0.4
instance 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
VNil       = String -> ShowS
showString String
"VNil"
    liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
d (a
x ::: Vec n a
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 -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
5 Vec n a
xs

-------------------------------------------------------------------------------
-- Construction
-------------------------------------------------------------------------------

-- | Empty 'Vec'.
empty :: Vec 'Z a
empty :: forall a. 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 :: forall a. a -> Vec ('S 'Z) a
singleton a
x = a
x a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil

-- | /O(n)/. Recover 'N.SNatI' (and 'N.SNatI') dictionary from a 'Vec' value.
--
-- Example: 'N.reflect' is constrained with @'N.SNatI' n@, but if we have a
-- @'Vec' n a@, we can recover that dictionary:
--
-- >>> let f :: forall n a. Vec n a -> N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil)
-- 1
--
-- /Note:/ using 'N.SNatI' will be suboptimal, as if GHC has no
-- opportunity to optimise the code, the recusion won't be unfold.
-- How bad such code will perform? I don't know, we'll need benchmarks.
--
withDict :: Vec n a -> (N.SNatI n => r) -> r
withDict :: forall (n :: Nat) a r. Vec n a -> (SNatI n => r) -> r
withDict Vec n a
VNil       SNatI n => r
r = r
SNatI n => r
r
withDict (a
_ ::: Vec n a
xs) SNatI n => r
r = Vec n a -> (SNatI n => r) -> r
forall (n :: Nat) a r. Vec n a -> (SNatI n => r) -> r
withDict Vec n a
xs r
SNatI n => r
SNatI n => r
r

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

-- | Convert to pull 'P.Vec'.
toPull :: Vec n a -> P.Vec n a
toPull :: forall (n :: Nat) a. Vec n a -> Vec n a
toPull Vec n a
VNil       = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec Fin n -> a
Fin 'Z -> a
forall b. Fin 'Z -> b
F.absurd
toPull (a
x ::: Vec n a
xs) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec ((Fin n -> a) -> Vec n a) -> (Fin n -> a) -> Vec n a
forall a b. (a -> b) -> a -> b
$ \Fin n
n -> case Fin n
n of
    Fin n
FZ   -> a
x
    FS Fin n1
m -> Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
P.unVec (Vec n a -> Vec n a
forall (n :: Nat) a. Vec n a -> Vec n a
toPull Vec n a
xs) Fin n
Fin n1
m

-- | Convert from pull 'P.Vec'.
fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
fromPull :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull (P.Vec Fin n -> a
f) = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
    SNat n
N.SZ -> Vec n a
Vec 'Z a
forall a. Vec 'Z a
VNil
    SNat n
N.SS -> Fin n -> a
f Fin n
Fin ('S n1)
forall (n1 :: Nat). Fin ('S n1)
FZ a -> Vec n1 a -> Vec ('S n1) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n1 a -> Vec n1 a
forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull ((Fin n1 -> a) -> Vec n1 a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec (Fin n -> a
f (Fin n -> a) -> (Fin n1 -> Fin n) -> Fin n1 -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n1 -> Fin n
Fin n1 -> Fin ('S n1)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS))

-- | Convert 'Vec' to list.
--
-- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
-- "foo"
toList :: Vec n a -> [a]
toList :: forall (n :: Nat) a. Vec n a -> [a]
toList Vec n a
VNil       = []
toList (a
x ::: Vec n a
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Vec n a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec n a
xs

-- |
--
-- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
-- 1 :| [2,3]
--
-- @since 0.4
toNonEmpty :: Vec ('S n) a -> NonEmpty a
toNonEmpty :: forall (n :: Nat) a. Vec ('S n) a -> NonEmpty a
toNonEmpty (a
x ::: Vec n a
xs) = a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| Vec n a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec n a
xs

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

-- | Convert list @[a]@ to @'Vec' n a@.
-- Returns 'Nothing' if input list is too short.
--
-- >>> fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)
-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- >>> fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)
-- Just ('q' ::: 'u' ::: 'u' ::: VNil)
--
-- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)
-- Nothing
--
fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)
fromListPrefix :: forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromListPrefix = 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 FromList m a -> FromList ('S m) a
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 :: forall a. 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 :: forall (n :: Nat) a. 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 a (n :: Nat). 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 :: forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList []       forall (n :: Nat). SNatI n => Vec n a -> r
f = 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 a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
xs')

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

-- | Indexing.
--
-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
-- 'b'
--
(!) :: Vec n a -> Fin n -> a
! :: forall (n :: Nat) a. Vec n a -> Fin n -> a
(!) (a
x ::: Vec n a
_)  Fin n
FZ     = a
x
(!) (a
_ ::: Vec n a
xs) (FS Fin n1
n) = Vec n a
xs Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
Fin n1
n
(!) Vec n a
VNil Fin n
n = case Fin n
n of {}

-- | Tabulating, inverse of '!'.
--
-- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
-- 0 ::: 1 ::: 2 ::: VNil
--
tabulate :: N.SNatI n => (Fin n -> a) -> Vec n a
tabulate :: forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate = 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 :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons = a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::)

-- | Add a single element at the end of a 'Vec'.
--
-- @since 0.2.1
snoc :: Vec n a -> a -> Vec ('S n) a
snoc :: forall (n :: Nat) a. Vec n a -> a -> Vec ('S n) a
snoc Vec n a
VNil       a
x = a
x a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
Vec 'Z a
forall a. Vec 'Z a
VNil
snoc (a
y ::: Vec n a
ys) a
x = a
y a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a -> a -> Vec ('S n) a
forall (n :: Nat) a. Vec n a -> a -> Vec ('S n) a
snoc Vec n a
ys a
x

-- | The first element of a 'Vec'.
head :: Vec ('S n) a -> a
head :: forall (n :: Nat) a. Vec ('S n) a -> a
head (a
x ::: Vec n a
_) = a
x

-- | The last element of a 'Vec'.
--
-- @since 0.4
last :: Vec ('S n) a -> a
last :: forall (n :: Nat) a. Vec ('S n) a -> a
last (a
x ::: Vec n a
VNil) = a
x
last (a
_ ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = Vec ('S n) a -> a
forall (n :: Nat) a. Vec ('S n) a -> a
last Vec n a
Vec ('S n) a
xs

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

-- | The elements before the 'last' of a 'Vec'.
--
-- @since 0.4
init :: Vec ('S n) a -> Vec n a
init :: forall (n :: Nat) a. Vec ('S n) a -> Vec n a
init (a
_ ::: Vec n a
VNil) = Vec n a
Vec 'Z a
forall a. Vec 'Z a
VNil
init (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = a
x a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec ('S n) a -> Vec n a
forall (n :: Nat) a. Vec ('S n) a -> Vec n a
init Vec n a
Vec ('S n) a
xs

-------------------------------------------------------------------------------
-- Reverse
-------------------------------------------------------------------------------

-- | Reverse 'Vec'.
--
-- >>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)
-- 'c' ::: 'b' ::: 'a' ::: VNil
--
-- @since 0.2.1
--
reverse :: Vec n a -> Vec n a
reverse :: forall (n :: Nat) a. Vec n a -> Vec n a
reverse Vec n a
xs = FlippedVec a n -> Vec n a
forall a (n :: Nat). FlippedVec a n -> Vec n a
unflipVec ((forall (m :: Nat). FlippedVec a m -> a -> FlippedVec a ('S m))
-> FlippedVec a 'Z -> Vec n a -> FlippedVec a n
forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl FlippedVec a m -> a -> FlippedVec a ('S m)
forall a (m :: Nat). FlippedVec a m -> a -> FlippedVec a ('S m)
forall (m :: Nat). FlippedVec a m -> a -> FlippedVec a ('S m)
c (Vec 'Z a -> FlippedVec a 'Z
forall a (n :: Nat). Vec n a -> FlippedVec a n
FlipVec Vec 'Z a
forall a. Vec 'Z a
VNil) Vec n a
xs)
  where
    c :: forall a m. FlippedVec a m -> a -> FlippedVec a ('S m)
    c :: forall a (m :: Nat). FlippedVec a m -> a -> FlippedVec a ('S m)
c = (Vec m a -> a -> Vec ('S m) a)
-> FlippedVec a m -> a -> FlippedVec a ('S m)
forall a b. Coercible @(*) a b => a -> b
coerce ((a -> Vec m a -> Vec ('S m) a) -> Vec m a -> a -> Vec ('S m) a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Vec m a -> Vec ('S m) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) :: Vec m a -> a -> Vec ('S m) a)

newtype FlippedVec a n = FlipVec { forall a (n :: Nat). FlippedVec a n -> Vec n a
unflipVec :: Vec n a }

-------------------------------------------------------------------------------
-- Indexed folds
-------------------------------------------------------------------------------

-- | Dependent right fold.
--
-- This could been called an indexed fold, but that name is already used.
--
-- @since 0.4.1
--
dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldr :: forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldr forall (m :: Nat). a -> f m -> f ('S m)
c f 'Z
n = Vec n a -> f n
forall (m :: Nat). Vec m a -> f m
go where
    go :: Vec m a -> f m
    go :: forall (m :: Nat). Vec m a -> f m
go Vec m a
VNil       = f m
f 'Z
n
    go (a
x ::: Vec n a
xs) = a -> f n -> f ('S n)
forall (m :: Nat). a -> f m -> f ('S m)
c a
x (Vec n a -> f n
forall (m :: Nat). Vec m a -> f m
go Vec n a
xs)

-- | Dependent left fold.
--
-- @since 0.4.1
--
dfoldl :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
dfoldl :: forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl forall (m :: Nat). f m -> a -> f ('S m)
_ f 'Z
n Vec n a
VNil       = f n
f 'Z
n
dfoldl forall (m :: Nat). f m -> a -> f ('S m)
c f 'Z
n (a
x ::: Vec n a
xs) = WrappedSucc f n -> f ('S n)
forall (f :: Nat -> *) (n :: Nat). WrappedSucc f n -> f ('S n)
unwrapSucc ((forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m))
-> WrappedSucc f 'Z -> Vec n a -> WrappedSucc f n
forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl WrappedSucc f m -> a -> WrappedSucc f ('S m)
forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' (f ('S 'Z) -> WrappedSucc f 'Z
forall (f :: Nat -> *) (n :: Nat). f ('S n) -> WrappedSucc f n
WrapSucc (f 'Z -> a -> f ('S 'Z)
forall (m :: Nat). f m -> a -> f ('S m)
c f 'Z
n a
x)) Vec n a
xs)
  where
    c' :: forall m. WrappedSucc f m -> a -> WrappedSucc f ('S m)
    c' :: forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' = (f ('S m) -> a -> f ('S ('S m)))
-> WrappedSucc f m -> a -> WrappedSucc f ('S m)
forall a b. Coercible @(*) a b => a -> b
coerce (f ('S m) -> a -> f ('S ('S m))
forall (m :: Nat). f m -> a -> f ('S m)
c :: f ('S m) -> a -> f ('S ('S m)))

-- | Dependent strict left fold.
--
-- @since 0.4.1
--
dfoldl' :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
dfoldl' :: forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl' forall (m :: Nat). f m -> a -> f ('S m)
_ !f 'Z
n Vec n a
VNil       = f n
f 'Z
n
dfoldl' forall (m :: Nat). f m -> a -> f ('S m)
c !f 'Z
n (a
x ::: Vec n a
xs) = WrappedSucc f n -> f ('S n)
forall (f :: Nat -> *) (n :: Nat). WrappedSucc f n -> f ('S n)
unwrapSucc ((forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m))
-> WrappedSucc f 'Z -> Vec n a -> WrappedSucc f n
forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl' WrappedSucc f m -> a -> WrappedSucc f ('S m)
forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' (f ('S 'Z) -> WrappedSucc f 'Z
forall (f :: Nat -> *) (n :: Nat). f ('S n) -> WrappedSucc f n
WrapSucc (f 'Z -> a -> f ('S 'Z)
forall (m :: Nat). f m -> a -> f ('S m)
c f 'Z
n a
x)) Vec n a
xs)
  where
    c' :: forall m. WrappedSucc f m -> a -> WrappedSucc f ('S m)
    c' :: forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' = (f ('S m) -> a -> f ('S ('S m)))
-> WrappedSucc f m -> a -> WrappedSucc f ('S m)
forall a b. Coercible @(*) a b => a -> b
coerce (f ('S m) -> a -> f ('S ('S m))
forall (m :: Nat). f m -> a -> f ('S m)
c :: f ('S m) -> a -> f ('S ('S m)))

newtype WrappedSucc f n = WrapSucc { forall (f :: Nat -> *) (n :: Nat). WrappedSucc f n -> f ('S n)
unwrapSucc :: f ('S n) }

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

infixr 5 ++

-- | Append two 'Vec'.
--
-- >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
-- 'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
--
(++) :: Vec n a -> Vec m a -> Vec (N.Plus n m) a
Vec n a
VNil       ++ :: forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec m a
ys = Vec m a
Vec (Plus n m) a
ys
(a
x ::: Vec n a
xs) ++ Vec m a
ys = a
x a -> Vec (Plus n m) a -> Vec ('S (Plus n m)) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
xs Vec n a -> Vec m a -> Vec (Plus n m) a
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec m a
ys

-- | Split vector into two parts. Inverse of '++'.
--
-- >>> split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)
-- ('a' ::: VNil,'b' ::: 'c' ::: VNil)
--
-- >>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))
-- 'a' ::: 'b' ::: 'c' ::: VNil
--
split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)
split :: forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec (Plus n m) a -> (Vec n a, Vec m a)
split = 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 Split m m a -> Split m ('S m) a
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 :: forall (m :: Nat) a. 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 :: forall (m :: Nat) (n :: Nat) a. Split m n a -> Split m ('S n) a
step (Split Vec (Plus n m) a -> (Vec n a, Vec m a)
f) = (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
$ \(a
x ::: Vec n a
xs) -> case Vec (Plus n m) a -> (Vec n a, Vec m a)
f Vec n a
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 a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
ys, Vec m a
zs)

newtype Split m n a = Split { forall (m :: Nat) (n :: Nat) a.
Split m n a -> Vec (Plus n m) a -> (Vec n a, Vec m a)
appSplit :: Vec (N.Plus n m) a -> (Vec n a, Vec m a) }

-- | Map over all the elements of a 'Vec' and concatenate the resulting 'Vec's.
--
-- >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
-- 'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil
--
concatMap :: (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
concatMap :: forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap a -> Vec m b
_ Vec n a
VNil       = Vec 'Z b
Vec (Mult n m) b
forall a. Vec 'Z a
VNil
concatMap a -> Vec m b
f (a
x ::: Vec n a
xs) = a -> Vec m b
f a
x Vec m b -> Vec (Mult n m) b -> Vec (Plus m (Mult n m)) b
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap a -> Vec m b
f Vec n a
xs

-- | @'concatMap' 'id'@
concat :: Vec n (Vec m a) -> Vec (N.Mult n m) a
concat :: forall (n :: Nat) (m :: Nat) a. 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 (m :: Nat) b (n :: Nat).
(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 :: forall (n :: Nat) (m :: Nat) a.
(SNatI n, SNatI m) =>
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 Chunks m m a -> Chunks m ('S m) a
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 :: forall (m :: Nat) a. 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 :: forall (m :: Nat) (n :: Nat) a.
SNatI m =>
Chunks m n a -> Chunks m ('S n) a
step (Chunks Vec (Mult n m) a -> Vec n (Vec m a)
go) = (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 (Mult ('S n) m) a
Vec (Plus m (Mult 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 a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec (Mult n m) a -> Vec n (Vec m a)
go Vec (Mult n m) a
zs

newtype Chunks  m n a = Chunks  { forall (m :: Nat) (n :: Nat) a.
Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
getChunks  :: Vec (N.Mult n m) a -> Vec n (Vec m a) }

-------------------------------------------------------------------------------
-- take and drop
-------------------------------------------------------------------------------

-- |
--
-- >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil
-- >>> take xs :: Vec N.Nat3 Char
-- 'a' ::: 'b' ::: 'c' ::: VNil
--
take :: forall n m a. (LE.ZS.LE n m) => Vec m a -> Vec n a
take :: forall (n :: Nat) (m :: Nat) a. LE n m => Vec m a -> Vec n a
take = LEProof n m -> Vec m a -> Vec n a
forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n m
forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
LE.ZS.leProof where
    go :: LE.ZS.LEProof n' m' -> Vec m' a -> Vec n' a
    go :: forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n' m'
LE.ZS.LEZero Vec m' a
_              = Vec n' a
Vec 'Z a
forall a. Vec 'Z a
VNil
    go (LE.ZS.LESucc LEProof n1 m1
p) (a
x ::: Vec n a
xs) = a
x a -> Vec n1 a -> Vec ('S n1) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: LEProof n1 m1 -> Vec m1 a -> Vec n1 a
forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n1 m1
p Vec m1 a
Vec n a
xs

-- |
--
-- >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil
-- >>> drop xs :: Vec N.Nat3 Char
-- 'c' ::: 'd' ::: 'e' ::: VNil
--
drop :: forall n m a. (LE.ZS.LE n m, N.SNatI m) => Vec m a -> Vec n a
drop :: forall (n :: Nat) (m :: Nat) a.
(LE n m, SNatI m) =>
Vec m a -> Vec n a
drop = LEProof n m -> Vec m a -> Vec n a
forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go (LEProof n m -> LEProof n m
forall (n :: Nat) (m :: Nat). SNatI m => LEProof n m -> LEProof n m
LE.RS.fromZeroSucc LEProof n m
forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
LE.ZS.leProof) where
    go :: LE.RS.LEProof n' m' -> Vec m' a -> Vec n' a
    go :: forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n' m'
LE.RS.LERefl Vec m' a
xs             = Vec n' a
Vec m' a
xs
    go (LE.RS.LEStep LEProof n' m1
p) (a
_ ::: Vec n a
xs) = LEProof n' m1 -> Vec m1 a -> Vec n' a
forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n' m1
p Vec m1 a
Vec n a
xs

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

-- | >>> map not $ True ::: False ::: VNil
-- False ::: True ::: VNil
--
map :: (a -> b) -> Vec n a -> Vec n b
map :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> b
_ Vec n a
VNil       = Vec n b
Vec 'Z b
forall a. Vec 'Z a
VNil
map a -> b
f (a
x ::: Vec n a
xs) = a -> b
f a
x b -> Vec n b -> Vec ('S n) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: (a -> b) -> Vec n a -> Vec n b
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Vec n a
xs

-- | >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
-- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b
imap :: forall (n :: Nat) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imap Fin n -> a -> b
_ Vec n a
VNil       = Vec n b
Vec 'Z b
forall a. Vec 'Z a
VNil
imap Fin n -> a -> b
f (a
x ::: Vec n a
xs) = Fin n -> a -> b
f Fin n
Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x b -> Vec n b -> Vec ('S n) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: (Fin n -> a -> b) -> Vec n a -> Vec n b
forall (n :: Nat) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imap (Fin n -> a -> b
f (Fin n -> a -> b) -> (Fin n -> Fin n) -> Fin n -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs

-- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.
traverse :: forall n f a b. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
traverse :: forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse a -> f b
f = Vec n a -> f (Vec n b)
forall (m :: Nat). Vec m a -> f (Vec m b)
go where
    go :: Vec m a -> f (Vec m b)
    go :: forall (m :: Nat). Vec m a -> f (Vec m b)
go Vec m a
VNil       = Vec m b -> f (Vec m b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vec m b
Vec 'Z b
forall a. Vec 'Z a
VNil
    go (a
x ::: Vec n a
xs) = b -> Vec n b -> Vec m b
b -> Vec n b -> Vec ('S n) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) (b -> Vec n b -> Vec m b) -> f b -> f (Vec n b -> Vec m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x f (Vec n b -> Vec m b) -> f (Vec n b) -> f (Vec m b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Vec n a -> f (Vec n b)
forall (m :: Nat). Vec m a -> f (Vec m b)
go Vec n a
xs

#ifdef MIN_VERSION_semigroupoids
-- | Apply an action to non-empty 'Vec', yielding a 'Vec' of results.
traverse1 :: forall n f a b. Apply f => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 :: forall (n :: Nat) (f :: * -> *) a b.
Apply f =>
(a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 a -> f b
f = Vec ('S n) a -> f (Vec ('S n) b)
forall (m :: Nat). Vec ('S m) a -> f (Vec ('S m) b)
go where
    go :: Vec ('S m) a -> f (Vec ('S m) b)
    go :: forall (m :: Nat). Vec ('S m) a -> f (Vec ('S m) b)
go (a
x ::: Vec n a
VNil)         = (b -> Vec m b -> Vec ('S m) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec m b
Vec 'Z b
forall a. Vec 'Z a
VNil) (b -> Vec ('S m) b) -> f b -> f (Vec ('S m) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
    go (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = b -> Vec m b -> Vec ('S m) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) (b -> Vec m b -> Vec ('S m) b)
-> f b -> f (Vec m b -> Vec ('S m) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x f (Vec m b -> Vec ('S m) b) -> f (Vec m b) -> f (Vec ('S m) b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> Vec ('S n) a -> f (Vec ('S n) b)
forall (m :: Nat). Vec ('S m) a -> f (Vec ('S m) b)
go Vec n a
Vec ('S n) a
xs
#endif

-- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.
itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse :: forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse Fin n -> a -> f b
_ Vec n a
VNil       = Vec n b -> f (Vec n b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vec n b
Vec 'Z b
forall a. Vec 'Z a
VNil
itraverse Fin n -> a -> f b
f (a
x ::: Vec n a
xs) = b -> Vec n b -> Vec n b
b -> Vec n b -> Vec ('S n) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) (b -> Vec n b -> Vec n b) -> f b -> f (Vec n b -> Vec n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fin n -> a -> f b
f Fin n
Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x f (Vec n b -> Vec n b) -> f (Vec n b) -> f (Vec n b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse (Fin n -> a -> f b
f (Fin n -> a -> f b) -> (Fin n -> Fin n) -> Fin n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs

-- | Apply an action to every element of a 'Vec' and its index, ignoring the results.
itraverse_ :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ :: forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ Fin n -> a -> f b
_ Vec n a
VNil       = () -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
itraverse_ Fin n -> a -> f b
f (a
x ::: Vec n a
xs) = Fin n -> a -> f b
f Fin n
Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x f b -> f () -> f ()
forall a b. f a -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Fin n -> a -> f b) -> Vec n a -> f ()
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ (Fin n -> a -> f b
f (Fin n -> a -> f b) -> (Fin n -> Fin n) -> Fin n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs

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

-- | See 'I.Foldable'.
foldMap :: Monoid m => (a -> m) -> Vec n a -> m
foldMap :: forall m a (n :: Nat). Monoid m => (a -> m) -> Vec n a -> m
foldMap a -> m
_ Vec n a
VNil       = m
forall a. Monoid a => a
mempty
foldMap a -> m
f (a
x ::: Vec n a
xs) = m -> m -> m
forall a. Monoid a => a -> a -> a
mappend (a -> m
f a
x) ((a -> m) -> Vec n a -> m
forall m a (n :: Nat). Monoid m => (a -> m) -> Vec n a -> m
foldMap a -> m
f Vec n a
xs)

-- | See 'I.Foldable1'.
foldMap1 :: Semigroup s => (a -> s) -> Vec ('S n) a -> s
foldMap1 :: forall s a (n :: Nat). Semigroup s => (a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f (a
x ::: Vec n a
VNil)         = a -> s
f a
x
foldMap1 a -> s
f (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = a -> s
f a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> (a -> s) -> Vec ('S n) a -> s
forall s a (n :: Nat). Semigroup s => (a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f Vec n a
Vec ('S n) a
xs

-- | See 'I.FoldableWithIndex'.
ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap :: forall m (n :: Nat) a.
Monoid m =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap Fin n -> a -> m
_ Vec n a
VNil       = m
forall a. Monoid a => a
mempty
ifoldMap Fin n -> a -> m
f (a
x ::: Vec n a
xs) = m -> m -> m
forall a. Monoid a => a -> a -> a
mappend (Fin n -> a -> m
f Fin n
Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x) ((Fin n -> a -> m) -> Vec n a -> m
forall m (n :: Nat) a.
Monoid m =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap (Fin n -> a -> m
f (Fin n -> a -> m) -> (Fin n -> Fin n) -> Fin n -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs)

-- | There is no type-class for this :(
ifoldMap1 :: Semigroup s => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 :: forall s (n :: Nat) a.
Semigroup s =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 Fin ('S n) -> a -> s
f (a
x ::: Vec n a
VNil)         = Fin ('S n) -> a -> s
f Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x
ifoldMap1 Fin ('S n) -> a -> s
f (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = Fin ('S n) -> a -> s
f Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
forall s (n :: Nat) a.
Semigroup s =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 (Fin ('S n) -> a -> s
f (Fin ('S n) -> a -> s)
-> (Fin ('S n) -> Fin ('S n)) -> Fin ('S n) -> a -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S n) -> Fin ('S n)
Fin ('S n) -> Fin ('S ('S n))
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
Vec ('S n) a
xs

-- | Right fold.
foldr :: forall a b n. (a -> b -> b) -> b -> Vec n a -> b
foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z = Vec n a -> b
forall (m :: Nat). Vec m a -> b
go where
    go :: Vec m a -> b
    go :: forall (m :: Nat). Vec m a -> b
go Vec m a
VNil       = b
z
    go (a
x ::: Vec n a
xs) = a -> b -> b
f a
x (Vec n a -> b
forall (m :: Nat). Vec m a -> b
go Vec n a
xs)

-- | Right fold with an index.
ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr :: forall a b (n :: Nat). (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr Fin n -> a -> b -> b
_ b
z Vec n a
VNil       = b
z
ifoldr Fin n -> a -> b -> b
f b
z (a
x ::: Vec n a
xs) = Fin n -> a -> b -> b
f Fin n
Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x ((Fin n -> a -> b -> b) -> b -> Vec n a -> b
forall a b (n :: Nat). (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr (Fin n -> a -> b -> b
f (Fin n -> a -> b -> b) -> (Fin n -> Fin n) -> Fin n -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) b
z Vec n a
xs)

-- | Strict left fold.
foldl' :: forall a b n. (b -> a -> b) -> b -> Vec n a -> b
foldl' :: forall a b (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl' b -> a -> b
f b
z = b -> Vec n a -> b
forall (m :: Nat). b -> Vec m a -> b
go b
z where
    go :: b -> Vec m a -> b
    go :: forall (m :: Nat). b -> Vec m a -> b
go !b
acc Vec m a
VNil       = b
acc
    go !b
acc (a
x ::: Vec n a
xs) = b -> Vec n a -> b
forall (m :: Nat). b -> Vec m a -> b
go (b -> a -> b
f b
acc a
x) Vec n a
xs

-- | Yield the length of a 'Vec'. /O(n)/
length :: Vec n a -> Int
length :: forall (n :: Nat) a. Vec n a -> Int
length = Int -> Vec n a -> Int
forall (n :: Nat) a. Int -> Vec n a -> Int
go Int
0 where
    go :: Int -> Vec n a -> Int
    go :: forall (n :: Nat) a. Int -> Vec n a -> Int
go !Int
acc Vec n a
VNil       = Int
acc
    go  Int
acc (a
_ ::: Vec n a
xs) = Int -> Vec n a -> Int
forall (n :: Nat) a. Int -> Vec n a -> Int
go (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
acc) Vec n a
xs

-- | Test whether a 'Vec' is empty. /O(1)/
null :: Vec n a -> Bool
null :: forall (n :: Nat) a. Vec n a -> Bool
null Vec n a
VNil      = Bool
True
null (a
_ ::: Vec n a
_) = Bool
False

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

-- | Non-strict 'sum'.
sum :: Num a => Vec n a -> a
sum :: forall a (n :: Nat). Num a => Vec n a -> a
sum Vec n a
VNil       = a
0
sum (a
x ::: Vec n a
xs) = a
x a -> a -> a
forall a. Num a => a -> a -> a
+ Vec n a -> a
forall a (n :: Nat). Num a => Vec n a -> a
sum Vec n a
xs

-- | Non-strict 'product'.
product :: Num a => Vec n a -> a
product :: forall a (n :: Nat). Num a => Vec n a -> a
product Vec n a
VNil       = a
1
product (a
x ::: Vec n a
xs) = a
x a -> a -> a
forall a. Num a => a -> a -> a
* Vec n a -> a
forall a (n :: Nat). Num a => Vec n a -> a
product Vec n a
xs

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

-- | Zip two 'Vec's with a function.
zipWith ::  (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith :: forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
_ Vec n a
VNil       Vec n b
VNil       = Vec n c
Vec 'Z c
forall a. Vec 'Z a
VNil
zipWith a -> b -> c
f (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = a -> b -> c
f a
x b
y c -> Vec n c -> Vec ('S n) c
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
f Vec n a
xs Vec n b
Vec n b
ys

-- | Zip two 'Vec's. with a function that also takes the elements' indices.
izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith :: forall (n :: Nat) a b c.
(Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith Fin n -> a -> b -> c
_ Vec n a
VNil       Vec n b
VNil       = Vec n c
Vec 'Z c
forall a. Vec 'Z a
VNil
izipWith Fin n -> a -> b -> c
f (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = Fin n -> a -> b -> c
f Fin n
Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ a
x b
y c -> Vec n c -> Vec ('S n) c
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall (n :: Nat) a b c.
(Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith (Fin n -> a -> b -> c
f (Fin n -> a -> b -> c) -> (Fin n -> Fin n) -> Fin n -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs Vec n b
Vec n b
ys

-- | Repeat a value.
--
-- >>> repeat 'x' :: Vec N.Nat3 Char
-- 'x' ::: 'x' ::: 'x' ::: VNil
--
-- @since 0.2.1
repeat :: N.SNatI n => x -> Vec n x
repeat :: forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat x
x = 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 a (n :: Nat). a -> Vec n a -> Vec ('S n) a
:::)

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

-- | Monadic bind.
bind :: Vec n a -> (a -> Vec n b) -> Vec n b
bind :: forall (n :: Nat) a b. Vec n a -> (a -> Vec n b) -> Vec n b
bind Vec n a
VNil       a -> Vec n b
_ = Vec n b
Vec 'Z b
forall a. Vec 'Z a
VNil
bind (a
x ::: Vec n a
xs) a -> Vec n b
f = Vec ('S n) b -> b
forall (n :: Nat) a. Vec ('S n) a -> a
head (a -> Vec n b
f a
x) b -> Vec n b -> Vec ('S n) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a -> (a -> Vec n b) -> Vec n b
forall (n :: Nat) a b. Vec n a -> (a -> Vec n b) -> Vec n b
bind Vec n a
xs (Vec ('S n) b -> Vec n b
forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail (Vec ('S n) b -> Vec n b) -> (a -> Vec ('S n) b) -> a -> Vec n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vec n b
a -> Vec ('S n) b
f)

-- | Monadic join.
--
-- >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
-- 'a' ::: 'd' ::: VNil
join :: Vec n (Vec n a) -> Vec n a
join :: forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join Vec n (Vec n a)
VNil       = Vec n a
Vec 'Z a
forall a. Vec 'Z a
VNil
join (Vec n a
x ::: Vec n (Vec n a)
xs) = Vec ('S n) a -> a
forall (n :: Nat) a. Vec ('S n) a -> a
head Vec n a
Vec ('S n) a
x a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n (Vec n a) -> Vec n a
forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join ((Vec ('S n) a -> Vec n a)
-> Vec n (Vec ('S n) a) -> Vec n (Vec n a)
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map Vec ('S n) a -> Vec n a
forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail Vec n (Vec n a)
Vec n (Vec ('S n) a)
xs)

-------------------------------------------------------------------------------
-- universe
-------------------------------------------------------------------------------

-- | Get all @'Fin' n@ in a @'Vec' n@.
--
-- >>> universe :: Vec N.Nat3 (Fin N.Nat3)
-- 0 ::: 1 ::: 2 ::: VNil
universe :: N.SNatI n => Vec n (Fin n)
universe :: forall (n :: Nat). SNatI n => Vec n (Fin n)
universe = 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
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Universe 'Z
first Universe m -> Universe ('S m)
forall (m :: Nat). SNatI m => Universe m -> Universe ('S m)
forall (m :: Nat). 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 :: Universe m -> Universe ('S m)
    step :: forall (m :: Nat). 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 a (n :: Nat). 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). (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 { forall (n :: Nat). Universe n -> Vec n (Fin n)
getUniverse :: Vec n (Fin n) }

-------------------------------------------------------------------------------
-- VecEach
-------------------------------------------------------------------------------

-- | Write functions on 'Vec'. Use them with tuples.
--
-- 'VecEach' can be used to avoid "this function won't change the length of the
-- list" in DSLs.
--
-- __bad:__ Instead of
--
-- @
-- [x, y] <- badDslMagic ["foo", "bar"]  -- list!
-- @
--
-- __good:__ we can write
--
-- @
-- (x, y) <- betterDslMagic ("foo", "bar") -- homogenic tuple!
-- @
--
-- where @betterDslMagic@ can be defined using 'traverseWithVec'.
--
-- Moreally @lens@ 'Each' should be a superclass, but
-- there's no strict need for it.
--
class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where
    mapWithVec :: (forall n. N.SNatI n => Vec n a -> Vec n b) -> s -> t
    traverseWithVec :: Applicative f => (forall n. N.SNatI n => Vec n a -> f (Vec n b)) -> s -> f t

instance (a ~ a', b ~ b') => VecEach (a, a') (b, b') a b where
    mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b)
-> (a, a') -> (b, b')
mapWithVec forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f ~(a
x, a'
y) = case Vec ('S ('S 'Z)) a -> Vec ('S ('S 'Z)) b
forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f (a
x a -> Vec ('S 'Z) a -> Vec ('S ('S 'Z)) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a'
y a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil) of
        b
x' ::: b
y' ::: Vec n b
VNil -> (b
x', b
b'
y')

    traverseWithVec :: forall (f :: * -> *).
Applicative f =>
(forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b))
-> (a, a') -> f (b, b')
traverseWithVec forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f ~(a
x, a'
y) = Vec ('S ('S 'Z)) a -> f (Vec ('S ('S 'Z)) b)
forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f (a
x a -> Vec ('S 'Z) a -> Vec ('S ('S 'Z)) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a'
y a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil) f (Vec ('S ('S 'Z)) b)
-> (Vec ('S ('S 'Z)) b -> (b, b')) -> f (b, b')
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Vec ('S ('S 'Z)) b
res -> case Vec ('S ('S 'Z)) b
res of
        b
x' ::: b
y' ::: Vec n b
VNil -> (b
x', b
b'
y')

instance (a ~ a2, a ~ a3, b ~ b2, b ~ b3) => VecEach (a, a2, a3) (b, b2, b3) a b where
    mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b)
-> (a, a2, a3) -> (b, b2, b3)
mapWithVec forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f ~(a
x, a2
y, a3
z) = case Vec ('S ('S ('S 'Z))) a -> Vec ('S ('S ('S 'Z))) b
forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f (a
x a -> Vec ('S ('S 'Z)) a -> Vec ('S ('S ('S 'Z))) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a2
y a -> Vec ('S 'Z) a -> Vec ('S ('S 'Z)) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a3
z a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil) of
        b
x' ::: b
y' ::: b
z' ::: Vec n b
VNil -> (b
x', b
b2
y', b
b3
z')

    traverseWithVec :: forall (f :: * -> *).
Applicative f =>
(forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b))
-> (a, a2, a3) -> f (b, b2, b3)
traverseWithVec forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f ~(a
x, a2
y, a3
z) = Vec ('S ('S ('S 'Z))) a -> f (Vec ('S ('S ('S 'Z))) b)
forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f (a
x a -> Vec ('S ('S 'Z)) a -> Vec ('S ('S ('S 'Z))) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a2
y a -> Vec ('S 'Z) a -> Vec ('S ('S 'Z)) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a3
z a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil) f (Vec ('S ('S ('S 'Z))) b)
-> (Vec ('S ('S ('S 'Z))) b -> (b, b2, b3)) -> f (b, b2, b3)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Vec ('S ('S ('S 'Z))) b
res -> case Vec ('S ('S ('S 'Z))) b
res of
        b
x' ::: b
y' ::: b
z' ::: Vec n b
VNil -> (b
x', b
b2
y', b
b3
z')

instance (a ~ a2, a ~ a3, a ~ a4, b ~ b2, b ~ b3, b ~ b4) => VecEach (a, a2, a3, a4) (b, b2, b3, b4) a b where
    mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b)
-> (a, a2, a3, a4) -> (b, b2, b3, b4)
mapWithVec forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f ~(a
x, a2
y, a3
z, a4
u) = case Vec ('S ('S ('S ('S 'Z)))) a -> Vec ('S ('S ('S ('S 'Z)))) b
forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f (a
x a -> Vec ('S ('S ('S 'Z))) a -> Vec ('S ('S ('S ('S 'Z)))) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a2
y a -> Vec ('S ('S 'Z)) a -> Vec ('S ('S ('S 'Z))) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a3
z a -> Vec ('S 'Z) a -> Vec ('S ('S 'Z)) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a4
u a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil) of
        b
x' ::: b
y' ::: b
z' ::: b
u' ::: Vec n b
VNil -> (b
x', b
b2
y', b
b3
z', b
b4
u')

    traverseWithVec :: forall (f :: * -> *).
Applicative f =>
(forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b))
-> (a, a2, a3, a4) -> f (b, b2, b3, b4)
traverseWithVec forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f ~(a
x, a2
y, a3
z, a4
u) = Vec ('S ('S ('S ('S 'Z)))) a -> f (Vec ('S ('S ('S ('S 'Z)))) b)
forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f (a
x a -> Vec ('S ('S ('S 'Z))) a -> Vec ('S ('S ('S ('S 'Z)))) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a2
y a -> Vec ('S ('S 'Z)) a -> Vec ('S ('S ('S 'Z))) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a3
z a -> Vec ('S 'Z) a -> Vec ('S ('S 'Z)) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a
a4
u a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil) f (Vec ('S ('S ('S ('S 'Z)))) b)
-> (Vec ('S ('S ('S ('S 'Z)))) b -> (b, b2, b3, b4))
-> f (b, b2, b3, b4)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Vec ('S ('S ('S ('S 'Z)))) b
res -> case Vec ('S ('S ('S ('S 'Z)))) b
res of
        b
x' ::: b
y' ::: b
z' ::: b
u' ::: Vec n b
VNil -> (b
x', b
b2
y', b
b3
z', b
b4
u')

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

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

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

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

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

instance (N.SNatI n, QC.Arbitrary a) => QC.Arbitrary (Vec n a) where
    arbitrary :: Gen (Vec n a)
arbitrary = 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 :: forall b. 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 (a
x ::: Vec n a
xs) -> (a, Vec n a) -> Gen b -> Gen b
forall b. (a, Vec n a) -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (a
x, Vec n a
xs))

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