{-# LANGUAGE CPP #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vector.Fixed.Cont (
PeanoNum(..)
, N1,N2,N3,N4,N5,N6,N7,N8
, Peano
, Add
, Fn
, Fun(..)
, Arity
, ArityPeano(..)
, apply
, applyM
, Index(..)
, constFun
, curryFirst
, uncurryFirst
, curryLast
, curryMany
, apLast
, shuffleFun
, withFun
, dimapFun
, Dim
, Vector(..)
, length
, ContVec(..)
, consPeano
, 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
, foldl'
, foldl1
, foldl1'
, foldr
, ifoldl
, 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.Kind (Type)
import Data.Functor.Identity (Identity(..))
import Data.Typeable (Proxy(..))
import qualified Data.Foldable as F
import qualified Data.Traversable as T
import Unsafe.Coerce (unsafeCoerce)
import GHC.TypeLits
import GHC.Exts (Proxy#, proxy#)
import Prelude ( Bool(..), Int, Maybe(..), Either(..)
, Eq(..), Ord(..), Num(..), Functor(..), Applicative(..), Monad(..)
, Semigroup(..), Monoid(..)
, (.), ($), (&&), (||), (<$>), id, error, otherwise, fst
)
data PeanoNum = Z
| S PeanoNum
type N1 = S Z
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
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 :: Type) (b :: Type) 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 (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
forall (t :: PeanoNum -> *) a b.
(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 -> 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 :: forall a. 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
forall (t :: PeanoNum -> *) a b.
(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)) <*> :: 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 (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
forall (t :: PeanoNum -> *) a b.
(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 -> 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 :: forall a. a -> Fun n a a
return = a -> Fun n a a
forall a. a -> Fun n a a
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 = (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 a b. 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 (>>=) #-}
newtype T_Flip a b n = T_Flip (Fun n a b)
data T_ap a b c n = T_ap (Fn n a b) (Fn n a c)
type Arity n = ArityPeano (Peano n)
class ArityPeano n where
accum :: (forall k. t ('S k) -> a -> t k)
-> (t 'Z -> b)
-> t n
-> Fun n a b
accumPeano
:: (forall k. ArityPeano 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
-> (ContVec n a, t 'Z)
applyFunM :: Applicative f
=> (forall k. t ('S k) -> (f a, t k))
-> t n
-> (f (ContVec n a), t 'Z)
reducePeano :: (forall k. t ('S k) -> t k)
-> t n
-> t 'Z
peanoToInt :: Proxy# n -> Int
dictionaryPred :: (n ~ S k) => Proxy# n -> (ArityPeano k => r) -> r
newtype T_gunfold c r a n = T_gunfold (c (Fn n a r))
apply :: ArityPeano n
=> (forall k. t ('S k) -> (a, t k))
-> t n
-> ContVec n a
{-# INLINE apply #-}
apply :: forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> ContVec n a
apply forall (k :: PeanoNum). t ('S k) -> (a, t k)
step t n
z = (ContVec n a, t 'Z) -> ContVec n a
forall a b. (a, b) -> a
fst ((forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
forall (t :: PeanoNum -> *) a.
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
applyFun t ('S k) -> (a, t k)
forall (k :: PeanoNum). t ('S k) -> (a, t k)
step t n
z)
applyM :: (Applicative f, ArityPeano n)
=> (forall k. t ('S k) -> (f a, t k))
-> t n
-> f (ContVec n a)
{-# INLINE applyM #-}
applyM :: forall (f :: * -> *) (n :: PeanoNum) (t :: PeanoNum -> *) a.
(Applicative f, ArityPeano n) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> f (ContVec n a)
applyM forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t n
t = (f (ContVec n a), t 'Z) -> f (ContVec n a)
forall a b. (a, b) -> a
fst ((f (ContVec n a), t 'Z) -> f (ContVec n a))
-> (f (ContVec n a), t 'Z) -> f (ContVec n a)
forall a b. (a -> b) -> a -> b
$ (forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (ContVec 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 (ContVec n a), t 'Z)
forall (f :: * -> *) (t :: PeanoNum -> *) a.
Applicative f =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (ContVec n a), t 'Z)
applyFunM t ('S k) -> (f a, t k)
forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t n
t
class Index (k :: PeanoNum) (n :: PeanoNum) where
getF :: Proxy# k -> Fun n a a
putF :: Proxy# k -> a -> Fun n a r -> Fun n a r
lensF :: Functor f => Proxy# k -> (a -> f a) -> Fun n a r -> Fun n a (f r)
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 = 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
accumPeano :: forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). ArityPeano k => t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t 'Z -> Fun 'Z a b
accumPeano forall (k :: PeanoNum). ArityPeano k => 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 (t :: PeanoNum -> *) a.
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t 'Z -> (ContVec 'Z a, t 'Z)
applyFun forall (k :: PeanoNum). t ('S k) -> (a, t k)
_ t 'Z
t = ((forall r. Fun 'Z a r -> r) -> ContVec 'Z a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec Fun 'Z a r -> r
Fun 'Z a r -> Fn 'Z a r
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 (f :: * -> *) (t :: PeanoNum -> *) a.
Applicative f =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t 'Z -> (f (ContVec 'Z a), t 'Z)
applyFunM forall (k :: PeanoNum). t ('S k) -> (f a, t k)
_ t 'Z
t = (ContVec 'Z a -> f (ContVec 'Z a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall r. Fun 'Z a r -> r) -> ContVec 'Z a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec Fun 'Z a r -> r
Fun 'Z a r -> Fn 'Z a r
forall r. Fun 'Z a r -> r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun), t 'Z
t)
reducePeano :: forall (t :: PeanoNum -> *).
(forall (k :: PeanoNum). t ('S k) -> t k) -> t 'Z -> t 'Z
reducePeano forall (k :: PeanoNum). t ('S k) -> t k
_ = t 'Z -> t 'Z
forall a. a -> a
id
peanoToInt :: Proxy# 'Z -> Int
peanoToInt Proxy# 'Z
_ = Int
0
{-# INLINE accum #-}
{-# INLINE accumPeano #-}
{-# INLINE applyFun #-}
{-# INLINE applyFunM #-}
{-# INLINE reducePeano #-}
{-# INLINE peanoToInt #-}
dictionaryPred :: forall (k :: PeanoNum) r.
('Z ~ 'S k) =>
Proxy# 'Z -> (ArityPeano k => r) -> r
dictionaryPred Proxy# 'Z
_ ArityPeano k => r
_ = [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"dictionaryPred: IMPOSSIBLE"
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 = 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum t ('S k) -> a -> t k
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)
accumPeano :: forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). ArityPeano k => t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t ('S n) -> Fun ('S n) a b
accumPeano forall (k :: PeanoNum). ArityPeano k => 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). ArityPeano k => 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). ArityPeano k => t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). ArityPeano k => t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accumPeano t ('S k) -> a -> t k
forall (k :: PeanoNum). ArityPeano k => t ('S k) -> a -> t k
f t 'Z -> b
g (t ('S n) -> a -> t n
forall (k :: PeanoNum). ArityPeano k => 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) -> (ContVec ('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
(ContVec n a
v,t 'Z
tZ) = (forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
forall (t :: PeanoNum -> *) a.
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
applyFun t ('S k) -> (a, t k)
forall (k :: PeanoNum). t ('S k) -> (a, t k)
f t n
t'
in (a -> ContVec n a -> ContVec ('S n) a
forall a (n :: PeanoNum). a -> ContVec n a -> ContVec ('S n) a
consPeano a
a ContVec 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 (ContVec ('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 (ContVec n a)
vec,t 'Z
t0) = (forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (ContVec 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 (ContVec n a), t 'Z)
forall (f :: * -> *) (t :: PeanoNum -> *) a.
Applicative f =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (ContVec n a), t 'Z)
applyFunM t ('S k) -> (f a, t k)
forall (k :: PeanoNum). t ('S k) -> (f a, t k)
f t n
t'
in (a -> ContVec n a -> ContVec ('S n) a
forall a (n :: PeanoNum). a -> ContVec n a -> ContVec ('S n) a
consPeano (a -> ContVec n a -> ContVec ('S n) a)
-> f a -> f (ContVec n a -> ContVec ('S n) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a f (ContVec n a -> ContVec ('S n) a)
-> f (ContVec n a) -> f (ContVec ('S n) a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (ContVec n a)
vec, t 'Z
t0)
reducePeano :: forall (t :: PeanoNum -> *).
(forall (k :: PeanoNum). t ('S k) -> t k) -> t ('S n) -> t 'Z
reducePeano forall (k :: PeanoNum). t ('S k) -> t k
f t ('S n)
t = (forall (k :: PeanoNum). t ('S k) -> t k) -> t n -> t 'Z
forall (n :: PeanoNum) (t :: PeanoNum -> *).
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> t k) -> t n -> t 'Z
forall (t :: PeanoNum -> *).
(forall (k :: PeanoNum). t ('S k) -> t k) -> t n -> t 'Z
reducePeano t ('S k) -> t k
forall (k :: PeanoNum). t ('S k) -> t k
f (t ('S n) -> t n
forall (k :: PeanoNum). t ('S k) -> t k
f t ('S n)
t)
peanoToInt :: Proxy# ('S n) -> Int
peanoToInt Proxy# ('S n)
_ = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy# n -> Int
forall (n :: PeanoNum). ArityPeano n => Proxy# n -> Int
peanoToInt (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @n)
{-# INLINE accum #-}
{-# INLINE applyFun #-}
{-# INLINE applyFunM #-}
{-# INLINE peanoToInt #-}
{-# INLINE reducePeano #-}
dictionaryPred :: forall (k :: PeanoNum) r.
('S n ~ 'S k) =>
Proxy# ('S n) -> (ArityPeano k => r) -> r
dictionaryPred Proxy# ('S n)
_ ArityPeano k => r
r = r
ArityPeano k => r
r
{-# INLINE dictionaryPred #-}
instance ArityPeano n => Index 'Z ('S n) where
getF :: forall a. Proxy# 'Z -> Fun ('S n) a a
getF Proxy# 'Z
_ = (a -> Fun n a a) -> Fun ('S n) a a
forall a (n :: PeanoNum) b. (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst a -> Fun n a a
forall a. a -> Fun n a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
putF :: forall a r. Proxy# 'Z -> a -> Fun ('S n) a r -> Fun ('S n) a r
putF Proxy# 'Z
_ a
a Fun ('S n) a r
f = Fn ('S n) a r -> Fun ('S n) a r
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn ('S n) a r -> Fun ('S n) a r)
-> Fn ('S n) a r -> Fun ('S n) a r
forall a b. (a -> b) -> a -> b
$ \a
_ -> Fun ('S n) a r -> Fn ('S n) a r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun Fun ('S n) a r
f a
a
lensF :: forall (f :: * -> *) a r.
Functor f =>
Proxy# 'Z -> (a -> f a) -> Fun ('S n) a r -> Fun ('S n) a (f r)
lensF Proxy# 'Z
_ a -> f a
f Fun ('S n) a r
fun = Fn ('S n) a (f r) -> Fun ('S n) a (f r)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn ('S n) a (f r) -> Fun ('S n) a (f r))
-> Fn ('S n) a (f r) -> Fun ('S n) a (f r)
forall a b. (a -> b) -> a -> b
$ \a
a -> Fun n a (f r) -> Fn n a (f r)
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun n a (f r) -> Fn n a (f r)) -> Fun n a (f r) -> Fn n a (f r)
forall a b. (a -> b) -> a -> b
$
(\a -> r
g -> a -> r
g (a -> r) -> f a -> f r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
a) ((a -> r) -> f r) -> Fun n a (a -> r) -> Fun n a (f r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Fun n a r) -> Fun n a (a -> r)
forall (n :: PeanoNum) b a r.
ArityPeano n =>
(b -> Fun n a r) -> Fun n a (b -> r)
shuffleFun (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
fun)
{-# INLINE getF #-}
{-# INLINE putF #-}
{-# INLINE lensF #-}
instance Index k n => Index (S k) (S n) where
getF :: forall a. Proxy# ('S k) -> Fun ('S n) a a
getF Proxy# ('S k)
_ = (a -> Fun n a a) -> Fun ('S n) a a
forall a (n :: PeanoNum) b. (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst ((a -> Fun n a a) -> Fun ('S n) a a)
-> (a -> Fun n a a) -> Fun ('S n) a a
forall a b. (a -> b) -> a -> b
$ \a
_ -> Proxy# k -> Fun n a a
forall a. Proxy# k -> Fun n a a
forall (k :: PeanoNum) (n :: PeanoNum) a.
Index k n =>
Proxy# k -> Fun n a a
getF (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @k)
putF :: forall a r. Proxy# ('S k) -> a -> Fun ('S n) a r -> Fun ('S n) a r
putF Proxy# ('S k)
_ a
a = (Fun n a r -> Fun n a r) -> Fun ('S n) a r -> Fun ('S n) a r
forall (n :: PeanoNum) a b c.
(Fun n a b -> Fun n a c) -> Fun ('S n) a b -> Fun ('S n) a c
withFun (Proxy# k -> a -> Fun n a r -> Fun n a r
forall a r. Proxy# k -> a -> Fun n a r -> Fun n a r
forall (k :: PeanoNum) (n :: PeanoNum) a r.
Index k n =>
Proxy# k -> a -> Fun n a r -> Fun n a r
putF (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @k) a
a)
lensF :: forall (f :: * -> *) a r.
Functor f =>
Proxy# ('S k) -> (a -> f a) -> Fun ('S n) a r -> Fun ('S n) a (f r)
lensF Proxy# ('S k)
_ a -> f a
f Fun ('S n) a r
fun = (Fun n a r -> Fun n a (f r))
-> Fun ('S n) a r -> Fun ('S n) a (f r)
forall (n :: PeanoNum) a b c.
(Fun n a b -> Fun n a c) -> Fun ('S n) a b -> Fun ('S n) a c
withFun (Proxy# k -> (a -> f a) -> Fun n a r -> Fun n a (f r)
forall (k :: PeanoNum) (n :: PeanoNum) (f :: * -> *) a r.
(Index k n, Functor f) =>
Proxy# k -> (a -> f a) -> Fun n a r -> Fun n a (f r)
forall (f :: * -> *) a r.
Functor f =>
Proxy# k -> (a -> f a) -> Fun n a r -> Fun n a (f r)
lensF (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @k) a -> f a
f) Fun ('S n) a r
fun
{-# INLINE getF #-}
{-# INLINE putF #-}
{-# INLINE lensF #-}
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) = 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 :: forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst = Fun ('S n) a b -> a -> Fun n a b
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 = (a -> Fun n a b) -> Fun ('S n) a b
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 = 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 :: 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 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 :: 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 = ((a -> b) -> b) -> Fun n a (a -> b) -> Fun n a b
forall a b. (a -> b) -> Fun n a a -> 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 c) -> Fun ('S n) a b -> Fun ('S n) a c
withFun :: forall (n :: PeanoNum) a b c.
(Fun n a b -> Fun n a c) -> Fun ('S n) a b -> Fun ('S n) a c
withFun Fun n a b -> Fun n a c
f Fun ('S n) a b
fun = Fn ('S n) a c -> Fun ('S n) a c
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (Fn ('S n) a c -> Fun ('S n) a c)
-> Fn ('S n) a c -> Fun ('S n) a c
forall a b. (a -> b) -> a -> b
$ \a
a -> Fun n a c -> Fn n a c
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun n a c -> Fn n a c) -> Fun n a c -> Fn n a c
forall a b. (a -> b) -> a -> b
$ Fun n a b -> Fun n a c
f (Fun n a b -> Fun n a c) -> Fun n a b -> Fun n a c
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 :: 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 (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
forall (t :: PeanoNum -> *) a b.
(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 -> (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
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 a b. (a -> b) -> (b -> a) -> b -> b
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)
dimapFun :: ArityPeano n => (a -> b) -> (c -> d) -> Fun n b c -> Fun n a d
{-# INLINE dimapFun #-}
dimapFun :: forall (n :: PeanoNum) a b c d.
ArityPeano n =>
(a -> b) -> (c -> d) -> Fun n b c -> Fun n a d
dimapFun a -> b
fA c -> d
fR Fun n b c
fun
= (forall (k :: PeanoNum). T_Flip b c ('S k) -> a -> T_Flip b c k)
-> (T_Flip b c 'Z -> d) -> T_Flip b c n -> Fun n a d
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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_Flip Fun ('S k) b c
g) a
a -> Fun k b c -> T_Flip b c k
forall a b (n :: PeanoNum). Fun n a b -> T_Flip a b n
T_Flip (Fun ('S k) b c -> b -> Fun k b c
forall (n :: PeanoNum) a b. Fun ('S n) a b -> a -> Fun n a b
curryFirst Fun ('S k) b c
g (a -> b
fA a
a)))
(\(T_Flip Fun 'Z b c
x) -> c -> d
fR (Fun 'Z b c -> Fn 'Z b c
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun Fun 'Z b c
x))
(Fun n b c -> T_Flip b c n
forall a b (n :: PeanoNum). Fun n a b -> T_Flip a b n
T_Flip Fun n b c
fun)
type family Dim (v :: Type -> Type) :: PeanoNum
class ArityPeano (Dim v) => Vector v a where
construct :: Fun (Dim v) a (v a)
inspect :: v a -> Fun (Dim v) a b -> b
basicIndex :: v a -> Int -> a
basicIndex v a
v Int
i = Int -> ContVec (Dim v) a -> a
forall (n :: PeanoNum) a. ArityPeano n => Int -> ContVec n a -> a
index Int
i (v a -> ContVec (Dim v) a
forall (v :: * -> *) a. Vector v a => v a -> ContVec (Dim v) a
cvec v a
v)
{-# INLINE basicIndex #-}
length :: forall v a. ArityPeano (Dim v) => v a -> Int
{-# INLINE length #-}
length :: forall (v :: * -> *) a. ArityPeano (Dim v) => v a -> Int
length v a
_ = Proxy# (Dim v) -> Int
forall (n :: PeanoNum). ArityPeano n => Proxy# n -> Int
peanoToInt (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @(Dim v))
newtype ContVec n a = ContVec (forall r. Fun n a r -> r)
type instance Dim (ContVec n) = n
consPeano :: a -> ContVec n a -> ContVec ('S n) a
consPeano :: forall a (n :: PeanoNum). a -> ContVec n a -> ContVec ('S n) a
consPeano a
a (ContVec forall r. Fun n a r -> r
cont) = (forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a)
-> (forall r. Fun ('S n) a r -> r) -> ContVec ('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 #-}
instance ArityPeano n => Vector (ContVec n) a where
construct :: Fun (Dim (ContVec n)) a (ContVec n a)
construct = (forall (k :: PeanoNum). T_mkN n a ('S k) -> a -> T_mkN n a k)
-> (T_mkN n a 'Z -> ContVec n a)
-> T_mkN n a n
-> Fun 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(T_mkN ContVec ('S k) a -> ContVec n a
f) a
a -> (ContVec k a -> ContVec n a) -> T_mkN n a k
forall (n_tot :: PeanoNum) a (n :: PeanoNum).
(ContVec n a -> ContVec n_tot a) -> T_mkN n_tot a n
T_mkN (ContVec ('S k) a -> ContVec n a
f (ContVec ('S k) a -> ContVec n a)
-> (ContVec k a -> ContVec ('S k) a) -> ContVec k a -> ContVec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ContVec k a -> ContVec ('S k) a
forall a (n :: PeanoNum). a -> ContVec n a -> ContVec ('S n) a
consPeano a
a))
(\(T_mkN ContVec 'Z a -> ContVec n a
f) -> ContVec 'Z a -> ContVec n a
f ((forall r. Fun 'Z a r -> r) -> ContVec 'Z a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec Fun 'Z a r -> r
Fun 'Z a r -> Fn 'Z a r
forall r. Fun 'Z a r -> r
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun))
((ContVec n a -> ContVec n a) -> T_mkN n a n
forall (n_tot :: PeanoNum) a (n :: PeanoNum).
(ContVec n a -> ContVec n_tot a) -> T_mkN n_tot a n
T_mkN ContVec n a -> ContVec n a
forall a. a -> a
id)
inspect :: forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
inspect (ContVec forall r. Fun n a r -> r
c) Fun (Dim (ContVec n)) a b
f = Fun n a b -> b
forall r. Fun n a r -> r
c Fun n a b
Fun (Dim (ContVec n)) a b
f
{-# INLINE construct #-}
{-# INLINE inspect #-}
newtype T_mkN n_tot a n = T_mkN (ContVec n a -> ContVec n_tot a)
instance (Eq a, ArityPeano n) => Eq (ContVec n a) where
ContVec n a
a == :: ContVec n a -> ContVec n a -> Bool
== ContVec n a
b = ContVec n Bool -> Bool
forall (n :: PeanoNum). ArityPeano n => ContVec n Bool -> Bool
and (ContVec n Bool -> Bool) -> ContVec n Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> a -> Bool) -> ContVec n a -> ContVec n a -> ContVec n Bool
forall (n :: PeanoNum) a b c.
ArityPeano n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) ContVec n a
a ContVec n a
b
{-# INLINE (==) #-}
instance (Ord a, ArityPeano n) => Ord (ContVec n a) where
compare :: ContVec n a -> ContVec n a -> Ordering
compare ContVec n a
a ContVec n a
b = (Ordering -> Ordering -> Ordering)
-> Ordering -> ContVec n Ordering -> Ordering
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
mappend Ordering
forall a. Monoid a => a
mempty (ContVec n Ordering -> Ordering) -> ContVec n Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ (a -> a -> Ordering)
-> ContVec n a -> ContVec n a -> ContVec n Ordering
forall (n :: PeanoNum) a b c.
ArityPeano n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ContVec n a
a ContVec n a
b
{-# INLINE compare #-}
instance (ArityPeano n, Monoid a) => Monoid (ContVec n a) where
mempty :: ContVec n a
mempty = a -> ContVec n a
forall (n :: PeanoNum) a. ArityPeano n => a -> ContVec n a
replicate a
forall a. Monoid a => a
mempty
{-# INLINE mempty #-}
instance (ArityPeano n, Semigroup a) => Semigroup (ContVec n a) where
<> :: ContVec n a -> ContVec n a -> ContVec n a
(<>) = (a -> a -> a) -> ContVec n a -> ContVec n a -> ContVec n a
forall (n :: PeanoNum) a b c.
ArityPeano n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)
{-# INLINE (<>) #-}
instance (ArityPeano n) => Functor (ContVec n) where
fmap :: forall a b. (a -> b) -> ContVec n a -> ContVec n b
fmap = (a -> b) -> ContVec n a -> ContVec n b
forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b) -> ContVec n a -> ContVec n b
map
{-# INLINE fmap #-}
instance (ArityPeano n) => Applicative (ContVec n) where
pure :: forall a. a -> ContVec n a
pure = a -> ContVec n a
forall (n :: PeanoNum) a. ArityPeano n => a -> ContVec n a
replicate
<*> :: forall a b. 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 :: PeanoNum) a b c.
ArityPeano 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 (ArityPeano n) => F.Foldable (ContVec n) where
foldMap' :: forall m a. Monoid m => (a -> m) -> ContVec n a -> m
foldMap' a -> m
f = (m -> a -> m) -> m -> ContVec n a -> m
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl' (\ m
acc a
a -> m
acc m -> m -> m
forall a. Semigroup a => a -> a -> a
<> a -> m
f a
a) m
forall a. Monoid a => a
mempty
foldr :: forall a b. (a -> b -> b) -> b -> ContVec n a -> b
foldr = (a -> b -> b) -> b -> ContVec n a -> b
forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr
foldl :: forall b a. (b -> a -> b) -> b -> ContVec n a -> b
foldl = (b -> a -> b) -> b -> ContVec n a -> b
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl
foldl' :: forall b a. (b -> a -> b) -> b -> ContVec n a -> b
foldl' = (b -> a -> b) -> b -> ContVec n a -> b
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl'
toList :: forall a. ContVec n a -> [a]
toList = ContVec n a -> [a]
forall (n :: PeanoNum) a. ArityPeano n => ContVec n a -> [a]
toList
sum :: forall a. Num a => ContVec n a -> a
sum = ContVec n a -> a
forall a (n :: PeanoNum). (Num a, ArityPeano n) => ContVec n a -> a
sum
product :: forall a. Num a => ContVec n a -> a
product = (a -> a -> a) -> a -> ContVec n a -> a
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl' a -> a -> a
forall a. Num a => a -> a -> a
(*) a
0
{-# INLINE foldMap' #-}
{-# INLINE foldr #-}
{-# INLINE foldl #-}
{-# INLINE foldl' #-}
{-# INLINE toList #-}
{-# INLINE sum #-}
{-# INLINE product #-}
#if MIN_VERSION_base(4,16,0)
length :: forall a. ContVec n a -> Int
length = ContVec n a -> Int
forall (v :: * -> *) a. ArityPeano (Dim v) => v a -> Int
length
{-# INLINE length #-}
#endif
instance (ArityPeano n) => T.Traversable (ContVec n) where
sequence :: forall (m :: * -> *) a.
Monad m =>
ContVec n (m a) -> m (ContVec n a)
sequence = ContVec n (m a) -> m (ContVec n a)
forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
ContVec n (f a) -> f (ContVec n a)
sequenceA = ContVec n (f a) -> f (ContVec n a)
forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ContVec n a -> f (ContVec n b)
traverse = (a -> f b) -> ContVec n a -> f (ContVec n b)
forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano n, Applicative f) =>
(a -> f b) -> ContVec n a -> f (ContVec n b)
mapM
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ContVec n a -> m (ContVec n b)
mapM = (a -> m b) -> ContVec n a -> m (ContVec n b)
forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano n, Applicative f) =>
(a -> f b) -> ContVec n a -> f (ContVec n b)
mapM
{-# INLINE sequence #-}
{-# INLINE sequenceA #-}
{-# INLINE mapM #-}
{-# INLINE traverse #-}
cvec :: (Vector v a) => v a -> ContVec (Dim v) a
cvec :: forall (v :: * -> *) a. Vector v a => v a -> ContVec (Dim v) a
cvec v a
v = (forall r. Fun (Dim v) a r -> r) -> ContVec (Dim v) a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec (v a -> Fun (Dim v) a r -> r
forall b. v a -> Fun (Dim v) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect v a
v)
{-# INLINE[0] cvec #-}
empty :: ContVec 'Z a
{-# INLINE empty #-}
empty :: forall a. ContVec 'Z a
empty = (forall r. Fun 'Z a r -> r) -> ContVec 'Z a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec (\(Fun Fn 'Z a r
r) -> r
Fn 'Z a r
r)
fromList :: ArityPeano n => [a] -> ContVec n a
{-# INLINE fromList #-}
fromList :: forall (n :: PeanoNum) a. ArityPeano n => [a] -> ContVec n a
fromList [a]
xs =
(forall (k :: PeanoNum). Const [a] ('S k) -> (a, Const [a] k))
-> Const [a] n -> ContVec n a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> ContVec n a
apply Const [a] ('S k) -> (a, Const [a] k)
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] 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. ArityPeano n => [a] -> ContVec n a
{-# INLINE fromList' #-}
fromList' :: forall (n :: PeanoNum) a. ArityPeano n => [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] n -> (ContVec n a, Const [a] 'Z)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
forall (t :: PeanoNum -> *) a.
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> (ContVec n a, t 'Z)
applyFun Const [a] ('S k) -> (a, Const [a] k)
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] n
forall {k} a (b :: k). a -> Const a b
Const [a]
xs :: Const [a] n) of
(ContVec n a
v,Const []) -> ContVec n a
v
(ContVec 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. ArityPeano n => [a] -> Maybe (ContVec n a)
{-# INLINE fromListM #-}
fromListM :: forall (n :: PeanoNum) a.
ArityPeano n =>
[a] -> Maybe (ContVec n a)
fromListM [a]
xs = case (forall (k :: PeanoNum).
Const [a] ('S k) -> (Maybe a, Const [a] k))
-> Const [a] n -> (Maybe (ContVec 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 (ContVec n a), t 'Z)
forall (f :: * -> *) (t :: PeanoNum -> *) a.
Applicative f =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> (f (ContVec n a), t 'Z)
applyFunM Const [a] ('S k) -> (Maybe a, Const [a] k)
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] n
forall {k} a (b :: k). a -> Const a b
Const [a]
xs :: Const [a] n) of
(Just ContVec n a
v, Const []) -> ContVec n a -> Maybe (ContVec n a)
forall a. a -> Maybe a
Just ContVec n a
v
(Maybe (ContVec 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 :: (ArityPeano n) => ContVec n a -> [a]
toList :: forall (n :: PeanoNum) a. ArityPeano n => ContVec n a -> [a]
toList = (a -> [a] -> [a]) -> [a] -> ContVec n a -> [a]
forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr (:) []
{-# INLINE toList #-}
replicate :: (ArityPeano n) => a -> ContVec n a
{-# INLINE replicate #-}
replicate :: forall (n :: PeanoNum) a. ArityPeano n => a -> ContVec n a
replicate a
a = (forall (k :: PeanoNum). Proxy ('S k) -> (a, Proxy k))
-> Proxy n -> ContVec n a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> ContVec n a
apply (\Proxy ('S k)
Proxy -> (a
a, Proxy k
forall {k} (t :: k). Proxy t
Proxy)) Proxy n
forall {k} (t :: k). Proxy t
Proxy
replicateM :: (ArityPeano n, Applicative f) => f a -> f (ContVec n a)
{-# INLINE replicateM #-}
replicateM :: forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano n, Applicative f) =>
f a -> f (ContVec n a)
replicateM f a
act
= (forall (k :: PeanoNum). Proxy ('S k) -> (f a, Proxy k))
-> Proxy n -> f (ContVec n a)
forall (f :: * -> *) (n :: PeanoNum) (t :: PeanoNum -> *) a.
(Applicative f, ArityPeano n) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> f (ContVec n a)
applyM (\Proxy ('S k)
Proxy -> (f a
act, Proxy k
forall {k} (t :: k). Proxy t
Proxy)) Proxy n
forall {k} (t :: k). Proxy t
Proxy
generate :: (ArityPeano n) => (Int -> a) -> ContVec n a
{-# INLINE generate #-}
generate :: forall (n :: PeanoNum) a. ArityPeano n => (Int -> a) -> ContVec n a
generate Int -> a
f =
(forall (k :: PeanoNum). Const Int ('S k) -> (a, Const Int k))
-> Const Int n -> ContVec n a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> ContVec n a
apply (\(Const Int
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 n
forall {k} a (b :: k). a -> Const a b
Const Int
0)
generateM :: (Applicative f, ArityPeano n) => (Int -> f a) -> f (ContVec n a)
{-# INLINE generateM #-}
generateM :: forall (f :: * -> *) (n :: PeanoNum) a.
(Applicative f, ArityPeano n) =>
(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 n -> f (ContVec n a)
forall (f :: * -> *) (n :: PeanoNum) (t :: PeanoNum -> *) a.
(Applicative f, ArityPeano n) =>
(forall (k :: PeanoNum). t ('S k) -> (f a, t k))
-> t n -> f (ContVec n a)
applyM (\(Const Int
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 n
forall {k} a (b :: k). a -> Const a b
Const Int
0)
unfoldr :: ArityPeano n => (b -> (a,b)) -> b -> ContVec n a
{-# INLINE unfoldr #-}
unfoldr :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(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 n -> ContVec n a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> ContVec n a
apply (\(Const b
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 n
forall {k} a (b :: k). a -> Const a b
Const b
b0)
basis :: (Num a, ArityPeano n) => Int -> ContVec n a
{-# INLINE basis #-}
basis :: forall a (n :: PeanoNum).
(Num a, ArityPeano n) =>
Int -> ContVec n a
basis Int
n0 =
(forall (k :: PeanoNum). Const Int ('S k) -> (a, Const Int k))
-> Const Int n -> ContVec n a
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> ContVec n a
apply (\(Const Int
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 n
forall {k} a (b :: k). a -> Const a b
Const Int
n0)
mk1 :: a -> ContVec N1 a
mk1 :: forall a. a -> ContVec N1 a
mk1 a
a1 = (forall r. Fun N1 a r -> r) -> ContVec N1 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N1 a r -> r) -> ContVec N1 a)
-> (forall r. Fun N1 a r -> r) -> ContVec N1 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N1 a r
f) -> Fn N1 a r
a -> r
f a
a1
{-# INLINE mk1 #-}
mk2 :: a -> a -> ContVec N2 a
mk2 :: forall a. a -> a -> ContVec N2 a
mk2 a
a1 a
a2 = (forall r. Fun N2 a r -> r) -> ContVec N2 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N2 a r -> r) -> ContVec N2 a)
-> (forall r. Fun N2 a r -> r) -> ContVec N2 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N2 a r
f) -> Fn N2 a r
a -> a -> r
f a
a1 a
a2
{-# INLINE mk2 #-}
mk3 :: a -> a -> a -> ContVec N3 a
mk3 :: forall a. a -> a -> a -> ContVec N3 a
mk3 a
a1 a
a2 a
a3 = (forall r. Fun N3 a r -> r) -> ContVec N3 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N3 a r -> r) -> ContVec N3 a)
-> (forall r. Fun N3 a r -> r) -> ContVec N3 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N3 a r
f) -> Fn N3 a r
a -> a -> a -> r
f a
a1 a
a2 a
a3
{-# INLINE mk3 #-}
mk4 :: a -> a -> a -> a -> ContVec N4 a
mk4 :: forall a. a -> a -> a -> a -> ContVec N4 a
mk4 a
a1 a
a2 a
a3 a
a4 = (forall r. Fun N4 a r -> r) -> ContVec N4 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N4 a r -> r) -> ContVec N4 a)
-> (forall r. Fun N4 a r -> r) -> ContVec N4 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N4 a r
f) -> Fn N4 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 N5 a
mk5 :: forall a. a -> a -> a -> a -> a -> ContVec N5 a
mk5 a
a1 a
a2 a
a3 a
a4 a
a5 = (forall r. Fun N5 a r -> r) -> ContVec N5 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N5 a r -> r) -> ContVec N5 a)
-> (forall r. Fun N5 a r -> r) -> ContVec N5 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N5 a r
f) -> Fn N5 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 N6 a
mk6 :: forall a. a -> a -> a -> a -> a -> a -> ContVec N6 a
mk6 a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 = (forall r. Fun N6 a r -> r) -> ContVec N6 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N6 a r -> r) -> ContVec N6 a)
-> (forall r. Fun N6 a r -> r) -> ContVec N6 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N6 a r
f) -> Fn N6 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 N7 a
mk7 :: forall a. a -> a -> a -> a -> a -> a -> a -> ContVec N7 a
mk7 a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 a
a7 = (forall r. Fun N7 a r -> r) -> ContVec N7 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N7 a r -> r) -> ContVec N7 a)
-> (forall r. Fun N7 a r -> r) -> ContVec N7 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N7 a r
f) -> Fn N7 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 N8 a
mk8 :: forall a. a -> a -> a -> a -> a -> a -> a -> a -> ContVec N8 a
mk8 a
a1 a
a2 a
a3 a
a4 a
a5 a
a6 a
a7 a
a8 = (forall r. Fun N8 a r -> r) -> ContVec N8 a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun N8 a r -> r) -> ContVec N8 a)
-> (forall r. Fun N8 a r -> r) -> ContVec N8 a
forall a b. (a -> b) -> a -> b
$ \(Fun Fn N8 a r
f) -> Fn N8 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 :: (ArityPeano n) => (a -> b) -> ContVec n a -> ContVec n b
{-# INLINE map #-}
map :: forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b) -> ContVec n a -> ContVec n b
map a -> b
f (ContVec forall r. Fun n a r -> r
contA) = (forall r. Fun n b r -> r) -> ContVec n b
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun n b r -> r) -> ContVec n b)
-> (forall r. Fun n b r -> r) -> ContVec n b
forall a b. (a -> b) -> a -> b
$
Fun n a r -> r
forall r. Fun n a r -> r
contA (Fun n a r -> r) -> (Fun n b r -> Fun n a r) -> Fun n b r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Fun n b r -> Fun n a r
forall (n :: PeanoNum) a b r.
ArityPeano n =>
(a -> b) -> Fun n b r -> Fun n a r
mapF a -> b
f
imap :: (ArityPeano n) => (Int -> a -> b) -> ContVec n a -> ContVec n b
{-# INLINE imap #-}
imap :: forall (n :: PeanoNum) a b.
ArityPeano n =>
(Int -> a -> b) -> ContVec n a -> ContVec n b
imap Int -> a -> b
f (ContVec forall r. Fun n a r -> r
contA) = (forall r. Fun n b r -> r) -> ContVec n b
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun n b r -> r) -> ContVec n b)
-> (forall r. Fun n b r -> r) -> ContVec n b
forall a b. (a -> b) -> a -> b
$
Fun n a r -> r
forall r. Fun n a r -> r
contA (Fun n a r -> r) -> (Fun n b r -> Fun n a r) -> Fun n b r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> b) -> Fun n b r -> Fun 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 :: (ArityPeano n, Applicative f) => (a -> f b) -> ContVec n a -> f (ContVec n b)
{-# INLINE mapM #-}
mapM :: forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano n, Applicative f) =>
(a -> f b) -> ContVec n a -> f (ContVec n b)
mapM a -> f b
f ContVec n a
v
= ContVec n a
-> Fun (Dim (ContVec n)) a (f (ContVec n b)) -> f (ContVec n b)
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
v
(Fun (Dim (ContVec n)) a (f (ContVec n b)) -> f (ContVec n b))
-> Fun (Dim (ContVec n)) a (f (ContVec n b)) -> f (ContVec n b)
forall a b. (a -> b) -> a -> b
$ (a -> f b) -> Fun n b (ContVec n b) -> Fun n a (f (ContVec n b))
forall (n :: PeanoNum) (f :: * -> *) a b r.
(ArityPeano n, Applicative f) =>
(a -> f b) -> Fun n b r -> Fun n a (f r)
mapMF a -> f b
f Fun n b (ContVec n b)
Fun (Dim (ContVec n)) b (ContVec n b)
forall (v :: * -> *) a. Vector v a => Fun (Dim v) a (v a)
construct
imapM :: (ArityPeano n, Applicative f)
=> (Int -> a -> f b) -> ContVec n a -> f (ContVec n b)
{-# INLINE imapM #-}
imapM :: forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano n, Applicative f) =>
(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 (Dim (ContVec n)) a (f (ContVec n b)) -> f (ContVec n b)
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
v
(Fun (Dim (ContVec n)) a (f (ContVec n b)) -> f (ContVec n b))
-> Fun (Dim (ContVec n)) a (f (ContVec n b)) -> f (ContVec n b)
forall a b. (a -> b) -> a -> b
$ (Int -> a -> f b)
-> Fun n b (ContVec n b) -> Fun 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 n b (ContVec n b)
Fun (Dim (ContVec n)) b (ContVec n b)
forall (v :: * -> *) a. Vector v a => Fun (Dim v) a (v a)
construct
mapM_ :: (ArityPeano n, Applicative f) => (a -> f b) -> ContVec n a -> f ()
{-# INLINE mapM_ #-}
mapM_ :: forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano n, Applicative f) =>
(a -> f b) -> ContVec n a -> f ()
mapM_ a -> f b
f = (f () -> a -> f ()) -> f () -> ContVec n a -> f ()
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl (\f ()
m a
a -> f ()
m f () -> f b -> f b
forall a b. f a -> 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 a b. f a -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (() -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
imapM_ :: (ArityPeano n, Applicative f) => (Int -> a -> f b) -> ContVec n a -> f ()
{-# INLINE imapM_ #-}
imapM_ :: forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano n, Applicative f) =>
(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 :: PeanoNum) b a.
ArityPeano 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 a b. f a -> 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 a b. f a -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (() -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
mapMF :: (ArityPeano n, Applicative f)
=> (a -> f b) -> Fun n b r -> Fun n a (f r)
{-# INLINE mapMF #-}
mapMF :: forall (n :: PeanoNum) (f :: * -> *) a b r.
(ArityPeano n, Applicative f) =>
(a -> f b) -> Fun n b r -> Fun n a (f r)
mapMF 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_mapM f (Fn ('S k) b r)
m) a
a -> f (Fn k b r) -> T_mapM b f r k
forall a (m :: * -> *) r (n :: PeanoNum).
m (Fn n a r) -> T_mapM a m r n
T_mapM ((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 a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
f a
a))
(\(T_mapM f (Fn 'Z b r)
m) -> f r
f (Fn 'Z b r)
m)
(f (Fn n b r) -> T_mapM b f r n
forall a (m :: * -> *) r (n :: PeanoNum).
m (Fn n a r) -> T_mapM a m r n
T_mapM (Fn n b r -> f (Fn n b r)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Fn n b r
funB))
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 (k :: PeanoNum).
T_imapM b f r ('S k) -> a -> T_imapM b f r k)
-> (T_imapM b f r 'Z -> f r) -> T_imapM 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_imapM Int
i f (Fn ('S k) b r)
m) a
a -> Int -> f (Fn k b r) -> T_imapM b f r k
forall a (m :: * -> *) r (n :: PeanoNum).
Int -> m (Fn n a r) -> T_imapM a m r n
T_imapM (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (f (Fn k b r) -> T_imapM b f r k)
-> f (Fn k b r) -> T_imapM 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 a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> a -> f b
f Int
i a
a)
(\(T_imapM Int
_ f (Fn 'Z b r)
m) -> f r
f (Fn 'Z b r)
m)
(Int -> f (Fn n b r) -> T_imapM b f r n
forall a (m :: * -> *) r (n :: PeanoNum).
Int -> m (Fn n a r) -> T_imapM a m r n
T_imapM Int
0 (Fn n b r -> f (Fn n b r)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Fn n b r
funB))
newtype T_mapM a m r n = T_mapM (m (Fn n a r))
data T_imapM a m r n = T_imapM Int (m (Fn n a r))
mapF :: ArityPeano n
=> (a -> b) -> Fun n b r -> Fun n a r
{-# INLINE mapF #-}
mapF :: forall (n :: PeanoNum) a b r.
ArityPeano n =>
(a -> b) -> Fun n b r -> Fun n a r
mapF 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_map Fn ('S k) b r
g) a
b -> Fn k b r -> T_map b r k
forall a r (n :: PeanoNum). Fn n a r -> T_map a r n
T_map (Fn ('S k) b r
b -> Fn k b r
g (a -> b
f a
b)))
(\(T_map Fn 'Z b r
r) -> r
Fn 'Z b r
r)
( Fn n b r -> T_map b r n
forall a r (n :: PeanoNum). Fn n a r -> T_map a r n
T_map Fn n b r
funB)
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 (k :: PeanoNum). T_imap b r ('S k) -> a -> T_imap b r k)
-> (T_imap b r 'Z -> r) -> T_imap 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_imap Int
i Fn ('S k) b r
g) a
b -> Int -> Fn k b r -> T_imap b r k
forall a r (n :: PeanoNum). Int -> Fn n a r -> T_imap a r n
T_imap (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_imap Int
_ Fn 'Z b r
r) -> r
Fn 'Z b r
r)
( Int -> Fn n b r -> T_imap b r n
forall a r (n :: PeanoNum). Int -> Fn n a r -> T_imap a r n
T_imap Int
0 Fn n b r
funB)
newtype T_map a r n = T_map (Fn n a r)
data T_imap a r n = T_imap Int (Fn n a r)
scanl :: (ArityPeano n) => (b -> a -> b) -> b -> ContVec n a -> ContVec ('S n) b
{-# INLINE scanl #-}
scanl :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> ContVec ('S n) b
scanl b -> a -> b
f b
b0 (ContVec forall r. Fun n a r -> r
cont) = (forall r. Fun ('S n) b r -> r) -> ContVec ('S n) b
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun ('S n) b r -> r) -> ContVec ('S n) b)
-> (forall r. Fun ('S n) b r -> r) -> ContVec ('S n) b
forall a b. (a -> b) -> a -> b
$
Fun n a r -> r
forall r. Fun n a r -> r
cont (Fun n a r -> r)
-> (Fun ('S n) b r -> Fun n a r) -> Fun ('S n) b r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a -> b) -> b -> Fun ('S n) b r -> Fun 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 :: (ArityPeano n) => (a -> a -> a) -> ContVec n a -> ContVec n a
{-# INLINE scanl1 #-}
scanl1 :: forall (n :: PeanoNum) a.
ArityPeano n =>
(a -> a -> a) -> ContVec n a -> ContVec n a
scanl1 a -> a -> a
f (ContVec forall r. Fun n a r -> r
cont) = (forall r. Fun n a r -> r) -> ContVec n a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun n a r -> r) -> ContVec n a)
-> (forall r. Fun n a r -> r) -> ContVec n a
forall a b. (a -> b) -> a -> b
$
Fun n a r -> r
forall r. Fun n a r -> r
cont (Fun n a r -> r) -> (Fun n a r -> Fun n a r) -> Fun n a r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a) -> Fun n a r -> Fun 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 :: 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 (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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum T_scanl r b ('S k) -> a -> T_scanl r b k
forall (k :: PeanoNum). T_scanl r b ('S k) -> a -> T_scanl r b k
step T_scanl r b 'Z -> r
T_scanl r b 'Z -> Fn 'Z b 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 :: 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 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 :: 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 (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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum T_scanl1 r a ('S k) -> a -> T_scanl1 r a k
forall (k :: PeanoNum). T_scanl1 r a ('S k) -> a -> T_scanl1 r a k
step T_scanl1 r a 'Z -> r
T_scanl1 r a 'Z -> Fn 'Z a 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 :: 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 = 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 :: (ArityPeano n, Applicative f) => ContVec n (f a) -> f (ContVec n a)
sequence :: forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano n, Applicative f) =>
ContVec n (f a) -> f (ContVec n a)
sequence = (f a -> f a) -> ContVec n (f a) -> f (ContVec n a)
forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano 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_ :: (ArityPeano n, Applicative f) => ContVec n (f a) -> f ()
sequence_ :: forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano n, Applicative f) =>
ContVec n (f a) -> f ()
sequence_ = (f a -> f a) -> ContVec n (f a) -> f ()
forall (n :: PeanoNum) (f :: * -> *) a b.
(ArityPeano 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, ArityPeano n) => f (ContVec n a) -> ContVec n (f a)
{-# INLINE distribute #-}
distribute :: forall (f :: * -> *) (n :: PeanoNum) a.
(Functor f, ArityPeano n) =>
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]) n -> ContVec n (f a)
forall (n :: PeanoNum) (t :: PeanoNum -> *) a.
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> (a, t k))
-> t n -> ContVec n a
apply Const (f [a]) ('S k) -> (f a, Const (f [a]) k)
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]) 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 a b. (a -> b) -> f a -> f b
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 a b. (a -> b) -> f a -> f 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]) n
start = f [a] -> Const (f [a]) n
forall {k} a (b :: k). a -> Const a b
Const ((ContVec n a -> [a]) -> f (ContVec n a) -> f [a]
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ContVec n a -> [a]
forall (n :: PeanoNum) a. ArityPeano n => ContVec n a -> [a]
toList f (ContVec n a)
f0)
collect :: (Functor f, ArityPeano n) => (a -> ContVec n b) -> f a -> ContVec n (f b)
collect :: forall (f :: * -> *) (n :: PeanoNum) a b.
(Functor f, ArityPeano n) =>
(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 :: PeanoNum) a.
(Functor f, ArityPeano 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 a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> ContVec n b
f
{-# INLINE collect #-}
tail :: ContVec (S n) a -> ContVec n a
tail :: forall (n :: PeanoNum) a. ContVec ('S n) a -> ContVec n a
tail (ContVec forall r. Fun ('S n) a r -> r
cont) = (forall r. Fun n a r -> r) -> ContVec n a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun n a r -> r) -> ContVec n a)
-> (forall r. Fun n a r -> r) -> ContVec n a
forall a b. (a -> b) -> a -> b
$ \Fun n a r
f -> Fun ('S n) a r -> r
forall r. Fun ('S n) a r -> r
cont (Fun ('S n) a r -> r) -> Fun ('S n) a r -> r
forall a b. (a -> b) -> a -> b
$ Fun n a r -> Fun ('S n) a r
forall (n :: PeanoNum) a b. Fun n a b -> Fun ('S n) a b
constFun Fun n a r
f
{-# INLINE tail #-}
cons :: a -> ContVec n a -> ContVec ('S n) a
cons :: forall a (n :: PeanoNum). a -> ContVec n a -> ContVec ('S n) a
cons a
a (ContVec forall r. Fun n a r -> r
cont) = (forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a)
-> (forall r. Fun ('S n) a r -> r) -> ContVec ('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 cons #-}
consV :: ArityPeano n => ContVec N1 a -> ContVec n a -> ContVec ('S n) a
{-# INLINE consV #-}
consV :: forall (n :: PeanoNum) a.
ArityPeano n =>
ContVec N1 a -> ContVec n a -> ContVec ('S n) a
consV (ContVec forall r. Fun N1 a r -> r
cont1) (ContVec forall r. Fun n a r -> r
cont)
= (forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a)
-> (forall r. Fun ('S n) a r -> r) -> ContVec ('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 -> Fun n a r) -> a -> Fun n a r
forall a b. (a -> b) -> a -> b
$ Fun N1 a a -> a
forall r. Fun N1 a r -> r
cont1 (Fun N1 a a -> a) -> Fun N1 a a -> a
forall a b. (a -> b) -> a -> b
$ Fn N1 a a -> Fun N1 a a
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn N1 a a
a -> a
forall a. a -> a
id
snoc :: ArityPeano n => a -> ContVec n a -> ContVec ('S n) a
snoc :: forall (n :: PeanoNum) a.
ArityPeano n =>
a -> ContVec n a -> ContVec ('S n) a
snoc a
a (ContVec forall r. Fun n a r -> r
cont) = (forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun ('S n) a r -> r) -> ContVec ('S n) a)
-> (forall r. Fun ('S n) a r -> r) -> ContVec ('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.
ArityPeano n =>
Fun ('S n) a b -> a -> Fun n a b
apLast Fun ('S n) a r
f a
a
{-# INLINE snoc #-}
concat :: ( ArityPeano n
, ArityPeano k
, ArityPeano (n `Add` k)
)
=> ContVec n a -> ContVec k a -> ContVec (Add n k) a
{-# INLINE concat #-}
concat :: forall (n :: PeanoNum) (k :: PeanoNum) a.
(ArityPeano n, ArityPeano k, ArityPeano (Add n k)) =>
ContVec n a -> ContVec k a -> ContVec (Add n k) a
concat ContVec n a
v ContVec k a
u = ContVec k a
-> Fun (Dim (ContVec k)) a (ContVec (Add n k) a)
-> ContVec (Add n k) a
forall b. ContVec k a -> Fun (Dim (ContVec k)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec k a
u
(Fun (Dim (ContVec k)) a (ContVec (Add n k) a)
-> ContVec (Add n k) a)
-> Fun (Dim (ContVec k)) a (ContVec (Add n k) a)
-> ContVec (Add n k) a
forall a b. (a -> b) -> a -> b
$ ContVec n a
-> Fun
(Dim (ContVec n)) a (Fun (Dim (ContVec k)) a (ContVec (Add n k) a))
-> Fun (Dim (ContVec k)) a (ContVec (Add n k) a)
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
v
(Fun
(Dim (ContVec n)) a (Fun (Dim (ContVec k)) a (ContVec (Add n k) a))
-> Fun (Dim (ContVec k)) a (ContVec (Add n k) a))
-> Fun
(Dim (ContVec n)) a (Fun (Dim (ContVec k)) a (ContVec (Add n k) a))
-> Fun (Dim (ContVec k)) a (ContVec (Add n k) a)
forall a b. (a -> b) -> a -> b
$ Fun (Add n k) a (ContVec (Add n k) a)
-> Fun n a (Fun k a (ContVec (Add 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 (Dim (ContVec (Add n k))) a (ContVec (Add n k) a)
Fun (Add n k) a (ContVec (Add n k) a)
forall (v :: * -> *) a. Vector v a => Fun (Dim v) a (v a)
construct
reverse :: ArityPeano n => ContVec n a -> ContVec n a
reverse :: forall (n :: PeanoNum) a.
ArityPeano n =>
ContVec n a -> ContVec n a
reverse (ContVec forall r. Fun n a r -> r
cont) = (forall r. Fun n a r -> r) -> ContVec n a
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun n a r -> r) -> ContVec n a)
-> (forall r. Fun n a r -> r) -> ContVec n a
forall a b. (a -> b) -> a -> b
$ Fun n a r -> r
forall r. Fun n a r -> r
cont (Fun n a r -> r) -> (Fun n a r -> Fun n a r) -> Fun n a r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun n a r -> Fun n a r
forall (n :: PeanoNum) a b. ArityPeano n => Fun n a b -> Fun n a b
reverseF
{-# INLINE reverse #-}
reverseF :: forall n a b. ArityPeano n => Fun n a b -> Fun n a b
reverseF :: forall (n :: PeanoNum) a b. ArityPeano n => Fun n a b -> Fun n a b
reverseF (Fun Fn n a b
fun0) = (forall (k :: PeanoNum).
ArityPeano k =>
T_map a b ('S k) -> a -> T_map a b k)
-> (T_map a b 'Z -> b) -> T_map a b n -> Fun n a b
forall (n :: PeanoNum) (t :: PeanoNum -> *) a b.
ArityPeano n =>
(forall (k :: PeanoNum). ArityPeano k => t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). ArityPeano k => t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accumPeano
T_map a b ('S k) -> a -> T_map a b k
forall (k :: PeanoNum).
ArityPeano k =>
T_map a b ('S k) -> a -> T_map a b k
step
(\(T_map Fn 'Z a b
b) -> b
Fn 'Z a b
b)
(Fn n a b -> T_map a b n
forall a r (n :: PeanoNum). Fn n a r -> T_map a r n
T_map Fn n a b
fun0 :: T_map a b n)
where
step :: forall k. ArityPeano k => T_map a b (S k) -> a -> T_map a b k
step :: forall (k :: PeanoNum).
ArityPeano k =>
T_map a b ('S k) -> a -> T_map a b k
step (T_map Fn ('S k) a b
f) a
a = Fn k a b -> T_map a b k
forall a r (n :: PeanoNum). Fn n a r -> T_map a r n
T_map (Fn k a b -> T_map a b k) -> Fn k a b -> T_map a b k
forall a b. (a -> b) -> a -> b
$ Fun k a b -> Fn k a b
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun k a b -> Fn k a b) -> Fun k a b -> Fn k a b
forall a b. (a -> b) -> a -> b
$ Fun ('S k) a b -> a -> Fun k a b
forall (n :: PeanoNum) a b.
ArityPeano n =>
Fun ('S n) a b -> a -> Fun n a b
apLast (Fn ('S k) a b -> Fun ('S k) a b
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn ('S k) a b
f :: Fun (S k) a b) a
a
zipWith :: (ArityPeano n) => (a -> b -> c)
-> ContVec n a -> ContVec n b -> ContVec n c
{-# INLINE zipWith #-}
zipWith :: forall (n :: PeanoNum) a b c.
ArityPeano n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith a -> b -> c
f ContVec n a
vecA ContVec n b
vecB = (forall r. Fun n c r -> r) -> ContVec n c
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun n c r -> r) -> ContVec n c)
-> (forall r. Fun n c r -> r) -> ContVec n c
forall a b. (a -> b) -> a -> b
$ \Fun n c r
funC ->
ContVec n b -> Fun (Dim (ContVec n)) b r -> r
forall b. ContVec n b -> Fun (Dim (ContVec n)) b b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n b
vecB
(Fun (Dim (ContVec n)) b r -> r) -> Fun (Dim (ContVec n)) b r -> r
forall a b. (a -> b) -> a -> b
$ ContVec n a
-> Fun (Dim (ContVec n)) a (Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) b r
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
vecA
(Fun (Dim (ContVec n)) a (Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) a (Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) b r
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> Fun n c r -> Fun n a (Fun n b r)
forall (n :: PeanoNum) a b c r.
ArityPeano n =>
(a -> b -> c) -> Fun n c r -> Fun n a (Fun n b r)
zipWithF a -> b -> c
f Fun n c r
funC
zipWith3 :: (ArityPeano n) => (a -> b -> c -> d)
-> ContVec n a -> ContVec n b -> ContVec n c -> ContVec n d
{-# INLINE zipWith3 #-}
zipWith3 :: forall (n :: PeanoNum) a b c d.
ArityPeano 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
= ((c -> d) -> c -> d)
-> ContVec n (c -> d) -> ContVec n c -> ContVec n d
forall (n :: PeanoNum) a b c.
ArityPeano n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith (c -> d) -> c -> d
forall a b. (a -> b) -> a -> b
($) ((a -> b -> c -> d)
-> ContVec n a -> ContVec n b -> ContVec n (c -> d)
forall (n :: PeanoNum) a b c.
ArityPeano n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith a -> b -> c -> d
f ContVec n a
v1 ContVec n b
v2) ContVec n c
v3
izipWith :: (ArityPeano n) => (Int -> a -> b -> c)
-> ContVec n a -> ContVec n b -> ContVec n c
{-# INLINE izipWith #-}
izipWith :: forall (n :: PeanoNum) a b c.
ArityPeano 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 r. Fun n c r -> r) -> ContVec n c
forall (n :: PeanoNum) a. (forall r. Fun n a r -> r) -> ContVec n a
ContVec ((forall r. Fun n c r -> r) -> ContVec n c)
-> (forall r. Fun n c r -> r) -> ContVec n c
forall a b. (a -> b) -> a -> b
$ \Fun n c r
funC ->
ContVec n b -> Fun (Dim (ContVec n)) b r -> r
forall b. ContVec n b -> Fun (Dim (ContVec n)) b b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n b
vecB
(Fun (Dim (ContVec n)) b r -> r) -> Fun (Dim (ContVec n)) b r -> r
forall a b. (a -> b) -> a -> b
$ ContVec n a
-> Fun (Dim (ContVec n)) a (Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) b r
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
vecA
(Fun (Dim (ContVec n)) a (Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) a (Fun (Dim (ContVec n)) b r)
-> Fun (Dim (ContVec n)) b r
forall a b. (a -> b) -> a -> b
$ (Int -> a -> b -> c) -> Fun n c r -> Fun n a (Fun 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 n c r
funC
izipWith3 :: (ArityPeano n) => (Int -> a -> b -> c -> d)
-> ContVec n a -> ContVec n b -> ContVec n c -> ContVec n d
{-# INLINE izipWith3 #-}
izipWith3 :: forall (n :: PeanoNum) a b c d.
ArityPeano 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 = (Int -> a -> (b, c) -> d)
-> ContVec n a -> ContVec n (b, c) -> ContVec n d
forall (n :: PeanoNum) a b c.
ArityPeano 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 :: PeanoNum) a b c.
ArityPeano n =>
(a -> b -> c) -> ContVec n a -> ContVec n b -> ContVec n c
zipWith (,) ContVec n b
v2 ContVec n c
v3)
zipWithM :: (ArityPeano n, Applicative f) => (a -> b -> f c)
-> ContVec n a -> ContVec n b -> f (ContVec n c)
{-# INLINE zipWithM #-}
zipWithM :: forall (n :: PeanoNum) (f :: * -> *) a b c.
(ArityPeano 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 = ContVec n (f c) -> f (ContVec n c)
forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano 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 :: PeanoNum) a b c.
ArityPeano 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_ :: (ArityPeano n, Applicative f)
=> (a -> b -> f c) -> ContVec n a -> ContVec n b -> f ()
{-# INLINE zipWithM_ #-}
zipWithM_ :: forall (n :: PeanoNum) (f :: * -> *) a b c.
(ArityPeano 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 = ContVec n (f c) -> f ()
forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano 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 :: PeanoNum) a b c.
ArityPeano 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 :: (ArityPeano n, Applicative f) => (Int -> a -> b -> f c)
-> ContVec n a -> ContVec n b -> f (ContVec n c)
{-# INLINE izipWithM #-}
izipWithM :: forall (n :: PeanoNum) (f :: * -> *) a b c.
(ArityPeano 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 = ContVec n (f c) -> f (ContVec n c)
forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano 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 :: PeanoNum) a b c.
ArityPeano 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_ :: (ArityPeano n, Applicative f)
=> (Int -> a -> b -> f c) -> ContVec n a -> ContVec n b -> f ()
{-# INLINE izipWithM_ #-}
izipWithM_ :: forall (n :: PeanoNum) (f :: * -> *) a b c.
(ArityPeano 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 = ContVec n (f c) -> f ()
forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano 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 :: PeanoNum) a b c.
ArityPeano 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)
zipWithF :: (ArityPeano n)
=> (a -> b -> c) -> Fun n c r -> Fun n a (Fun n b r)
{-# INLINE zipWithF #-}
zipWithF :: forall (n :: PeanoNum) a b c r.
ArityPeano n =>
(a -> b -> c) -> Fun n c r -> Fun n a (Fun n b r)
zipWithF a -> b -> c
f (Fun Fn n c r
g0)
= ([a] -> Fun n b r) -> Fun n a (Fun n b r)
forall (n :: PeanoNum) a b. ArityPeano n => ([a] -> b) -> Fun n a b
makeList
(([a] -> Fun n b r) -> Fun n a (Fun n b r))
-> ([a] -> Fun n b r) -> Fun n a (Fun n b r)
forall a b. (a -> b) -> a -> b
$ \[a]
v -> (forall (k :: PeanoNum). T_zip a c r ('S k) -> b -> T_zip a c r k)
-> (T_zip a c r 'Z -> r) -> T_zip 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_zip (a
a:[a]
as) Fn ('S k) c r
g) b
b -> [a] -> Fn k c r -> T_zip a c r k
forall a c r (n :: PeanoNum). [a] -> Fn n c r -> T_zip a c r n
T_zip [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
$ a -> b -> c
f a
a b
b))
(\(T_zip [a]
_ Fn 'Z c r
x) -> r
Fn 'Z c r
x)
([a] -> Fn n c r -> T_zip a c r n
forall a c r (n :: PeanoNum). [a] -> Fn n c r -> T_zip a c r n
T_zip [a]
v Fn n c r
g0)
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)
= ([a] -> Fun n b r) -> Fun n a (Fun n b r)
forall (n :: PeanoNum) a b. ArityPeano n => ([a] -> b) -> Fun n a b
makeList
(([a] -> Fun n b r) -> Fun n a (Fun n b r))
-> ([a] -> Fun n b r) -> Fun n a (Fun n b r)
forall a b. (a -> b) -> a -> b
$ \[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
forall (t :: PeanoNum -> *) a b.
(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 -> 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)
makeList :: ArityPeano n => ([a] -> b) -> Fun n a b
{-# INLINE makeList #-}
makeList :: forall (n :: PeanoNum) a b. ArityPeano n => ([a] -> b) -> Fun n a b
makeList [a] -> b
cont = (forall (k :: PeanoNum).
Const ([a] -> [a]) ('S k) -> a -> Const ([a] -> [a]) k)
-> (Const ([a] -> [a]) 'Z -> b)
-> Const ([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
forall (t :: PeanoNum -> *) a b.
(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 -> ([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
x:)))
(\(Const [a] -> [a]
xs) -> [a] -> b
cont ([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)
data T_zip a c r n = T_zip [a] (Fn n c r)
runContVec :: Fun n a r
-> ContVec n a
-> r
runContVec :: forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec Fun n a r
f (ContVec forall r. Fun n a r -> r
c) = Fun n a r -> r
forall r. Fun n a r -> r
c Fun n a r
f
{-# INLINE runContVec #-}
vector :: (Vector v a) => ContVec (Dim v) a -> v a
vector :: forall (v :: * -> *) a. Vector v a => ContVec (Dim v) a -> v a
vector = Fun (Dim v) a (v a) -> ContVec (Dim v) a -> v a
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec Fun (Dim v) a (v a)
forall (v :: * -> *) a. Vector v a => Fun (Dim v) a (v a)
construct
{-# INLINE[1] vector #-}
head :: forall n k a. (ArityPeano n, n ~ 'S k) => ContVec n a -> a
{-# INLINE head #-}
head :: forall (n :: PeanoNum) (k :: PeanoNum) a.
(ArityPeano n, n ~ 'S k) =>
ContVec n a -> a
head
= Proxy# n -> (ArityPeano k => ContVec n a -> a) -> ContVec n a -> a
forall (n :: PeanoNum) (k :: PeanoNum) r.
(ArityPeano n, n ~ 'S k) =>
Proxy# n -> (ArityPeano k => r) -> r
forall (k :: PeanoNum) r.
(n ~ 'S k) =>
Proxy# n -> (ArityPeano k => r) -> r
dictionaryPred (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @n)
((ArityPeano k => ContVec n a -> a) -> ContVec n a -> a)
-> (ArityPeano k => ContVec n a -> a) -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ Fun n a a -> ContVec n a -> a
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec
(Fun n a a -> ContVec n a -> a) -> Fun n a a -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ (a -> Fun k a a) -> Fun ('S k) a a
forall a (n :: PeanoNum) b. (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst a -> Fun k a a
forall a. a -> Fun k a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
index :: ArityPeano n => Int -> ContVec n a -> a
{-# INLINE index #-}
index :: forall (n :: PeanoNum) a. ArityPeano n => 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 n a a -> ContVec n a -> a
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec (Fun n a a -> ContVec n a -> a) -> Fun 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) 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
forall (t :: PeanoNum -> *) a b.
(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 -> 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) 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 :: (ArityPeano n, Functor f)
=> Int -> (a -> f a) -> ContVec n a -> f (ContVec n a)
{-# INLINE element #-}
element :: forall (n :: PeanoNum) (f :: * -> *) a.
(ArityPeano 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 = ContVec n a
-> Fun (Dim (ContVec n)) a (f (ContVec n a)) -> f (ContVec n a)
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
v
(Fun (Dim (ContVec n)) a (f (ContVec n a)) -> f (ContVec n a))
-> Fun (Dim (ContVec n)) a (f (ContVec n a)) -> f (ContVec n a)
forall a b. (a -> b) -> a -> b
$ Int
-> (a -> f a) -> Fun n a (ContVec n a) -> Fun 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 n a (ContVec n a)
Fun (Dim (ContVec n)) a (ContVec n a)
forall (v :: * -> *) a. Vector v a => Fun (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 (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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum T_lens f a r ('S k) -> a -> T_lens f a r k
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 = 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 a b. (a -> b) -> f a -> f b
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 a b. (a -> b) -> f a -> f b
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 :: ArityPeano n => (b -> a -> b) -> b -> ContVec n a -> b
{-# INLINE foldl #-}
foldl :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl b -> a -> b
f b
b0 = Fun n a b -> ContVec n a -> b
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec ((b -> a -> b) -> b -> Fun n a b
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> Fun n a b
foldlF b -> a -> b
f b
b0)
foldl' :: ArityPeano n => (b -> a -> b) -> b -> ContVec n a -> b
{-# INLINE foldl' #-}
foldl' :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> ContVec n a -> b
foldl' b -> a -> b
f b
b0 = Fun n a b -> ContVec n a -> b
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec ((b -> a -> b) -> b -> Fun n a b
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> Fun n a b
foldlF' b -> a -> b
f b
b0)
ifoldl :: ArityPeano n => (b -> Int -> a -> b) -> b -> ContVec n a -> b
{-# INLINE ifoldl #-}
ifoldl :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(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 (Dim (ContVec n)) a b -> b
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
v
(Fun (Dim (ContVec n)) a b -> b) -> Fun (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 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
forall (t :: PeanoNum -> *) a b.
(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 -> 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 n
forall {k} b (n :: k). Int -> b -> T_ifoldl b n
T_ifoldl Int
0 b
b)
ifoldl' :: ArityPeano n => (b -> Int -> a -> b) -> b -> ContVec n a -> b
{-# INLINE ifoldl' #-}
ifoldl' :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(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 (Dim (ContVec n)) a b -> b
forall b. ContVec n a -> Fun (Dim (ContVec n)) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect ContVec n a
v
(Fun (Dim (ContVec n)) a b -> b) -> Fun (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 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
forall (t :: PeanoNum -> *) a b.
(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 -> 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 n
forall {k} b (n :: k). Int -> b -> T_ifoldl b n
T_ifoldl Int
0 b
b)
foldM :: (ArityPeano n, Monad m)
=> (b -> a -> m b) -> b -> ContVec n a -> m b
{-# INLINE foldM #-}
foldM :: forall (n :: PeanoNum) (m :: * -> *) b a.
(ArityPeano n, Monad m) =>
(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 :: PeanoNum) b a.
ArityPeano 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return b
x)
ifoldM :: (ArityPeano n, Monad m)
=> (b -> Int -> a -> m b) -> b -> ContVec n a -> m b
{-# INLINE ifoldM #-}
ifoldM :: forall (n :: PeanoNum) (m :: * -> *) b a.
(ArityPeano n, Monad m) =>
(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 :: PeanoNum) b a.
ArityPeano 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return b
x)
foldl1 :: forall n k a. (ArityPeano n, n ~ 'S k)
=> (a -> a -> a) -> ContVec n a -> a
{-# INLINE foldl1 #-}
foldl1 :: forall (n :: PeanoNum) (k :: PeanoNum) a.
(ArityPeano n, n ~ 'S k) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 a -> a -> a
f
= Proxy# n -> (ArityPeano k => ContVec n a -> a) -> ContVec n a -> a
forall (n :: PeanoNum) (k :: PeanoNum) r.
(ArityPeano n, n ~ 'S k) =>
Proxy# n -> (ArityPeano k => r) -> r
forall (k :: PeanoNum) r.
(n ~ 'S k) =>
Proxy# n -> (ArityPeano k => r) -> r
dictionaryPred (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @n)
((ArityPeano k => ContVec n a -> a) -> ContVec n a -> a)
-> (ArityPeano k => ContVec n a -> a) -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ Fun n a a -> ContVec n a -> a
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec
(Fun n a a -> ContVec n a -> a) -> Fun n a a -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ (a -> Fun k a a) -> Fun ('S k) a a
forall a (n :: PeanoNum) b. (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst ((a -> a -> a) -> a -> Fun k a a
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> Fun n a b
foldlF a -> a -> a
f)
foldl1' :: forall n k a. (ArityPeano n, n ~ 'S k)
=> (a -> a -> a) -> ContVec n a -> a
{-# INLINE foldl1' #-}
foldl1' :: forall (n :: PeanoNum) (k :: PeanoNum) a.
(ArityPeano n, n ~ 'S k) =>
(a -> a -> a) -> ContVec n a -> a
foldl1' a -> a -> a
f
= Proxy# n -> (ArityPeano k => ContVec n a -> a) -> ContVec n a -> a
forall (n :: PeanoNum) (k :: PeanoNum) r.
(ArityPeano n, n ~ 'S k) =>
Proxy# n -> (ArityPeano k => r) -> r
forall (k :: PeanoNum) r.
(n ~ 'S k) =>
Proxy# n -> (ArityPeano k => r) -> r
dictionaryPred (forall {k} (a :: k). Proxy# a
forall (a :: PeanoNum). Proxy# a
proxy# @n)
((ArityPeano k => ContVec n a -> a) -> ContVec n a -> a)
-> (ArityPeano k => ContVec n a -> a) -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ Fun n a a -> ContVec n a -> a
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec
(Fun n a a -> ContVec n a -> a) -> Fun n a a -> ContVec n a -> a
forall a b. (a -> b) -> a -> b
$ (a -> Fun k a a) -> Fun ('S k) a a
forall a (n :: PeanoNum) b. (a -> Fun n a b) -> Fun ('S n) a b
uncurryFirst ((a -> a -> a) -> a -> Fun k a a
forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> Fun n a b
foldlF' a -> a -> a
f)
foldlF :: ArityPeano n => (b -> a -> b) -> b -> Fun n a b
{-# INLINE foldlF #-}
foldlF :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> Fun n a b
foldlF b -> a -> b
f b
b0
= (forall (k :: PeanoNum). T_foldl b ('S k) -> a -> T_foldl b k)
-> (T_foldl b 'Z -> b) -> T_foldl b 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_foldl b
b) a
a -> b -> T_foldl b k
forall {k} b (n :: k). b -> T_foldl b n
T_foldl (b -> a -> b
f b
b a
a))
(\(T_foldl b
b) -> b
b)
(b -> T_foldl b n
forall {k} b (n :: k). b -> T_foldl b n
T_foldl b
b0)
foldlF' :: ArityPeano n => (b -> a -> b) -> b -> Fun n a b
{-# INLINE foldlF' #-}
foldlF' :: forall (n :: PeanoNum) b a.
ArityPeano n =>
(b -> a -> b) -> b -> Fun n a b
foldlF' b -> a -> b
f b
b0
= (forall (k :: PeanoNum). T_foldl b ('S k) -> a -> T_foldl b k)
-> (T_foldl b 'Z -> b) -> T_foldl b 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum (\(T_foldl !b
b) a
a -> b -> T_foldl b k
forall {k} b (n :: k). b -> T_foldl b n
T_foldl (b -> a -> b
f b
b a
a))
(\(T_foldl b
b) -> b
b)
(b -> T_foldl b n
forall {k} b (n :: k). b -> T_foldl b n
T_foldl b
b0)
newtype T_foldl b n = T_foldl b
data T_ifoldl b n = T_ifoldl !Int b
foldr :: ArityPeano n => (a -> b -> b) -> b -> ContVec n a -> b
{-# INLINE foldr #-}
foldr :: forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr a -> b -> b
f b
b0 = Fun n a b -> ContVec n a -> b
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec (Fun n a b -> ContVec n a -> b) -> Fun n a b -> ContVec n a -> b
forall a b. (a -> b) -> a -> b
$ (a -> b -> b) -> b -> Fun n a b
forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b -> b) -> b -> Fun n a b
foldrF a -> b -> b
f b
b0
ifoldr :: ArityPeano n => (Int -> a -> b -> b) -> b -> ContVec n a -> b
{-# INLINE ifoldr #-}
ifoldr :: forall (n :: PeanoNum) a b.
ArityPeano n =>
(Int -> a -> b -> b) -> b -> ContVec n a -> b
ifoldr Int -> a -> b -> b
f b
b0 = Fun n a b -> ContVec n a -> b
forall (n :: PeanoNum) a r. Fun n a r -> ContVec n a -> r
runContVec (Fun n a b -> ContVec n a -> b) -> Fun n a b -> ContVec n a -> b
forall a b. (a -> b) -> a -> b
$ (Int -> a -> b -> b) -> b -> Fun n a b
forall (n :: PeanoNum) a b.
ArityPeano n =>
(Int -> a -> b -> b) -> b -> Fun n a b
ifoldrF Int -> a -> b -> b
f b
b0
foldrF :: ArityPeano n => (a -> b -> b) -> b -> Fun n a b
{-# INLINE foldrF #-}
foldrF :: forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b -> b) -> b -> Fun n a b
foldrF a -> b -> b
f b
b0 = (forall (k :: PeanoNum). T_foldr b ('S k) -> a -> T_foldr b k)
-> (T_foldr b 'Z -> b) -> T_foldr b 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(T_foldr b -> b
g) a
a -> (b -> b) -> T_foldr b k
forall {k} b (n :: k). (b -> b) -> T_foldr b n
T_foldr (b -> b
g (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> b
f a
a))
(\(T_foldr b -> b
g) -> b -> b
g b
b0)
((b -> b) -> T_foldr b n
forall {k} b (n :: k). (b -> b) -> T_foldr b n
T_foldr b -> b
forall a. a -> a
id)
ifoldrF :: ArityPeano n => (Int -> a -> b -> b) -> b -> Fun n a b
{-# INLINE ifoldrF #-}
ifoldrF :: forall (n :: PeanoNum) a b.
ArityPeano n =>
(Int -> a -> b -> b) -> b -> Fun n a b
ifoldrF Int -> a -> b -> b
f b
b0 = (forall (k :: PeanoNum). T_ifoldr b ('S k) -> a -> T_ifoldr b k)
-> (T_ifoldr b 'Z -> b) -> T_ifoldr b 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
forall (t :: PeanoNum -> *) a b.
(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 -> 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
b0)
(Int -> (b -> b) -> T_ifoldr b 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_foldr b n = T_foldr (b -> b)
data T_ifoldr b n = T_ifoldr Int (b -> b)
sum :: (Num a, ArityPeano n) => ContVec n a -> a
sum :: forall a (n :: PeanoNum). (Num a, ArityPeano n) => ContVec n a -> a
sum = (a -> a -> a) -> a -> ContVec n a -> a
forall (n :: PeanoNum) b a.
ArityPeano 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, ArityPeano n, n ~ 'S k) => ContVec n a -> a
minimum :: forall a (n :: PeanoNum) (k :: PeanoNum).
(Ord a, ArityPeano n, n ~ 'S k) =>
ContVec n a -> a
minimum = (a -> a -> a) -> ContVec n a -> a
forall (n :: PeanoNum) (k :: PeanoNum) a.
(ArityPeano n, n ~ 'S k) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 a -> a -> a
forall a. Ord a => a -> a -> a
min
{-# INLINE minimum #-}
maximum :: (Ord a, ArityPeano n, n ~ 'S k) => ContVec n a -> a
maximum :: forall a (n :: PeanoNum) (k :: PeanoNum).
(Ord a, ArityPeano n, n ~ 'S k) =>
ContVec n a -> a
maximum = (a -> a -> a) -> ContVec n a -> a
forall (n :: PeanoNum) (k :: PeanoNum) a.
(ArityPeano n, n ~ 'S k) =>
(a -> a -> a) -> ContVec n a -> a
foldl1 a -> a -> a
forall a. Ord a => a -> a -> a
max
{-# INLINE maximum #-}
and :: ArityPeano n => ContVec n Bool -> Bool
and :: forall (n :: PeanoNum). ArityPeano n => ContVec n Bool -> Bool
and = (Bool -> Bool -> Bool) -> Bool -> ContVec n Bool -> Bool
forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr Bool -> Bool -> Bool
(&&) Bool
True
{-# INLINE and #-}
or :: ArityPeano n => ContVec n Bool -> Bool
or :: forall (n :: PeanoNum). ArityPeano n => ContVec n Bool -> Bool
or = (Bool -> Bool -> Bool) -> Bool -> ContVec n Bool -> Bool
forall (n :: PeanoNum) a b.
ArityPeano n =>
(a -> b -> b) -> b -> ContVec n a -> b
foldr Bool -> Bool -> Bool
(||) Bool
False
{-# INLINE or #-}
all :: ArityPeano n => (a -> Bool) -> ContVec n a -> Bool
all :: forall (n :: PeanoNum) a.
ArityPeano n =>
(a -> Bool) -> ContVec n a -> Bool
all a -> Bool
f = (a -> Bool -> Bool) -> Bool -> ContVec n a -> Bool
forall (n :: PeanoNum) a b.
ArityPeano 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 :: ArityPeano n => (a -> Bool) -> ContVec n a -> Bool
any :: forall (n :: PeanoNum) a.
ArityPeano n =>
(a -> Bool) -> ContVec n a -> Bool
any a -> Bool
f = (a -> Bool -> Bool) -> Bool -> ContVec n a -> Bool
forall (n :: PeanoNum) a b.
ArityPeano 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 :: ArityPeano n => (a -> Bool) -> ContVec n a -> Maybe a
find :: forall (n :: PeanoNum) a.
ArityPeano n =>
(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 :: PeanoNum) b a.
ArityPeano 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 a. 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 (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
= v a -> Fun (Dim v) a (c (v a)) -> c (v a)
forall b. v a -> Fun (Dim v) a b -> b
forall (v :: * -> *) a b. Vector v a => v a -> Fun (Dim v) a b -> b
inspect v a
v
(Fun (Dim v) a (c (v a)) -> c (v a))
-> Fun (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 (Dim v) a (v a)) -> Fun (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 c (x -> y) -> x -> c y
forall x y. Data x => c (x -> y) -> x -> c y
f (Fn (Dim v) a (v a) -> c (Fn (Dim v) a (v a))
forall x. x -> c x
inj (Fn (Dim v) a (v a) -> c (Fn (Dim v) a (v a)))
-> Fn (Dim v) a (v a) -> c (Fn (Dim v) a (v a))
forall a b. (a -> b) -> a -> b
$ Fun (Dim v) a (v a) -> Fn (Dim v) a (v a)
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun (Fun (Dim v) a (v a)
forall (v :: * -> *) a. Vector v a => Fun (Dim v) a (v a)
construct :: Fun (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
_ =
case (forall (k :: PeanoNum).
T_gunfold c (v a) a ('S k) -> T_gunfold c (v a) a k)
-> T_gunfold c (v a) a (Dim v) -> T_gunfold c (v a) a 'Z
forall (n :: PeanoNum) (t :: PeanoNum -> *).
ArityPeano n =>
(forall (k :: PeanoNum). t ('S k) -> t k) -> t n -> t 'Z
forall (t :: PeanoNum -> *).
(forall (k :: PeanoNum). t ('S k) -> t k) -> t (Dim v) -> t 'Z
reducePeano T_gunfold c (v a) a ('S k) -> T_gunfold c (v a) a k
forall (k :: PeanoNum).
T_gunfold c (v a) a ('S k) -> T_gunfold c (v a) a k
forall (k :: PeanoNum) r.
T_gunfold c r a ('S k) -> T_gunfold c r a k
step T_gunfold c (v a) a (Dim v)
gun of
T_gunfold c (Fn 'Z a (v a))
c -> c (v a)
c (Fn 'Z a (v a))
c
where
con :: Fun (Dim v) a (v a)
con = forall (v :: * -> *) a. Vector v a => Fun (Dim v) a (v a)
construct @v @a
gun :: T_gunfold c (v a) a (Dim v)
gun = c (Fn (Dim v) a (v a)) -> T_gunfold c (v a) a (Dim v)
forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gunfold c r a n
T_gunfold (Fn (Dim v) a (v a) -> c (Fn (Dim v) a (v a))
forall r. r -> c r
inj (Fn (Dim v) a (v a) -> c (Fn (Dim v) a (v a)))
-> Fn (Dim v) a (v a) -> c (Fn (Dim v) a (v a))
forall a b. (a -> b) -> a -> b
$ Fun (Dim v) a (v a) -> Fn (Dim v) a (v a)
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun Fun (Dim v) a (v a)
con) :: T_gunfold c (v a) a (Dim v)
step :: forall k r. T_gunfold c r a ('S k) -> T_gunfold c r a k
step :: forall (k :: PeanoNum) r.
T_gunfold c r a ('S k) -> T_gunfold c r a k
step (T_gunfold c (Fn ('S k) a r)
c) = c (Fn k a r) -> T_gunfold c r a k
forall (c :: * -> *) r a (n :: PeanoNum).
c (Fn n a r) -> T_gunfold c r a n
T_gunfold (c (a -> Fn k a r) -> c (Fn k a r)
forall b r. Data b => c (b -> r) -> c r
f c (Fn ('S k) a r)
c (a -> Fn k a r)
c)
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 (k :: PeanoNum).
T_mapM a c r ('S k) -> a -> T_mapM a c r k)
-> (T_mapM a c r 'Z -> c r) -> T_mapM a c r 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
forall (t :: PeanoNum -> *) a b.
(forall (k :: PeanoNum). t ('S k) -> a -> t k)
-> (t 'Z -> b) -> t n -> Fun n a b
accum
(\(T_mapM c (Fn ('S k) a r)
c) a
x -> c (Fn k a r) -> T_mapM a c r k
forall a (m :: * -> *) r (n :: PeanoNum).
m (Fn n a r) -> T_mapM a m r n
T_mapM (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_mapM c (Fn 'Z a r)
c) -> c r
c (Fn 'Z a r)
c)
(c (Fn n a r) -> T_mapM a c r n
forall a (m :: * -> *) r (n :: PeanoNum).
m (Fn n a r) -> T_mapM a m r n
T_mapM c (Fn n a r)
c0)
{-# RULES
"cvec/vector" forall v.
cvec (vector v) = v
#-}
type instance Dim Complex = N2
instance Vector Complex a where
construct :: Fun (Dim Complex) a (Complex a)
construct = Fn N2 a (Complex a) -> Fun N2 a (Complex a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn N2 a (Complex a)
a -> a -> Complex a
forall a. a -> a -> Complex a
(:+)
inspect :: forall b. Complex a -> Fun (Dim Complex) a b -> b
inspect (a
x :+ a
y) (Fun Fn (Dim Complex) a b
f) = Fn (Dim Complex) a b
a -> a -> b
f a
x a
y
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim Identity = N1
instance Vector Identity a where
construct :: Fun (Dim Identity) a (Identity a)
construct = Fn N1 a (Identity a) -> Fun N1 a (Identity a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun Fn N1 a (Identity a)
a -> Identity a
forall a. a -> Identity a
Identity
inspect :: forall b. Identity a -> Fun (Dim Identity) a b -> b
inspect (Identity a
x) (Fun Fn (Dim Identity) a b
f) = Fn (Dim Identity) a b
a -> b
f a
x
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,) a) = N2
instance (b~a) => Vector ((,) b) a where
construct :: Fun (Dim ((,) b)) a (b, a)
construct = Fn N2 a (b, a) -> Fun N2 a (b, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,)
inspect :: forall b. (b, a) -> Fun (Dim ((,) b)) a b -> b
inspect (b
a,a
b) (Fun Fn (Dim ((,) b)) a b
f) = Fn (Dim ((,) b)) a b
b -> a -> b
f b
a a
b
{-# INLINE construct #-}
{-# INLINE inspect #-}
type instance Dim ((,,) a b) = N3
instance (b~a, c~a) => Vector ((,,) b c) a where
construct :: Fun (Dim ((,,) b c)) a (b, c, a)
construct = Fn N3 a (b, c, a) -> Fun N3 a (b, c, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,)
inspect :: forall b. (b, c, a) -> Fun (Dim ((,,) b c)) a b -> b
inspect (b
a,c
b,a
c) (Fun Fn (Dim ((,,) b c)) a b
f) = Fn (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) = N4
instance (b~a, c~a, d~a) => Vector ((,,,) b c d) a where
construct :: Fun (Dim ((,,,) b c d)) a (b, c, d, a)
construct = Fn N4 a (b, c, d, a) -> Fun N4 a (b, c, d, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,)
inspect :: forall b. (b, c, d, a) -> Fun (Dim ((,,,) b c d)) a b -> b
inspect (b
a,c
b,d
c,a
d) (Fun Fn (Dim ((,,,) b c d)) a b
f) = Fn (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) = N5
instance (b~a, c~a, d~a, e~a) => Vector ((,,,,) b c d e) a where
construct :: Fun (Dim ((,,,,) b c d e)) a (b, c, d, e, a)
construct = Fn N5 a (b, c, d, e, a) -> Fun N5 a (b, c, d, e, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,)
inspect :: forall b. (b, c, d, e, a) -> Fun (Dim ((,,,,) b c d e)) a b -> b
inspect (b
a,c
b,d
c,e
d,a
e) (Fun Fn (Dim ((,,,,) b c d e)) a b
f) = Fn (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) = N6
instance (b~a, c~a, d~a, e~a, f~a) => Vector ((,,,,,) b c d e f) a where
construct :: Fun (Dim ((,,,,,) b c d e f)) a (b, c, d, e, f, a)
construct = Fn N6 a (b, c, d, e, f, a) -> Fun N6 a (b, c, d, e, f, a)
forall (n :: PeanoNum) a b. Fn n a b -> Fun n a b
Fun (,,,,,)
inspect :: forall b.
(b, c, d, e, f, a) -> Fun (Dim ((,,,,,) b c d e f)) a b -> b
inspect (b
a,c
b,d
c,e
d,f
e,a
f) (Fun Fn (Dim ((,,,,,) b c d e f)) a b
fun) = Fn (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) = N7
instance (b~a, c~a, d~a, e~a, f~a, g~a) => Vector ((,,,,,,) b c d e f g) a where
construct :: Fun (Dim ((,,,,,,) b c d e f g)) a (b, c, d, e, f, g, a)
construct = Fn N7 a (b, c, d, e, f, g, a) -> Fun N7 a (b, c, d, e, f, g, a)
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 (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 (Dim ((,,,,,,) b c d e f g)) a b
fun) = Fn (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 = Z
instance Vector Proxy a where
construct :: Fun (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 Proxy a
Fn 'Z a (Proxy a)
forall {k} (t :: k). Proxy t
Proxy
inspect :: forall b. Proxy a -> Fun (Dim Proxy) a b -> b
inspect Proxy a
_ = Fun (Dim Proxy) a b -> b
Fun 'Z a b -> Fn 'Z a b
forall (n :: PeanoNum) a b. Fun n a b -> Fn n a b
unFun