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

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

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