{-# 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.Boring         (Boring (..))
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 on purpose doesn'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 { forall (n :: Nat) a. 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Fin n
i -> Fin n -> a
u Fin n
i forall a. Eq a => a -> a -> Bool
== Fin n -> a
v Fin n
i) forall (n :: Nat). SNatI n => [Fin n]
F.universe

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

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

-- | @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 = 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 :: forall m a. Monoid m => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap = forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap
    ifoldr :: forall a b. (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr   = forall (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 :: forall m a. Semigroup m => (a -> m) -> Vec n a -> m
foldMap1 = forall s (n :: Nat) a.
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1
#endif

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

instance Monad (Vec n) where
    return :: forall a. a -> Vec n a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: forall a b. Vec n a -> (a -> Vec n b) -> Vec n b
(>>=)  = forall (n :: Nat) a b. 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 Distributive (Vec n) where
    distribute :: forall (f :: * -> *) a. Functor f => f (Vec n a) -> Vec n (f a)
distribute = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 :: forall a. (Rep (Vec n) -> a) -> Vec n a
tabulate = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec
    index :: forall a. Vec n a -> Rep (Vec n) -> a
index    = 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 = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
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 = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec 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 = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (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
    <.> :: forall 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 forall a b. (a -> b) -> a -> b
($)
    Vec n a
_ .> :: forall a b. Vec n a -> Vec n b -> Vec n b
.> Vec n b
x = Vec n b
x
    Vec n a
x <. :: forall a b. Vec n a -> Vec n b -> Vec n a
<. Vec n b
_ = Vec n a
x
    liftF2 :: forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftF2 = forall a b c (n :: Nat).
(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
(>>-) = 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  = 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 = forall a. Vec 'Z a
empty

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

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

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

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

-- | Convert 'Vec' to NonEmpty.
toNonEmpty :: N.SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty Vec ('S n) a
v = forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S n) a
v forall a. a -> [a] -> NonEmpty a
:| forall (n :: Nat) a. SNatI n => Vec n a -> [a]
toList (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 :: forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromList = forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. FromList 'Z a
start forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
    start :: FromList 'Z a
    start :: forall a. FromList 'Z a
start = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
        []      -> forall a. a -> Maybe a
Just forall a. Vec 'Z a
empty
        (a
_ : [a]
_) -> forall a. Maybe a
Nothing

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

    step :: FromList n a -> FromList ('N.S n) a
    step :: forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step (FromList [a] -> Maybe (Vec n a)
f) = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
        []       -> forall a. Maybe a
Nothing
        (a
x : [a]
xs') -> forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Vec n a)
f [a]
xs'

-- | Reify any list @[a]@ to @'Vec' n a@.
--
-- >>> reifyList "foo" length
-- 3
reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r
reifyList :: forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList []       forall (n :: Nat). SNatI n => Vec n a -> r
f = forall (n :: Nat). SNatI n => Vec n a -> r
f forall a. Vec 'Z a
empty
reifyList (a
x : [a]
xs) forall (n :: Nat). SNatI n => Vec n a -> r
f = forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [a]
xs forall a b. (a -> b) -> a -> b
$ \Vec n a
xs' -> forall (n :: Nat). SNatI n => Vec n a -> r
f (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
! :: forall (n :: Nat) 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 :: forall (n :: Nat) a. (Fin n -> a) -> Vec n a
tabulate = 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 :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec 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 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 :: forall a (n :: Nat). SNatI n => Vec n a -> a -> Vec ('S n) a
snoc (Vec Fin n -> a
xs) a
x = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
i -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x Fin n -> a
xs (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 :: forall (n :: Nat) a. Vec ('S n) a -> a
head (Vec Fin ('S n) -> a
v) = Fin ('S n) -> a
v 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 :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> a
last (Vec Fin ('S n) -> a
v) = Fin ('S n) -> a
v forall a. Bounded a => a
maxBound

-- | 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 (Vec Fin ('S n) -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> Vec n a
init (Vec Fin ('S n) -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
reverse (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> b
f (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (a -> b
f 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 :: forall (n :: Nat) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imap Fin n -> a -> b
f (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec 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 :: forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(a -> m) -> Vec n a -> m
foldMap a -> m
f (Vec Fin n -> a
v) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
I.foldMap (a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v) 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 :: forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap Fin n -> a -> m
f (Vec Fin n -> a
v) = 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)) 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 :: forall s (n :: Nat) a.
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f (Vec Fin ('S n) -> a
v) = forall s a. Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap (a -> s
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S n) -> a
v) 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 :: forall s (n :: Nat) a.
(Semigroup s, SNatI n) =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 Fin ('S n) -> a -> s
f (Vec Fin ('S n) -> a
v) = 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)) forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
F.universe1

neFoldMap :: Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap :: forall s a. Semigroup s => (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 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 :: forall (n :: Nat) a b.
SNatI n =>
(a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z (Vec Fin n -> a
v) = 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 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 :: forall (n :: Nat) a b.
SNatI n =>
(Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr Fin n -> a -> b -> b
f b
z (Vec Fin n -> a
v) = 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 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' :: forall (n :: Nat) b a.
SNatI n =>
(b -> a -> b) -> b -> Vec n a -> b
foldl' b -> a -> b
f b
z (Vec Fin n -> a
v) = 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 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 :: forall (n :: Nat) a. SNatI n => Vec n a -> Int
length Vec n a
_ = forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (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 :: forall (n :: Nat) a. SNatI n => Vec n a -> Bool
null Vec n a
_ = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
    SNat n
N.SZ -> Bool
True
    SNat n
N.SS -> Bool
False

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

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

-- | Strict 'product'.
product :: (Num a, N.SNatI n) => Vec n a -> a
product :: forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
product (Vec Fin n -> a
v) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\a
x Fin n
i -> a
x forall a. Num a => a -> a -> a
* Fin n -> a
v Fin n
i) a
1 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 :: forall a b c (n :: Nat).
(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) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec 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 :: 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 (Vec Fin n -> a
xs) (Vec Fin n -> b
ys) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec 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 :: forall x (n :: Nat). x -> Vec n x
repeat = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

-------------------------------------------------------------------------------
-- 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
m a -> Vec n b
k = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec Vec n a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec 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 :: forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join (Vec Fin n -> Vec n a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin n
i -> 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 :: forall (n :: Nat). SNatI n => Vec n (Fin n)
universe = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a. a -> a
id