{-# 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 { forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun :: Fn n a b }
instance ArityPeano n => Functor (Fun n a) where
fmap :: forall a b. (a -> b) -> Fun n a a -> Fun n a b
fmap a -> b
f Fun n a a
fun
= 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 Fun ('S k) a a
g) a
a -> forall a b (n :: PeanoNum). Fun n a b -> T_Flip a b n
T_Flip (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 (forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun Fun 'Z a a
x))
(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 :: forall a. a -> Fun n a a
pure a
x = 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
_ -> forall {k} (t :: k). Proxy t
Proxy)
(\Proxy 'Z
Proxy -> a
x)
forall {k} (t :: k). Proxy t
Proxy
(Fun Fn n a (a -> b)
f0 :: Fun n a (p -> q)) <*> :: forall a b. Fun n a (a -> b) -> Fun n a a -> Fun n a b
<*> (Fun Fn n a a
g0 :: Fun n a p)
= 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 Fn ('S k) a (a -> b)
f Fn ('S k) a a
g) a
a -> 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)
f a
a) (Fn ('S k) a a
g a
a))
(\(T_ap Fn 'Z a (a -> b)
f Fn 'Z a a
g) -> Fn 'Z a (a -> b)
f Fn 'Z a a
g)
(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 :: forall a. a -> Fun n a a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
Fun n a a
f >>= :: forall a b. Fun n a a -> (a -> Fun n a b) -> Fun n a b
>>= a -> Fun n a b
g = 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 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 (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 :: PeanoNum). t ('S k) -> (a, t k)
step t (Peano n)
z = forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (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 (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 forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t (Peano n)
t = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ 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 :: forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Int
arity = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal
instance ArityPeano 'Z where
accum :: forall (t :: PeanoNum -> *) a b.
(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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall a b. (a -> b) -> a -> b
$ t 'Z -> b
g t 'Z
t
applyFun :: forall (t :: PeanoNum -> *) a.
(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 (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun, t 'Z
t)
applyFunM :: forall (f :: * -> *) (t :: PeanoNum -> *) a.
Applicative f =>
(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 = (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun), t 'Z
t)
{-# INLINE accum #-}
{-# INLINE applyFun #-}
{-# INLINE applyFunM #-}
reverseF :: forall a b. Fun 'Z a b -> Fun 'Z a b
reverseF = forall a. a -> a
id
gunfoldF :: forall a (c :: * -> *) r.
Data a =>
(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 (Fn 'Z a r)
c
{-# INLINE reverseF #-}
{-# INLINE gunfoldF #-}
instance ArityPeano n => ArityPeano ('S n) where
accum :: forall (t :: PeanoNum -> *) a b.
(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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall a b. (a -> b) -> a -> b
$ \a
a -> forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun forall a b. (a -> b) -> 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 (forall (k :: PeanoNum). t ('S k) -> a -> t k
f t ('S n)
t a
a)
applyFun :: forall (t :: PeanoNum -> *) a.
(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') = forall (k :: PeanoNum). t ('S k) -> (a, t k)
f t ('S n)
t
(CVecPeano n a
v,t 'Z
tZ) = 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 (forall a (n :: PeanoNum). a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano a
a CVecPeano n a
v, t 'Z
tZ)
applyFunM :: forall (f :: * -> *) (t :: PeanoNum -> *) a.
Applicative f =>
(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') = forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t ('S n)
t
(f (CVecPeano n a)
vec,t 'Z
t0) = 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 (forall a (n :: PeanoNum). a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
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 :: forall a b. Fun ('S n) a b -> Fun ('S n) a b
reverseF Fun ('S n) a b
f = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall a b. (a -> b) -> a -> b
$ \a
a -> forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (forall (n :: PeanoNum) a b. ArityPeano n => Fun n a b -> Fun n a b
reverseF forall a b. (a -> b) -> 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 a (c :: * -> *) r.
Data a =>
(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 (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 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 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 (Fn ('S n) a r)
c) = forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gunfold c r a n
T_gunfold forall a b. (a -> b) -> a -> b
$ forall b x. Data b => c (b -> x) -> c x
f c (Fn ('S 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 :: forall (n :: PeanoNum) a b. Fun n a b -> Fun ('S n) a b
constFun (Fun Fn n a b
f) = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun 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 :: forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst = coerce :: forall a b. Coercible a b => a -> b
coerce
{-# INLINE curryFirst #-}
uncurryFirst :: (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst :: forall a (n :: PeanoNum) b. (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst = coerce :: forall a b. Coercible a b => a -> b
coerce
{-# INLINE uncurryFirst #-}
curryLast :: ArityPeano n => Fun ('S n) a b -> Fun n a (a -> b)
{-# INLINE curryLast #-}
curryLast :: forall (n :: PeanoNum) a b.
ArityPeano n =>
Fun ('S n) a b -> Fun n a (a -> b)
curryLast = 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 :: forall (n :: PeanoNum) (k :: PeanoNum) a b.
ArityPeano n =>
Fun (Add n k) a b -> Fun n a (Fun k a b)
curryMany = forall a b. a -> b
unsafeCoerce
apLast :: ArityPeano n => Fun ('S n) a b -> a -> Fun n a b
apLast :: 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
x = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> a -> b
$ a
x) forall a b. (a -> b) -> 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 :: forall (n :: PeanoNum) a b.
(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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall a b. (a -> b) -> a -> b
$ \a
a -> forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun forall a b. (a -> b) -> a -> b
$ Fun n a b -> Fun n a b
f forall a b. (a -> b) -> 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 :: forall (n :: PeanoNum) b a r.
ArityPeano n =>
(b -> Fun n a r) -> Fun n a (b -> r)
shuffleFun b -> Fun n a r
f0
= 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 b -> Fn ('S k) a r
f) a
a -> forall x a r (n :: PeanoNum). (x -> Fn n a r) -> T_shuffle x a r n
T_shuffle forall a b. (a -> b) -> a -> b
$ \b
x -> b -> Fn ('S k) a r
f b
x a
a)
(\(T_shuffle b -> Fn 'Z a r
f) -> b -> Fn 'Z a r
f)
(forall x a r (n :: PeanoNum). (x -> Fn n a r) -> T_shuffle x a r n
T_shuffle (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 = forall (n :: Nat) a. Arity n => Int -> ContVec n a -> a
index Int
i (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 :: forall (v :: * -> *) a. KnownNat (Dim v) => v a -> Int
length v a
_ = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Int
arity (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 :: forall a (n :: PeanoNum). a -> CVecPeano n a -> CVecPeano ('S n) a
consPeano a
a (CVecPeano forall r. Fun n a r -> r
cont) = forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano forall a b. (a -> b) -> a -> b
$ \Fun ('S n) a r
f -> forall r. Fun n a r -> r
cont forall a b. (a -> b) -> a -> b
$ 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 :: forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec = coerce :: forall a b. Coercible a b => a -> b
coerce
instance Arity n => Vector (ContVec n) a where
construct :: Fun (Peano (Dim (ContVec n))) a (ContVec n a)
construct = 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 CVecPeano ('S k) a -> CVecPeano (Peano n) a
f) a
a -> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) -> forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec forall a b. (a -> b) -> a -> b
$ CVecPeano 'Z a -> CVecPeano (Peano n) a
f (forall (n :: PeanoNum) a.
(forall r. Fun n a r -> r) -> CVecPeano n a
CVecPeano forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun))
(forall (n_tot :: PeanoNum) a (n :: PeanoNum).
(CVecPeano n a -> CVecPeano n_tot a) -> T_mkN n_tot a n
T_mkN forall a. a -> a
id)
inspect :: forall b. 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 = forall r. Fun (Peano n) a r -> r
c 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 :: forall a b. (a -> b) -> ContVec n a -> ContVec n b
fmap = 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 :: forall a. a -> ContVec n a
pure = forall (n :: Nat) a. Arity n => a -> ContVec n a
replicate
<*> :: forall 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 forall a b. (a -> b) -> a -> b
($)
{-# INLINE pure #-}
{-# INLINE (<*>) #-}
instance (Arity n) => F.Foldable (ContVec n) where
foldr :: forall a b. (a -> b -> b) -> b -> ContVec n a -> b
foldr = 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 :: forall (f :: * -> *) a.
Applicative f =>
ContVec n (f a) -> f (ContVec n a)
sequenceA ContVec n (f a)
v = forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n (f a)
v forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (n :: PeanoNum) a b.
(Applicative f, ArityPeano n) =>
Fun n a b -> Fun n (f a) (f b)
sequenceAF 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 :: forall (f :: * -> *) (n :: PeanoNum) a b.
(Applicative f, ArityPeano n) =>
Fun n a b -> Fun n (f a) (f b)
sequenceAF (Fun Fn n a b
f0)
= 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 (Fn ('S k) a b)
f) f a
a -> 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 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 (Fn 'Z a b)
f)
(forall (f :: * -> *) a b (n :: PeanoNum).
f (Fn n a b) -> T_sequenceA f a b n
T_sequenceA (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 :: forall (v :: * -> *) a (n :: Nat).
(Vector v a, Dim v ~ n) =>
v a -> ContVec n a
cvec v a
v = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec (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 :: forall a. ContVec 0 a
empty = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec (\(Fun Fn (Peano 0) a r
r) -> Fn (Peano 0) a r
r)
fromList :: Arity n => [a] -> ContVec n a
{-# INLINE fromList #-}
fromList :: forall (n :: Nat) a. Arity n => [a] -> ContVec n a
fromList [a]
xs =
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)
step (forall {k} a (b :: k). a -> Const a b
Const [a]
xs)
where
step :: Const [a] b -> (a, Const [a] b)
step (Const [] ) = forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.Cont.fromList: too few elements"
step (Const (a
a:[a]
as)) = (a
a, 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' :: forall (n :: Nat) a. Arity n => [a] -> ContVec n a
fromList' [a]
xs =
let step :: Const [a] b -> (a, Const [a] b)
step (Const [] ) = forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.Cont.fromList': too few elements"
step (Const (a
a:[a]
as)) = (a
a, forall {k} a (b :: k). a -> Const a b
Const [a]
as)
in case 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)
step (forall {k} a (b :: k). a -> Const a b
Const [a]
xs :: Const [a] (Peano n)) of
(CVecPeano (Peano n) a
v,Const []) -> forall (n :: Nat) a. CVecPeano (Peano n) a -> ContVec n a
toContVec CVecPeano (Peano n) a
v
(CVecPeano (Peano n) a, Const [a] 'Z)
_ -> 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 :: forall (n :: Nat) a. Arity n => [a] -> Maybe (ContVec n a)
fromListM [a]
xs = case 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)
step (forall {k} a (b :: k). a -> Const a b
Const [a]
xs :: Const [a] (Peano n)) of
(Just CVecPeano (Peano n) a
v, Const []) -> forall a. a -> Maybe a
Just (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)
_ -> forall a. Maybe a
Nothing
where
step :: Const [a] b -> (Maybe a, Const [a] b)
step (Const [] ) = (forall a. Maybe a
Nothing, forall {k} a (b :: k). a -> Const a b
Const [])
step (Const (a
a:[a]
as)) = (forall a. a -> Maybe a
Just a
a , forall {k} a (b :: k). a -> Const a b
Const [a]
as)
toList :: (Arity n) => ContVec n a -> [a]
toList :: forall (n :: Nat) a. Arity n => ContVec n a -> [a]
toList = 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 :: forall (n :: Nat) a. Arity n => a -> ContVec n a
replicate a
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, forall {k} (t :: k). Proxy t
Proxy)) forall {k} (t :: k). Proxy t
Proxy
replicateM :: (Arity n, Applicative f) => f a -> f (ContVec n a)
{-# INLINE replicateM #-}
replicateM :: forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
f a -> f (ContVec n a)
replicateM f a
act
= 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, forall {k} (t :: k). Proxy t
Proxy)) forall {k} (t :: k). Proxy t
Proxy
generate :: (Arity n) => (Int -> a) -> ContVec n a
{-# INLINE generate #-}
generate :: forall (n :: Nat) a. Arity n => (Int -> a) -> ContVec n a
generate Int -> a
f =
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 Int
n) -> (Int -> a
f Int
n, forall {k} a (b :: k). a -> Const a b
Const (Int
n forall a. Num a => a -> a -> a
+ Int
1))) (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 :: forall (f :: * -> *) (n :: Nat) a.
(Applicative f, Arity n) =>
(Int -> f a) -> f (ContVec n a)
generateM Int -> f a
f =
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 Int
n) -> (Int -> f a
f Int
n, forall {k} a (b :: k). a -> Const a b
Const (Int
n forall a. Num a => a -> a -> a
+ Int
1))) (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 :: forall (n :: Nat) b a. Arity n => (b -> (a, b)) -> b -> ContVec n a
unfoldr b -> (a, b)
f b
b0 =
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
b) -> let (a
a,b
b') = b -> (a, b)
f b
b in (a
a, forall {k} a (b :: k). a -> Const a b
Const b
b'))
(forall {k} a (b :: k). a -> Const a b
Const b
b0)
basis :: (Num a, Arity n) => Int -> ContVec n a
{-# INLINE basis #-}
basis :: forall a (n :: Nat). (Num a, Arity n) => Int -> ContVec n a
basis Int
n0 =
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 Int
n) -> (if Int
n forall a. Eq a => a -> a -> Bool
== Int
0 then a
1 else a
0, forall {k} a (b :: k). a -> Const a b
Const (Int
n forall a. Num a => a -> a -> a
- Int
1)))
(forall {k} a (b :: k). a -> Const a b
Const Int
n0)
mk1 :: a -> ContVec 1 a
mk1 :: forall a. a -> ContVec 1 a
mk1 a
a1 = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 1) a r
f) -> Fn (Peano 1) a r
f a
a1
{-# INLINE mk1 #-}
mk2 :: a -> a -> ContVec 2 a
mk2 :: forall a. a -> a -> ContVec 2 a
mk2 a
a1 a
a2 = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 2) a r
f) -> Fn (Peano 2) a r
f a
a1 a
a2
{-# INLINE mk2 #-}
mk3 :: a -> a -> a -> ContVec 3 a
mk3 :: forall a. a -> a -> a -> ContVec 3 a
mk3 a
a1 a
a2 a
a3 = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 3) a r
f) -> Fn (Peano 3) a r
f a
a1 a
a2 a
a3
{-# INLINE mk3 #-}
mk4 :: a -> a -> a -> a -> ContVec 4 a
mk4 :: forall a. a -> a -> a -> a -> ContVec 4 a
mk4 a
a1 a
a2 a
a3 a
a4 = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 4) a r
f) -> Fn (Peano 4) a r
f a
a1 a
a2 a
a3 a
a4
{-# INLINE mk4 #-}
mk5 :: a -> a -> a -> a -> a -> ContVec 5 a
mk5 :: forall a. a -> a -> a -> a -> a -> ContVec 5 a
mk5 a
a1 a
a2 a
a3 a
a4 a
a5 = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 5) a r
f) -> Fn (Peano 5) 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 :: forall a. a -> a -> a -> a -> a -> a -> ContVec 6 a
mk6 a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 6) a r
f) -> Fn (Peano 6) 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 :: forall a. 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 (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 7) a r
f) -> Fn (Peano 7) 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 :: forall a. 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 (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \(Fun Fn (Peano 8) a r
f) -> Fn (Peano 8) 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 :: forall (n :: Nat) a b.
Arity n =>
(a -> b) -> ContVec n a -> ContVec n b
map = forall (n :: Nat) a b.
Arity n =>
(Int -> a -> b) -> ContVec n a -> ContVec n b
imap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
imap :: (Arity n) => (Int -> a -> b) -> ContVec n a -> ContVec n b
{-# INLINE imap #-}
imap :: forall (n :: Nat) a b.
Arity n =>
(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 (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$
forall r. Fun (Peano n) a r -> r
contA forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(a -> f b) -> ContVec n a -> f (ContVec n b)
mapM = forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(Int -> a -> f b) -> ContVec n a -> f (ContVec n b)
imapM forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: 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
f ContVec n a
v
= forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
forall a b. (a -> b) -> a -> 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 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_ :: forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(a -> f b) -> ContVec n a -> f ()
mapM_ a -> f b
f = forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl (\f ()
m a
a -> f ()
m forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> a -> f b
f a
a forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (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_ :: forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(Int -> a -> f b) -> ContVec n a -> f ()
imapM_ Int -> a -> f b
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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> a -> f b
f Int
i a
a forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (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 :: 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 Fn n b r
funB) =
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 Int
i f (Fn ('S k) b r)
m) a
a -> forall a (m :: * -> *) r (n :: PeanoNum).
Int -> m (Fn n a r) -> T_mapM a m r n
T_mapM (Int
iforall a. Num a => a -> a -> a
+Int
1) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> a -> b
($) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Fn ('S k) b r)
m 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 (Fn 'Z b r)
m)
(forall a (m :: * -> *) r (n :: PeanoNum).
Int -> m (Fn n a r) -> T_mapM a m r n
T_mapM Int
0 (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 :: forall (n :: PeanoNum) a b r.
ArityPeano n =>
(Int -> a -> b) -> Fun n b r -> Fun n a r
imapF Int -> a -> b
f (Fun Fn n b r
funB) =
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 Int
i Fn ('S k) b r
g) a
b -> forall a r (n :: PeanoNum). Int -> Fn n a r -> T_map a r n
T_map (Int
iforall a. Num a => a -> a -> a
+Int
1) (Fn ('S k) b r
g (Int -> a -> b
f Int
i a
b)))
(\(T_map Int
_ Fn 'Z b r
r) -> Fn 'Z b r
r)
( 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 :: forall (n :: Nat) b a.
Arity n =>
(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 (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$
forall r. Fun (Peano n) a r -> r
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (n :: Nat) a.
Arity n =>
(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 (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$
forall r. Fun (Peano n) a r -> r
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: 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 (Fun Fn ('S n) b r
fun0)
= 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 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 :: forall (k :: PeanoNum). 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 forall r a (n :: PeanoNum). a -> Fn n a r -> T_scanl r a n
T_scanl b
b' (Fn ('S 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 = forall r a (n :: PeanoNum). a -> Fn n a r -> T_scanl r a n
T_scanl b
b0 (Fn ('S 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 :: forall (n :: PeanoNum) a r.
ArityPeano n =>
(a -> a -> a) -> Fun n a r -> Fun n a r
scanl1F a -> a -> a
f (Fun Fn n a r
fun0) = 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 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 :: forall (k :: PeanoNum). 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 = forall r a (n :: PeanoNum). Maybe a -> Fn n a r -> T_scanl1 r a n
T_scanl1 (forall a. a -> Maybe a
Just a
a) (Fn ('S 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 forall r a (n :: PeanoNum). Maybe a -> Fn n a r -> T_scanl1 r a n
T_scanl1 (forall a. a -> Maybe a
Just a
a') (Fn ('S 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 = forall r a (n :: PeanoNum). Maybe a -> Fn n a r -> T_scanl1 r a n
T_scanl1 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 :: forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence = forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(a -> f b) -> ContVec n a -> f (ContVec n b)
mapM forall a. a -> a
id
{-# INLINE sequence #-}
sequence_ :: (Arity n, Applicative f) => ContVec n (f a) -> f ()
sequence_ :: forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f ()
sequence_ = forall (n :: Nat) (f :: * -> *) a b.
(Arity n, Applicative f) =>
(a -> f b) -> ContVec n a -> f ()
mapM_ forall a. a -> a
id
{-# INLINE sequence_ #-}
distribute :: (Functor f, Arity n) => f (ContVec n a) -> ContVec n (f a)
{-# INLINE distribute #-}
distribute :: forall (f :: * -> *) (n :: Nat) a.
(Functor f, Arity n) =>
f (ContVec n a) -> ContVec n (f a)
distribute f (ContVec n a)
f0
= 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)
step Const (f [a]) (Peano n)
start
where
step :: Const (f [a]) b -> (f a, Const (f [a]) b)
step (Const f [a]
f) = ( forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
x:[a]
_) -> a
x) f [a]
f
, forall {k} a (b :: k). a -> Const a b
Const forall a b. (a -> b) -> a -> b
$ 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 = forall {k} a (b :: k). a -> Const a b
Const (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 :: forall (f :: * -> *) (n :: Nat) a b.
(Functor f, Arity n) =>
(a -> ContVec n b) -> f a -> ContVec n (f b)
collect a -> ContVec n b
f = forall (f :: * -> *) (n :: Nat) a.
(Functor f, Arity n) =>
f (ContVec n a) -> ContVec n (f a)
distribute forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> ContVec n b
f
{-# INLINE collect #-}
tail :: Arity n => ContVec (n+1) a -> ContVec n a
tail :: forall (n :: Nat) a. Arity n => ContVec (n + 1) a -> ContVec n a
tail (ContVec forall r. Fun (Peano (n + 1)) a r -> r
cont) = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \Fun (Peano n) a r
f -> forall r. Fun (Peano (n + 1)) a r -> r
cont forall a b. (a -> b) -> a -> b
$ 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 :: forall (n :: Nat) a.
Arity n =>
a -> ContVec n a -> ContVec (n + 1) a
cons a
a (ContVec forall r. Fun (Peano n) a r -> r
cont) = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \Fun (Peano (n + 1)) a r
f -> forall r. Fun (Peano n) a r -> r
cont forall a b. (a -> b) -> a -> b
$ forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun (Peano (n + 1)) a r
f a
a
{-# INLINE cons #-}
consV :: Arity n => ContVec 1 a -> ContVec n a -> ContVec (n+1) a
{-# INLINE consV #-}
consV :: forall (n :: Nat) a.
Arity n =>
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 (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \Fun (Peano (n + 1)) a r
f -> forall r. Fun (Peano n) a r -> r
cont forall a b. (a -> b) -> a -> b
$ forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun (Peano (n + 1)) a r
f forall a b. (a -> b) -> a -> b
$ forall r. Fun (Peano 1) a r -> r
cont1 forall a b. (a -> b) -> a -> b
$ forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall a. a -> a
id
snoc :: Arity n => a -> ContVec n a -> ContVec (n+1) a
snoc :: forall (n :: Nat) a.
Arity n =>
a -> ContVec n a -> ContVec (n + 1) a
snoc a
a (ContVec forall r. Fun (Peano n) a r -> r
cont) = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \Fun (Peano (n + 1)) a r
f -> forall r. Fun (Peano n) a r -> r
cont forall a b. (a -> b) -> a -> b
$ forall (n :: PeanoNum) a b.
ArityPeano n =>
Fun ('S n) a b -> a -> Fun n a b
apLast Fun (Peano (n + 1)) 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 :: forall (n :: Nat) (k :: Nat) a.
(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
concat ContVec n a
v ContVec k a
u = forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec k a
u
forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
forall a b. (a -> b) -> a -> b
$ forall (n :: PeanoNum) (k :: PeanoNum) a b.
ArityPeano n =>
Fun (Add n k) a b -> Fun n a (Fun k a b)
curryMany forall (v :: * -> *) a. Vector v a => Fun (Peano (Dim v)) a (v a)
construct
reverse :: Arity n => ContVec n a -> ContVec n a
reverse :: forall (n :: Nat) a. Arity n => ContVec n a -> ContVec n a
reverse (ContVec forall r. Fun (Peano n) a r -> r
cont) = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ forall r. Fun (Peano n) a r -> r
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (n :: Nat) a b c.
Arity n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith = forall (n :: Nat) a b c.
Arity n =>
(Int -> a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
izipWith forall b c a. (b -> c) -> (a -> b) -> a -> 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 :: forall (n :: Nat) a b c d.
Arity n =>
(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 = 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 (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 :: 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
f ContVec n a
vecA ContVec n b
vecB = forall (n :: Nat) a.
(forall r. Fun (Peano n) a r -> r) -> ContVec n a
ContVec forall a b. (a -> b) -> a -> b
$ \Fun (Peano n) c r
funC ->
forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n b
vecB
forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
vecA
forall a b. (a -> b) -> a -> b
$ 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 :: forall (n :: Nat) a b c d.
Arity n =>
(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 = 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 (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 :: forall (n :: Nat) (f :: * -> *) a b c.
(Arity n, Applicative f) =>
(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 = forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence forall a b. (a -> b) -> a -> b
$ 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_ :: forall (n :: Nat) (f :: * -> *) a b c.
(Arity n, Applicative f) =>
(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 = forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f ()
sequence_ (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 :: forall (n :: Nat) (f :: * -> *) a b c.
(Arity n, Applicative f) =>
(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 = forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence forall a b. (a -> b) -> a -> b
$ 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_ :: forall (n :: Nat) (f :: * -> *) a b c.
(Arity n, Applicative f) =>
(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 = forall (n :: Nat) (f :: * -> *) a.
(Arity n, Applicative f) =>
ContVec n (f a) -> f ()
sequence_ (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 :: 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 Fn n c r
g0) =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[a]
v -> 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 Int
i (a
a:[a]
as) Fn ('S k) c r
g) b
b -> forall a c r (n :: PeanoNum).
Int -> [a] -> Fn n c r -> T_izip a c r n
T_izip (Int
iforall a. Num a => a -> a -> a
+Int
1) [a]
as (Fn ('S k) c r
g 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) -> Fn 'Z c r
x)
(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)
) forall (n :: PeanoNum) a. ArityPeano n => Fun n a [a]
makeList
makeList :: ArityPeano n => Fun n a [a]
{-# INLINE makeList #-}
makeList :: forall (n :: PeanoNum) a. ArityPeano n => Fun n a [a]
makeList = 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 [a] -> [a]
xs) a
x -> forall {k} a (b :: k). a -> Const a b
Const ([a] -> [a]
xs forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
xforall a. a -> [a] -> [a]
:)))
(\(Const [a] -> [a]
xs) -> [a] -> [a]
xs [])
(forall {k} a (b :: k). a -> Const a b
Const 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 :: forall (n :: Nat) a r. 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) = 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 :: forall (v :: * -> *) a (n :: Nat).
(Vector v a, Dim v ~ n) =>
ContVec n a -> v a
vector = forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec 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 :: forall (n :: Nat) a. (Arity n, 1 <= n) => ContVec n a -> a
head
= forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec
forall a b. (a -> b) -> 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 (\(Const Maybe a
m) a
a -> forall {k} a (b :: k). a -> Const a b
Const forall a b. (a -> b) -> a -> b
$ case Maybe a
m of { Maybe a
Nothing -> forall a. a -> Maybe a
Just a
a; Maybe a
x -> Maybe a
x })
(\(Const (Just a
x)) -> a
x)
(forall {k} a (b :: k). a -> Const a b
Const forall a. Maybe a
Nothing)
index :: Arity n => Int -> ContVec n a -> a
{-# INLINE index #-}
index :: forall (n :: Nat) a. Arity n => Int -> ContVec n a -> a
index Int
n
| Int
n forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.Cont.index: index out of range"
| Bool
otherwise = forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec forall a b. (a -> b) -> 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
(\(Const Either Int a
x) a
a -> forall {k} a (b :: k). a -> Const a b
Const forall a b. (a -> b) -> a -> b
$ case Either Int a
x of
Left Int
0 -> forall a b. b -> Either a b
Right a
a
Left Int
i -> forall a b. a -> Either a b
Left (Int
i 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
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Vector.Fixed.index: index out of range"
Right a
a -> a
a
)
(forall {k} a (b :: k). a -> Const a b
Const (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 :: forall (n :: Nat) (f :: * -> *) a.
(Arity n, Functor f) =>
Int -> (a -> f a) -> ContVec n a -> f (ContVec n a)
element Int
i a -> f a
f ContVec n a
v = forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
forall a b. (a -> b) -> a -> b
$ 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 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 :: 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
n a -> f a
f (Fun Fn n a r
fun0) = 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 :: forall (k :: PeanoNum). 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 = 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fn ('S k) a r
fun 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 = 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 forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (Int
iforall a. Num a => a -> a -> a
-Int
1, Fn ('S k) a r
fun a
a)
step (T_lens (Right f (Fn ('S k) a r)
fun)) a
a = 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> a -> b
$ a
a) f (Fn ('S 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)
_)) = 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 (Fn 'Z a r)
r
start :: T_lens f a r n
start :: T_lens f a r n
start = 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 forall a b. (a -> b) -> a -> b
$ 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 :: forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl b -> a -> b
f = 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 :: forall (n :: Nat) b a.
Arity n =>
(b -> Int -> a -> b) -> b -> ContVec n a -> b
ifoldl b -> Int -> a -> b
f b
b ContVec n a
v
= forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect ContVec n a
v
forall a b. (a -> b) -> 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 Int
i b
r) a
a -> forall {k} b (n :: k). Int -> b -> T_ifoldl b n
T_ifoldl (Int
iforall 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)
(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 :: forall (n :: Nat) (m :: * -> *) b a.
(Arity n, Monad m) =>
(b -> a -> m b) -> b -> ContVec n a -> m b
foldM b -> a -> m b
f b
x
= 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}) (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 :: forall (n :: Nat) (m :: * -> *) b a.
(Arity n, Monad m) =>
(b -> Int -> a -> m b) -> b -> ContVec n a -> m b
ifoldM b -> Int -> a -> m b
f b
x
= 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}) (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 :: forall (n :: Nat) a.
(Arity n, 1 <= n) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 a -> a -> a
f
= forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec
forall a b. (a -> b) -> 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 (\(Const Maybe a
r ) a
a -> forall {k} a (b :: k). a -> Const a b
Const forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe 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)
(forall {k} a (b :: k). a -> Const a b
Const forall a. Maybe a
Nothing)
foldr :: Arity n => (a -> b -> b) -> b -> ContVec n a -> b
{-# INLINE foldr #-}
foldr :: forall (n :: Nat) a b.
Arity n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr = forall (n :: Nat) a b.
Arity n =>
(Int -> a -> b -> b) -> b -> ContVec n a -> b
ifoldr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
ifoldr :: Arity n => (Int -> a -> b -> b) -> b -> ContVec n a -> b
{-# INLINE ifoldr #-}
ifoldr :: forall (n :: Nat) a b.
Arity n =>
(Int -> a -> b -> b) -> b -> ContVec n a -> b
ifoldr Int -> a -> b -> b
f b
z
= forall (n :: Nat) a r. Fun (Peano n) a r -> ContVec n a -> r
runContVec
forall a b. (a -> b) -> 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 Int
i b -> b
g) a
a -> forall {k} b (n :: k). Int -> (b -> b) -> T_ifoldr b n
T_ifoldr (Int
iforall a. Num a => a -> a -> a
+Int
1) (b -> b
g 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)
(forall {k} b (n :: k). Int -> (b -> b) -> T_ifoldr b n
T_ifoldr Int
0 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 :: forall a (n :: Nat). (Num a, Arity n) => ContVec n a -> a
sum = forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl forall a. Num a => a -> a -> a
(+) a
0
{-# INLINE sum #-}
minimum :: (Ord a, Arity n, 1<=n) => ContVec n a -> a
minimum :: forall a (n :: Nat). (Ord a, Arity n, 1 <= n) => ContVec n a -> a
minimum = forall (n :: Nat) a.
(Arity n, 1 <= n) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 forall a. Ord a => a -> a -> a
min
{-# INLINE minimum #-}
maximum :: (Ord a, Arity n, 1<=n) => ContVec n a -> a
maximum :: forall a (n :: Nat). (Ord a, Arity n, 1 <= n) => ContVec n a -> a
maximum = forall (n :: Nat) a.
(Arity n, 1 <= n) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 forall a. Ord a => a -> a -> a
max
{-# INLINE maximum #-}
and :: Arity n => ContVec n Bool -> Bool
and :: forall (n :: Nat). Arity n => ContVec n Bool -> Bool
and = 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 :: forall (n :: Nat). Arity n => ContVec n Bool -> Bool
or = 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 :: forall (n :: Nat) a. Arity n => (a -> Bool) -> ContVec n a -> Bool
all a -> Bool
f = 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 :: forall (n :: Nat) a. Arity n => (a -> Bool) -> ContVec n a -> Bool
any a -> Bool
f = 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
False
{-# INLINE any #-}
find :: Arity n => (a -> Bool) -> ContVec n a -> Maybe a
find :: forall (n :: Nat) a.
Arity n =>
(a -> Bool) -> ContVec n a -> Maybe a
find a -> Bool
f = forall (n :: Nat) b a.
Arity n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl (\Maybe a
r a
x -> Maybe a
r forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> if a -> Bool
f a
x then forall a. a -> Maybe a
Just a
x else forall a. Maybe a
Nothing) 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 (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
f forall x. x -> c x
inj v a
v
= forall (v :: * -> *) a b.
Vector v a =>
v a -> Fun (Peano (Dim v)) a b -> b
inspect v a
v
forall a b. (a -> b) -> a -> b
$ 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 (forall x. x -> c x
inj forall a b. (a -> b) -> a -> b
$ forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (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 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
f forall r. r -> c r
inj con
_
= 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 = 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 = forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gunfold c r a n
T_gunfold (forall r. r -> c r
inj forall a b. (a -> b) -> a -> b
$ 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 (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 c (Fn n a r)
c0 = 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 (Fn ('S k) a r)
c) a
x -> forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gfoldl c r a n
T_gfoldl (forall x y. Data x => c (x -> y) -> x -> c y
f c (Fn ('S k) a r)
c a
x))
(\(T_gfoldl c (Fn 'Z a r)
c) -> c (Fn 'Z a r)
c)
(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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall a. a -> a -> Complex a
(:+)
inspect :: forall b. 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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall a. a -> Identity a
Identity
inspect :: forall b. 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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,)
inspect :: forall b. (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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,)
inspect :: forall b. (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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,)
inspect :: forall b. (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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,)
inspect :: forall b.
(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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,,)
inspect :: forall b.
(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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,,,)
inspect :: forall b.
(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
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 = forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun forall {k} (t :: k). Proxy t
Proxy
inspect :: forall b. Proxy a -> Fun (Peano (Dim Proxy)) a b -> b
inspect Proxy a
_ = forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun