{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
-- | Pull/representable @'Vec' n a = 'Fin' n -> a@.
--
-- The module tries to have same API as "Data.Vec.Lazy", missing bits:
-- @withDict@, @toPull@, @fromPull@, @traverse@ (and variants),
-- @(++)@, @concat@ and @split@.
module Data.Vec.Pull (
    Vec (..),
    -- * Construction
    empty,
    singleton,
    -- * Conversions
    toList,
    toNonEmpty,
    fromList,
    fromListPrefix,
    reifyList,
    -- * Indexing
    (!),
    tabulate,
    cons,
    snoc,
    head,
    last,
    tail,
    init,
    -- * Reverse
    reverse,
    -- * Folds
    foldMap,
    foldMap1,
    ifoldMap,
    ifoldMap1,
    foldr,
    ifoldr,
    foldl',
    -- * Special folds
    length,
    null,
    sum,
    product,
    -- * Mapping
    map,
    imap,
    -- * Zipping
    zipWith,
    izipWith,
    repeat,
    -- * Monadic
    bind,
    join,
    -- * Universe
    universe,
    ) where

import Prelude
       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
       all, const, id, maxBound, maybe, ($), (.))

import Control.Applicative (Applicative (..), (<$>))
import Data.Fin            (Fin (..))
import Data.List.NonEmpty  (NonEmpty (..))
import Data.Monoid         (Monoid (..))
import Data.Nat            (Nat (..))
import Data.Proxy          (Proxy (..))
import Data.Semigroup      (Semigroup (..))
import Data.Typeable       (Typeable)

--- Instances
import qualified Data.Foldable as I (Foldable (..))

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

#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 (..))
#endif

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

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

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

-- | Easily fuseable 'Vec'.
--
-- It unpurpose don't have /bad/ (fusion-wise) instances, like 'Traversable'.
-- Generally, there aren't functions which would be __bad consumers__ or __bad producers__.
newtype Vec n a = Vec { Vec n a -> Fin n -> a
unVec :: Fin n -> a }
  deriving (Typeable)

instance (Eq a, N.SNatI n) => Eq (Vec n a) where
    Vec Fin n -> a
v == :: Vec n a -> Vec n a -> Bool
== Vec Fin n -> a
u = (Fin n -> Bool) -> [Fin n] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Fin n
i -> Fin n -> a
u Fin n
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Fin n -> a
v Fin n
i) [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

instance Functor (Vec n) where
    fmap :: (a -> b) -> Vec n a -> Vec n b
fmap a -> b
f (Vec Fin n -> a
v) = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (a -> b
f (a -> b) -> (Fin n -> a) -> Fin n -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v)

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

-- | @since 0.4
instance 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. (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 m (n :: Nat) a.
(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 (n :: Nat) a b.
SNatI n =>
(Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr

#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 (n :: Nat) a.
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1
#endif

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

instance 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. 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 Distributive (Vec n) where
    distribute :: f (Vec n a) -> Vec n (f a)
distribute = (Fin n -> f a) -> Vec n (f a)
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> f a) -> Vec n (f a))
-> (f (Vec n a) -> Fin n -> f a) -> f (Vec n a) -> Vec n (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Fin n -> a) -> Fin n -> f a
forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute (f (Fin n -> a) -> Fin n -> f a)
-> (f (Vec n a) -> f (Fin n -> a)) -> f (Vec n a) -> Fin n -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n a -> Fin n -> a) -> f (Vec n a) -> f (Fin n -> a)
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
unVec

#ifdef MIN_VERSION_adjunctions
instance 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. (Fin n -> a) -> Vec n a
Vec
    index :: Vec n a -> Rep (Vec n) -> a
index    = Vec n a -> Rep (Vec n) -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec
#endif
#endif

instance Semigroup a => Semigroup (Vec n a) where
    Vec Fin n -> a
a <> :: Vec n a -> Vec n a -> Vec n a
<> Vec Fin n -> a
b = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
a (Fin n -> a) -> (Fin n -> a) -> Fin n -> a
forall a. Semigroup a => a -> a -> a
<> Fin n -> a
b)

instance Monoid a => Monoid (Vec n a) where
    mempty :: Vec n a
mempty = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec Fin n -> a
forall a. Monoid a => a
mempty
    Vec Fin n -> a
a mappend :: Vec n a -> Vec n a -> Vec n a
`mappend` Vec Fin n -> a
b = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> a) -> (Fin n -> a) -> Fin n -> a
forall a. Monoid a => a -> a -> a
mappend Fin n -> a
a Fin n -> a
b)

