{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vector.HFixed.Cont (
Fn
, Fun
, TFun(..)
, Arity(..)
, HVector(..)
, tupleSize
, HVectorF(..)
, tupleSizeF
, ValueAt
, Index
, ContVec
, ContVecF(..)
, VecList(..)
, VecListF(..)
, cvec
, vector
, cvecF
, vectorF
, head
, tail
, cons
, consF
, concat
, index
, set
, tyLookup
, tyLookupF
, foldlF
, foldrF
, foldMapF
, foldlNatF
, foldrNatF
, foldMapNatF
, unfoldrF
, replicateF
, replicateNatF
, zipWithF
, zipWithNatF
, zipFoldF
, monomorphizeF
, 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
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 #-}
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 #-}
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 :: 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 #-}
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 #-}
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 :: 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 #-}
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 #-}
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 #-}
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)
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)
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))
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)
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)
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
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)
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)
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)
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)
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)
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)
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)
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)
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)
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
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)