{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
-- |
-- CPS encoded heterogeneous vectors.
module Data.Vector.HFixed.Cont (
    -- * CPS-encoded vector
    -- ** Type classes
    Fn
  , Fun
  , TFun(..)
  , Arity(..)
  , HVector(..)
  , tupleSize
  , HVectorF(..)
  , tupleSizeF
  , ValueAt
  , Index
    -- ** CPS-encoded vector
  , ContVec
  , ContVecF(..)
    -- ** Other data types
  , VecList(..)
  , VecListF(..)
    -- * Conversion to/from vector
  , cvec
  , vector
  , cvecF
  , vectorF
    -- * Generic API for tuples
    -- ** Position based functions
  , head
  , tail
  , cons
  , consF
  , concat
    -- ** Indexing
  , index
  , set
  , tyLookup
  , tyLookupF
    -- ** Folds and unfolds
  , foldlF
  , foldrF
  , foldMapF
  , foldlNatF
  , foldrNatF
  , foldMapNatF
  , unfoldrF
    -- ** Replicate variants
  , replicateF
  , replicateNatF
    -- ** Zip variants
  , zipWithF
  , zipWithNatF
  , zipFoldF
    -- ** Monomorphization of vectors
  , monomorphizeF
    -- ** Manipulation with type constructor
  , map
  , mapNat
  , sequenceF
  , distributeF
  ) where

import Control.Applicative   (Applicative(..),Const(..))
import Data.Monoid           (Monoid(..),(<>))
import Data.Functor.Compose  (Compose(..))
import Data.Functor.Identity (Identity(..))
import qualified Data.Vector.Fixed.Cont as F
import Prelude               (Functor(..),id,(.),($))

import Data.Vector.HFixed.Class



----------------------------------------------------------------
-- Conversions between vectors
----------------------------------------------------------------

-- | Convert heterogeneous vector to CPS form
cvec :: (HVector v, Elems v ~ xs) => v -> ContVec xs
cvec :: v -> ContVec xs
cvec v
v = (forall r. TFun Identity xs r -> r) -> ContVec xs
forall α (xs :: [α]) (f :: α -> *).
(forall r. TFun f xs r -> r) -> ContVecF xs f
ContVecF (v -> Fun (Elems v) r -> r
forall v a. HVector v => v -> Fun (Elems v) a -> a
inspect v
v)
{-# INLINE cvec #-}

-- | Convert CPS-vector to heterogeneous vector
vector :: (HVector v, Elems v ~ xs) => ContVec xs -> v
vector :: ContVec xs -> v
vector (ContVecF forall r. TFun Identity xs r -> r
cont) = TFun Identity xs v -> v
forall r. TFun Identity xs r -> r
cont TFun Identity xs v
forall v. HVector v => Fun (Elems v) v
construct
{-# INLINE vector #-}

cvecF :: HVectorF v => v f -> ContVecF (ElemsF v) f
cvecF :: v f -> ContVecF (ElemsF v) f
cvecF v f
v = (forall r. TFun f (ElemsF v) r -> r) -> ContVecF (ElemsF v) f
forall α (xs :: [α]) (f :: α -> *).
(forall r. TFun f xs r -> r) -> ContVecF xs f
ContVecF (v f -> TFun f (ElemsF v) r -> r
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF v f
v)
{-# INLINE cvecF #-}

vectorF :: HVectorF v => ContVecF (ElemsF v) f -> v f
vectorF :: ContVecF (ElemsF v) f -> v f
vectorF (ContVecF forall r. TFun f (ElemsF v) r -> r
cont) = TFun f (ElemsF v) (v f) -> v f
forall r. TFun f (ElemsF v) r -> r
cont TFun f (ElemsF v) (v f)
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
TFun f (ElemsF v) (v f)
constructF
{-# INLINE vectorF #-}



----------------------------------------------------------------
-- Position based functions
----------------------------------------------------------------

-- | Head of vector
head :: Arity xs => ContVec (x : xs) -> x
head :: ContVec (x : xs) -> x
head ContVec (x : xs)
v = ContVec (x : xs) -> Fun (Elems (ContVec (x : xs))) x -> x
forall v a. HVector v => v -> Fun (Elems v) a -> a
inspect ContVec (x : xs)
v ((x -> Fun xs x) -> Fun (x : xs) x
forall x (xs :: [*]) r. (x -> Fun xs r) -> Fun (x : xs) r
uncurryFun x -> Fun xs x
forall (f :: * -> *) a. Applicative f => a -> f a
pure)
{-# INLINE head #-}

-- | Tail of CPS-encoded vector
tail :: ContVec (x : xs) -> ContVec xs
tail :: ContVec (x : xs) -> ContVec xs
tail (ContVecF forall r. TFun Identity (x : xs) r -> r
cont) = (forall r. TFun Identity xs r -> r) -> ContVec xs
forall α (xs :: [α]) (f :: α -> *).
(forall r. TFun f xs r -> r) -> ContVecF xs f
ContVecF ((forall r. TFun Identity xs r -> r) -> ContVec xs)
-> (forall r. TFun Identity xs r -> r) -> ContVec xs
forall a b. (a -> b) -> a -> b
$ TFun Identity (x : xs) r -> r
forall r. TFun Identity (x : xs) r -> r
cont (TFun Identity (x : xs) r -> r)
-> (Fun xs r -> TFun Identity (x : xs) r) -> Fun xs r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun xs r -> TFun Identity (x : xs) r
forall (xs :: [*]) r x. Fun xs r -> Fun (x : xs) r
constFun
{-# INLINE tail #-}

-- | Concatenate two vectors
concat :: Arity xs => ContVec xs -> ContVec ys -> ContVec (xs ++ ys)
concat :: ContVec xs -> ContVec ys -> ContVec (xs ++ ys)
concat (ContVecF forall r. TFun Identity xs r -> r
contX) (ContVecF forall r. TFun Identity ys r -> r
contY) = (forall r. TFun Identity (xs ++ ys) r -> r) -> ContVec (xs ++ ys)
forall α (xs :: [α]) (f :: α -> *).
(forall r. TFun f xs r -> r) -> ContVecF xs f
ContVecF ((forall r. TFun Identity (xs ++ ys) r -> r) -> ContVec (xs ++ ys))
-> (forall r. TFun Identity (xs ++ ys) r -> r)
-> ContVec (xs ++ ys)
forall a b. (a -> b) -> a -> b
$ TFun Identity ys r -> r
forall r. TFun Identity ys r -> r
contY (TFun Identity ys r -> r)
-> (TFun Identity (xs ++ ys) r -> TFun Identity ys r)
-> TFun Identity (xs ++ ys) r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TFun Identity xs (TFun Identity ys r) -> TFun Identity ys r
forall r. TFun Identity xs r -> r
contX (TFun Identity xs (TFun Identity ys r) -> TFun Identity ys r)
-> (TFun Identity (xs ++ ys) r
    -> TFun Identity xs (TFun Identity ys r))
-> TFun Identity (xs ++ ys) r
-> TFun Identity ys r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TFun Identity (xs ++ ys) r -> TFun Identity xs (TFun Identity ys r)
forall (xs :: [*]) (ys :: [*]) r.
Arity xs =>
Fun (xs ++ ys) r -> Fun xs (Fun ys r)
curryMany
{-# INLINE concat #-}

-- | Get value at @n@th position.
index :: Index n xs => ContVec xs -> proxy n -> ValueAt n xs
index :: ContVec xs -> proxy n -> ValueAt n xs
index (ContVecF forall r. TFun Identity xs r -> r
cont) = TFun Identity xs (ValueAt n xs) -> ValueAt n xs
forall r. TFun Identity xs r -> r
cont (TFun Identity xs (ValueAt n xs) -> ValueAt n xs)
-> (proxy n -> TFun Identity xs (ValueAt n xs))
-> proxy n
-> ValueAt n xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> TFun Identity xs (ValueAt n xs)
forall (n :: PeanoNum) (xs :: [*]) (proxy :: PeanoNum -> *).
Index n xs =>
proxy n -> Fun xs (ValueAt n xs)
getF
{-# INLINE index #-}

-- | Set value on nth position.
set :: Index n xs => proxy n -> ValueAt n xs -> ContVec xs -> ContVec xs
set :: proxy n -> ValueAt n xs -> ContVec xs -> ContVec xs
set proxy n
n ValueAt n xs
x (ContVecF forall r. TFun Identity xs r -> r
cont) = (forall r. TFun Identity xs r -> r) -> ContVec xs
forall α (xs :: [α]) (f :: α -> *).
(forall r. TFun f xs r -> r) -> ContVecF xs f
ContVecF ((forall r. TFun Identity xs r -> r) -> ContVec xs)
-> (forall r. TFun Identity xs r -> r) -> ContVec xs
forall a b. (a -> b) -> a -> b
$ TFun Identity xs r -> r
forall r. TFun Identity xs r -> r
cont (TFun Identity xs r -> r)
-> (TFun Identity xs r -> TFun Identity xs r)
-> TFun Identity xs r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> ValueAt n xs -> TFun Identity xs r -> TFun Identity xs r
forall (n :: PeanoNum) (xs :: [*]) (proxy :: PeanoNum -> *) r.
Index n xs =>
proxy n -> ValueAt n xs -> Fun xs r -> Fun xs r
putF proxy n
n ValueAt n xs
x
{-# INLINE set #-}

-- | Lookup value by its type
tyLookup :: TyLookup a xs => ContVec xs -> a
tyLookup :: ContVec xs -> a
tyLookup (ContVecF forall r. TFun Identity xs r -> r
cont) = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ TFun Identity xs (Identity a) -> Identity a
forall r. TFun Identity xs r -> r
cont TFun Identity xs (Identity a)
forall α (x :: α) (xs :: [α]) (f :: α -> *).
TyLookup x xs =>
TFun f xs (f x)
lookupTFun
{-# INLINE tyLookup #-}

-- | Lookup value by its type
tyLookupF :: TyLookup a xs => ContVecF xs f -> f a
tyLookupF :: ContVecF xs f -> f a
tyLookupF (ContVecF forall r. TFun f xs r -> r
cont) = TFun f xs (f a) -> f a
forall r. TFun f xs r -> r
cont TFun f xs (f a)
forall α (x :: α) (xs :: [α]) (f :: α -> *).
TyLookup x xs =>
TFun f xs (f x)
lookupTFun
{-# INLINE tyLookupF #-}


----------------------------------------------------------------
-- Monadic/applicative API
----------------------------------------------------------------

-- | Apply transformation to every element of the tuple.
map :: (ArityC c xs)
    => Proxy c
    -> (forall a. c a => f a -> g a)
    -> ContVecF xs f
    -> ContVecF xs g
map :: Proxy c
-> (forall (a :: α). c a => f a -> g a)
-> ContVecF xs f
-> ContVecF xs g
map Proxy c
cls forall (a :: α). c a => f a -> g a
f (ContVecF forall r. TFun f xs r -> r
cont) = (forall r. TFun g xs r -> r) -> ContVecF xs g
forall α (xs :: [α]) (f :: α -> *).
(forall r. TFun f xs r -> r) -> ContVecF xs f
ContVecF ((forall r. TFun g xs r -> r) -> ContVecF xs g)
-> (forall r. TFun g xs r -> r) -> ContVecF xs g
forall a b. (a -> b) -> a -> b
$ TFun f xs r -> r
forall r. TFun f xs r -> r
cont (TFun f xs r -> r)
-> (TFun g xs r -> TFun f xs r) -> TFun g xs r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy c
-> (forall (a :: α). c a => f a -> g a)
-> TFun g xs r
-> TFun f xs r
forall α (c :: α -> Constraint) (f :: α -> *) (g :: α -> *) r
       (xs :: [α]).
ArityC c xs =>
Proxy c
-> (forall (a :: α). c a => f a -> g a)
-> TFun g xs r
-> TFun f xs r
mapF Proxy c
cls forall (a :: α). c a => f a -> g a
f
{-# INLINE map #-}

mapF :: forall c f g r xs. (ArityC c xs)
     => Proxy c
     -> (forall a. c a => f a -> g a)
     -> TFun g xs r
     -> TFun f xs r
mapF :: Proxy c
-> (forall (a :: α). c a => f a -> g a)
-> TFun g xs r
-> TFun f xs r
mapF Proxy c
cls forall (a :: α). c a => f a -> g a
g (TFun Fn g xs r
f0) = Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    TF_map r g (a : as) -> f a -> TF_map r g as)
-> (TF_map r g '[] -> r)
-> TF_map r g xs
-> TFun f xs r
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *) b.
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> f a -> t as)
-> (t '[] -> b)
-> t xs
-> TFun f xs b
accumC Proxy c
cls
  (\(TF_map f) f a
a -> Fn g as r -> TF_map r g as
forall α r (g :: α -> *) (xs :: [α]). Fn g xs r -> TF_map r g xs
TF_map (Fn g as r -> TF_map r g as) -> Fn g as r -> TF_map r g as
forall a b. (a -> b) -> a -> b
$ Fn g (a : as) r
g a -> Fn g as r
f (f a -> g a
forall (a :: α). c a => f a -> g a
g f a
a))
  (\(TF_map Fn g '[] r
r)   -> r
Fn g '[] r
r)
  (Fn g xs r -> TF_map r g xs
forall α r (g :: α -> *) (xs :: [α]). Fn g xs r -> TF_map r g xs
TF_map Fn g xs r
f0 :: TF_map r g xs)

-- | Apply natural transformation to every element of the tuple.
mapNat :: (Arity xs)
       => (forall a. f a -> g a)
       -> ContVecF xs f
       -> ContVecF xs g
mapNat :: (forall (a :: α). f a -> g a) -> ContVecF xs f -> ContVecF xs g
mapNat forall (a :: α). f a -> g a
f (ContVecF forall r. TFun f xs r -> r
cont) = (forall r. TFun g xs r -> r) -> ContVecF xs g
forall α (xs :: [α]) (f :: α -> *).
(forall r. TFun f xs r -> r) -> ContVecF xs f
ContVecF ((forall r. TFun g xs r -> r) -> ContVecF xs g)
-> (forall r. TFun g xs r -> r) -> ContVecF xs g
forall a b. (a -> b) -> a -> b
$ TFun f xs r -> r
forall r. TFun f xs r -> r
cont (TFun f xs r -> r)
-> (TFun g xs r -> TFun f xs r) -> TFun g xs r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: α). f a -> g a) -> TFun g xs r -> TFun f xs r
forall α (xs :: [α]) (f :: α -> *) (g :: α -> *) r.
Arity xs =>
(forall (a :: α). f a -> g a) -> TFun g xs r -> TFun f xs r
mapFF forall (a :: α). f a -> g a
f
{-# INLINE mapNat #-}

mapFF :: (Arity xs)
      => (forall a. f a -> g a) -> TFun g xs r -> TFun f xs r
{-# INLINE mapFF #-}
mapFF :: (forall (a :: α). f a -> g a) -> TFun g xs r -> TFun f xs r
mapFF forall (a :: α). f a -> g a
g (TFun Fn g xs r
f0) = (forall (a :: α) (as :: [α]).
 TF_map r g (a : as) -> f a -> TF_map r g as)
-> (TF_map r g '[] -> r) -> TF_map r g xs -> TFun f xs r
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *) b.
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> f a -> t as)
-> (t '[] -> b) -> t xs -> TFun f xs b
accum
  (\(TF_map f) f a
a -> Fn g as r -> TF_map r g as
forall α r (g :: α -> *) (xs :: [α]). Fn g xs r -> TF_map r g xs
TF_map (Fn g as r -> TF_map r g as) -> Fn g as r -> TF_map r g as
forall a b. (a -> b) -> a -> b
$ Fn g (a : as) r
g a -> Fn g as r
f (f a -> g a
forall (a :: α). f a -> g a
g f a
a))
  (\(TF_map Fn g '[] r
r)   -> r
Fn g '[] r
r)
  (Fn g xs r -> TF_map r g xs
forall α r (g :: α -> *) (xs :: [α]). Fn g xs r -> TF_map r g xs
TF_map Fn g xs r
f0)

newtype TF_map r g xs = TF_map (Fn g xs r)


-- | Apply sequence to outer level of parametrized tuple elements.
sequenceF :: (Arity xs, Applicative f)
          => ContVecF xs (f `Compose` g) -> f (ContVecF xs g)
sequenceF :: ContVecF xs (Compose f g) -> f (ContVecF xs g)
sequenceF (ContVecF forall r. TFun (Compose f g) xs r -> r
cont)
  = TFun (Compose f g) xs (f (ContVecF xs g)) -> f (ContVecF xs g)
forall r. TFun (Compose f g) xs r -> r
cont (TFun (Compose f g) xs (f (ContVecF xs g)) -> f (ContVecF xs g))
-> TFun (Compose f g) xs (f (ContVecF xs g)) -> f (ContVecF xs g)
forall a b. (a -> b) -> a -> b
$ TFun g xs (ContVecF xs g)
-> TFun (Compose f g) xs (f (ContVecF xs g))
forall α (f :: * -> *) (xs :: [α]) (g :: α -> *) r.
(Applicative f, Arity xs) =>
TFun g xs r -> TFun (Compose f g) xs (f r)
sequenceF_F TFun g xs (ContVecF xs g)
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
TFun f (ElemsF v) (v f)
constructF
{-# INLINE sequenceF #-}

sequenceF_F :: (Applicative f, Arity xs)
            => TFun g xs r -> TFun (f `Compose` g) xs (f r)
{-# INLINE sequenceF_F #-}
sequenceF_F :: TFun g xs r -> TFun (Compose f g) xs (f r)
sequenceF_F (TFun Fn g xs r
f) =
  (forall (a :: α) (as :: [α]).
 T_seq2 f g r (a : as) -> Compose f g a -> T_seq2 f g r as)
-> (T_seq2 f g r '[] -> f r)
-> T_seq2 f g r xs
-> TFun (Compose f g) xs (f r)
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *) b.
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> f a -> t as)
-> (t '[] -> b) -> t xs -> TFun f xs b
accum (\(T_seq2 m) (Compose a) -> f (Fn g as r) -> T_seq2 f g r as
forall α (f :: * -> *) (g :: α -> *) r (xs :: [α]).
f (Fn g xs r) -> T_seq2 f g r xs
T_seq2 (f (Fn g as r) -> T_seq2 f g r as)
-> f (Fn g as r) -> T_seq2 f g r as
forall a b. (a -> b) -> a -> b
$ f (Fn g (a : as) r)
f (g a -> Fn g as r)
m f (g a -> Fn g as r) -> f (g a) -> f (Fn g as r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (g a)
a)
        (\(T_seq2 f (Fn g '[] r)
m)             -> f r
f (Fn g '[] r)
m)
        (f (Fn g xs r) -> T_seq2 f g r xs
forall α (f :: * -> *) (g :: α -> *) r (xs :: [α]).
f (Fn g xs r) -> T_seq2 f g r xs
T_seq2 (Fn g xs r -> f (Fn g xs r)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Fn g xs r
f))

newtype T_seq2 f g r xs = T_seq2 (f (Fn g xs r))



distributeF :: forall f g xs. (Arity xs, Functor f)
            => f (ContVecF xs g)
            -> ContVecF xs (f `Compose` g)
{-# INLINE distributeF #-}
distributeF :: f (ContVecF xs g) -> ContVecF xs (Compose f g)
distributeF f (ContVecF xs g)
f0
  = (forall (a :: k1) (as :: [k1]).
 T_distributeF f g (a : as)
 -> (Compose f g a, T_distributeF f g as))
-> T_distributeF f g xs -> ContVecF xs (Compose f g)
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *).
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> (f a, t as))
-> t xs -> ContVecF xs f
apply forall (a :: k1) (as :: [k1]).
T_distributeF f g (a : as) -> (Compose f g a, T_distributeF f g as)
step T_distributeF f g xs
start
  where
    step :: forall a as. T_distributeF f g (a : as) -> ((Compose f g) a, T_distributeF f g as)
    step :: T_distributeF f g (a : as) -> (Compose f g a, T_distributeF f g as)
step (T_distributeF f (VecListF (a : as) g)
v) = ( f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g a) -> Compose f g a) -> f (g a) -> Compose f g a
forall a b. (a -> b) -> a -> b
$ (VecListF (a : as) g -> g a) -> f (VecListF (a : as) g) -> f (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(ConsF g x
x VecListF xs g
_) -> g a
g x
x) f (VecListF (a : as) g)
v
                             , f (VecListF as g) -> T_distributeF f g as
forall α (f :: * -> *) (g :: α -> *) (xs :: [α]).
f (VecListF xs g) -> T_distributeF f g xs
T_distributeF (f (VecListF as g) -> T_distributeF f g as)
-> f (VecListF as g) -> T_distributeF f g as
forall a b. (a -> b) -> a -> b
$ (VecListF (a : as) g -> VecListF as g)
-> f (VecListF (a : as) g) -> f (VecListF as g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(ConsF g x
_ VecListF xs g
x) -> VecListF as g
VecListF xs g
x) f (VecListF (a : as) g)
v
                             )
    start :: T_distributeF f g xs
    start :: T_distributeF f g xs
start = f (VecListF xs g) -> T_distributeF f g xs
forall α (f :: * -> *) (g :: α -> *) (xs :: [α]).
f (VecListF xs g) -> T_distributeF f g xs
T_distributeF (f (VecListF xs g) -> T_distributeF f g xs)
-> f (VecListF xs g) -> T_distributeF f g xs
forall a b. (a -> b) -> a -> b
$ (ContVecF xs g -> VecListF xs g)
-> f (ContVecF xs g) -> f (VecListF xs g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ContVecF xs g -> VecListF xs g
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
ContVecF (ElemsF v) f -> v f
vectorF f (ContVecF xs g)
f0

newtype T_distributeF f g xs = T_distributeF (f (VecListF xs g))



----------------------------------------------------------------
-- Other vectors
----------------------------------------------------------------

-- | List like heterogeneous vector.
data VecList :: [*] -> * where
  Nil  :: VecList '[]
  Cons :: x -> VecList xs -> VecList (x : xs)

instance Arity xs => HVector (VecList xs) where
  type Elems (VecList xs) = xs
  construct :: Fun (Elems (VecList xs)) (VecList xs)
construct = (forall a (as :: [*]).
 T_List xs (a : as) -> Identity a -> T_List xs as)
-> (T_List xs '[] -> VecList xs)
-> T_List xs xs
-> TFun Identity xs (VecList xs)
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *) b.
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> f a -> t as)
-> (t '[] -> b) -> t xs -> TFun f xs b
accum
    (\(T_List f) (Identity a) -> (VecList as -> VecList xs) -> T_List xs as
forall (all :: [*]) (xs :: [*]).
(VecList xs -> VecList all) -> T_List all xs
T_List (VecList (a : as) -> VecList xs
f (VecList (a : as) -> VecList xs)
-> (VecList as -> VecList (a : as)) -> VecList as -> VecList xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> VecList as -> VecList (a : as)
forall x (xs :: [*]). x -> VecList xs -> VecList (x : xs)
Cons a
a))
    (\(T_List VecList '[] -> VecList xs
f)              -> VecList '[] -> VecList xs
f VecList '[]
Nil)
    ((VecList xs -> VecList xs) -> T_List xs xs
forall (all :: [*]) (xs :: [*]).
(VecList xs -> VecList all) -> T_List all xs
T_List VecList xs -> VecList xs
forall a. a -> a
id)
  inspect :: VecList xs -> Fun (Elems (VecList xs)) a -> a
inspect VecList xs
f = ContVecF xs Identity -> forall r. TFun Identity xs r -> r
forall α (xs :: [α]) (f :: α -> *).
ContVecF xs f -> forall r. TFun f xs r -> r
runContVecF ((forall a (as :: [*]).
 VecList (a : as) -> (Identity a, VecList as))
-> VecList xs -> ContVecF xs Identity
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *).
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> (f a, t as))
-> t xs -> ContVecF xs f
apply forall a (as :: [*]). VecList (a : as) -> (Identity a, VecList as)
step VecList xs
f)
    where
      step :: VecList (a : as) -> (Identity a, VecList as)
      step :: VecList (a : as) -> (Identity a, VecList as)
step (Cons x
a VecList xs
xs) = (x -> Identity x
forall a. a -> Identity a
Identity x
a, VecList as
VecList xs
xs)
  {-# INLINE construct #-}
  {-# INLINE inspect   #-}

newtype T_List all xs = T_List (VecList xs -> VecList all)


-- | List-like vector
data VecListF (xs :: [α]) (f :: α -> *) where
  NilF  :: VecListF '[] f
  ConsF :: f x -> VecListF xs f -> VecListF (x : xs) f

instance Arity xs => HVectorF (VecListF xs) where
  type ElemsF (VecListF xs) = xs
  constructF :: TFun f (ElemsF (VecListF xs)) (VecListF xs f)
constructF   = TFun f (ElemsF (VecListF xs)) (VecListF xs f)
forall α (xs :: [α]) (f :: α -> *).
Arity xs =>
TFun f xs (VecListF xs f)
conVecF
  inspectF :: VecListF xs f -> TFun f (ElemsF (VecListF xs)) a -> a
inspectF   VecListF xs f
v = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) a -> a
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ((forall (a :: α) (as :: [α]).
 TF_insp f (a : as) -> (f a, TF_insp f as))
-> TF_insp f xs -> ContVecF xs f
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *).
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> (f a, t as))
-> t xs -> ContVecF xs f
apply forall (a :: α) (as :: [α]).
TF_insp f (a : as) -> (f a, TF_insp f as)
forall α (f :: α -> *) (a :: α) (as :: [α]).
TF_insp f (a : as) -> (f a, TF_insp f as)
step (VecListF xs f -> TF_insp f xs
forall α (f :: α -> *) (xs :: [α]). VecListF xs f -> TF_insp f xs
TF_insp VecListF xs f
v))
    where
      step :: TF_insp f (a : as) -> (f a, TF_insp f as)
      step :: TF_insp f (a : as) -> (f a, TF_insp f as)
step (TF_insp (ConsF f x
a VecListF xs f
xs)) = (f a
f x
a, VecListF xs f -> TF_insp f xs
forall α (f :: α -> *) (xs :: [α]). VecListF xs f -> TF_insp f xs
TF_insp VecListF xs f
xs)
  {-# INLINE constructF #-}
  {-# INLINE inspectF   #-}

conVecF :: (Arity xs) => TFun f xs (VecListF xs f)
{-# INLINE conVecF #-}
conVecF :: TFun f xs (VecListF xs f)
conVecF = (forall (a :: α) (as :: [α]).
 TF_List f xs (a : as) -> f a -> TF_List f xs as)
-> (TF_List f xs '[] -> VecListF xs f)
-> TF_List f xs xs
-> TFun f xs (VecListF xs f)
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *) b.
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> f a -> t as)
-> (t '[] -> b) -> t xs -> TFun f xs b
accum (\(TF_List f) f a
a -> (VecListF as f -> VecListF xs f) -> TF_List f xs as
forall α (f :: α -> *) (all :: [α]) (xs :: [α]).
(VecListF xs f -> VecListF all f) -> TF_List f all xs
TF_List (VecListF (a : as) f -> VecListF xs f
f (VecListF (a : as) f -> VecListF xs f)
-> (VecListF as f -> VecListF (a : as) f)
-> VecListF as f
-> VecListF xs f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> VecListF as f -> VecListF (a : as) f
forall α (f :: α -> *) (x :: α) (xs :: [α]).
f x -> VecListF xs f -> VecListF (x : xs) f
ConsF f a
a))
                (\(TF_List VecListF '[] f -> VecListF xs f
f)   -> VecListF '[] f -> VecListF xs f
f VecListF '[] f
forall α (f :: α -> *). VecListF '[] f
NilF)
                ((VecListF xs f -> VecListF xs f) -> TF_List f xs xs
forall α (f :: α -> *) (all :: [α]) (xs :: [α]).
(VecListF xs f -> VecListF all f) -> TF_List f all xs
TF_List VecListF xs f -> VecListF xs f
forall a. a -> a
id)

newtype TF_insp f     xs = TF_insp (VecListF xs f)
newtype TF_List f all xs = TF_List (VecListF xs f -> VecListF all f)



----------------------------------------------------------------
-- More combinators
----------------------------------------------------------------

replicateNatF :: Arity xs => (forall a. f a) -> ContVecF xs f
{-# INLINE replicateNatF #-}
replicateNatF :: (forall (a :: α). f a) -> ContVecF xs f
replicateNatF forall (a :: α). f a
f = (forall (a :: α) (as :: [α]). Proxy (a : as) -> (f a, Proxy as))
-> Proxy xs -> ContVecF xs f
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *).
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> (f a, t as))
-> t xs -> ContVecF xs f
apply (\Proxy (a : as)
Proxy -> (f a
forall (a :: α). f a
f, Proxy as
forall k (t :: k). Proxy t
Proxy)) (Proxy xs
forall k (t :: k). Proxy t
Proxy)

replicateF :: ArityC c xs => Proxy c -> (forall a. c a => f a) -> ContVecF xs f
{-# INLINE replicateF #-}
replicateF :: Proxy c -> (forall (a :: α). c a => f a) -> ContVecF xs f
replicateF Proxy c
cls forall (a :: α). c a => f a
f = Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    Proxy (a : as) -> (f a, Proxy as))
-> Proxy xs
-> ContVecF xs f
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *).
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> (f a, t as))
-> t xs
-> ContVecF xs f
applyC Proxy c
cls (\Proxy (a : as)
Proxy -> (f a
forall (a :: α). c a => f a
f,Proxy as
forall k (t :: k). Proxy t
Proxy)) Proxy xs
forall k (t :: k). Proxy t
Proxy



----------------------------------------------------------------
-- Folds
----------------------------------------------------------------

-- | Monoidal fold over vector
foldMapNatF
  :: (Monoid m, Arity xs)
  => (forall a. f a -> m) -> ContVecF xs f -> m
{-# INLINE foldMapNatF #-}
foldMapNatF :: (forall (a :: α). f a -> m) -> ContVecF xs f -> m
foldMapNatF forall (a :: α). f a -> m
f ContVecF xs f
v
  = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) m -> m
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
v
  (TFun f (ElemsF (ContVecF xs)) m -> m)
-> TFun f (ElemsF (ContVecF xs)) m -> m
forall a b. (a -> b) -> a -> b
$ (forall (a :: α) (as :: [α]).
 Const m (a : as) -> f a -> Const m as)
-> (Const m '[] -> m) -> Const m xs -> TFun f xs m
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *) b.
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> f a -> t as)
-> (t '[] -> b) -> t xs -> TFun f xs b
accum (\(Const m) f a
a -> m -> Const m as
forall k a (b :: k). a -> Const a b
Const (m
m m -> m -> m
forall a. Semigroup a => a -> a -> a
<> f a -> m
forall (a :: α). f a -> m
f f a
a))
          (\(Const m
m)   -> m
m)
          (m -> Const m xs
forall k a (b :: k). a -> Const a b
Const m
forall a. Monoid a => a
mempty)

-- | Monoidal fold over vector
foldMapF
  :: (Monoid m, ArityC c xs)
  => Proxy c -> (forall a. c a => f a -> m) -> ContVecF xs f -> m
{-# INLINE foldMapF #-}
foldMapF :: Proxy c -> (forall (a :: α). c a => f a -> m) -> ContVecF xs f -> m
foldMapF Proxy c
cls forall (a :: α). c a => f a -> m
f ContVecF xs f
v
  = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) m -> m
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
v
  (TFun f (ElemsF (ContVecF xs)) m -> m)
-> TFun f (ElemsF (ContVecF xs)) m -> m
forall a b. (a -> b) -> a -> b
$ Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    Const m (a : as) -> f a -> Const m as)
-> (Const m '[] -> m)
-> Const m xs
-> TFun f xs m
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *) b.
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> f a -> t as)
-> (t '[] -> b)
-> t xs
-> TFun f xs b
accumC Proxy c
cls (\(Const m) f a
a -> m -> Const m as
forall k a (b :: k). a -> Const a b
Const (m
m m -> m -> m
forall a. Semigroup a => a -> a -> a
<> f a -> m
forall (a :: α). c a => f a -> m
f f a
a))
               (\(Const m
m)   -> m
m)
               (m -> Const m xs
forall k a (b :: k). a -> Const a b
Const m
forall a. Monoid a => a
mempty)

-- | Right fold over vector
foldrF :: (ArityC c xs)
       => Proxy c -> (forall a. c a => f a -> b -> b) -> b -> ContVecF xs f -> b
{-# INLINE foldrF #-}
foldrF :: Proxy c
-> (forall (a :: α). c a => f a -> b -> b)
-> b
-> ContVecF xs f
-> b
foldrF Proxy c
cls forall (a :: α). c a => f a -> b -> b
f b
b0 ContVecF xs f
v
  = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) b -> b
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
v
  (TFun f (ElemsF (ContVecF xs)) b -> b)
-> TFun f (ElemsF (ContVecF xs)) b -> b
forall a b. (a -> b) -> a -> b
$ Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    Const (b -> b) (a : as) -> f a -> Const (b -> b) as)
-> (Const (b -> b) '[] -> b)
-> Const (b -> b) xs
-> TFun f xs b
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *) b.
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> f a -> t as)
-> (t '[] -> b)
-> t xs
-> TFun f xs b
accumC Proxy c
cls (\(Const b) f a
a -> (b -> b) -> Const (b -> b) as
forall k a (b :: k). a -> Const a b
Const (b -> b
b (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> b -> b
forall (a :: α). c a => f a -> b -> b
f f a
a))
               (\(Const b -> b
b)   -> b -> b
b b
b0)
               ((b -> b) -> Const (b -> b) xs
forall k a (b :: k). a -> Const a b
Const b -> b
forall a. a -> a
id)

-- | Left fold over vector
foldlF :: (ArityC c xs)
       => Proxy c -> (forall a. c a => b -> f a -> b) -> b -> ContVecF xs f -> b
{-# INLINE foldlF #-}
foldlF :: Proxy c
-> (forall (a :: α). c a => b -> f a -> b)
-> b
-> ContVecF xs f
-> b
foldlF Proxy c
cls forall (a :: α). c a => b -> f a -> b
f b
b0 ContVecF xs f
v
  = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) b -> b
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
v
  (TFun f (ElemsF (ContVecF xs)) b -> b)
-> TFun f (ElemsF (ContVecF xs)) b -> b
forall a b. (a -> b) -> a -> b
$ Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    Const b (a : as) -> f a -> Const b as)
-> (Const b '[] -> b)
-> Const b xs
-> TFun f xs b
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *) b.
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> f a -> t as)
-> (t '[] -> b)
-> t xs
-> TFun f xs b
accumC Proxy c
cls (\(Const b) f a
a -> b -> Const b as
forall k a (b :: k). a -> Const a b
Const (b -> f a -> b
forall (a :: α). c a => b -> f a -> b
f b
b f a
a))
               (\(Const b
b)   -> b
b)
               (b -> Const b xs
forall k a (b :: k). a -> Const a b
Const b
b0)

-- | Right fold over vector
foldrNatF :: (Arity xs)
       => (forall a. f a -> b -> b) -> b -> ContVecF xs f -> b
{-# INLINE foldrNatF #-}
foldrNatF :: (forall (a :: α). f a -> b -> b) -> b -> ContVecF xs f -> b
foldrNatF forall (a :: α). f a -> b -> b
f b
b0 ContVecF xs f
v
  = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) b -> b
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
v
  (TFun f (ElemsF (ContVecF xs)) b -> b)
-> TFun f (ElemsF (ContVecF xs)) b -> b
forall a b. (a -> b) -> a -> b
$ (forall (a :: α) (as :: [α]).
 Const (b -> b) (a : as) -> f a -> Const (b -> b) as)
-> (Const (b -> b) '[] -> b) -> Const (b -> b) xs -> TFun f xs b
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *) b.
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> f a -> t as)
-> (t '[] -> b) -> t xs -> TFun f xs b
accum (\(Const b) f a
a -> (b -> b) -> Const (b -> b) as
forall k a (b :: k). a -> Const a b
Const (b -> b
b (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> b -> b
forall (a :: α). f a -> b -> b
f f a
a))
          (\(Const b -> b
b)   -> b -> b
b b
b0)
          ((b -> b) -> Const (b -> b) xs
forall k a (b :: k). a -> Const a b
Const b -> b
forall a. a -> a
id)

-- | Left fold over vector
foldlNatF :: (Arity xs)
          => (forall a. b -> f a -> b) -> b -> ContVecF xs f -> b
{-# INLINE foldlNatF #-}
foldlNatF :: (forall (a :: α). b -> f a -> b) -> b -> ContVecF xs f -> b
foldlNatF forall (a :: α). b -> f a -> b
f b
b0 ContVecF xs f
v
  = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) b -> b
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
v
  (TFun f (ElemsF (ContVecF xs)) b -> b)
-> TFun f (ElemsF (ContVecF xs)) b -> b
forall a b. (a -> b) -> a -> b
$ (forall (a :: α) (as :: [α]).
 Const b (a : as) -> f a -> Const b as)
-> (Const b '[] -> b) -> Const b xs -> TFun f xs b
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *) b.
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> f a -> t as)
-> (t '[] -> b) -> t xs -> TFun f xs b
accum (\(Const b) f a
a -> b -> Const b as
forall k a (b :: k). a -> Const a b
Const (b -> f a -> b
forall (a :: α). b -> f a -> b
f b
b f a
a))
          (\(Const b
b)   -> b
b)
          (b -> Const b xs
forall k a (b :: k). a -> Const a b
Const b
b0)

-- | Convert heterogeneous vector to homogeneous
monomorphizeF :: forall c xs a f n. ( ArityC c xs
                                    , F.Peano n ~ Len xs
                                    )
              => Proxy c -> (forall x. c x => f x -> a)
              -> ContVecF xs f -> F.ContVec n a
{-# INLINE monomorphizeF #-}
monomorphizeF :: Proxy c
-> (forall (x :: α). c x => f x -> a)
-> ContVecF xs f
-> ContVec n a
monomorphizeF Proxy c
cls forall (x :: α). c x => f x -> a
f ContVecF xs f
v
  = ContVecF xs f
-> TFun f (ElemsF (ContVecF xs)) (ContVec n a) -> ContVec n a
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
v
  (TFun f (ElemsF (ContVecF xs)) (ContVec n a) -> ContVec n a)
-> TFun f (ElemsF (ContVecF xs)) (ContVec n a) -> ContVec n a
forall a b. (a -> b) -> a -> b
$ Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    T_mono a xs (a : as) -> f a -> T_mono a xs as)
-> (T_mono a xs '[] -> ContVec n a)
-> T_mono a xs xs
-> TFun f xs (ContVec n a)
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *) b.
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> f a -> t as)
-> (t '[] -> b)
-> t xs
-> TFun f xs b
accumC Proxy c
cls (\(T_mono cont) f a
a -> (CVecPeano (Len as) a -> CVecPeano (Len xs) a) -> T_mono a xs as
forall α α a (all :: [α]) (xs :: [α]).
(CVecPeano (Len xs) a -> CVecPeano (Len all) a) -> T_mono a all xs
T_mono (CVecPeano ('S (Len as)) a -> CVecPeano (Len xs) a
CVecPeano (Len (a : as)) a -> CVecPeano (Len xs) a
cont (CVecPeano ('S (Len as)) a -> CVecPeano (Len xs) a)
-> (CVecPeano (Len as) a -> CVecPeano ('S (Len as)) a)
-> CVecPeano (Len as) a
-> CVecPeano (Len xs) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> CVecPeano (Len as) a -> CVecPeano ('S (Len as)) a
forall a (n :: PeanoNum). a -> CVecPeano n a -> CVecPeano ('S n) a
F.consPeano (f a -> a
forall (x :: α). c x => f x -> a
f f a
a)))
               (\(T_mono CVecPeano (Len '[]) a -> CVecPeano (Len xs) a
cont)   -> CVecPeano (Peano n) a -> ContVec n a
forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
fini (CVecPeano (Len '[]) a -> CVecPeano (Len xs) a
cont ((forall r. Fun 'Z a r -> r) -> CVecPeano 'Z a
forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
F.CVecPeano forall r. Fun 'Z a r -> r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
F.unFun)))
               ((CVecPeano (Len xs) a -> CVecPeano (Len xs) a) -> T_mono a xs xs
forall α α a (all :: [α]) (xs :: [α]).
(CVecPeano (Len xs) a -> CVecPeano (Len all) a) -> T_mono a all xs
T_mono CVecPeano (Len xs) a -> CVecPeano (Len xs) a
forall a. a -> a
id :: T_mono a xs xs)
  where
    fini :: CVecPeano (Peano n) a -> ContVec n a
fini (F.CVecPeano forall r. Fun (Peano n) a r -> r
cont) = (forall r. Fun (Peano n) a r -> r) -> ContVec n a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
F.ContVec forall r. Fun (Peano n) a r -> r
cont

data T_mono a all xs = T_mono (F.CVecPeano (Len xs) a -> F.CVecPeano (Len all) a)


-- | Unfold vector.
unfoldrF :: (ArityC c xs)
         => Proxy c
         -> (forall a. c a => b -> (f a, b))
         -> b
         -> ContVecF xs f
{-# INLINE unfoldrF #-}
unfoldrF :: Proxy c
-> (forall (a :: α). c a => b -> (f a, b)) -> b -> ContVecF xs f
unfoldrF Proxy c
cls forall (a :: α). c a => b -> (f a, b)
f b
b0 = Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    Const b (a : as) -> (f a, Const b as))
-> Const b xs
-> ContVecF xs f
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *).
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> (f a, t as))
-> t xs
-> ContVecF xs f
applyC Proxy c
cls
  (\(Const b) -> let (f a
a,b
b') = b -> (f a, b)
forall (a :: α). c a => b -> (f a, b)
f b
b in (f a
a, b -> Const b as
forall k a (b :: k). a -> Const a b
Const b
b'))
  (b -> Const b xs
forall k a (b :: k). a -> Const a b
Const b
b0)



----------------------------------------------------------------
-- Zip variants
----------------------------------------------------------------

-- | Zip two heterogeneous vectors
zipWithF :: (ArityC c xs)
         => Proxy c
         -> (forall a. c a => f a -> g a -> h a)
         -> ContVecF xs f
         -> ContVecF xs g
         -> ContVecF xs h
{-# INLINE zipWithF #-}
zipWithF :: Proxy c
-> (forall (a :: α). c a => f a -> g a -> h a)
-> ContVecF xs f
-> ContVecF xs g
-> ContVecF xs h
zipWithF Proxy c
cls forall (a :: α). c a => f a -> g a -> h a
f ContVecF xs f
cvecA ContVecF xs g
cvecB = Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    T_zipWithF f g (a : as) -> (h a, T_zipWithF f g as))
-> T_zipWithF f g xs
-> ContVecF xs h
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *).
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> (f a, t as))
-> t xs
-> ContVecF xs f
applyC Proxy c
cls
  (\(T_zipWithF (ConsF a va) (ConsF b vb)) ->
      (f x -> g x -> h x
forall (a :: α). c a => f a -> g a -> h a
f f x
a g x
g x
b, VecListF xs f -> VecListF xs g -> T_zipWithF f g xs
forall α (f :: α -> *) (g :: α -> *) (xs :: [α]).
VecListF xs f -> VecListF xs g -> T_zipWithF f g xs
T_zipWithF VecListF xs f
va VecListF xs g
VecListF xs g
vb))
  (VecListF xs f -> VecListF xs g -> T_zipWithF f g xs
forall α (f :: α -> *) (g :: α -> *) (xs :: [α]).
VecListF xs f -> VecListF xs g -> T_zipWithF f g xs
T_zipWithF (ContVecF (ElemsF (VecListF xs)) f -> VecListF xs f
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
ContVecF (ElemsF v) f -> v f
vectorF ContVecF xs f
ContVecF (ElemsF (VecListF xs)) f
cvecA) (ContVecF (ElemsF (VecListF xs)) g -> VecListF xs g
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
ContVecF (ElemsF v) f -> v f
vectorF ContVecF xs g
ContVecF (ElemsF (VecListF xs)) g
cvecB))

data T_zipWithF f g xs = T_zipWithF (VecListF xs f) (VecListF xs g)


-- | Zip vector and fold result using monoid
zipFoldF :: forall xs c m f. (ArityC c xs, Monoid m)
         => Proxy c
         -> (forall a. c a => f a -> f a -> m)
         -> ContVecF xs f
         -> ContVecF xs f
         -> m
{-# INLINE zipFoldF #-}
zipFoldF :: Proxy c
-> (forall (a :: α). c a => f a -> f a -> m)
-> ContVecF xs f
-> ContVecF xs f
-> m
zipFoldF Proxy c
cls forall (a :: α). c a => f a -> f a -> m
f ContVecF xs f
cvecA ContVecF xs f
cvecB
  = ContVecF xs f -> TFun f (ElemsF (ContVecF xs)) m -> m
forall α (v :: (α -> *) -> *) (f :: α -> *) a.
HVectorF v =>
v f -> TFun f (ElemsF v) a -> a
inspectF ContVecF xs f
cvecB TFun f xs m
TFun f (ElemsF (ContVecF xs)) m
zipF
  where
    zipF :: TFun f xs m
    zipF :: TFun f xs m
zipF = Proxy c
-> (forall (a :: α) (as :: [α]).
    c a =>
    T_zipFoldF m f (a : as) -> f a -> T_zipFoldF m f as)
-> (T_zipFoldF m f '[] -> m)
-> T_zipFoldF m f xs
-> TFun f xs m
forall α (c :: α -> Constraint) (xs :: [α])
       (proxy :: (α -> Constraint) -> *) (t :: [α] -> *) (f :: α -> *) b.
ArityC c xs =>
proxy c
-> (forall (a :: α) (as :: [α]). c a => t (a : as) -> f a -> t as)
-> (t '[] -> b)
-> t xs
-> TFun f xs b
accumC Proxy c
cls
      (\(T_zipFoldF (ConsF a va) m) f a
b -> VecListF xs f -> m -> T_zipFoldF m f xs
forall α m (f :: α -> *) (xs :: [α]).
VecListF xs f -> m -> T_zipFoldF m f xs
T_zipFoldF VecListF xs f
va (m
m m -> m -> m
forall a. Semigroup a => a -> a -> a
<> f x -> f x -> m
forall (a :: α). c a => f a -> f a -> m
f f x
a f a
f x
b))
      (\(T_zipFoldF VecListF '[] f
_            m
m)   -> m
m)
      (VecListF xs f -> m -> T_zipFoldF m f xs
forall α m (f :: α -> *) (xs :: [α]).
VecListF xs f -> m -> T_zipFoldF m f xs
T_zipFoldF (ContVecF (ElemsF (VecListF xs)) f -> VecListF xs f
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
ContVecF (ElemsF v) f -> v f
vectorF ContVecF xs f
ContVecF (ElemsF (VecListF xs)) f
cvecA) m
forall a. Monoid a => a
mempty :: T_zipFoldF m f xs)

data T_zipFoldF m f xs = T_zipFoldF (VecListF xs f) m


-- | Zip two heterogeneous vectors
zipWithNatF :: (Arity xs)
            => (forall a. f a -> g a -> h a)
            -> ContVecF xs f
            -> ContVecF xs g
            -> ContVecF xs h
{-# INLINE zipWithNatF #-}
zipWithNatF :: (forall (a :: α). f a -> g a -> h a)
-> ContVecF xs f -> ContVecF xs g -> ContVecF xs h
zipWithNatF forall (a :: α). f a -> g a -> h a
f ContVecF xs f
cvecA ContVecF xs g
cvecB
  = (forall (a :: α) (as :: [α]).
 T_zipNatF f g (a : as) -> (h a, T_zipNatF f g as))
-> T_zipNatF f g xs -> ContVecF xs h
forall α (xs :: [α]) (t :: [α] -> *) (f :: α -> *).
Arity xs =>
(forall (a :: α) (as :: [α]). t (a : as) -> (f a, t as))
-> t xs -> ContVecF xs f
apply (\(T_zipNatF (ConsF a va) (ConsF b vb)) -> (f a -> g a -> h a
forall (a :: α). f a -> g a -> h a
f f a
f x
a g a
g x
b, VecListF xs f -> VecListF xs g -> T_zipNatF f g xs
forall α (f :: α -> *) (g :: α -> *) (xs :: [α]).
VecListF xs f -> VecListF xs g -> T_zipNatF f g xs
T_zipNatF VecListF xs f
va VecListF xs g
VecListF xs g
vb))
          (VecListF xs f -> VecListF xs g -> T_zipNatF f g xs
forall α (f :: α -> *) (g :: α -> *) (xs :: [α]).
VecListF xs f -> VecListF xs g -> T_zipNatF f g xs
T_zipNatF (ContVecF (ElemsF (VecListF xs)) f -> VecListF xs f
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
ContVecF (ElemsF v) f -> v f
vectorF ContVecF xs f
ContVecF (ElemsF (VecListF xs)) f
cvecA) (ContVecF (ElemsF (VecListF xs)) g -> VecListF xs g
forall α (v :: (α -> *) -> *) (f :: α -> *).
HVectorF v =>
ContVecF (ElemsF v) f -> v f
vectorF ContVecF xs g
ContVecF (ElemsF (VecListF xs)) g
cvecB))

data T_zipNatF f g xs = T_zipNatF (VecListF xs f) (VecListF xs g)