#ifdef MIN_VERSION_semigroupoids
instance 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).
(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).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith

instance 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. 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. Vec n (Vec n a) -> Vec n a
join
#endif

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

-- | Empty 'Vec'.
empty :: Vec 'Z a
empty :: Vec 'Z a
empty = (Fin 'Z -> a) -> Vec 'Z a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec Fin 'Z -> a
forall b. Fin 'Z -> b
F.absurd

-- | 'Vec' with exactly one element.
--
-- >>> L.fromPull $ singleton True
-- True ::: VNil
--
singleton :: a -> Vec ('S 'Z) a
singleton :: a -> Vec ('S 'Z) a
singleton = (Fin ('S 'Z) -> a) -> Vec ('S 'Z) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin ('S 'Z) -> a) -> Vec ('S 'Z) a)
-> (a -> Fin ('S 'Z) -> a) -> a -> Vec ('S 'Z) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Fin ('S 'Z) -> a
forall a b. a -> b -> a
const

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

-- | Convert 'Vec' to list.
toList :: N.SNatI n => Vec n a -> [a]
toList :: Vec n a -> [a]
toList Vec n a
v = Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec Vec n a
v (Fin n -> a) -> [Fin n] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

-- | Convert 'Vec' to NonEmpty.
toNonEmpty :: N.SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty :: Vec ('S n) a -> NonEmpty a
toNonEmpty Vec ('S n) a
v = Vec ('S n) a -> a
forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S n) a
v 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 ('S n) a -> Vec n a
forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail Vec ('S n) a
v)

-- | Convert list @[a]@ to @'Vec' n a@.
-- Returns 'Nothing' if lengths don't match exactly.
--
-- >>> L.fromPull <$> fromList "foo" :: Maybe (L.Vec N.Nat3 Char)
-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- >>> L.fromPull <$> fromList "quux" :: Maybe (L.Vec N.Nat3 Char)
-- Nothing
--
-- >>> L.fromPull <$> fromList "xy" :: Maybe (L.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
empty
        (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 -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x (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.
--
-- >>> L.fromPull <$> fromListPrefix "foo" :: Maybe (L.Vec N.Nat3 Char)
-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- >>> L.fromPull <$> fromListPrefix "quux" :: Maybe (L.Vec N.Nat3 Char)
-- Just ('q' ::: 'u' ::: 'u' ::: VNil)
--
-- >>> L.fromPull <$> fromListPrefix "xy" :: Maybe (L.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
empty -- 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 -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x (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
empty
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 -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x Vec n a
xs')

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

-- | Indexing.
(!) :: Vec n a -> Fin n -> a
(!) = Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec

-- Tabulating, inverse of '!'.
tabulate :: (Fin n -> a) -> Vec n a
tabulate :: (Fin n -> a) -> Vec n a
tabulate = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec

-- | 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
x (Vec Fin n -> a
v) = (Fin ('S n) -> a) -> Vec ('S n) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin ('S n) -> a) -> Vec ('S n) a)
-> (Fin ('S n) -> a) -> Vec ('S n) a
forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
i -> case Fin ('S n)
i of
    Fin ('S n)
FZ   -> a
x
    FS Fin n1
j -> Fin n -> a
v Fin n
Fin n1
j

-- | Add a single element at the end of a 'Vec'.
--
-- @since 0.2.1
snoc :: forall a n. N.SNatI n => Vec n a -> a -> Vec ('S n) a
snoc :: Vec n a -> a -> Vec ('S n) a
snoc (Vec Fin n -> a
xs) a
x = (Fin ('S n) -> a) -> Vec ('S n) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin ('S n) -> a) -> Vec ('S n) a)
-> (Fin ('S n) -> a) -> Vec ('S n) a
forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
i -> a -> (Fin n -> a) -> Maybe (Fin n) -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x Fin n -> a
xs (Fin ('S n) -> Maybe (Fin n)
forall (n :: Nat). SNatI n => Fin ('S n) -> Maybe (Fin n)
F.isMax Fin ('S n)
i)

-- | The first element of a 'Vec'.
head :: Vec ('S n) a -> a
head :: Vec ('S n) a -> a
head (Vec Fin ('S n) -> a
v) = Fin ('S n) -> a
v Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ

-- | The last element of a 'Vec'.
last :: forall n a. N.SNatI n => Vec ('S n) a -> a
last :: Vec ('S n) a -> a
last (Vec Fin ('S n) -> a
v) = Fin ('S n) -> a
v Fin ('S n)
forall a. Bounded a => a
maxBound 

-- | 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 (Vec Fin ('S n) -> a
v) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v (Fin ('S n) -> a) -> (Fin n -> Fin ('S n)) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS)

-- | The elements before the 'last' of a 'Vec'.
init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a
init :: Vec ('S n) a -> Vec n a
init (Vec Fin ('S n) -> a
v) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v (Fin ('S n) -> a) -> (Fin n -> Fin ('S n)) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin ('S n)
forall (n :: Nat). SNatI n => Fin n -> Fin ('S n)
F.weakenLeft1)

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

-- | Reverse 'Vec'.
--
-- @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 (Vec Fin n -> a
v) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
v (Fin n -> a) -> (Fin n -> Fin n) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
forall (n :: Nat). SNatI n => Fin n -> Fin n
F.mirror)

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

-- | >>> L.fromPull $ map not $ L.toPull $ True L.::: False L.::: L.VNil
-- False ::: True ::: VNil
--
map :: (a -> b) -> Vec n a -> Vec n b
map :: (a -> b) -> Vec n a -> Vec n b
map a -> b
f (Vec Fin n -> a
v) = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (a -> b
f (a -> b) -> (Fin n -> a) -> Fin n -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v)

-- | >>> L.fromPull $ imap (,) $ L.toPull $ 'a' L.::: 'b' L.::: 'c' L.::: L.VNil
-- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b
imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b
imap Fin n -> a -> b
f (Vec Fin n -> a
v) = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> b) -> Vec n b) -> (Fin n -> b) -> Vec n b
forall a b. (a -> b) -> a -> b
$ \Fin n
i -> Fin n -> a -> b
f Fin n
i (Fin n -> a
v Fin n
i)

-------------------------------------------------------------------------------
-- 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 (Vec Fin n -> a
v) = (Fin n -> m) -> [Fin n] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
I.foldMap (a -> m
f (a -> m) -> (Fin n -> a) -> Fin n -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v) [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

-- | See 'I.FoldableWithIndex'.
ifoldMap :: (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap :: (Fin n -> a -> m) -> Vec n a -> m
ifoldMap Fin n -> a -> m
f (Vec Fin n -> a
v) = (Fin n -> m) -> [Fin n] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
I.foldMap (\Fin n
i -> Fin n -> a -> m
f Fin n
i (Fin n -> a
v Fin n
i)) [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

-- | See 'I.Foldable1'.
foldMap1 :: (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s
foldMap1 :: (a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f (Vec Fin ('S n) -> a
v) = (Fin ('S n) -> s) -> NonEmpty (Fin ('S n)) -> s
forall s a. Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap (a -> s
f (a -> s) -> (Fin ('S n) -> a) -> Fin ('S n) -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S n) -> a
v) NonEmpty (Fin ('S n))
forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
F.universe1

-- | There is no type-class for this :(
ifoldMap1 :: (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 Fin ('S n) -> a -> s
f (Vec Fin ('S n) -> a
v) = (Fin ('S n) -> s) -> NonEmpty (Fin ('S n)) -> s
forall s a. Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap (\Fin ('S n)
i -> Fin ('S n) -> a -> s
f Fin ('S n)
i (Fin ('S n) -> a
v Fin ('S n)
i)) NonEmpty (Fin ('S n))
forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
F.universe1

neFoldMap :: Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap :: (a -> s) -> NonEmpty a -> s
neFoldMap a -> s
f (a
z :| [a]
zs) = a -> [a] -> s
go a
z [a]
zs where
    go :: a -> [a] -> s
go a
x []       = a -> s
f a
x
    go a
x (a
y : [a]
ys) = a -> s
f a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> a -> [a] -> s
go a
y [a]
ys

-- | Right fold.
foldr :: 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 (Vec Fin n -> a
v) = (Fin n -> b -> b) -> b -> [Fin n] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
I.foldr (\Fin n
a b
b -> a -> b -> b
f (Fin n -> a
v Fin n
a) b
b) b
z [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

-- | Right fold with an index.
ifoldr :: 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 Fin n -> a -> b -> b
f b
z (Vec Fin n -> a
v) = (Fin n -> b -> b) -> b -> [Fin n] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
I.foldr (\Fin n
a b
b -> Fin n -> a -> b -> b
f Fin n
a (Fin n -> a
v Fin n
a) b
b) b
z [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

-- | Strict left fold.
foldl' :: N.SNatI n => (b -> a -> b) -> b -> Vec n a -> b
foldl' :: (b -> a -> b) -> b -> Vec n a -> b
foldl' b -> a -> b
f b
z (Vec Fin n -> a
v) = (b -> Fin n -> b) -> b -> [Fin n] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\b
b Fin n
a -> b -> a -> b
f b
b (Fin n -> a
v Fin n
a)) b
z [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

-- | Yield the length of a 'Vec'.
length :: forall n a. N.SNatI n => Vec n a -> Int
length :: Vec n a -> Int
length Vec n a
_ = Proxy @Nat n -> Int
forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (Proxy @Nat n
forall k (t :: k). Proxy @k t
Proxy :: Proxy n)

-- | Test whether a 'Vec' is empty.
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
-------------------------------------------------------------------------------

-- | Strict 'sum'.
sum :: (Num a, N.SNatI n) => Vec n a -> a
sum :: Vec n a -> a
sum (Vec Fin n -> a
v) = (a -> Fin n -> a) -> a -> [Fin n] -> a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\a
x Fin n
i -> a
x a -> a -> a
forall a. Num a => a -> a -> a
+ Fin n -> a
v Fin n
i) a
0 [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

-- | Strict 'product'.
product :: (Num a, N.SNatI n) => Vec n a -> a
product :: Vec n a -> a
product (Vec Fin n -> a
v) = (a -> Fin n -> a) -> a -> [Fin n] -> a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\a
x Fin n
i -> a
x a -> a -> a
forall a. Num a => a -> a -> a
* Fin n -> a
v Fin n
i) a
1 [Fin n]
forall (n :: Nat). SNatI n => [Fin n]
F.universe

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

-- | Zip two 'Vec's with a function.
zipWith :: (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 (Vec Fin n -> a
xs) (Vec Fin n -> b
ys) = (Fin n -> c) -> Vec n c
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> c) -> Vec n c) -> (Fin n -> c) -> Vec n c
forall a b. (a -> b) -> a -> b
$ \Fin n
i -> a -> b -> c
f (Fin n -> a
xs Fin n
i) (Fin n -> b
ys Fin n
i)

-- | 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 :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith Fin n -> a -> b -> c
f (Vec Fin n -> a
xs) (Vec Fin n -> b
ys) = (Fin n -> c) -> Vec n c
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> c) -> Vec n c) -> (Fin n -> c) -> Vec n c
forall a b. (a -> b) -> a -> b
$ \Fin n
i -> Fin n -> a -> b -> c
f Fin n
i (Fin n -> a
xs Fin n
i) (Fin n -> b
ys Fin n
i)

-- | Repeat value
--
-- @since 0.2.1
repeat :: x -> Vec n x
repeat :: x -> Vec n x
repeat = (Fin n -> x) -> Vec n x
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> x) -> Vec n x) -> (x -> Fin n -> x) -> x -> Vec n x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Fin n -> x
forall (f :: * -> *) a. Applicative f => a -> f a
pure

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

-- | Monadic bind.
bind :: Vec n a -> (a -> Vec n b) -> Vec n b
bind :: Vec n a -> (a -> Vec n b) -> Vec n b
bind Vec n a
m a -> Vec n b
k = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> b) -> Vec n b) -> (Fin n -> b) -> Vec n b
forall a b. (a -> b) -> a -> b
$ Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec Vec n a
m (Fin n -> a) -> (a -> Fin n -> b) -> Fin n -> b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vec n b -> Fin n -> b
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec (Vec n b -> Fin n -> b) -> (a -> Vec n b) -> a -> Fin n -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vec n b
k

-- | Monadic join.
join :: Vec n (Vec n a) -> Vec n a
join :: Vec n (Vec n a) -> Vec n a
join (Vec Fin n -> Vec n a
v) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> a) -> Vec n a) -> (Fin n -> a) -> Vec n a
forall a b. (a -> b) -> a -> b
$ \Fin n
i -> Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec (Fin n -> Vec n a
v Fin n
i) Fin n
i

-------------------------------------------------------------------------------
-- Universe
-------------------------------------------------------------------------------

-- | Get all @'Fin' n@ in a @'Vec' n@.
--
-- >>> L.fromPull (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 = (Fin n -> Fin n) -> Vec n (Fin n)
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec Fin n -> Fin n
forall a. a -> a
id