{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vector.Fixed.Cont (
PeanoNum(..)
, Peano
, Add
, Fn
, Fun(..)
, Arity
, ArityPeano(..)
, arity
, apply
, applyM
, constFun
, curryFirst
, uncurryFirst
, curryLast
, curryMany
, apLast
, shuffleFun
, withFun
, Dim
, Vector(..)
, VectorN
, length
, ContVec(..)
, CVecPeano(..)
, consPeano
, toContVec
, runContVec
, cvec
, fromList
, fromList'
, fromListM
, toList
, replicate
, replicateM
, generate
, generateM
, unfoldr
, basis
, empty
, cons
, consV
, snoc
, concat
, mk1
, mk2
, mk3
, mk4
, mk5
, mk6
, mk7
, mk8
, map
, imap
, mapM
, imapM
, mapM_
, imapM_
, scanl
, scanl1
, sequence
, sequence_
, distribute
, collect
, tail
, reverse
, zipWith
, zipWith3
, izipWith
, izipWith3
, zipWithM
, zipWithM_
, izipWithM
, izipWithM_
, head
, index
, element
, vector
, foldl
, foldl1
, foldr
, ifoldl
, ifoldr
, foldM
, ifoldM
, sum
, minimum
, maximum
, and
, or
, all
, any
, find
, gfoldl
, gunfold
) where
import Control.Applicative ((<|>), Const(..))
import Data.Coerce
import Data.Complex (Complex(..))
import Data.Data (Data)
import Data.Functor.Identity (Identity(..))
import Data.Typeable (Proxy(..))
import qualified Data.Foldable as F
import qualified Data.Traversable as F
import Unsafe.Coerce (unsafeCoerce)
import GHC.TypeLits
import Prelude hiding ( replicate,map,zipWith,zipWith3,maximum,minimum,and,or,any,all
, foldl,foldr,foldl1,length,sum,reverse,scanl,scanl1
, head,tail,mapM,mapM_,sequence,sequence_,concat
)
data PeanoNum = Z
| S PeanoNum
type family Peano (n :: Nat) :: PeanoNum where
Peano 0 = 'Z
Peano n = 'S (Peano (n - 1))
type family Add (n :: PeanoNum) (m :: PeanoNum) :: PeanoNum where
Add 'Z n = n
Add ('S n) k = 'S (Add n k)
type family Fn (n :: PeanoNum) (a :: *) (b :: *) where
Fn 'Z a b = b
Fn ('S n) a b = a -> Fn n a b
newtype Fun n a b = Fun { Fun n a b -> Fn n a b
unFun :: Fn n a b }
instance ArityPeano n => Functor (Fun n a) where
fmap :: (a -> b) -> Fun n a a -> Fun n a b
fmap a -> b
f Fun n a a
fun
= (forall (k :: PeanoNum). T_Flip a a ('S k) -> a -> T_Flip a a k)
-> (T_Flip a a 'Z -> b) -> T_Flip a a n -> Fun n a b
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_Flip g) a
a -> Fun k a a -> T_Flip a a k
forall a b (n :: PeanoNum). Fun n a b -> T_Flip a b n
T_Flip (Fun ('S k) a a -> a -> Fun k a a
forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun ('S k) a a
g a
a))
(\(T_Flip Fun 'Z a a
x) -> a -> b
f (Fun 'Z a a -> Fn 'Z a a
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun Fun 'Z a a
x))
(Fun n a a -> T_Flip a a n
forall a b (n :: PeanoNum). Fun n a b -> T_Flip a b n
T_Flip Fun n a a
fun)
{-# INLINE fmap #-}
instance ArityPeano n => Applicative (Fun n a) where
pure :: a -> Fun n a a
pure a
x = (forall (k :: PeanoNum). Proxy ('S k) -> a -> Proxy k)
-> (Proxy 'Z -> a) -> Proxy n -> Fun n a a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\Proxy ('S k)
Proxy a
_ -> Proxy k
forall k (t :: k). Proxy t
Proxy)
(\Proxy 'Z
Proxy -> a
x)
Proxy n
forall k (t :: k). Proxy t
Proxy
(Fun Fn n a (a -> b)
f0 :: Fun n a (p -> q)) <*> :: Fun n a (a -> b) -> Fun n a a -> Fun n a b
<*> (Fun Fn n a a
g0 :: Fun n a p)
= (forall (k :: PeanoNum).
T_ap a (a -> b) a ('S k) -> a -> T_ap a (a -> b) a k)
-> (T_ap a (a -> b) a 'Z -> b) -> T_ap a (a -> b) a n -> Fun n a b
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_ap f g) a
a -> Fn k a (a -> b) -> Fn k a a -> T_ap a (a -> b) a k
forall a b c (n :: PeanoNum). Fn n a b -> Fn n a c -> T_ap a b c n
T_ap (Fn ('S k) a (a -> b)
a -> Fn k a (a -> b)
f a
a) (Fn ('S k) a a
a -> Fn k a a
g a
a))
(\(T_ap Fn 'Z a (a -> b)
f Fn 'Z a a
g) -> Fn 'Z a (a -> b)
a -> b
f a
Fn 'Z a a
g)
(Fn n a (a -> b) -> Fn n a a -> T_ap a (a -> b) a n
forall a b c (n :: PeanoNum). Fn n a b -> Fn n a c -> T_ap a b c n
T_ap Fn n a (a -> b)
f0 Fn n a a
g0 :: T_ap a (p -> q) p n)
{-# INLINE pure #-}
{-# INLINE (<*>) #-}
instance ArityPeano n => Monad (Fun n a) where
return :: a -> Fun n a a
return = a -> Fun n a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Fun n a a
f >>= :: Fun n a a -> (a -> Fun n a b) -> Fun n a b
>>= a -> Fun n a b
g = (a -> Fun n a b) -> Fun n a (a -> b)
forall (n :: PeanoNum) b a r.
ArityPeano n =>
(b -> Fun n a r) -> Fun n a (b -> r)
shuffleFun a -> Fun n a b
g Fun n a (a -> b) -> Fun n a a -> Fun n a b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Fun n a a
f
{-# INLINE return #-}
{-# INLINE (>>=) #-}
data T_ap a b c n = T_ap (Fn n a b) (Fn n a c)
type Arity n = ( ArityPeano (Peano n)
, KnownNat n
, Peano (n+1) ~ 'S (Peano n)
)
class ArityPeano n where
accum :: (forall k. t ('S k) -> a -> t k)
-> (t 'Z -> b)
-> t n
-> Fun n a b
applyFun :: (forall k. t ('S k) -> (a, t k))
-> t n
-> (CVecPeano n a, t 'Z)
applyFunM :: Applicative f
=> (forall k. t ('S k) -> (f a, t k))
-> t n
-> (f (CVecPeano n a), t 'Z)
reverseF :: Fun n a b -> Fun n a b
gunfoldF :: (Data a)
=> (forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a n -> c r
newtype T_gunfold c r a n = T_gunfold (c (Fn n a r))
apply :: Arity n
=> (forall k. t ('S k) -> (a, t k))
-> t (Peano n)
-> ContVec n a
{-# INLINE apply #-}
apply :: (forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> ContVec n a
apply forall (k :: PeanoNum). t ('S k) -> (a, t k)
step t (Peano n)
z = CVecPeano (Peano n) a -> ContVec n a
forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec (CVecPeano (Peano n) a -> ContVec n a)
-> CVecPeano (Peano n) a -> ContVec n a
forall a b. (a -> b) -> a -> b
$ (CVecPeano (Peano n) a, t 'Z) -> CVecPeano (Peano n) a
forall a b. (a, b) -> a
fst ((forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> (CVecPeano (Peano n) a, t 'Z)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (CVecPeano n a, t 'Z)
applyFun forall (k :: PeanoNum). t ('S k) -> (a, t k)
step t (Peano n)
z)
applyM :: (Applicative f, Arity n)
=> (forall k. t ('S k) -> (f a, t k))
-> t (Peano n)
-> f (ContVec n a)
{-# INLINE applyM #-}
applyM :: (forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t (Peano n) -> f (ContVec n a)
applyM forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t (Peano n)
t = (CVecPeano (Peano n) a -> ContVec n a)
-> f (CVecPeano (Peano n) a) -> f (ContVec n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CVecPeano (Peano n) a -> ContVec n a
forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec (f (CVecPeano (Peano n) a) -> f (ContVec n a))
-> f (CVecPeano (Peano n) a) -> f (ContVec n a)
forall a b. (a -> b) -> a -> b
$ (f (CVecPeano (Peano n) a), t 'Z) -> f (CVecPeano (Peano n) a)
forall a b. (a, b) -> a
fst ((f (CVecPeano (Peano n) a), t 'Z) -> f (CVecPeano (Peano n) a))
-> (f (CVecPeano (Peano n) a), t 'Z) -> f (CVecPeano (Peano n) a)
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t (Peano n) -> (f (CVecPeano (Peano n) a), t 'Z)
forall (n :: PeanoNum) (f :: * -> *) (t :: PeanoNum -> *) a.
(ArityPeano n, Applicative f) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (CVecPeano n a), t 'Z)
applyFunM forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t (Peano n)
t
arity :: KnownNat n => proxy n -> Int
{-# INLINE arity #-}
arity :: proxy n -> Int
arity = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (proxy n -> Integer) -> proxy n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal
instance ArityPeano 'Z where
accum :: (forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t 'Z -> Fun 'Z a b
accum forall (k :: PeanoNum). t ('S k) -> a -> t k
_ t 'Z -> b
g t 'Z
t = Fn 'Z a b -> Fun 'Z a b
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn 'Z a b -> Fun 'Z a b) -> Fn 'Z a b -> Fun 'Z a b
forall a b. (a -> b) -> a -> b
$ t 'Z -> b
g t 'Z
t
applyFun :: (forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t 'Z -> (CVecPeano 'Z a, t 'Z)
applyFun forall (k :: PeanoNum). t ('S k) -> (a, t k)
_ t 'Z
t = ((forall r. Fun 'Z a r -> r) -> CVecPeano 'Z a
forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano forall r. Fun 'Z a r -> r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun, t 'Z
t)
applyFunM :: (forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t 'Z -> (f (CVecPeano 'Z a), t 'Z)
applyFunM forall (k :: PeanoNum). t ('S k) -> (f a, t k)
_ t 'Z
t = (CVecPeano 'Z a -> f (CVecPeano 'Z a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall r. Fun 'Z a r -> r) -> CVecPeano 'Z a
forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano forall r. Fun 'Z a r -> r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun), t 'Z
t)
{-# INLINE accum #-}
{-# INLINE applyFun #-}
{-# INLINE applyFunM #-}
reverseF :: Fun 'Z a b -> Fun 'Z a b
reverseF = Fun 'Z a b -> Fun 'Z a b
forall a. a -> a
id
gunfoldF :: (forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a 'Z -> c r
gunfoldF forall b x. Data b => c (b -> x) -> c x
_ (T_gunfold c (Fn 'Z a r)
c) = c r
c (Fn 'Z a r)
c
{-# INLINE reverseF #-}
{-# INLINE gunfoldF #-}
instance ArityPeano n => ArityPeano ('S n) where
accum :: (forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t ('S n) -> Fun ('S n) a b
accum forall (k :: PeanoNum). t ('S k) -> a -> t k
f t 'Z -> b
g t ('S n)
t = Fn ('S n) a b -> Fun ('S n) a b
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn ('S n) a b -> Fun ('S n) a b)
-> Fn ('S n) a b -> Fun ('S n) a b
forall a b. (a -> b) -> a -> b
$ \a
a -> Fun n a b -> Fn n a b
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun n a b -> Fn n a b) -> Fun n a b -> Fn n a b
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum forall (k :: PeanoNum). t ('S k) -> a -> t k
f t 'Z -> b
g (t ('S n) -> a -> t n
forall (k :: PeanoNum). t ('S k) -> a -> t k
f t ('S n)
t a
a)
applyFun :: (forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t ('S n) -> (CVecPeano ('S n) a, t 'Z)
applyFun forall (k :: PeanoNum). t ('S k) -> (a, t k)
f t ('S n)
t = let (a
a,t n
t') = t ('S n) -> (a, t n)
forall (k :: PeanoNum). t ('S k) -> (a, t k)
f t ('S n)
t
(CVecPeano n a
v,t 'Z
tZ) = (forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (CVecPeano n a, t 'Z)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (CVecPeano n a, t 'Z)
applyFun forall (k :: PeanoNum). t ('S k) -> (a, t k)
f t n
t'
in (a -> CVecPeano n a -> CVecPeano ('S n) a
forall a (n :: PeanoNum). a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano a
a CVecPeano n a
v, t 'Z
tZ)
applyFunM :: (forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t ('S n) -> (f (CVecPeano ('S n) a), t 'Z)
applyFunM forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t ('S n)
t = let (f a
a,t n
t') = t ('S n) -> (f a, t n)
forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t ('S n)
t
(f (CVecPeano n a)
vec,t 'Z
t0) = (forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (CVecPeano n a), t 'Z)
forall (n :: PeanoNum) (f :: * -> *) (t :: PeanoNum -> *) a.
(ArityPeano n, Applicative f) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (CVecPeano n a), t 'Z)
applyFunM forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t n
t'
in (a -> CVecPeano n a -> CVecPeano ('S n) a
forall a (n :: PeanoNum). a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano (a -> CVecPeano n a -> CVecPeano ('S n) a)
-> f a -> f (CVecPeano n a -> CVecPeano ('S n) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a f (CVecPeano n a -> CVecPeano ('S n) a)
-> f (CVecPeano n a) -> f (CVecPeano ('S n) a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (CVecPeano n a)
vec, t 'Z
t0)
{-# INLINE accum #-}
{-# INLINE applyFun #-}
{-# INLINE applyFunM #-}
reverseF :: Fun ('S n) a b -> Fun ('S n) a b
reverseF Fun ('S n) a b
f = Fn ('S n) a b -> Fun ('S n) a b
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn ('S n) a b -> Fun ('S n) a b)
-> Fn ('S n) a b -> Fun ('S n) a b
forall a b. (a -> b) -> a -> b
$ \a
a -> Fun n a b -> Fn n a b
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun n a b -> Fun n a b
forall (n :: PeanoNum) a b. ArityPeano n => Fun n a b -> Fun n a b
reverseF (Fun n a b -> Fun n a b) -> Fun n a b -> Fun n a b
forall a b. (a -> b) -> a -> b
$ Fun ('S n) a b -> a -> Fun n a b
forall (n :: PeanoNum) a b.
ArityPeano n =>
Fun ('S n) a b -> a -> Fun n a b
apLast Fun ('S n) a b
f a
a)
gunfoldF :: (forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a ('S n) -> c r
gunfoldF forall b x. Data b => c (b -> x) -> c x
f T_gunfold c r a ('S n)
c = (forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a n -> c r
forall (n :: PeanoNum) a (c :: * -> *) r.
(ArityPeano n, Data a) =>
(forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a n -> c r
gunfoldF forall b x. Data b => c (b -> x) -> c x
f ((forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a ('S n) -> T_gunfold c r a n
forall a (c :: * -> *) r (n :: PeanoNum).
Data a =>
(forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a ('S n) -> T_gunfold c r a n
apGunfold forall b x. Data b => c (b -> x) -> c x
f T_gunfold c r a ('S n)
c)
{-# INLINE reverseF #-}
{-# INLINE gunfoldF #-}
apGunfold :: Data a
=> (forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a ('S n)
-> T_gunfold c r a n
apGunfold :: (forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a ('S n) -> T_gunfold c r a n
apGunfold forall b x. Data b => c (b -> x) -> c x
f (T_gunfold c (Fn ('S n) a r)
c) = c (Fn n a r) -> T_gunfold c r a n
forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gunfold c r a n
T_gunfold (c (Fn n a r) -> T_gunfold c r a n)
-> c (Fn n a r) -> T_gunfold c r a n
forall a b. (a -> b) -> a -> b
$ c (a -> Fn n a r) -> c (Fn n a r)
forall b x. Data b => c (b -> x) -> c x
f c (Fn ('S n) a r)
c (a -> Fn n a r)
c
{-# INLINE apGunfold #-}
newtype T_Flip a b n = T_Flip (Fun n a b)
constFun :: Fun n a b -> Fun ('S n) a b
constFun :: Fun n a b -> Fun ('S n) a b
constFun (Fun Fn n a b
f) = Fn ('S n) a b -> Fun ('S n) a b
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn ('S n) a b -> Fun ('S n) a b)
-> Fn ('S n) a b -> Fun ('S n) a b
forall a b. (a -> b) -> a -> b
$ \a
_ -> Fn n a b
f
{-# INLINE constFun #-}
curryFirst :: Fun ('S n) a b -> a -> Fun n a b
curryFirst :: Fun ('S n) a b -> a -> Fun n a b
curryFirst = Fun ('S n) a b -> a -> Fun n a b
coerce
{-# INLINE curryFirst #-}
uncurryFirst :: (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst :: (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst = (a -> Fun n a b) -> Fun ('S n) a b
coerce
{-# INLINE uncurryFirst #-}
curryLast :: ArityPeano n => Fun ('S n) a b -> Fun n a (a -> b)
{-# INLINE curryLast #-}
curryLast :: Fun ('S n) a b -> Fun n a (a -> b)
curryLast = Fun ('S n) a b -> Fun n a (a -> b)
forall a b. a -> b
unsafeCoerce
curryMany :: forall n k a b. ArityPeano n
=> Fun (Add n k) a b -> Fun n a (Fun k a b)
{-# INLINE curryMany #-}
curryMany :: Fun (Add n k) a b -> Fun n a (Fun k a b)
curryMany = Fun (Add n k) a b -> Fun n a (Fun k a b)
forall a b. a -> b
unsafeCoerce
apLast :: ArityPeano n => Fun ('S n) a b -> a -> Fun n a b
apLast :: Fun ('S n) a b -> a -> Fun n a b
apLast Fun ('S n) a b
f a
x = ((a -> b) -> b) -> Fun n a (a -> b) -> Fun n a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a
x) (Fun n a (a -> b) -> Fun n a b) -> Fun n a (a -> b) -> Fun n a b
forall a b. (a -> b) -> a -> b
$ Fun ('S n) a b -> Fun n a (a -> b)
forall (n :: PeanoNum) a b.
ArityPeano n =>
Fun ('S n) a b -> Fun n a (a -> b)
curryLast Fun ('S n) a b
f
{-# INLINE apLast #-}
withFun :: (Fun n a b -> Fun n a b) -> Fun ('S n) a b -> Fun ('S n) a b
withFun :: (Fun n a b -> Fun n a b) -> Fun ('S n) a b -> Fun ('S n) a b
withFun Fun n a b -> Fun n a b
f Fun ('S n) a b
fun = Fn ('S n) a b -> Fun ('S n) a b
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn ('S n) a b -> Fun ('S n) a b)
-> Fn ('S n) a b -> Fun ('S n) a b
forall a b. (a -> b) -> a -> b
$ \a
a -> Fun n a b -> Fn n a b
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun n a b -> Fn n a b) -> Fun n a b -> Fn n a b
forall a b. (a -> b) -> a -> b
$ Fun n a b -> Fun n a b
f (Fun n a b -> Fun n a b) -> Fun n a b -> Fun n a b
forall a b. (a -> b) -> a -> b
$ Fun ('S n) a b -> a -> Fun n a b
forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun ('S n) a b
fun a
a
{-# INLINE withFun #-}
shuffleFun :: ArityPeano n
=> (b -> Fun n a r) -> Fun n a (b -> r)
{-# INLINE shuffleFun #-}
shuffleFun :: (b -> Fun n a r) -> Fun n a (b -> r)
shuffleFun b -> Fun n a r
f0
= (forall (k :: PeanoNum).
T_shuffle b a r ('S k) -> a -> T_shuffle b a r k)
-> (T_shuffle b a r 'Z -> b -> r)
-> T_shuffle b a r n
-> Fun n a (b -> r)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_shuffle f) a
a -> (b -> Fn k a r) -> T_shuffle b a r k
forall x a r (n :: PeanoNum). (x -> Fn n a r) -> T_shuffle x a r n
T_shuffle ((b -> Fn k a r) -> T_shuffle b a r k)
-> (b -> Fn k a r) -> T_shuffle b a r k
forall a b. (a -> b) -> a -> b
$ \b
x -> b -> Fn ('S k) a r
b -> a -> Fn k a r
f b
x a
a)
(\(T_shuffle b -> Fn 'Z a r
f) -> b -> r
b -> Fn 'Z a r
f)
((b -> Fn n a r) -> T_shuffle b a r n
forall x a r (n :: PeanoNum). (x -> Fn n a r) -> T_shuffle x a r n
T_shuffle ((Fun n a r -> Fn n a r) -> (b -> Fun n a r) -> b -> Fn n a r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fun n a r -> Fn n a r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun b -> Fun n a r
f0))
newtype T_shuffle x a r n = T_shuffle (x -> Fn n a r)
type family Dim (v :: * -> *) :: Nat
class Arity (Dim v) => Vector v a where
construct :: Fun (Peano (Dim v)) a (v a)
inspect :: v a -> Fun (Peano (Dim v)) a b -> b
basicIndex :: v a -> Int -> a
basicIndex v a
v Int
i = Int -> ContVec (Dim v) a -> a
forall (n :: Nat) a. Arity n => Int -> ContVec n a -> a
index Int
i (v a -> ContVec (Dim v) a
forall (v :: * -> *) a (n :: Nat).
(Vector v a, Dim v ~ n) =>
v a -> ContVec n a
cvec v a
v)
{-# INLINE basicIndex #-}
class (Vector (v n) a, Dim (v n) ~ n) => VectorN v n a
length :: forall v a. KnownNat (Dim v) => v a -> Int
{-# INLINE length #-}
length :: v a -> Int
length v a
_ = Proxy (Dim v) -> Int
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Int
arity (Proxy (Dim v)
forall k (t :: k). Proxy t
Proxy :: Proxy (Dim v))
newtype ContVec n a = ContVec (forall r. Fun (Peano n) a r -> r)
type instance Dim (ContVec n) = n
newtype CVecPeano n a = CVecPeano (forall r. Fun n a r -> r)
consPeano :: a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano :: a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano a
a (CVecPeano forall r. Fun n a r -> r
cont) = (forall r. Fun ('S n) a r -> r) -> CVecPeano ('S n) a
forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano ((forall r. Fun ('S n) a r -> r) -> CVecPeano ('S n) a)
-> (forall r. Fun ('S n) a r -> r) -> CVecPeano ('S n) a
forall a b. (a -> b) -> a -> b
$ \Fun ('S n) a r
f -> Fun n a r -> r
forall r. Fun n a r -> r
cont (Fun n a r -> r) -> Fun n a r -> r
forall a b. (a -> b) -> a -> b
$ Fun ('S n) a r -> a -> Fun n a r
forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun ('S n) a r
f a
a
{-# INLINE consPeano #-}
toContVec :: CVecPeano (Peano n) a -> ContVec n a
toContVec :: CVecPeano (Peano n) a -> ContVec n a
toContVec = CVecPeano (Peano n) a -> ContVec n a
coerce
instance Arity n => Vector (ContVec n) a where
construct :: Fun (Peano (Dim (ContVec n))) a (ContVec n a)
construct = (forall (k :: PeanoNum).
T_mkN (Peano n) a ('S k) -> a -> T_mkN (Peano n) a k)
-> (T_mkN (Peano n) a 'Z -> ContVec n a)
-> T_mkN (Peano n) a (Peano n)
-> Fun (Peano n) a (ContVec n a)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(T_mkN f) a
a -> (CVecPeano k a -> CVecPeano (Peano n) a) -> T_mkN (Peano n) a k
forall (n_tot :: PeanoNum) a (n :: PeanoNum).
(CVecPeano n a -> CVecPeano n_tot a) -> T_mkN n_tot a n
T_mkN (CVecPeano ('S k) a -> CVecPeano (Peano n) a
f (CVecPeano ('S k) a -> CVecPeano (Peano n) a)
-> (CVecPeano k a -> CVecPeano ('S k) a)
-> CVecPeano k a
-> CVecPeano (Peano n) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> CVecPeano k a -> CVecPeano ('S k) a
forall a (n :: PeanoNum). a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano a
a))
(\(T_mkN CVecPeano 'Z a -> CVecPeano (Peano n) a
f) -> CVecPeano (Peano n) a -> ContVec n a
forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec (CVecPeano (Peano n) a -> ContVec n a)
-> CVecPeano (Peano n) a -> ContVec n a
forall a b. (a -> b) -> a -> b
$ CVecPeano 'Z a -> CVecPeano (Peano n) a
f ((forall r. Fun 'Z a r -> r) -> CVecPeano 'Z a
forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano forall r. Fun 'Z a r -> r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun))
((CVecPeano (Peano n) a -> CVecPeano (Peano n) a)
-> T_mkN (Peano n) a (Peano n)
forall (n_tot :: PeanoNum) a (n :: PeanoNum).
(CVecPeano n a -> CVecPeano n_tot a) -> T_mkN n_tot a n
T_mkN CVecPeano (Peano n) a -> CVecPeano (Peano n) a
forall a. a -> a
id)
inspect :: ContVec n a -> Fun (Peano (Dim (ContVec n))) a b -> b
inspect (ContVec forall r. Fun (Peano n) a r -> r
c) Fun (Peano (Dim (ContVec n))) a b
f = Fun (Peano n) a b -> b
forall r. Fun (Peano n) a r -> r
c Fun (Peano n) a b
Fun (Peano (Dim (ContVec n))) a b
f
{-# INLINE construct #-}
{-# INLINE inspect #-}
newtype T_mkN n_tot a n = T_mkN (CVecPeano n a -> CVecPeano n_tot a)
instance Arity n => VectorN ContVec n a
instance (Arity n) => Functor (ContVec n) where
fmap :: (a -> b) -> ContVec n a -> ContVec n b
fmap = (a -> b) -> ContVec n a -> ContVec n b
forall (n :: Nat) a b.
Arity n =>
(a -> b) -> ContVec n a -> ContVec n b
map
{-# INLINE fmap #-}
instance (Arity n) => Applicative (ContVec n) where
pure :: a -> ContVec n a
pure = a -> ContVec n a
forall (n :: Nat) a. Arity n => a -> ContVec n a
replicate
<*> :: ContVec n (a -> b) -> ContVec n a -> ContVec n b
(<*>) = ((a -> b) -> a -> b)
-> ContVec n (a -> b) -> ContVec n a -> ContVec n b
forall (n :: Nat) a b c.
Arity n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
{-# INLINE pure #-}
{-# INLINE (<*>) #-}
instance (Arity n) => F.Foldable (ContVec n) where
foldr :: (a -> b -> b) -> b -> ContVec n a -> b
foldr = (a -> b -> b) -> b -> ContVec n a -> b
forall (n :: Nat) a b.
Arity n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr
{-# INLINE foldr #-}
instance (Arity n) => F.Traversable (ContVec n) where
sequenceA :: ContVec n (f a) -> f (ContVec n a)
sequenceA ContVec n (f a)
v = ContVec n (f a)
-> Fun (Peano (Dim (ContVec n))) (f a) (f (ContVec n a))
-> f (ContVec n a)
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n (f a)
v (Fun (Peano (Dim (ContVec n))) (f a) (f (ContVec n a))
-> f (ContVec n a))
-> Fun (Peano (Dim (ContVec n))) (f a) (f (ContVec n a))
-> f (ContVec n a)
forall a b. (a -> b) -> a -> b
$ Fun (Peano n) a (ContVec n a)
-> Fun (Peano n) (f a) (f (ContVec n a))
forall (f :: * -> *) (n :: PeanoNum) a b.
(Applicative f, ArityPeano n) =>
Fun n a b -> Fun n (f a) (f b)
sequenceAF Fun (Peano n) a (ContVec n a)
forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct
{-# INLINE sequenceA #-}
sequenceAF :: forall f n a b. (Applicative f, ArityPeano n)
=> Fun n a b -> Fun n (f a) (f b)
{-# INLINE sequenceAF #-}
sequenceAF :: Fun n a b -> Fun n (f a) (f b)
sequenceAF (Fun Fn n a b
f0)
= (forall (k :: PeanoNum).
T_sequenceA f a b ('S k) -> f a -> T_sequenceA f a b k)
-> (T_sequenceA f a b 'Z -> f b)
-> T_sequenceA f a b n
-> Fun n (f a) (f b)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_sequenceA f) f a
a -> f (Fn k a b) -> T_sequenceA f a b k
forall (f :: * -> *) a b (n :: PeanoNum).
f (Fn n a b) -> T_sequenceA f a b n
T_sequenceA (f (Fn ('S k) a b)
f (a -> Fn k a b)
f f (a -> Fn k a b) -> f a -> f (Fn k a b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a
a))
(\(T_sequenceA f (Fn 'Z a b)
f) -> f b
f (Fn 'Z a b)
f)
(f (Fn n a b) -> T_sequenceA f a b n
forall (f :: * -> *) a b (n :: PeanoNum).
f (Fn n a b) -> T_sequenceA f a b n
T_sequenceA (Fn n a b -> f (Fn n a b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Fn n a b
f0) :: T_sequenceA f a b n)
newtype T_sequenceA f a b n = T_sequenceA (f (Fn n a b))
cvec :: (Vector v a, Dim v ~ n) => v a -> ContVec n a
cvec :: v a -> ContVec n a
cvec v a
v = (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
ContVec (v a -> Fun (Peano (Dim v)) a r -> r
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect v a
v)
{-# INLINE[0] cvec #-}
empty :: ContVec 0 a
{-# INLINE empty #-}
empty :: ContVec 0 a
empty = (forall r. Fun (Peano 0) a r -> r) -> ContVec 0 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec (\(Fun Fn (Peano 0) a r
r) -> r
Fn (Peano 0) a r
r)
fromList :: Arity n => [a] -> ContVec n a
{-# INLINE fromList #-}
fromList :: [a] -> ContVec n a
fromList [a]
xs =
(forall (k :: PeanoNum). Const [a] ('S k) -> (a, Const [a] k))
-> Const [a] (Peano n) -> ContVec n a
forall (n :: Nat) (t :: PeanoNum -> *) a.
Arity n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> ContVec n a
apply forall k k a (b :: k) (b :: k). Const [a] b -> (a, Const [a] b)
forall (k :: PeanoNum). Const [a] ('S k) -> (a, Const [a] k)
step ([a] -> Const [a] (Peano n)
forall k a (b :: k). a -> Const a b
Const [a]
xs)
where
step :: Const [a] b -> (a, Const [a] b)
step (Const [] ) = [Char] -> (a, Const [a] b)
forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.Cont.fromList: too few elements"
step (Const (a
a:[a]
as)) = (a
a, [a] -> Const [a] b
forall k a (b :: k). a -> Const a b
Const [a]
as)
fromList' :: forall n a. Arity n => [a] -> ContVec n a
{-# INLINE fromList' #-}
fromList' :: [a] -> ContVec n a
fromList' [a]
xs =
let step :: Const [a] b -> (a, Const [a] b)
step (Const [] ) = [Char] -> (a, Const [a] b)
forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.Cont.fromList': too few elements"
step (Const (a
a:[a]
as)) = (a
a, [a] -> Const [a] b
forall k a (b :: k). a -> Const a b
Const [a]
as)
in case (forall (k :: PeanoNum). Const [a] ('S k) -> (a, Const [a] k))
-> Const [a] (Peano n) -> (CVecPeano (Peano n) a, Const [a] 'Z)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (CVecPeano n a, t 'Z)
applyFun forall k k a (b :: k) (b :: k). Const [a] b -> (a, Const [a] b)
forall (k :: PeanoNum). Const [a] ('S k) -> (a, Const [a] k)
step ([a] -> Const [a] (Peano n)
forall k a (b :: k). a -> Const a b
Const [a]
xs :: Const [a] (Peano n)) of
(CVecPeano (Peano n) a
v,Const []) -> CVecPeano (Peano n) a -> ContVec n a
forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec CVecPeano (Peano n) a
v
(CVecPeano (Peano n) a, Const [a] 'Z)
_ -> [Char] -> ContVec n a
forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.Cont.fromList': too many elements"
fromListM :: forall n a. Arity n => [a] -> Maybe (ContVec n a)
{-# INLINE fromListM #-}
fromListM :: [a] -> Maybe (ContVec n a)
fromListM [a]
xs = case (forall (k :: PeanoNum).
Const [a] ('S k) -> (Maybe a, Const [a] k))
-> Const [a] (Peano n)
-> (Maybe (CVecPeano (Peano n) a), Const [a] 'Z)
forall (n :: PeanoNum) (f :: * -> *) (t :: PeanoNum -> *) a.
(ArityPeano n, Applicative f) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (CVecPeano n a), t 'Z)
applyFunM forall k k a (b :: k) (b :: k).
Const [a] b -> (Maybe a, Const [a] b)
forall (k :: PeanoNum). Const [a] ('S k) -> (Maybe a, Const [a] k)
step ([a] -> Const [a] (Peano n)
forall k a (b :: k). a -> Const a b
Const [a]
xs :: Const [a] (Peano n)) of
(Just CVecPeano (Peano n) a
v, Const []) -> ContVec n a -> Maybe (ContVec n a)
forall a. a -> Maybe a
Just (CVecPeano (Peano n) a -> ContVec n a
forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec CVecPeano (Peano n) a
v)
(Maybe (CVecPeano (Peano n) a), Const [a] 'Z)
_ -> Maybe (ContVec n a)
forall a. Maybe a
Nothing
where
step :: Const [a] b -> (Maybe a, Const [a] b)
step (Const [] ) = (Maybe a
forall a. Maybe a
Nothing, [a] -> Const [a] b
forall k a (b :: k). a -> Const a b
Const [])
step (Const (a
a:[a]
as)) = (a -> Maybe a
forall a. a -> Maybe a
Just a
a , [a] -> Const [a] b
forall k a (b :: k). a -> Const a b
Const [a]
as)
toList :: (Arity n) => ContVec n a -> [a]
toList :: ContVec n a -> [a]
toList = (a -> [a] -> [a]) -> [a] -> ContVec n a -> [a]
forall (n :: Nat) a b.
Arity n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr (:) []
{-# INLINE toList #-}
replicate :: (Arity n) => a -> ContVec n a
{-# INLINE replicate #-}
replicate :: a -> ContVec n a
replicate a
a = (forall (k :: PeanoNum). Proxy ('S k) -> (a, Proxy k))
-> Proxy (Peano n) -> ContVec n a
forall (n :: Nat) (t :: PeanoNum -> *) a.
Arity n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> ContVec n a
apply (\Proxy ('S k)
Proxy -> (a
a, Proxy k
forall k (t :: k). Proxy t
Proxy)) Proxy (Peano n)
forall k (t :: k). Proxy t
Proxy
replicateM :: (Arity n, Applicative f) => f a -> f (ContVec n a)
{-# INLINE replicateM #-}
replicateM :: f a -> f (ContVec n a)
replicateM f a
act
= (forall (k :: PeanoNum). Proxy ('S k) -> (f a, Proxy k))
-> Proxy (Peano n) -> f (ContVec n a)
forall (f :: * -> *) (n :: Nat) (t :: PeanoNum -> *) a.
(Applicative f, Arity n) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t (Peano n) -> f (ContVec n a)
applyM (\Proxy ('S k)
Proxy -> (f a
act, Proxy k
forall k (t :: k). Proxy t
Proxy)) Proxy (Peano n)
forall k (t :: k). Proxy t
Proxy
generate :: (Arity n) => (Int -> a) -> ContVec n a
{-# INLINE generate #-}
generate :: (Int -> a) -> ContVec n a
generate Int -> a
f =
(forall (k :: PeanoNum). Const Int ('S k) -> (a, Const Int k))
-> Const Int (Peano n) -> ContVec n a
forall (n :: Nat) (t :: PeanoNum -> *) a.
Arity n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> ContVec n a
apply (\(Const n) -> (Int -> a
f Int
n, Int -> Const Int k
forall k a (b :: k). a -> Const a b
Const (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))) (Int -> Const Int (Peano n)
forall k a (b :: k). a -> Const a b
Const Int
0)
generateM :: (Applicative f, Arity n) => (Int -> f a) -> f (ContVec n a)
{-# INLINE generateM #-}
generateM :: (Int -> f a) -> f (ContVec n a)
generateM Int -> f a
f =
(forall (k :: PeanoNum). Const Int ('S k) -> (f a, Const Int k))
-> Const Int (Peano n) -> f (ContVec n a)
forall (f :: * -> *) (n :: Nat) (t :: PeanoNum -> *) a.
(Applicative f, Arity n) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t (Peano n) -> f (ContVec n a)
applyM (\(Const n) -> (Int -> f a
f Int
n, Int -> Const Int k
forall k a (b :: k). a -> Const a b
Const (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))) (Int -> Const Int (Peano n)
forall k a (b :: k). a -> Const a b
Const Int
0)
unfoldr :: Arity n => (b -> (a,b)) -> b -> ContVec n a
{-# INLINE unfoldr #-}
unfoldr :: (b -> (a, b)) -> b -> ContVec n a
unfoldr b -> (a, b)
f b
b0 =
(forall (k :: PeanoNum). Const b ('S k) -> (a, Const b k))
-> Const b (Peano n) -> ContVec n a
forall (n :: Nat) (t :: PeanoNum -> *) a.
Arity n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> ContVec n a
apply (\(Const b) -> let (a
a,b
b') = b -> (a, b)
f b
b in (a
a, b -> Const b k
forall k a (b :: k). a -> Const a b
Const b
b'))
(b -> Const b (Peano n)
forall k a (b :: k). a -> Const a b
Const b
b0)
basis :: (Num a, Arity n) => Int -> ContVec n a
{-# INLINE basis #-}
basis :: Int -> ContVec n a
basis Int
n0 =
(forall (k :: PeanoNum). Const Int ('S k) -> (a, Const Int k))
-> Const Int (Peano n) -> ContVec n a
forall (n :: Nat) (t :: PeanoNum -> *) a.
Arity n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> ContVec n a
apply (\(Const n) -> (if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then a
1 else a
0, Int -> Const Int k
forall k a (b :: k). a -> Const a b
Const (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)))
(Int -> Const Int (Peano n)
forall k a (b :: k). a -> Const a b
Const Int
n0)
mk1 :: a -> ContVec 1 a
mk1 :: a -> ContVec 1 a
mk1 a
a1 = (forall r. Fun (Peano 1) a r -> r) -> ContVec 1 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 1) a r -> r) -> ContVec 1 a)
-> (forall r. Fun (Peano 1) a r -> r) -> ContVec 1 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 1) a r
f) -> Fn (Peano 1) a r
a -> r
f a
a1
{-# INLINE mk1 #-}
mk2 :: a -> a -> ContVec 2 a
mk2 :: a -> a -> ContVec 2 a
mk2 a
a1 a
a2 = (forall r. Fun (Peano 2) a r -> r) -> ContVec 2 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 2) a r -> r) -> ContVec 2 a)
-> (forall r. Fun (Peano 2) a r -> r) -> ContVec 2 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 2) a r
f) -> Fn (Peano 2) a r
a -> a -> r
f a
a1 a
a2
{-# INLINE mk2 #-}
mk3 :: a -> a -> a -> ContVec 3 a
mk3 :: a -> a -> a -> ContVec 3 a
mk3 a
a1 a
a2 a
a3 = (forall r. Fun (Peano 3) a r -> r) -> ContVec 3 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 3) a r -> r) -> ContVec 3 a)
-> (forall r. Fun (Peano 3) a r -> r) -> ContVec 3 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 3) a r
f) -> Fn (Peano 3) a r
a -> a -> a -> r
f a
a1 a
a2 a
a3
{-# INLINE mk3 #-}
mk4 :: a -> a -> a -> a -> ContVec 4 a
mk4 :: a -> a -> a -> a -> ContVec 4 a
mk4 a
a1 a
a2 a
a3 a
a4 = (forall r. Fun (Peano 4) a r -> r) -> ContVec 4 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 4) a r -> r) -> ContVec 4 a)
-> (forall r. Fun (Peano 4) a r -> r) -> ContVec 4 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 4) a r
f) -> Fn (Peano 4) a r
a -> a -> a -> a -> r
f a
a1 a
a2 a
a3 a
a4
{-# INLINE mk4 #-}
mk5 :: a -> a -> a -> a -> a -> ContVec 5 a
mk5 :: a -> a -> a -> a -> a -> ContVec 5 a
mk5 a
a1 a
a2 a
a3 a
a4 a
a5 = (forall r. Fun (Peano 5) a r -> r) -> ContVec 5 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 5) a r -> r) -> ContVec 5 a)
-> (forall r. Fun (Peano 5) a r -> r) -> ContVec 5 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 5) a r
f) -> Fn (Peano 5) a r
a -> a -> a -> a -> a -> r
f a
a1 a
a2 a
a3 a
a4 a
a5
{-# INLINE mk5 #-}
mk6 :: a -> a -> a -> a -> a -> a -> ContVec 6 a
mk6 :: a -> a -> a -> a -> a -> a -> ContVec 6 a
mk6 a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 = (forall r. Fun (Peano 6) a r -> r) -> ContVec 6 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 6) a r -> r) -> ContVec 6 a)
-> (forall r. Fun (Peano 6) a r -> r) -> ContVec 6 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 6) a r
f) -> Fn (Peano 6) a r
a -> a -> a -> a -> a -> a -> r
f a
a1 a
a2 a
a3 a
a4 a
a5 a
a6
{-# INLINE mk6 #-}
mk7 :: a -> a -> a -> a -> a -> a -> a -> ContVec 7 a
mk7 :: a -> a -> a -> a -> a -> a -> a -> ContVec 7 a
mk7 a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 a
a7 = (forall r. Fun (Peano 7) a r -> r) -> ContVec 7 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 7) a r -> r) -> ContVec 7 a)
-> (forall r. Fun (Peano 7) a r -> r) -> ContVec 7 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 7) a r
f) -> Fn (Peano 7) a r
a -> a -> a -> a -> a -> a -> a -> r
f a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 a
a7
{-# INLINE mk7 #-}
mk8 :: a -> a -> a -> a -> a -> a -> a -> a -> ContVec 8 a
mk8 :: a -> a -> a -> a -> a -> a -> a -> a -> ContVec 8 a
mk8 a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 a
a7 a
a8 = (forall r. Fun (Peano 8) a r -> r) -> ContVec 8 a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano 8) a r -> r) -> ContVec 8 a)
-> (forall r. Fun (Peano 8) a r -> r) -> ContVec 8 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 8) a r
f) -> Fn (Peano 8) a r
a -> a -> a -> a -> a -> a -> a -> a -> r
f a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 a
a7 a
a8
{-# INLINE mk8 #-}
map :: (Arity n) => (a -> b) -> ContVec n a -> ContVec n b
{-# INLINE map #-}
map :: (a -> b) -> ContVec n a -> ContVec n b
map = (Int -> a -> b) -> ContVec n a -> ContVec n b
forall (n :: Nat) a b.
Arity n =>
(Int -> a -> b) -> ContVec n a -> ContVec n b
imap ((Int -> a -> b) -> ContVec n a -> ContVec n b)
-> ((a -> b) -> Int -> a -> b)
-> (a -> b)
-> ContVec n a
-> ContVec n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Int -> a -> b
forall a b. a -> b -> a
const
imap :: (Arity n) => (Int -> a -> b) -> ContVec n a -> ContVec n b
{-# INLINE imap #-}
imap :: (Int -> a -> b) -> ContVec n a -> ContVec n b
imap Int -> a -> b
f (ContVec forall r. Fun (Peano n) a r -> r
contA) = (forall r. Fun (Peano n) b r -> r) -> ContVec n b
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano n) b r -> r) -> ContVec n b)
-> (forall r. Fun (Peano n) b r -> r) -> ContVec n b
forall a b. (a -> b) -> a -> b
$
Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
contA (Fun (Peano n) a r -> r)
-> (Fun (Peano n) b r -> Fun (Peano n) a r)
-> Fun (Peano n) b r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> b) -> Fun (Peano n) b r -> Fun (Peano n) a r
forall (n :: PeanoNum) a b r.
ArityPeano n =>
(Int -> a -> b) -> Fun n b r -> Fun n a r
imapF Int -> a -> b
f
mapM :: (Arity n, Applicative f) => (a -> f b) -> ContVec n a -> f (ContVec n b)
{-# INLINE mapM #-}
mapM :: (a -> f b) -> ContVec n a -> f (ContVec n b)
mapM = (Int -> a -> f b) -> ContVec n a -> f (ContVec n b)
forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(Int -> a -> f b) -> ContVec n a -> f (ContVec n b)
imapM ((Int -> a -> f b) -> ContVec n a -> f (ContVec n b))
-> ((a -> f b) -> Int -> a -> f b)
-> (a -> f b)
-> ContVec n a
-> f (ContVec n b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f b) -> Int -> a -> f b
forall a b. a -> b -> a
const
imapM :: (Arity n, Applicative f)
=> (Int -> a -> f b) -> ContVec n a -> f (ContVec n b)
{-# INLINE imapM #-}
imapM :: (Int -> a -> f b) -> ContVec n a -> f (ContVec n b)
imapM Int -> a -> f b
f ContVec n a
v
= ContVec n a
-> Fun (Peano (Dim (ContVec n))) a (f (ContVec n b))
-> f (ContVec n b)
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
(Fun (Peano (Dim (ContVec n))) a (f (ContVec n b))
-> f (ContVec n b))
-> Fun (Peano (Dim (ContVec n))) a (f (ContVec n b))
-> f (ContVec n b)
forall a b. (a -> b) -> a -> b
$ (Int -> a -> f b)
-> Fun (Peano n) b (ContVec n b)
-> Fun (Peano n) a (f (ContVec n b))
forall (n :: PeanoNum) (f :: * -> *) a b r.
(ArityPeano n, Applicative f) =>
(Int -> a -> f b) -> Fun n b r -> Fun n a (f r)
imapMF Int -> a -> f b
f Fun (Peano n) b (ContVec n b)
forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct
mapM_ :: (Arity n, Applicative f) => (a -> f b) -> ContVec n a -> f ()
{-# INLINE mapM_ #-}
mapM_ :: (a -> f b) -> ContVec n a -> f ()
mapM_ a -> f b
f = (f () -> a -> f ()) -> f () -> ContVec n a -> f ()
forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl (\f ()
m a
a -> f ()
m f () -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> a -> f b
f a
a f b -> f () -> f ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (() -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
imapM_ :: (Arity n, Applicative f) => (Int -> a -> f b) -> ContVec n a -> f ()
{-# INLINE imapM_ #-}
imapM_ :: (Int -> a -> f b) -> ContVec n a -> f ()
imapM_ Int -> a -> f b
f = (f () -> Int -> a -> f ()) -> f () -> ContVec n a -> f ()
forall (n :: Nat) b a.
Arity n =>
(b -> Int -> a -> b) -> b -> ContVec n a -> b
ifoldl (\f ()
m Int
i a
a -> f ()
m f () -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> a -> f b
f Int
i a
a f b -> f () -> f ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (() -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
imapMF :: (ArityPeano n, Applicative f)
=> (Int -> a -> f b) -> Fun n b r -> Fun n a (f r)
{-# INLINE imapMF #-}
imapMF :: (Int -> a -> f b) -> Fun n b r -> Fun n a (f r)
imapMF Int -> a -> f b
f (Fun Fn n b r
funB) =
(forall (k :: PeanoNum).
T_mapM b f r ('S k) -> a -> T_mapM b f r k)
-> (T_mapM b f r 'Z -> f r) -> T_mapM b f r n -> Fun n a (f r)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_mapM i m) a
a -> Int -> f (Fn k b r) -> T_mapM b f r k
forall a (m :: * -> *) r (n :: PeanoNum).
Int -> m (Fn n a r) -> T_mapM a m r n
T_mapM (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (f (Fn k b r) -> T_mapM b f r k) -> f (Fn k b r) -> T_mapM b f r k
forall a b. (a -> b) -> a -> b
$ (b -> Fn k b r) -> b -> Fn k b r
forall a b. (a -> b) -> a -> b
($) ((b -> Fn k b r) -> b -> Fn k b r)
-> f (b -> Fn k b r) -> f (b -> Fn k b r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Fn ('S k) b r)
f (b -> Fn k b r)
m f (b -> Fn k b r) -> f b -> f (Fn k b r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> a -> f b
f Int
i a
a)
(\(T_mapM Int
_ f (Fn 'Z b r)
m) -> f r
f (Fn 'Z b r)
m)
(Int -> f (Fn n b r) -> T_mapM b f r n
forall a (m :: * -> *) r (n :: PeanoNum).
Int -> m (Fn n a r) -> T_mapM a m r n
T_mapM Int
0 (Fn n b r -> f (Fn n b r)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Fn n b r
funB))
data T_mapM a m r n = T_mapM Int (m (Fn n a r))
imapF :: ArityPeano n
=> (Int -> a -> b) -> Fun n b r -> Fun n a r
{-# INLINE imapF #-}
imapF :: (Int -> a -> b) -> Fun n b r -> Fun n a r
imapF Int -> a -> b
f (Fun Fn n b r
funB) =
(forall (k :: PeanoNum). T_map b r ('S k) -> a -> T_map b r k)
-> (T_map b r 'Z -> r) -> T_map b r n -> Fun n a r
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_map i g) a
b -> Int -> Fn k b r -> T_map b r k
forall a r (n :: PeanoNum). Int -> Fn n a r -> T_map a r n
T_map (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Fn ('S k) b r
b -> Fn k b r
g (Int -> a -> b
f Int
i a
b)))
(\(T_map Int
_ Fn 'Z b r
r) -> r
Fn 'Z b r
r)
( Int -> Fn n b r -> T_map b r n
forall a r (n :: PeanoNum). Int -> Fn n a r -> T_map a r n
T_map Int
0 Fn n b r
funB)
data T_map a r n = T_map Int (Fn n a r)
scanl :: (Arity n) => (b -> a -> b) -> b -> ContVec n a -> ContVec (n+1) b
{-# INLINE scanl #-}
scanl :: (b -> a -> b) -> b -> ContVec n a -> ContVec (n + 1) b
scanl b -> a -> b
f b
b0 (ContVec forall r. Fun (Peano n) a r -> r
cont) = (forall r. Fun (Peano (n + 1)) b r -> r) -> ContVec (n + 1) b
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano (n + 1)) b r -> r) -> ContVec (n + 1) b)
-> (forall r. Fun (Peano (n + 1)) b r -> r) -> ContVec (n + 1) b
forall a b. (a -> b) -> a -> b
$
Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
cont (Fun (Peano n) a r -> r)
-> (Fun ('S (Peano n)) b r -> Fun (Peano n) a r)
-> Fun ('S (Peano n)) b r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a -> b) -> b -> Fun ('S (Peano n)) b r -> Fun (Peano n) a r
forall (n :: PeanoNum) a b r.
ArityPeano n =>
(b -> a -> b) -> b -> Fun ('S n) b r -> Fun n a r
scanlF b -> a -> b
f b
b0
scanl1 :: (Arity n) => (a -> a -> a) -> ContVec n a -> ContVec n a
{-# INLINE scanl1 #-}
scanl1 :: (a -> a -> a) -> ContVec n a -> ContVec n a
scanl1 a -> a -> a
f (ContVec 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
ContVec ((forall r. Fun (Peano n) a r -> r) -> ContVec n a)
-> (forall r. Fun (Peano n) a r -> r) -> ContVec n a
forall a b. (a -> b) -> a -> b
$
Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
cont (Fun (Peano n) a r -> r)
-> (Fun (Peano n) a r -> Fun (Peano n) a r)
-> Fun (Peano n) a r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a) -> Fun (Peano n) a r -> Fun (Peano n) a r
forall (n :: PeanoNum) a r.
ArityPeano n =>
(a -> a -> a) -> Fun n a r -> Fun n a r
scanl1F a -> a -> a
f
scanlF :: forall n a b r. (ArityPeano n) => (b -> a -> b) -> b -> Fun ('S n) b r -> Fun n a r
scanlF :: (b -> a -> b) -> b -> Fun ('S n) b r -> Fun n a r
scanlF b -> a -> b
f b
b0 (Fun Fn ('S n) b r
fun0)
= (forall (k :: PeanoNum). T_scanl r b ('S k) -> a -> T_scanl r b k)
-> (T_scanl r b 'Z -> r) -> T_scanl r b n -> Fun n a r
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum forall (k :: PeanoNum). T_scanl r b ('S k) -> a -> T_scanl r b k
step T_scanl r b 'Z -> r
forall r a (n :: PeanoNum). T_scanl r a n -> Fn n a r
fini T_scanl r b n
start
where
step :: forall k. T_scanl r b ('S k) -> a -> T_scanl r b k
step :: T_scanl r b ('S k) -> a -> T_scanl r b k
step (T_scanl b
b Fn ('S k) b r
fn) a
a = let b' :: b
b' = b -> a -> b
f b
b a
a in b -> Fn k b r -> T_scanl r b k
forall r a (n :: PeanoNum). a -> Fn n a r -> T_scanl r a n
T_scanl b
b' (Fn ('S k) b r
b -> Fn k b r
fn b
b')
fini :: T_scanl r a n -> Fn n a r
fini (T_scanl a
_ Fn n a r
r) = Fn n a r
r
start :: T_scanl r b n
start = b -> Fn n b r -> T_scanl r b n
forall r a (n :: PeanoNum). a -> Fn n a r -> T_scanl r a n
T_scanl b
b0 (Fn ('S n) b r
b -> Fn n b r
fun0 b
b0) :: T_scanl r b n
scanl1F :: forall n a r. (ArityPeano n) => (a -> a -> a) -> Fun n a r -> Fun n a r
scanl1F :: (a -> a -> a) -> Fun n a r -> Fun n a r
scanl1F a -> a -> a
f (Fun Fn n a r
fun0) = (forall (k :: PeanoNum).
T_scanl1 r a ('S k) -> a -> T_scanl1 r a k)
-> (T_scanl1 r a 'Z -> r) -> T_scanl1 r a n -> Fun n a r
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum forall (k :: PeanoNum). T_scanl1 r a ('S k) -> a -> T_scanl1 r a k
step T_scanl1 r a 'Z -> r
forall r a (n :: PeanoNum). T_scanl1 r a n -> Fn n a r
fini T_scanl1 r a n
start
where
step :: forall k. T_scanl1 r a ('S k) -> a -> T_scanl1 r a k
step :: T_scanl1 r a ('S k) -> a -> T_scanl1 r a k
step (T_scanl1 Maybe a
Nothing Fn ('S k) a r
fn) a
a = Maybe a -> Fn k a r -> T_scanl1 r a k
forall r a (n :: PeanoNum). Maybe a -> Fn n a r -> T_scanl1 r a n
T_scanl1 (a -> Maybe a
forall a. a -> Maybe a
Just a
a) (Fn ('S k) a r
a -> Fn k a r
fn a
a)
step (T_scanl1 (Just a
x) Fn ('S k) a r
fn) a
a = let a' :: a
a' = a -> a -> a
f a
x a
a in Maybe a -> Fn k a r -> T_scanl1 r a k
forall r a (n :: PeanoNum). Maybe a -> Fn n a r -> T_scanl1 r a n
T_scanl1 (a -> Maybe a
forall a. a -> Maybe a
Just a
a') (Fn ('S k) a r
a -> Fn k a r
fn a
a')
fini :: T_scanl1 r a n -> Fn n a r
fini (T_scanl1 Maybe a
_ Fn n a r
r) = Fn n a r
r
start :: T_scanl1 r a n
start = Maybe a -> Fn n a r -> T_scanl1 r a n
forall r a (n :: PeanoNum). Maybe a -> Fn n a r -> T_scanl1 r a n
T_scanl1 Maybe a
forall a. Maybe a
Nothing Fn n a r
fun0 :: T_scanl1 r a n
data T_scanl r a n = T_scanl a (Fn n a r)
data T_scanl1 r a n = T_scanl1 (Maybe a) (Fn n a r)
sequence :: (Arity n, Applicative f) => ContVec n (f a) -> f (ContVec n a)
sequence :: ContVec n (f a) -> f (ContVec n a)
sequence = (f a -> f a) -> ContVec n (f a) -> f (ContVec n a)
forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(a -> f b) -> ContVec n a -> f (ContVec n b)
mapM f a -> f a
forall a. a -> a
id
{-# INLINE sequence #-}
sequence_ :: (Arity n, Applicative f) => ContVec n (f a) -> f ()
sequence_ :: ContVec n (f a) -> f ()
sequence_ = (f a -> f a) -> ContVec n (f a) -> f ()
forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(a -> f b) -> ContVec n a -> f ()
mapM_ f a -> f a
forall a. a -> a
id
{-# INLINE sequence_ #-}
distribute :: (Functor f, Arity n) => f (ContVec n a) -> ContVec n (f a)
{-# INLINE distribute #-}
distribute :: f (ContVec n a) -> ContVec n (f a)
distribute f (ContVec n a)
f0
= (forall (k :: PeanoNum).
Const (f [a]) ('S k) -> (f a, Const (f [a]) k))
-> Const (f [a]) (Peano n) -> ContVec n (f a)
forall (n :: Nat) (t :: PeanoNum -> *) a.
Arity n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t (Peano n) -> ContVec n a
apply forall k k (f :: * -> *) a (b :: k) (b :: k).
Functor f =>
Const (f [a]) b -> (f a, Const (f [a]) b)
forall (k :: PeanoNum).
Const (f [a]) ('S k) -> (f a, Const (f [a]) k)
step Const (f [a]) (Peano n)
start
where
step :: Const (f [a]) b -> (f a, Const (f [a]) b)
step (Const f [a]
f) = ( ([a] -> a) -> f [a] -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
x:[a]
_) -> a
x) f [a]
f
, f [a] -> Const (f [a]) b
forall k a (b :: k). a -> Const a b
Const (f [a] -> Const (f [a]) b) -> f [a] -> Const (f [a]) b
forall a b. (a -> b) -> a -> b
$ ([a] -> [a]) -> f [a] -> f [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
_:[a]
x) -> [a]
x) f [a]
f)
start :: Const (f [a]) (Peano n)
start = f [a] -> Const (f [a]) (Peano n)
forall k a (b :: k). a -> Const a b
Const ((ContVec n a -> [a]) -> f (ContVec n a) -> f [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ContVec n a -> [a]
forall (n :: Nat) a. Arity n => ContVec n a -> [a]
toList f (ContVec n a)
f0)
collect :: (Functor f, Arity n) => (a -> ContVec n b) -> f a -> ContVec n (f b)
collect :: (a -> ContVec n b) -> f a -> ContVec n (f b)
collect a -> ContVec n b
f = f (ContVec n b) -> ContVec n (f b)
forall (f :: * -> *) (n :: Nat) a.
(Functor f, Arity n) =>
f (ContVec n a) -> ContVec n (f a)
distribute (f (ContVec n b) -> ContVec n (f b))
-> (f a -> f (ContVec n b)) -> f a -> ContVec n (f b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> ContVec n b) -> f a -> f (ContVec n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> ContVec n b
f
{-# INLINE collect #-}
tail :: Arity n => ContVec (n+1) a -> ContVec n a
tail :: ContVec (n + 1) a -> ContVec n a
tail (ContVec forall r. Fun (Peano (n + 1)) 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
ContVec ((forall r. Fun (Peano n) a r -> r) -> ContVec n a)
-> (forall r. Fun (Peano n) a r -> r) -> ContVec n a
forall a b. (a -> b) -> a -> b
$ \Fun (Peano n) a r
f -> Fun (Peano (n + 1)) a r -> r
forall r. Fun (Peano (n + 1)) a r -> r
cont (Fun (Peano (n + 1)) a r -> r) -> Fun (Peano (n + 1)) a r -> r
forall a b. (a -> b) -> a -> b
$ Fun (Peano n) a r -> Fun ('S (Peano n)) a r
forall (n :: PeanoNum) a b. Fun n a b -> Fun ('S n) a b
constFun Fun (Peano n) a r
f
{-# INLINE tail #-}
cons :: Arity n => a -> ContVec n a -> ContVec (n+1) a
cons :: a -> ContVec n a -> ContVec (n + 1) a
cons a
a (ContVec forall r. Fun (Peano n) a r -> r
cont) = (forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a)
-> (forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a
forall a b. (a -> b) -> a -> b
$ \Fun (Peano (n + 1)) a r
f -> Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
cont (Fun (Peano n) a r -> r) -> Fun (Peano n) a r -> r
forall a b. (a -> b) -> a -> b
$ Fun ('S (Peano n)) a r -> a -> Fun (Peano n) a r
forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun (Peano (n + 1)) a r
Fun ('S (Peano n)) a r
f a
a
{-# INLINE cons #-}
consV :: Arity n => ContVec 1 a -> ContVec n a -> ContVec (n+1) a
{-# INLINE consV #-}
consV :: ContVec 1 a -> ContVec n a -> ContVec (n + 1) a
consV (ContVec forall r. Fun (Peano 1) a r -> r
cont1) (ContVec forall r. Fun (Peano n) a r -> r
cont)
= (forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a)
-> (forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a
forall a b. (a -> b) -> a -> b
$ \Fun (Peano (n + 1)) a r
f -> Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
cont (Fun (Peano n) a r -> r) -> Fun (Peano n) a r -> r
forall a b. (a -> b) -> a -> b
$ Fun ('S (Peano n)) a r -> a -> Fun (Peano n) a r
forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun (Peano (n + 1)) a r
Fun ('S (Peano n)) a r
f (a -> Fun (Peano n) a r) -> a -> Fun (Peano n) a r
forall a b. (a -> b) -> a -> b
$ Fun (Peano 1) a a -> a
forall r. Fun (Peano 1) a r -> r
cont1 (Fun (Peano 1) a a -> a) -> Fun (Peano 1) a a -> a
forall a b. (a -> b) -> a -> b
$ Fn ('S 'Z) a a -> Fun ('S 'Z) a a
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn ('S 'Z) a a
forall a. a -> a
id
snoc :: Arity n => a -> ContVec n a -> ContVec (n+1) a
snoc :: a -> ContVec n a -> ContVec (n + 1) a
snoc a
a (ContVec forall r. Fun (Peano n) a r -> r
cont) = (forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a)
-> (forall r. Fun (Peano (n + 1)) a r -> r) -> ContVec (n + 1) a
forall a b. (a -> b) -> a -> b
$ \Fun (Peano (n + 1)) a r
f -> Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
cont (Fun (Peano n) a r -> r) -> Fun (Peano n) a r -> r
forall a b. (a -> b) -> a -> b
$ Fun ('S (Peano n)) a r -> a -> Fun (Peano n) a r
forall (n :: PeanoNum) a b.
ArityPeano n =>
Fun ('S n) a b -> a -> Fun n a b
apLast Fun (Peano (n + 1)) a r
Fun ('S (Peano n)) a r
f a
a
{-# INLINE snoc #-}
concat :: ( Arity n
, Arity k
, Arity (n + k)
, Peano (n + k) ~ Add (Peano n) (Peano k)
)
=> ContVec n a -> ContVec k a -> ContVec (n + k) a
{-# INLINE concat #-}
concat :: ContVec n a -> ContVec k a -> ContVec (n + k) a
concat ContVec n a
v ContVec k a
u = ContVec k a
-> Fun (Peano (Dim (ContVec k))) a (ContVec (n + k) a)
-> ContVec (n + k) a
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec k a
u
(Fun (Peano (Dim (ContVec k))) a (ContVec (n + k) a)
-> ContVec (n + k) a)
-> Fun (Peano (Dim (ContVec k))) a (ContVec (n + k) a)
-> ContVec (n + k) a
forall a b. (a -> b) -> a -> b
$ ContVec n a
-> Fun
(Peano (Dim (ContVec n))) a (Fun (Peano k) a (ContVec (n + k) a))
-> Fun (Peano k) a (ContVec (n + k) a)
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
(Fun
(Peano (Dim (ContVec n))) a (Fun (Peano k) a (ContVec (n + k) a))
-> Fun (Peano k) a (ContVec (n + k) a))
-> Fun
(Peano (Dim (ContVec n))) a (Fun (Peano k) a (ContVec (n + k) a))
-> Fun (Peano k) a (ContVec (n + k) a)
forall a b. (a -> b) -> a -> b
$ Fun (Add (Peano n) (Peano k)) a (ContVec (n + k) a)
-> Fun (Peano n) a (Fun (Peano k) a (ContVec (n + k) a))
forall (n :: PeanoNum) (k :: PeanoNum) a b.
ArityPeano n =>
Fun (Add n k) a b -> Fun n a (Fun k a b)
curryMany Fun (Add (Peano n) (Peano k)) a (ContVec (n + k) a)
forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct
reverse :: Arity n => ContVec n a -> ContVec n a
reverse :: ContVec n a -> ContVec n a
reverse (ContVec 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
ContVec ((forall r. Fun (Peano n) a r -> r) -> ContVec n a)
-> (forall r. Fun (Peano n) a r -> r) -> ContVec n a
forall a b. (a -> b) -> a -> b
$ Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
cont (Fun (Peano n) a r -> r)
-> (Fun (Peano n) a r -> Fun (Peano n) a r)
-> Fun (Peano n) a r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun (Peano n) a r -> Fun (Peano n) a r
forall (n :: PeanoNum) a b. ArityPeano n => Fun n a b -> Fun n a b
reverseF
{-# INLINE reverse #-}
zipWith :: (Arity n) => (a -> b -> c)
-> ContVec n a -> ContVec n b -> ContVec n c
{-# INLINE zipWith #-}
zipWith :: (a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith = (Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
forall (n :: Nat) a b c.
Arity n =>
(Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
izipWith ((Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c)
-> ((a -> b -> c) -> Int -> a -> b -> c)
-> (a -> b -> c)
-> ContVec n a
-> ContVec n b
-> ContVec n c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> c) -> Int -> a -> b -> c
forall a b. a -> b -> a
const
zipWith3 :: (Arity n) => (a -> b -> c -> d)
-> ContVec n a -> ContVec n b -> ContVec n c -> ContVec n d
{-# INLINE zipWith3 #-}
zipWith3 :: (a -> b -> c -> d)
-> ContVec n a -> ContVec n b -> ContVec n c -> ContVec n d
zipWith3 a -> b -> c -> d
f ContVec n a
v1 ContVec n b
v2 ContVec n c
v3 = (a -> (b, c) -> d)
-> ContVec n a -> ContVec n (b, c) -> ContVec n d
forall (n :: Nat) a b c.
Arity n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith (\a
a (b
b, c
c) -> a -> b -> c -> d
f a
a b
b c
c) ContVec n a
v1 ((b -> c -> (b, c))
-> ContVec n b -> ContVec n c -> ContVec n (b, c)
forall (n :: Nat) a b c.
Arity n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith (,) ContVec n b
v2 ContVec n c
v3)
izipWith :: (Arity n) => (Int -> a -> b -> c)
-> ContVec n a -> ContVec n b -> ContVec n c
{-# INLINE izipWith #-}
izipWith :: (Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
izipWith Int -> a -> b -> c
f ContVec n a
vecA ContVec n b
vecB = (forall r. Fun (Peano n) c r -> r) -> ContVec n c
forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec ((forall r. Fun (Peano n) c r -> r) -> ContVec n c)
-> (forall r. Fun (Peano n) c r -> r) -> ContVec n c
forall a b. (a -> b) -> a -> b
$ \Fun (Peano n) c r
funC ->
ContVec n b -> Fun (Peano (Dim (ContVec n))) b r -> r
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n b
vecB
(Fun (Peano (Dim (ContVec n))) b r -> r)
-> Fun (Peano (Dim (ContVec n))) b r -> r
forall a b. (a -> b) -> a -> b
$ ContVec n a
-> Fun (Peano (Dim (ContVec n))) a (Fun (Peano n) b r)
-> Fun (Peano n) b r
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
vecA
(Fun (Peano (Dim (ContVec n))) a (Fun (Peano n) b r)
-> Fun (Peano n) b r)
-> Fun (Peano (Dim (ContVec n))) a (Fun (Peano n) b r)
-> Fun (Peano n) b r
forall a b. (a -> b) -> a -> b
$ (Int -> a -> b -> c)
-> Fun (Peano n) c r -> Fun (Peano n) a (Fun (Peano n) b r)
forall (n :: PeanoNum) a b c r.
ArityPeano n =>
(Int -> a -> b -> c) -> Fun n c r -> Fun n a (Fun n b r)
izipWithF Int -> a -> b -> c
f Fun (Peano n) c r
funC
izipWith3 :: (Arity n) => (Int -> a -> b -> c -> d)
-> ContVec n a -> ContVec n b -> ContVec n c -> ContVec n d
{-# INLINE izipWith3 #-}
izipWith3 :: (Int -> a -> b -> c -> d)
-> ContVec n a -> ContVec n b -> ContVec n c -> ContVec n d
izipWith3 Int -> a -> b -> c -> d
f ContVec n a
v1 ContVec n b
v2 ContVec n c
v3 = (Int -> a -> (b, c) -> d)
-> ContVec n a -> ContVec n (b, c) -> ContVec n d
forall (n :: Nat) a b c.
Arity n =>
(Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
izipWith (\Int
i a
a (b
b, c
c) -> Int -> a -> b -> c -> d
f Int
i a
a b
b c
c) ContVec n a
v1 ((b -> c -> (b, c))
-> ContVec n b -> ContVec n c -> ContVec n (b, c)
forall (n :: Nat) a b c.
Arity n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith (,) ContVec n b
v2 ContVec n c
v3)
zipWithM :: (Arity n, Applicative f) => (a -> b -> f c)
-> ContVec n a -> ContVec n b -> f (ContVec n c)
{-# INLINE zipWithM #-}
zipWithM :: (a -> b -> f c) -> ContVec n a -> ContVec n b -> f (ContVec n c)
zipWithM a -> b -> f c
f ContVec n a
v ContVec n b
w = ContVec n (f c) -> f (ContVec n c)
forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence (ContVec n (f c) -> f (ContVec n c))
-> ContVec n (f c) -> f (ContVec n c)
forall a b. (a -> b) -> a -> b
$ (a -> b -> f c) -> ContVec n a -> ContVec n b -> ContVec n (f c)
forall (n :: Nat) a b c.
Arity n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith a -> b -> f c
f ContVec n a
v ContVec n b
w
zipWithM_ :: (Arity n, Applicative f)
=> (a -> b -> f c) -> ContVec n a -> ContVec n b -> f ()
{-# INLINE zipWithM_ #-}
zipWithM_ :: (a -> b -> f c) -> ContVec n a -> ContVec n b -> f ()
zipWithM_ a -> b -> f c
f ContVec n a
xs ContVec n b
ys = ContVec n (f c) -> f ()
forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f ()
sequence_ ((a -> b -> f c) -> ContVec n a -> ContVec n b -> ContVec n (f c)
forall (n :: Nat) a b c.
Arity n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith a -> b -> f c
f ContVec n a
xs ContVec n b
ys)
izipWithM :: (Arity n, Applicative f) => (Int -> a -> b -> f c)
-> ContVec n a -> ContVec n b -> f (ContVec n c)
{-# INLINE izipWithM #-}
izipWithM :: (Int -> a -> b -> f c)
-> ContVec n a -> ContVec n b -> f (ContVec n c)
izipWithM Int -> a -> b -> f c
f ContVec n a
v ContVec n b
w = ContVec n (f c) -> f (ContVec n c)
forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence (ContVec n (f c) -> f (ContVec n c))
-> ContVec n (f c) -> f (ContVec n c)
forall a b. (a -> b) -> a -> b
$ (Int -> a -> b -> f c)
-> ContVec n a -> ContVec n b -> ContVec n (f c)
forall (n :: Nat) a b c.
Arity n =>
(Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
izipWith Int -> a -> b -> f c
f ContVec n a
v ContVec n b
w
izipWithM_ :: (Arity n, Applicative f)
=> (Int -> a -> b -> f c) -> ContVec n a -> ContVec n b -> f ()
{-# INLINE izipWithM_ #-}
izipWithM_ :: (Int -> a -> b -> f c) -> ContVec n a -> ContVec n b -> f ()
izipWithM_ Int -> a -> b -> f c
f ContVec n a
xs ContVec n b
ys = ContVec n (f c) -> f ()
forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f ()
sequence_ ((Int -> a -> b -> f c)
-> ContVec n a -> ContVec n b -> ContVec n (f c)
forall (n :: Nat) a b c.
Arity n =>
(Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
izipWith Int -> a -> b -> f c
f ContVec n a
xs ContVec n b
ys)
izipWithF :: (ArityPeano n)
=> (Int -> a -> b -> c) -> Fun n c r -> Fun n a (Fun n b r)
{-# INLINE izipWithF #-}
izipWithF :: (Int -> a -> b -> c) -> Fun n c r -> Fun n a (Fun n b r)
izipWithF Int -> a -> b -> c
f (Fun Fn n c r
g0) =
([a] -> Fun n b r) -> Fun n a [a] -> Fun n a (Fun n b r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[a]
v -> (forall (k :: PeanoNum).
T_izip a c r ('S k) -> b -> T_izip a c r k)
-> (T_izip a c r 'Z -> r) -> T_izip a c r n -> Fun n b r
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(T_izip i (a:as) g) b
b -> Int -> [a] -> Fn k c r -> T_izip a c r k
forall a c r (n :: PeanoNum).
Int -> [a] -> Fn n c r -> T_izip a c r n
T_izip (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [a]
as (Fn ('S k) c r
c -> Fn k c r
g (c -> Fn k c r) -> c -> Fn k c r
forall a b. (a -> b) -> a -> b
$ Int -> a -> b -> c
f Int
i a
a b
b))
(\(T_izip Int
_ [a]
_ Fn 'Z c r
x) -> r
Fn 'Z c r
x)
(Int -> [a] -> Fn n c r -> T_izip a c r n
forall a c r (n :: PeanoNum).
Int -> [a] -> Fn n c r -> T_izip a c r n
T_izip Int
0 [a]
v Fn n c r
g0)
) Fun n a [a]
forall (n :: PeanoNum) a. ArityPeano n => Fun n a [a]
makeList
makeList :: ArityPeano n => Fun n a [a]
{-# INLINE makeList #-}
makeList :: Fun n a [a]
makeList = (forall (k :: PeanoNum).
Const ([a] -> [a]) ('S k) -> a -> Const ([a] -> [a]) k)
-> (Const ([a] -> [a]) 'Z -> [a])
-> Const ([a] -> [a]) n
-> Fun n a [a]
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(Const xs) a
x -> ([a] -> [a]) -> Const ([a] -> [a]) k
forall k a (b :: k). a -> Const a b
Const ([a] -> [a]
xs ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:)))
(\(Const [a] -> [a]
xs) -> [a] -> [a]
xs [])
(([a] -> [a]) -> Const ([a] -> [a]) n
forall k a (b :: k). a -> Const a b
Const [a] -> [a]
forall a. a -> a
id)
data T_izip a c r n = T_izip Int [a] (Fn n c r)
runContVec :: Fun (Peano n) a r
-> ContVec n a
-> r
runContVec :: Fun (Peano n) a r -> ContVec n a -> r
runContVec Fun (Peano n) a r
f (ContVec forall r. Fun (Peano n) a r -> r
c) = Fun (Peano n) a r -> r
forall r. Fun (Peano n) a r -> r
c Fun (Peano n) a r
f
{-# INLINE runContVec #-}
vector :: (Vector v a, Dim v ~ n) => ContVec n a -> v a
vector :: ContVec n a -> v a
vector = Fun (Peano n) a (v a) -> ContVec n a -> v a
forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec Fun (Peano n) a (v a)
forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct
{-# INLINE[1] vector #-}
head :: (Arity n, 1<=n) => ContVec n a -> a
{-# INLINE head #-}
head :: ContVec n a -> a
head
= Fun (Peano n) a a -> ContVec n a -> a
forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec
(Fun (Peano n) a a -> ContVec n a -> a)
-> Fun (Peano n) a a -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum).
Const (Maybe a) ('S k) -> a -> Const (Maybe a) k)
-> (Const (Maybe a) 'Z -> a)
-> Const (Maybe a) (Peano n)
-> Fun (Peano n) a a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(Const m) a
a -> Maybe a -> Const (Maybe a) k
forall k a (b :: k). a -> Const a b
Const (Maybe a -> Const (Maybe a) k) -> Maybe a -> Const (Maybe a) k
forall a b. (a -> b) -> a -> b
$ case Maybe a
m of { Maybe a
Nothing -> a -> Maybe a
forall a. a -> Maybe a
Just a
a; Maybe a
x -> Maybe a
x })
(\(Const (Just a
x)) -> a
x)
(Maybe a -> Const (Maybe a) (Peano n)
forall k a (b :: k). a -> Const a b
Const Maybe a
forall a. Maybe a
Nothing)
index :: Arity n => Int -> ContVec n a -> a
{-# INLINE index #-}
index :: Int -> ContVec n a -> a
index Int
n
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = [Char] -> ContVec n a -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.Cont.index: index out of range"
| Bool
otherwise = Fun (Peano n) a a -> ContVec n a -> a
forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec (Fun (Peano n) a a -> ContVec n a -> a)
-> Fun (Peano n) a a -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum).
Const (Either Int a) ('S k) -> a -> Const (Either Int a) k)
-> (Const (Either Int a) 'Z -> a)
-> Const (Either Int a) (Peano n)
-> Fun (Peano n) a a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(Const x) a
a -> Either Int a -> Const (Either Int a) k
forall k a (b :: k). a -> Const a b
Const (Either Int a -> Const (Either Int a) k)
-> Either Int a -> Const (Either Int a) k
forall a b. (a -> b) -> a -> b
$ case Either Int a
x of
Left Int
0 -> a -> Either Int a
forall a b. b -> Either a b
Right a
a
Left Int
i -> Int -> Either Int a
forall a b. a -> Either a b
Left (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
Either Int a
r -> Either Int a
r
)
(\(Const Either Int a
x) -> case Either Int a
x of
Left Int
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.index: index out of range"
Right a
a -> a
a
)
(Either Int a -> Const (Either Int a) (Peano n)
forall k a (b :: k). a -> Const a b
Const (Int -> Either Int a
forall a b. a -> Either a b
Left Int
n))
element :: (Arity n, Functor f)
=> Int -> (a -> f a) -> ContVec n a -> f (ContVec n a)
{-# INLINE element #-}
element :: Int -> (a -> f a) -> ContVec n a -> f (ContVec n a)
element Int
i a -> f a
f ContVec n a
v = ContVec n a
-> Fun (Peano (Dim (ContVec n))) a (f (ContVec n a))
-> f (ContVec n a)
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
(Fun (Peano (Dim (ContVec n))) a (f (ContVec n a))
-> f (ContVec n a))
-> Fun (Peano (Dim (ContVec n))) a (f (ContVec n a))
-> f (ContVec n a)
forall a b. (a -> b) -> a -> b
$ Int
-> (a -> f a)
-> Fun (Peano n) a (ContVec n a)
-> Fun (Peano n) a (f (ContVec n a))
forall a (n :: PeanoNum) (f :: * -> *) r.
(ArityPeano n, Functor f) =>
Int -> (a -> f a) -> Fun n a r -> Fun n a (f r)
elementF Int
i a -> f a
f Fun (Peano n) a (ContVec n a)
forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct
elementF :: forall a n f r. (ArityPeano n, Functor f)
=> Int -> (a -> f a) -> Fun n a r -> Fun n a (f r)
{-# INLINE elementF #-}
elementF :: Int -> (a -> f a) -> Fun n a r -> Fun n a (f r)
elementF Int
n a -> f a
f (Fun Fn n a r
fun0) = (forall (k :: PeanoNum).
T_lens f a r ('S k) -> a -> T_lens f a r k)
-> (T_lens f a r 'Z -> f r) -> T_lens f a r n -> Fun n a (f r)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum forall (k :: PeanoNum). T_lens f a r ('S k) -> a -> T_lens f a r k
step T_lens f a r 'Z -> f r
fini T_lens f a r n
start
where
step :: forall k. T_lens f a r ('S k) -> a -> T_lens f a r k
step :: T_lens f a r ('S k) -> a -> T_lens f a r k
step (T_lens (Left (Int
0,Fn ('S k) a r
fun))) a
a = Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k
forall (f :: * -> *) a r (n :: PeanoNum).
Either (Int, Fn n a r) (f (Fn n a r)) -> T_lens f a r n
T_lens (Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k)
-> Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k
forall a b. (a -> b) -> a -> b
$ f (Fn k a r) -> Either (Int, Fn k a r) (f (Fn k a r))
forall a b. b -> Either a b
Right (f (Fn k a r) -> Either (Int, Fn k a r) (f (Fn k a r)))
-> f (Fn k a r) -> Either (Int, Fn k a r) (f (Fn k a r))
forall a b. (a -> b) -> a -> b
$ (a -> Fn k a r) -> f a -> f (Fn k a r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fn ('S k) a r
a -> Fn k a r
fun (f a -> f (Fn k a r)) -> f a -> f (Fn k a r)
forall a b. (a -> b) -> a -> b
$ a -> f a
f a
a
step (T_lens (Left (Int
i,Fn ('S k) a r
fun))) a
a = Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k
forall (f :: * -> *) a r (n :: PeanoNum).
Either (Int, Fn n a r) (f (Fn n a r)) -> T_lens f a r n
T_lens (Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k)
-> Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k
forall a b. (a -> b) -> a -> b
$ (Int, Fn k a r) -> Either (Int, Fn k a r) (f (Fn k a r))
forall a b. a -> Either a b
Left (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Fn ('S k) a r
a -> Fn k a r
fun a
a)
step (T_lens (Right f (Fn ('S k) a r)
fun)) a
a = Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k
forall (f :: * -> *) a r (n :: PeanoNum).
Either (Int, Fn n a r) (f (Fn n a r)) -> T_lens f a r n
T_lens (Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k)
-> Either (Int, Fn k a r) (f (Fn k a r)) -> T_lens f a r k
forall a b. (a -> b) -> a -> b
$ f (Fn k a r) -> Either (Int, Fn k a r) (f (Fn k a r))
forall a b. b -> Either a b
Right (f (Fn k a r) -> Either (Int, Fn k a r) (f (Fn k a r)))
-> f (Fn k a r) -> Either (Int, Fn k a r) (f (Fn k a r))
forall a b. (a -> b) -> a -> b
$ ((a -> Fn k a r) -> Fn k a r) -> f (a -> Fn k a r) -> f (Fn k a r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Fn k a r) -> a -> Fn k a r
forall a b. (a -> b) -> a -> b
$ a
a) f (Fn ('S k) a r)
f (a -> Fn k a r)
fun
fini :: T_lens f a r 'Z -> f r
fini :: T_lens f a r 'Z -> f r
fini (T_lens (Left (Int, Fn 'Z a r)
_)) = [Char] -> f r
forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.lensF: Index out of range"
fini (T_lens (Right f (Fn 'Z a r)
r)) = f r
f (Fn 'Z a r)
r
start :: T_lens f a r n
start :: T_lens f a r n
start = Either (Int, Fn n a r) (f (Fn n a r)) -> T_lens f a r n
forall (f :: * -> *) a r (n :: PeanoNum).
Either (Int, Fn n a r) (f (Fn n a r)) -> T_lens f a r n
T_lens (Either (Int, Fn n a r) (f (Fn n a r)) -> T_lens f a r n)
-> Either (Int, Fn n a r) (f (Fn n a r)) -> T_lens f a r n
forall a b. (a -> b) -> a -> b
$ (Int, Fn n a r) -> Either (Int, Fn n a r) (f (Fn n a r))
forall a b. a -> Either a b
Left (Int
n,Fn n a r
fun0)
data T_lens f a r n = T_lens (Either (Int,(Fn n a r)) (f (Fn n a r)))
foldl :: Arity n => (b -> a -> b) -> b -> ContVec n a -> b
{-# INLINE foldl #-}
foldl :: (b -> a -> b) -> b -> ContVec n a -> b
foldl b -> a -> b
f = (b -> Int -> a -> b) -> b -> ContVec n a -> b
forall (n :: Nat) b a.
Arity n =>
(b -> Int -> a -> b) -> b -> ContVec n a -> b
ifoldl (\b
b Int
_ a
a -> b -> a -> b
f b
b a
a)
ifoldl :: Arity n => (b -> Int -> a -> b) -> b -> ContVec n a -> b
{-# INLINE ifoldl #-}
ifoldl :: (b -> Int -> a -> b) -> b -> ContVec n a -> b
ifoldl b -> Int -> a -> b
f b
b ContVec n a
v
= ContVec n a -> Fun (Peano (Dim (ContVec n))) a b -> b
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
(Fun (Peano (Dim (ContVec n))) a b -> b)
-> Fun (Peano (Dim (ContVec n))) a b -> b
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum). T_ifoldl b ('S k) -> a -> T_ifoldl b k)
-> (T_ifoldl b 'Z -> b)
-> T_ifoldl b (Peano n)
-> Fun (Peano n) a b
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_ifoldl i r) a
a -> Int -> b -> T_ifoldl b k
forall k b (n :: k). Int -> b -> T_ifoldl b n
T_ifoldl (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (b -> Int -> a -> b
f b
r Int
i a
a))
(\(T_ifoldl Int
_ b
r) -> b
r)
(Int -> b -> T_ifoldl b (Peano n)
forall k b (n :: k). Int -> b -> T_ifoldl b n
T_ifoldl Int
0 b
b)
foldM :: (Arity n, Monad m)
=> (b -> a -> m b) -> b -> ContVec n a -> m b
{-# INLINE foldM #-}
foldM :: (b -> a -> m b) -> b -> ContVec n a -> m b
foldM b -> a -> m b
f b
x
= (m b -> a -> m b) -> m b -> ContVec n a -> m b
forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl (\m b
m a
a -> do{ b
b <- m b
m; b -> a -> m b
f b
b a
a}) (b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
x)
ifoldM :: (Arity n, Monad m)
=> (b -> Int -> a -> m b) -> b -> ContVec n a -> m b
{-# INLINE ifoldM #-}
ifoldM :: (b -> Int -> a -> m b) -> b -> ContVec n a -> m b
ifoldM b -> Int -> a -> m b
f b
x
= (m b -> Int -> a -> m b) -> m b -> ContVec n a -> m b
forall (n :: Nat) b a.
Arity n =>
(b -> Int -> a -> b) -> b -> ContVec n a -> b
ifoldl (\m b
m Int
i a
a -> do{ b
b <- m b
m; b -> Int -> a -> m b
f b
b Int
i a
a}) (b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
x)
data T_ifoldl b n = T_ifoldl !Int b
foldl1 :: (Arity n, 1 <= n) => (a -> a -> a) -> ContVec n a -> a
{-# INLINE foldl1 #-}
foldl1 :: (a -> a -> a) -> ContVec n a -> a
foldl1 a -> a -> a
f
= Fun (Peano n) a a -> ContVec n a -> a
forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec
(Fun (Peano n) a a -> ContVec n a -> a)
-> Fun (Peano n) a a -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum).
Const (Maybe a) ('S k) -> a -> Const (Maybe a) k)
-> (Const (Maybe a) 'Z -> a)
-> Const (Maybe a) (Peano n)
-> Fun (Peano n) a a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(Const r ) a
a -> Maybe a -> Const (Maybe a) k
forall k a (b :: k). a -> Const a b
Const (Maybe a -> Const (Maybe a) k) -> Maybe a -> Const (Maybe a) k
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
a ((a -> a -> a) -> a -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> a
f a
a) Maybe a
r)
(\(Const (Just a
x)) -> a
x)
(Maybe a -> Const (Maybe a) (Peano n)
forall k a (b :: k). a -> Const a b
Const Maybe a
forall a. Maybe a
Nothing)
foldr :: Arity n => (a -> b -> b) -> b -> ContVec n a -> b
{-# INLINE foldr #-}
foldr :: (a -> b -> b) -> b -> ContVec n a -> b
foldr = (Int -> a -> b -> b) -> b -> ContVec n a -> b
forall (n :: Nat) a b.
Arity n =>
(Int -> a -> b -> b) -> b -> ContVec n a -> b
ifoldr ((Int -> a -> b -> b) -> b -> ContVec n a -> b)
-> ((a -> b -> b) -> Int -> a -> b -> b)
-> (a -> b -> b)
-> b
-> ContVec n a
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> b) -> Int -> a -> b -> b
forall a b. a -> b -> a
const
ifoldr :: Arity n => (Int -> a -> b -> b) -> b -> ContVec n a -> b
{-# INLINE ifoldr #-}
ifoldr :: (Int -> a -> b -> b) -> b -> ContVec n a -> b
ifoldr Int -> a -> b -> b
f b
z
= Fun (Peano n) a b -> ContVec n a -> b
forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec
(Fun (Peano n) a b -> ContVec n a -> b)
-> Fun (Peano n) a b -> ContVec n a -> b
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum). T_ifoldr b ('S k) -> a -> T_ifoldr b k)
-> (T_ifoldr b 'Z -> b)
-> T_ifoldr b (Peano n)
-> Fun (Peano n) a b
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_ifoldr i g) a
a -> Int -> (b -> b) -> T_ifoldr b k
forall k b (n :: k). Int -> (b -> b) -> T_ifoldr b n
T_ifoldr (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (b -> b
g (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> b -> b
f Int
i a
a))
(\(T_ifoldr Int
_ b -> b
g) -> b -> b
g b
z)
(Int -> (b -> b) -> T_ifoldr b (Peano n)
forall k b (n :: k). Int -> (b -> b) -> T_ifoldr b n
T_ifoldr Int
0 b -> b
forall a. a -> a
id)
data T_ifoldr b n = T_ifoldr Int (b -> b)
sum :: (Num a, Arity n) => ContVec n a -> a
sum :: ContVec n a -> a
sum = (a -> a -> a) -> a -> ContVec n a -> a
forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl a -> a -> a
forall a. Num a => a -> a -> a
(+) a
0
{-# INLINE sum #-}
minimum :: (Ord a, Arity n, 1<=n) => ContVec n a -> a
minimum :: ContVec n a -> a
minimum = (a -> a -> a) -> ContVec n a -> a
forall (n :: Nat) a.
(Arity n, 1 <= n) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 a -> a -> a
forall a. Ord a => a -> a -> a
min
{-# INLINE minimum #-}
maximum :: (Ord a, Arity n, 1<=n) => ContVec n a -> a
maximum :: ContVec n a -> a
maximum = (a -> a -> a) -> ContVec n a -> a
forall (n :: Nat) a.
(Arity n, 1 <= n) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 a -> a -> a
forall a. Ord a => a -> a -> a
max
{-# INLINE maximum #-}
and :: Arity n => ContVec n Bool -> Bool
and :: ContVec n Bool -> Bool
and = (Bool -> Bool -> Bool) -> Bool -> ContVec n Bool -> Bool
forall (n :: Nat) a b.
Arity n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr Bool -> Bool -> Bool
(&&) Bool
True
{-# INLINE and #-}
or :: Arity n => ContVec n Bool -> Bool
or :: ContVec n Bool -> Bool
or = (Bool -> Bool -> Bool) -> Bool -> ContVec n Bool -> Bool
forall (n :: Nat) a b.
Arity n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr Bool -> Bool -> Bool
(||) Bool
False
{-# INLINE or #-}
all :: Arity n => (a -> Bool) -> ContVec n a -> Bool
all :: (a -> Bool) -> ContVec n a -> Bool
all a -> Bool
f = (a -> Bool -> Bool) -> Bool -> ContVec n a -> Bool
forall (n :: Nat) a b.
Arity n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr (\a
x Bool
b -> a -> Bool
f a
x Bool -> Bool -> Bool
&& Bool
b) Bool
True
{-# INLINE all #-}
any :: Arity n => (a -> Bool) -> ContVec n a -> Bool
any :: (a -> Bool) -> ContVec n a -> Bool
any a -> Bool
f = (a -> Bool -> Bool) -> Bool -> ContVec n a -> Bool
forall (n :: Nat) a b.
Arity n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr (\a
x Bool
b -> a -> Bool
f a
x Bool -> Bool -> Bool
|| Bool
b) Bool
True
{-# INLINE any #-}
find :: Arity n => (a -> Bool) -> ContVec n a -> Maybe a
find :: (a -> Bool) -> ContVec n a -> Maybe a
find a -> Bool
f = (Maybe a -> a -> Maybe a) -> Maybe a -> ContVec n a -> Maybe a
forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl (\Maybe a
r a
x -> Maybe a
r Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> if a -> Bool
f a
x then a -> Maybe a
forall a. a -> Maybe a
Just a
x else Maybe a
forall a. Maybe a
Nothing) Maybe a
forall a. Maybe a
Nothing
{-# INLINE find #-}
gfoldl :: forall c v a. (Vector v a, Data a)
=> (forall x y. Data x => c (x -> y) -> x -> c y)
-> (forall x . x -> c x)
-> v a -> c (v a)
gfoldl :: (forall x y. Data x => c (x -> y) -> x -> c y)
-> (forall x. x -> c x) -> v a -> c (v a)
gfoldl forall x y. Data x => c (x -> y) -> x -> c y
f forall x. x -> c x
inj v a
v
= v a -> Fun (Peano (Dim v)) a (c (v a)) -> c (v a)
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect v a
v
(Fun (Peano (Dim v)) a (c (v a)) -> c (v a))
-> Fun (Peano (Dim v)) a (c (v a)) -> c (v a)
forall a b. (a -> b) -> a -> b
$ (forall x y. Data x => c (x -> y) -> x -> c y)
-> c (Fn (Peano (Dim v)) a (v a))
-> Fun (Peano (Dim v)) a (c (v a))
forall (n :: PeanoNum) a (c :: * -> *) r.
(ArityPeano n, Data a) =>
(forall x y. Data x => c (x -> y) -> x -> c y)
-> c (Fn n a r) -> Fun n a (c r)
gfoldlF forall x y. Data x => c (x -> y) -> x -> c y
f (Fn (Peano (Dim v)) a (v a) -> c (Fn (Peano (Dim v)) a (v a))
forall x. x -> c x
inj (Fn (Peano (Dim v)) a (v a) -> c (Fn (Peano (Dim v)) a (v a)))
-> Fn (Peano (Dim v)) a (v a) -> c (Fn (Peano (Dim v)) a (v a))
forall a b. (a -> b) -> a -> b
$ Fun (Peano (Dim v)) a (v a) -> Fn (Peano (Dim v)) a (v a)
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun (Peano (Dim v)) a (v a)
forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct :: Fun (Peano (Dim v)) a (v a)))
gunfold :: forall con c v a. (Vector v a, Data a)
=> (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r)
-> con -> c (v a)
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> con -> c (v a)
gunfold forall b r. Data b => c (b -> r) -> c r
f forall r. r -> c r
inj con
_
= (forall b r. Data b => c (b -> r) -> c r)
-> T_gunfold c (v a) a (Peano (Dim v)) -> c (v a)
forall (n :: PeanoNum) a (c :: * -> *) r.
(ArityPeano n, Data a) =>
(forall b x. Data b => c (b -> x) -> c x)
-> T_gunfold c r a n -> c r
gunfoldF forall b r. Data b => c (b -> r) -> c r
f T_gunfold c (v a) a (Peano (Dim v))
gun
where
con :: Fun (Peano (Dim v)) a (v a)
con = Fun (Peano (Dim v)) a (v a)
forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct :: Fun (Peano (Dim v)) a (v a)
gun :: T_gunfold c (v a) a (Peano (Dim v))
gun = c (Fn (Peano (Dim v)) a (v a))
-> T_gunfold c (v a) a (Peano (Dim v))
forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gunfold c r a n
T_gunfold (Fn (Peano (Dim v)) a (v a) -> c (Fn (Peano (Dim v)) a (v a))
forall r. r -> c r
inj (Fn (Peano (Dim v)) a (v a) -> c (Fn (Peano (Dim v)) a (v a)))
-> Fn (Peano (Dim v)) a (v a) -> c (Fn (Peano (Dim v)) a (v a))
forall a b. (a -> b) -> a -> b
$ Fun (Peano (Dim v)) a (v a) -> Fn (Peano (Dim v)) a (v a)
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun Fun (Peano (Dim v)) a (v a)
con) :: T_gunfold c (v a) a (Peano (Dim v))
gfoldlF :: (ArityPeano n, Data a)
=> (forall x y. Data x => c (x -> y) -> x -> c y)
-> c (Fn n a r) -> Fun n a (c r)
gfoldlF :: (forall x y. Data x => c (x -> y) -> x -> c y)
-> c (Fn n a r) -> Fun n a (c r)
gfoldlF forall x y. Data x => c (x -> y) -> x -> c y
f c (Fn n a r)
c0 = (forall (k :: PeanoNum).
T_gfoldl c r a ('S k) -> a -> T_gfoldl c r a k)
-> (T_gfoldl c r a 'Z -> c r) -> T_gfoldl c r a n -> Fun n a (c r)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(T_gfoldl c) a
x -> c (Fn k a r) -> T_gfoldl c r a k
forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gfoldl c r a n
T_gfoldl (c (a -> Fn k a r) -> a -> c (Fn k a r)
forall x y. Data x => c (x -> y) -> x -> c y
f c (Fn ('S k) a r)
c (a -> Fn k a r)
c a
x))
(\(T_gfoldl c (Fn 'Z a r)
c) -> c r
c (Fn 'Z a r)
c)
(c (Fn n a r) -> T_gfoldl c r a n
forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gfoldl c r a n
T_gfoldl c (Fn n a r)
c0)
newtype T_gfoldl c r a n = T_gfoldl (c (Fn n a r))
{-# RULES
"cvec/vector" forall v.
cvec (vector v) = v
#-}
type instance Dim Complex = 2
instance Vector Complex a where
construct :: Fun (Peano (Dim Complex)) a (Complex a)
construct = Fn ('S ('S 'Z)) a (Complex a) -> Fun ('S ('S 'Z)) a (Complex a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn ('S ('S 'Z)) a (Complex a)
forall a. a -> a -> Complex a
(:+)
inspect :: Complex a -> Fun (Peano (Dim Complex)) a b -> b
inspect (a
x :+ a
y) (Fun Fn (Peano (Dim Complex)) a b
f) = Fn (Peano (Dim Complex)) a b
a -> a -> b
f a
x a
y
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim Identity = 1
instance Vector Identity a where
construct :: Fun (Peano (Dim Identity)) a (Identity a)
construct = Fn ('S 'Z) a (Identity a) -> Fun ('S 'Z) a (Identity a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn ('S 'Z) a (Identity a)
forall a. a -> Identity a
Identity
inspect :: Identity a -> Fun (Peano (Dim Identity)) a b -> b
inspect (Identity a
x) (Fun Fn (Peano (Dim Identity)) a b
f) = Fn (Peano (Dim Identity)) a b
a -> b
f a
x
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,) a) = 2
instance (b~a) => Vector ((,) b) a where
construct :: Fun (Peano (Dim ((,) b))) a (b, a)
construct = Fn ('S ('S 'Z)) a (b, a) -> Fun ('S ('S 'Z)) a (b, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,)
inspect :: (b, a) -> Fun (Peano (Dim ((,) b))) a b -> b
inspect (b
a,a
b) (Fun Fn (Peano (Dim ((,) b))) a b
f) = Fn (Peano (Dim ((,) b))) a b
b -> a -> b
f b
a a
b
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,,) a b) = 3
instance (b~a, c~a) => Vector ((,,) b c) a where
construct :: Fun (Peano (Dim ((,,) b c))) a (b, c, a)
construct = Fn ('S ('S ('S 'Z))) a (b, c, a)
-> Fun ('S ('S ('S 'Z))) a (b, c, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,)
inspect :: (b, c, a) -> Fun (Peano (Dim ((,,) b c))) a b -> b
inspect (b
a,c
b,a
c) (Fun Fn (Peano (Dim ((,,) b c))) a b
f) = Fn (Peano (Dim ((,,) b c))) a b
b -> c -> a -> b
f b
a c
b a
c
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,,,) a b c) = 4
instance (b~a, c~a, d~a) => Vector ((,,,) b c d) a where
construct :: Fun (Peano (Dim ((,,,) b c d))) a (b, c, d, a)
construct = Fn ('S ('S ('S ('S 'Z)))) a (b, c, d, a)
-> Fun ('S ('S ('S ('S 'Z)))) a (b, c, d, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,)
inspect :: (b, c, d, a) -> Fun (Peano (Dim ((,,,) b c d))) a b -> b
inspect (b
a,c
b,d
c,a
d) (Fun Fn (Peano (Dim ((,,,) b c d))) a b
f) = Fn (Peano (Dim ((,,,) b c d))) a b
b -> c -> d -> a -> b
f b
a c
b d
c a
d
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,,,,) a b c d) = 5
instance (b~a, c~a, d~a, e~a) => Vector ((,,,,) b c d e) a where
construct :: Fun (Peano (Dim ((,,,,) b c d e))) a (b, c, d, e, a)
construct = Fn ('S ('S ('S ('S ('S 'Z))))) a (b, c, d, e, a)
-> Fun ('S ('S ('S ('S ('S 'Z))))) a (b, c, d, e, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,)
inspect :: (b, c, d, e, a) -> Fun (Peano (Dim ((,,,,) b c d e))) a b -> b
inspect (b
a,c
b,d
c,e
d,a
e) (Fun Fn (Peano (Dim ((,,,,) b c d e))) a b
f) = Fn (Peano (Dim ((,,,,) b c d e))) a b
b -> c -> d -> e -> a -> b
f b
a c
b d
c e
d a
e
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,,,,,) a b c d e) = 6
instance (b~a, c~a, d~a, e~a, f~a) => Vector ((,,,,,) b c d e f) a where
construct :: Fun (Peano (Dim ((,,,,,) b c d e f))) a (b, c, d, e, f, a)
construct = Fn ('S ('S ('S ('S ('S ('S 'Z)))))) a (b, c, d, e, f, a)
-> Fun ('S ('S ('S ('S ('S ('S 'Z)))))) a (b, c, d, e, f, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,,)
inspect :: (b, c, d, e, f, a)
-> Fun (Peano (Dim ((,,,,,) b c d e f))) a b -> b
inspect (b
a,c
b,d
c,e
d,f
e,a
f) (Fun Fn (Peano (Dim ((,,,,,) b c d e f))) a b
fun) = Fn (Peano (Dim ((,,,,,) b c d e f))) a b
b -> c -> d -> e -> f -> a -> b
fun b
a c
b d
c e
d f
e a
f
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,,,,,,) a b c d e f) = 7
instance (b~a, c~a, d~a, e~a, f~a, g~a) => Vector ((,,,,,,) b c d e f g) a where
construct :: Fun (Peano (Dim ((,,,,,,) b c d e f g))) a (b, c, d, e, f, g, a)
construct = Fn ('S ('S ('S ('S ('S ('S ('S 'Z))))))) a (b, c, d, e, f, g, a)
-> Fun
('S ('S ('S ('S ('S ('S ('S 'Z))))))) a (b, c, d, e, f, g, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,,,)
inspect :: (b, c, d, e, f, g, a)
-> Fun (Peano (Dim ((,,,,,,) b c d e f g))) a b -> b
inspect (b
a,c
b,d
c,e
d,f
e,g
f,a
g) (Fun Fn (Peano (Dim ((,,,,,,) b c d e f g))) a b
fun) = Fn (Peano (Dim ((,,,,,,) b c d e f g))) a b
b -> c -> d -> e -> f -> g -> a -> b
fun b
a c
b d
c e
d f
e g
f a
g
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim Proxy = 0
instance Vector Proxy a where
construct :: Fun (Peano (Dim Proxy)) a (Proxy a)
construct = Fn 'Z a (Proxy a) -> Fun 'Z a (Proxy a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn 'Z a (Proxy a)
forall k (t :: k). Proxy t
Proxy
inspect :: Proxy a -> Fun (Peano (Dim Proxy)) a b -> b
inspect Proxy a
_ = Fun (Peano (Dim Proxy)) a b -> b
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun