{-# LANGUAGE TypeFamilies, FlexibleInstances, PostfixOperators #-}
{-# OPTIONS_HADDOCK hide #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ForSyDe.MoC.SDF
-- Copyright   :  (c) George Ungureanu, KTH/ICT/E 2015; 
--                    SAM Group, KTH/ICT/ECS 2007-2008
-- License     :  BSD-style (see the file LICENSE)
-- 
-- Maintainer  :  ugeorge@kth.se
-- Stability   :  experimental
-- Portability :  portable
--
-- The synchronuous library defines process constructors, processes and a signal conduit
-- for the synchronous computational model. A process constructor is a
-- higher order function which together with combinational function(s)
-- and values as arguments constructs a process. 
-----------------------------------------------------------------------------
module ForSyDe.Atom.MoC.SDF.Core where

import ForSyDe.Atom.MoC
import ForSyDe.Atom.MoC.Stream
import ForSyDe.Atom.Utility.Tuple

-- | Type synonym for production rate
type Cons = Int

-- | Type synonym for consumption rate
type Prod = Int

-- | Type synonym for a SY signal, i.e. "a signal of SY events"
type Signal a   = Stream (SDF a)

-- | The SDF event. It identifies a synchronous dataflow signal, and
-- wraps only a value.
newtype SDF a = SDF { SDF a -> a
val :: a }

-- | Implenents the SDF semantics for the MoC atoms.
instance MoC SDF where
  type Fun SDF a b = (Cons, [a] -> b)
  type Ret SDF a   = (Prod, [a])
  ---------------------
  _ -.- :: Fun SDF a b -> Stream (SDF a) -> Stream (SDF b)
-.- NullS = Stream (SDF b)
forall e. Stream e
NullS
  (c,f) -.- s :: Stream (SDF a)
s = (Int -> ([a] -> b) -> [a] -> Stream (SDF b)
forall a a. Int -> ([a] -> a) -> [a] -> Stream (SDF a)
comb Int
c [a] -> b
f ([a] -> Stream (SDF b))
-> (Stream (SDF a) -> [a]) -> Stream (SDF a) -> Stream (SDF b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SDF a -> a) -> [SDF a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map SDF a -> a
forall a. SDF a -> a
val ([SDF a] -> [a])
-> (Stream (SDF a) -> [SDF a]) -> Stream (SDF a) -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stream (SDF a) -> [SDF a]
forall a. Stream a -> [a]
fromStream) Stream (SDF a)
s
    where comb :: Int -> ([a] -> a) -> [a] -> Stream (SDF a)
comb c :: Int
c f :: [a] -> a
f l :: [a]
l = let x' :: [a]
x'  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
c [a]
l
                           xs' :: [a]
xs' = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
c [a]
l
                       in if   [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c
                          then a -> SDF a
forall a. a -> SDF a
SDF ([a] -> a
f [a]
x') SDF a -> Stream (SDF a) -> Stream (SDF a)
forall e. e -> Stream e -> Stream e
:- Int -> ([a] -> a) -> [a] -> Stream (SDF a)
comb Int
c [a] -> a
f [a]
xs'
                          else Stream (SDF a)
forall e. Stream e
NullS
  ---------------------
  cfs :: Stream (SDF (Fun SDF a b))
cfs -*- :: Stream (SDF (Fun SDF a b)) -> Stream (SDF a) -> Stream (SDF b)
-*- s :: Stream (SDF a)
s = (Stream (SDF (Int, [a] -> b)) -> [a] -> Stream (SDF b)
forall a a. Stream (SDF (Int, [a] -> a)) -> [a] -> Stream (SDF a)
comb2 Stream (SDF (Int, [a] -> b))
Stream (SDF (Fun SDF a b))
cfs ([a] -> Stream (SDF b))
-> (Stream (SDF a) -> [a]) -> Stream (SDF a) -> Stream (SDF b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SDF a -> a) -> [SDF a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map SDF a -> a
forall a. SDF a -> a
val ([SDF a] -> [a])
-> (Stream (SDF a) -> [SDF a]) -> Stream (SDF a) -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stream (SDF a) -> [SDF a]
forall a. Stream a -> [a]
fromStream) Stream (SDF a)
s
    where comb2 :: Stream (SDF (Int, [a] -> a)) -> [a] -> Stream (SDF a)
comb2 NullS           _ = Stream (SDF a)
forall e. Stream e
NullS
          comb2 (SDF (c :: Int
c,f :: [a] -> a
f):-fs :: Stream (SDF (Int, [a] -> a))
fs) l :: [a]
l = let x' :: [a]
x'  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
c [a]
l
                                        xs' :: [a]
xs' = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
c [a]
l
                                    in if   [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c
                                       then a -> SDF a
forall a. a -> SDF a
SDF ([a] -> a
f [a]
x') SDF a -> Stream (SDF a) -> Stream (SDF a)
forall e. e -> Stream e -> Stream e
:- Stream (SDF (Int, [a] -> a)) -> [a] -> Stream (SDF a)
comb2 Stream (SDF (Int, [a] -> a))
fs [a]
xs'
                                       else Stream (SDF a)
forall e. Stream e
NullS
  ---------------------
  -* :: Stream (SDF (Ret SDF b)) -> Stream (SDF b)
(-*) NullS = Stream (SDF b)
forall e. Stream e
NullS
  (-*) ((SDF (p,r)):-xs :: Stream (SDF (Ret SDF b))
xs)
    | [b] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
p = [SDF b] -> Stream (SDF b)
forall a. [a] -> Stream a
stream ((b -> SDF b) -> [b] -> [SDF b]
forall a b. (a -> b) -> [a] -> [b]
map b -> SDF b
forall a. a -> SDF a
SDF [b]
r) Stream (SDF b) -> Stream (SDF b) -> Stream (SDF b)
forall e. Stream e -> Stream e -> Stream e
+-+ (Stream (SDF (Ret SDF b))
xs Stream (SDF (Ret SDF b)) -> Stream (SDF b)
forall (e :: * -> *) b.
MoC e =>
Stream (e (Ret e b)) -> Stream (e b)
-*)
    | Bool
otherwise     = [Char] -> Stream (SDF b)
forall a. HasCallStack => [Char] -> a
error "[MoC.SDF] Wrong production"
  ---------------------
  -<- :: Stream (SDF a) -> Stream (SDF a) -> Stream (SDF a)
(-<-) = Stream (SDF a) -> Stream (SDF a) -> Stream (SDF a)
forall e. Stream e -> Stream e -> Stream e
(+-+)
  ---------------------
  -&- :: Stream (SDF a) -> Stream (SDF a) -> Stream (SDF a)
(-&-) _ a :: Stream (SDF a)
a = Stream (SDF a)
a
  ---------------------

-- | Allows for mapping of functions on a SDF event.
instance Functor SDF where
  fmap :: (a -> b) -> SDF a -> SDF b
fmap f :: a -> b
f (SDF a :: a
a) = b -> SDF b
forall a. a -> SDF a
SDF (a -> b
f a
a)

-- | Allows for lifting functions on a pair of SDF events.
instance Applicative SDF where
  pure :: a -> SDF a
pure = a -> SDF a
forall a. a -> SDF a
SDF 
  (SDF a :: a -> b
a) <*> :: SDF (a -> b) -> SDF a -> SDF b
<*> (SDF b :: a
b) = b -> SDF b
forall a. a -> SDF a
SDF (a -> b
a a
b)

instance Foldable SDF where
    foldr :: (a -> b -> b) -> b -> SDF a -> b
foldr f :: a -> b -> b
f z :: b
z (SDF x :: a
x) = a -> b -> b
f a
x b
z
    foldl :: (b -> a -> b) -> b -> SDF a -> b
foldl f :: b -> a -> b
f z :: b
z (SDF x :: a
x) = b -> a -> b
f b
z a
x

instance Traversable SDF where
    traverse :: (a -> f b) -> SDF a -> f (SDF b)
traverse f :: a -> f b
f (SDF x :: a
x) = b -> SDF b
forall a. a -> SDF a
SDF (b -> SDF b) -> f b -> f (SDF b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x

-- | Shows the value wrapped
instance Show a => Show (SDF a) where
  showsPrec :: Int -> SDF a -> ShowS
showsPrec _ (SDF x :: a
x) = [Char] -> ShowS
forall a. [a] -> [a] -> [a]
(++) (a -> [Char]
forall a. Show a => a -> [Char]
show a
x)

-- | Reads the value wrapped
instance Read a => Read (SDF a) where
  readsPrec :: Int -> ReadS (SDF a)
readsPrec _ s :: [Char]
s = [(a -> SDF a
forall a. a -> SDF a
SDF a
x, [Char]
r) | (x :: a
x, r :: [Char]
r) <- ReadS a
forall a. Read a => ReadS a
reads [Char]
s]

-----------------------------------------------------------------------------

-- | Transforms a list of values into a SDF signal with only one
-- partition, i.e. all events share the same (initial) tag.
signal :: [a] -> Signal a
signal :: [a] -> Signal a
signal l :: [a]
l = [SDF a] -> Signal a
forall a. [a] -> Stream a
stream (a -> SDF a
forall a. a -> SDF a
SDF (a -> SDF a) -> [a] -> [SDF a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
l)

signal2 :: ([a], [a]) -> (Signal a, Signal a)
signal2 (l1 :: [a]
l1,l2 :: [a]
l2)       = ([a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l1, [a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l2)
signal3 :: ([a], [a], [a]) -> (Signal a, Signal a, Signal a)
signal3 (l1 :: [a]
l1,l2 :: [a]
l2,l3 :: [a]
l3)    = ([a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l1, [a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l2, [a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l3)
signal4 :: ([a], [a], [a], [a]) -> (Signal a, Signal a, Signal a, Signal a)
signal4 (l1 :: [a]
l1,l2 :: [a]
l2,l3 :: [a]
l3,l4 :: [a]
l4) = ([a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l1, [a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l2, [a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l3, [a] -> Signal a
forall a. [a] -> Signal a
signal [a]
l4)

-- | Reads a signal from a string. Like with the @read@ function from
-- @Prelude@, you must specify the tipe of the signal.
--
-- >>> readSignal "{1,2,3,4,5}" :: Signal Int
-- {1,2,3,4,5}
readSignal :: Read a => String -> Signal a
readSignal :: [Char] -> Signal a
readSignal = [Char] -> Signal a
forall a. Read a => [Char] -> a
read

----------------------------------------------------------------------

scen11 :: (c, p, a -> b) -> (c, a -> (p, b))
scen11 (c :: c
c,p :: p
p,f :: a -> b
f) = c -> p -> (a -> b) -> (c, a -> (p, b))
forall c p a b. c -> p -> (a -> b) -> (c, a -> (p, b))
ctxt11 c
c p
p a -> b
f 
scen12 :: (c, (p1, p2), a -> (b1, b2)) -> (c, a -> ((p1, b1), (p2, b2)))
scen12 (c :: c
c,p :: (p1, p2)
p,f :: a -> (b1, b2)
f) = c -> (p1, p2) -> (a -> (b1, b2)) -> (c, a -> ((p1, b1), (p2, b2)))
forall c p1 p2 a b1 b2.
c -> (p1, p2) -> (a -> (b1, b2)) -> (c, a -> ((p1, b1), (p2, b2)))
ctxt12 c
c (p1, p2)
p a -> (b1, b2)
f 
scen13 :: (c, (p1, p2, p3), a -> (b1, b2, b3))
-> (c, a -> ((p1, b1), (p2, b2), (p3, b3)))
scen13 (c :: c
c,p :: (p1, p2, p3)
p,f :: a -> (b1, b2, b3)
f) = c
-> (p1, p2, p3)
-> (a -> (b1, b2, b3))
-> (c, a -> ((p1, b1), (p2, b2), (p3, b3)))
forall c p1 p2 p3 a b1 b2 b3.
c
-> (p1, p2, p3)
-> (a -> (b1, b2, b3))
-> (c, a -> ((p1, b1), (p2, b2), (p3, b3)))
ctxt13 c
c (p1, p2, p3)
p a -> (b1, b2, b3)
f 
scen14 :: (c, (p1, p2, p3, p4), a -> (b1, b2, b3, b4))
-> (c, a -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))
scen14 (c :: c
c,p :: (p1, p2, p3, p4)
p,f :: a -> (b1, b2, b3, b4)
f) = c
-> (p1, p2, p3, p4)
-> (a -> (b1, b2, b3, b4))
-> (c, a -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))
forall c p1 p2 p3 p4 a b1 b2 b3 b4.
c
-> (p1, p2, p3, p4)
-> (a -> (b1, b2, b3, b4))
-> (c, a -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))
ctxt14 c
c (p1, p2, p3, p4)
p a -> (b1, b2, b3, b4)
f 
scen21 :: ((c1, c2), p, a1 -> a2 -> b) -> (c1, a1 -> (c2, a2 -> (p, b)))
scen21 (c :: (c1, c2)
c,p :: p
p,f :: a1 -> a2 -> b
f) = (c1, c2) -> p -> (a1 -> a2 -> b) -> (c1, a1 -> (c2, a2 -> (p, b)))
forall c1 c2 p a1 a2 b.
(c1, c2) -> p -> (a1 -> a2 -> b) -> (c1, a1 -> (c2, a2 -> (p, b)))
ctxt21 (c1, c2)
c p
p a1 -> a2 -> b
f 
scen22 :: ((ctxa, ctxa), (ctxb, ctxb), a1 -> a2 -> (b1, b2))
-> (ctxa, a1 -> (ctxa, a2 -> ((ctxb, b1), (ctxb, b2))))
scen22 (c :: (ctxa, ctxa)
c,p :: (ctxb, ctxb)
p,f :: a1 -> a2 -> (b1, b2)
f) = (ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> (b1, b2))
-> (ctxa, a1 -> (ctxa, a2 -> ((ctxb, b1), (ctxb, b2))))
forall ctxa ctxb a1 a2 b1 b2.
(ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> (b1, b2))
-> (ctxa, a1 -> (ctxa, a2 -> ((ctxb, b1), (ctxb, b2))))
ctxt22 (ctxa, ctxa)
c (ctxb, ctxb)
p a1 -> a2 -> (b1, b2)
f 
scen23 :: ((c1, c2), (p1, p2, p3), a1 -> a2 -> (b1, b2, b3))
-> (c1, a1 -> (c2, a2 -> ((p1, b1), (p2, b2), (p3, b3))))
scen23 (c :: (c1, c2)
c,p :: (p1, p2, p3)
p,f :: a1 -> a2 -> (b1, b2, b3)
f) = (c1, c2)
-> (p1, p2, p3)
-> (a1 -> a2 -> (b1, b2, b3))
-> (c1, a1 -> (c2, a2 -> ((p1, b1), (p2, b2), (p3, b3))))
forall c1 c2 p1 p2 p3 a1 a2 b1 b2 b3.
(c1, c2)
-> (p1, p2, p3)
-> (a1 -> a2 -> (b1, b2, b3))
-> (c1, a1 -> (c2, a2 -> ((p1, b1), (p2, b2), (p3, b3))))
ctxt23 (c1, c2)
c (p1, p2, p3)
p a1 -> a2 -> (b1, b2, b3)
f 
scen24 :: ((c1, c2), (p1, p2, p3, p4), a1 -> a2 -> (b1, b2, b3, b4))
-> (c1, a1 -> (c2, a2 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))
scen24 (c :: (c1, c2)
c,p :: (p1, p2, p3, p4)
p,f :: a1 -> a2 -> (b1, b2, b3, b4)
f) = (c1, c2)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> (b1, b2, b3, b4))
-> (c1, a1 -> (c2, a2 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))
forall c1 c2 p1 p2 p3 p4 a1 a2 b1 b2 b3 b4.
(c1, c2)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> (b1, b2, b3, b4))
-> (c1, a1 -> (c2, a2 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))
ctxt24 (c1, c2)
c (p1, p2, p3, p4)
p a1 -> a2 -> (b1, b2, b3, b4)
f
scen31 :: ((c1, c2, c3), p, a1 -> a2 -> a3 -> b)
-> (c1, a1 -> (c2, a2 -> (c3, a3 -> (p, b))))
scen31 (c :: (c1, c2, c3)
c,p :: p
p,f :: a1 -> a2 -> a3 -> b
f) = (c1, c2, c3)
-> p
-> (a1 -> a2 -> a3 -> b)
-> (c1, a1 -> (c2, a2 -> (c3, a3 -> (p, b))))
forall c1 c2 c3 p a1 a2 a3 b.
(c1, c2, c3)
-> p
-> (a1 -> a2 -> a3 -> b)
-> (c1, a1 -> (c2, a2 -> (c3, a3 -> (p, b))))
ctxt31 (c1, c2, c3)
c p
p a1 -> a2 -> a3 -> b
f 
scen32 :: ((c, ctxa, ctxa), (ctxb, ctxb), a -> a1 -> a2 -> (b1, b2))
-> (c, a -> (ctxa, a1 -> (ctxa, a2 -> ((ctxb, b1), (ctxb, b2)))))
scen32 (c :: (c, ctxa, ctxa)
c,p :: (ctxb, ctxb)
p,f :: a -> a1 -> a2 -> (b1, b2)
f) = (c, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a -> a1 -> a2 -> (b1, b2))
-> (c, a -> (ctxa, a1 -> (ctxa, a2 -> ((ctxb, b1), (ctxb, b2)))))
forall c ctxa ctxb a a1 a2 b1 b2.
(c, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a -> a1 -> a2 -> (b1, b2))
-> (c, a -> (ctxa, a1 -> (ctxa, a2 -> ((ctxb, b1), (ctxb, b2)))))
ctxt32 (c, ctxa, ctxa)
c (ctxb, ctxb)
p a -> a1 -> a2 -> (b1, b2)
f 
scen33 :: ((c1, c2, c3), (p1, p2, p3), a1 -> a2 -> a3 -> (b1, b2, b3))
-> (c1,
    a1 -> (c2, a2 -> (c3, a3 -> ((p1, b1), (p2, b2), (p3, b3)))))
scen33 (c :: (c1, c2, c3)
c,p :: (p1, p2, p3)
p,f :: a1 -> a2 -> a3 -> (b1, b2, b3)
f) = (c1, c2, c3)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> (b1, b2, b3))
-> (c1,
    a1 -> (c2, a2 -> (c3, a3 -> ((p1, b1), (p2, b2), (p3, b3)))))
forall c1 c2 c3 p1 p2 p3 a1 a2 a3 b1 b2 b3.
(c1, c2, c3)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> (b1, b2, b3))
-> (c1,
    a1 -> (c2, a2 -> (c3, a3 -> ((p1, b1), (p2, b2), (p3, b3)))))
ctxt33 (c1, c2, c3)
c (p1, p2, p3)
p a1 -> a2 -> a3 -> (b1, b2, b3)
f 
scen34 :: ((c1, c2, c3), (p1, p2, p3, p4),
 a1 -> a2 -> a3 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))
scen34 (c :: (c1, c2, c3)
c,p :: (p1, p2, p3, p4)
p,f :: a1 -> a2 -> a3 -> (b1, b2, b3, b4)
f) = (c1, c2, c3)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))
forall c1 c2 c3 p1 p2 p3 p4 a1 a2 a3 b1 b2 b3 b4.
(c1, c2, c3)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))
ctxt34 (c1, c2, c3)
c (p1, p2, p3, p4)
p a1 -> a2 -> a3 -> (b1, b2, b3, b4)
f 
scen41 :: ((c1, c2, c3, c4), p, a1 -> a2 -> a3 -> a4 -> b)
-> (c1, a1 -> (c2, a2 -> (c3, a3 -> (c4, a4 -> (p, b)))))
scen41 (c :: (c1, c2, c3, c4)
c,p :: p
p,f :: a1 -> a2 -> a3 -> a4 -> b
f) = (c1, c2, c3, c4)
-> p
-> (a1 -> a2 -> a3 -> a4 -> b)
-> (c1, a1 -> (c2, a2 -> (c3, a3 -> (c4, a4 -> (p, b)))))
forall c1 c2 c3 c4 p a1 a2 a3 a4 b.
(c1, c2, c3, c4)
-> p
-> (a1 -> a2 -> a3 -> a4 -> b)
-> (c1, a1 -> (c2, a2 -> (c3, a3 -> (c4, a4 -> (p, b)))))
ctxt41 (c1, c2, c3, c4)
c p
p a1 -> a2 -> a3 -> a4 -> b
f 
scen42 :: ((c1, c2, ctxa, ctxa), (ctxb, ctxb),
 a1 -> a2 -> a3 -> a4 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2 -> (ctxa, a3 -> (ctxa, a4 -> ((ctxb, b1), (ctxb, b2))))))
scen42 (c :: (c1, c2, ctxa, ctxa)
c,p :: (ctxb, ctxb)
p,f :: a1 -> a2 -> a3 -> a4 -> (b1, b2)
f) = (c1, c2, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2 -> (ctxa, a3 -> (ctxa, a4 -> ((ctxb, b1), (ctxb, b2))))))
forall c1 c2 ctxa ctxb a1 a2 a3 a4 b1 b2.
(c1, c2, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2 -> (ctxa, a3 -> (ctxa, a4 -> ((ctxb, b1), (ctxb, b2))))))
ctxt42 (c1, c2, ctxa, ctxa)
c (ctxb, ctxb)
p a1 -> a2 -> a3 -> a4 -> (b1, b2)
f 
scen43 :: ((c1, c2, c3, c4), (p1, p2, p3),
 a1 -> a2 -> a3 -> a4 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> (c4, a4 -> ((p1, b1), (p2, b2), (p3, b3))))))
scen43 (c :: (c1, c2, c3, c4)
c,p :: (p1, p2, p3)
p,f :: a1 -> a2 -> a3 -> a4 -> (b1, b2, b3)
f) = (c1, c2, c3, c4)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> (c4, a4 -> ((p1, b1), (p2, b2), (p3, b3))))))
forall c1 c2 c3 c4 p1 p2 p3 a1 a2 a3 a4 b1 b2 b3.
(c1, c2, c3, c4)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> (c4, a4 -> ((p1, b1), (p2, b2), (p3, b3))))))
ctxt43 (c1, c2, c3, c4)
c (p1, p2, p3)
p a1 -> a2 -> a3 -> a4 -> (b1, b2, b3)
f 
scen44 :: ((c1, c2, c3, c4), (p1, p2, p3, p4),
 a1 -> a2 -> a3 -> a4 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))
scen44 (c :: (c1, c2, c3, c4)
c,p :: (p1, p2, p3, p4)
p,f :: a1 -> a2 -> a3 -> a4 -> (b1, b2, b3, b4)
f) = (c1, c2, c3, c4)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))
forall c1 c2 c3 c4 p1 p2 p3 p4 a1 a2 a3 a4 b1 b2 b3 b4.
(c1, c2, c3, c4)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))
ctxt44 (c1, c2, c3, c4)
c (p1, p2, p3, p4)
p a1 -> a2 -> a3 -> a4 -> (b1, b2, b3, b4)
f
scen51 :: ((c1, c2, c3, c4, c5), p, a1 -> a2 -> a3 -> a4 -> a5 -> b)
-> (c1,
    a1 -> (c2, a2 -> (c3, a3 -> (c4, a4 -> (c5, a5 -> (p, b))))))
scen51 (c :: (c1, c2, c3, c4, c5)
c,p :: p
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> b
f) = (c1, c2, c3, c4, c5)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> b)
-> (c1,
    a1 -> (c2, a2 -> (c3, a3 -> (c4, a4 -> (c5, a5 -> (p, b))))))
forall c1 c2 c3 c4 c5 p a1 a2 a3 a4 a5 b.
(c1, c2, c3, c4, c5)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> b)
-> (c1,
    a1 -> (c2, a2 -> (c3, a3 -> (c4, a4 -> (c5, a5 -> (p, b))))))
ctxt51 (c1, c2, c3, c4, c5)
c p
p a1 -> a2 -> a3 -> a4 -> a5 -> b
f 
scen52 :: ((c1, c2, c3, ctxa, ctxa), (ctxb, ctxb),
 a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (ctxa, a4 -> (ctxa, a5 -> ((ctxb, b1), (ctxb, b2)))))))
scen52 (c :: (c1, c2, c3, ctxa, ctxa)
c,p :: (ctxb, ctxb)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2)
f) = (c1, c2, c3, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (ctxa, a4 -> (ctxa, a5 -> ((ctxb, b1), (ctxb, b2)))))))
forall c1 c2 c3 ctxa ctxb a1 a2 a3 a4 a5 b1 b2.
(c1, c2, c3, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (ctxa, a4 -> (ctxa, a5 -> ((ctxb, b1), (ctxb, b2)))))))
ctxt52 (c1, c2, c3, ctxa, ctxa)
c (ctxb, ctxb)
p a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2)
f 
scen53 :: ((c1, c2, c3, c4, c5), (p1, p2, p3),
 a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> (c5, a5 -> ((p1, b1), (p2, b2), (p3, b3)))))))
scen53 (c :: (c1, c2, c3, c4, c5)
c,p :: (p1, p2, p3)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3)
f) = (c1, c2, c3, c4, c5)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> (c5, a5 -> ((p1, b1), (p2, b2), (p3, b3)))))))
forall c1 c2 c3 c4 c5 p1 p2 p3 a1 a2 a3 a4 a5 b1 b2 b3.
(c1, c2, c3, c4, c5)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> (c5, a5 -> ((p1, b1), (p2, b2), (p3, b3)))))))
ctxt53 (c1, c2, c3, c4, c5)
c (p1, p2, p3)
p a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3)
f 
scen54 :: ((c1, c2, c3, c4, c5), (p1, p2, p3, p4),
 a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))))
scen54 (c :: (c1, c2, c3, c4, c5)
c,p :: (p1, p2, p3, p4)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3, b4)
f) = (c1, c2, c3, c4, c5)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))))
forall c1 c2 c3 c4 c5 p1 p2 p3 p4 a1 a2 a3 a4 a5 b1 b2 b3 b4.
(c1, c2, c3, c4, c5)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))))
ctxt54 (c1, c2, c3, c4, c5)
c (p1, p2, p3, p4)
p a1 -> a2 -> a3 -> a4 -> a5 -> (b1, b2, b3, b4)
f 
scen61 :: ((c1, c2, c3, c4, c5, c6), p,
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> b)
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> (c4, a4 -> (c5, a5 -> (c6, a6 -> (p, b)))))))
scen61 (c :: (c1, c2, c3, c4, c5, c6)
c,p :: p
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> b
f) = (c1, c2, c3, c4, c5, c6)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> b)
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> (c4, a4 -> (c5, a5 -> (c6, a6 -> (p, b)))))))
forall c1 c2 c3 c4 c5 c6 p a1 a2 a3 a4 a5 a6 b.
(c1, c2, c3, c4, c5, c6)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> b)
-> (c1,
    a1
    -> (c2,
        a2 -> (c3, a3 -> (c4, a4 -> (c5, a5 -> (c6, a6 -> (p, b)))))))
ctxt61 (c1, c2, c3, c4, c5, c6)
c p
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> b
f 
scen62 :: ((c1, c2, c3, c4, ctxa, ctxa), (ctxb, ctxb),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (ctxa, a5 -> (ctxa, a6 -> ((ctxb, b1), (ctxb, b2))))))))
scen62 (c :: (c1, c2, c3, c4, ctxa, ctxa)
c,p :: (ctxb, ctxb)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2)
f) = (c1, c2, c3, c4, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (ctxa, a5 -> (ctxa, a6 -> ((ctxb, b1), (ctxb, b2))))))))
forall c1 c2 c3 c4 ctxa ctxb a1 a2 a3 a4 a5 a6 b1 b2.
(c1, c2, c3, c4, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (ctxa, a5 -> (ctxa, a6 -> ((ctxb, b1), (ctxb, b2))))))))
ctxt62 (c1, c2, c3, c4, ctxa, ctxa)
c (ctxb, ctxb)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2)
f 
scen63 :: ((c1, c2, c3, c4, c5, c6), (p1, p2, p3),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> (c6, a6 -> ((p1, b1), (p2, b2), (p3, b3))))))))
scen63 (c :: (c1, c2, c3, c4, c5, c6)
c,p :: (p1, p2, p3)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3)
f) = (c1, c2, c3, c4, c5, c6)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> (c6, a6 -> ((p1, b1), (p2, b2), (p3, b3))))))))
forall c1 c2 c3 c4 c5 c6 p1 p2 p3 a1 a2 a3 a4 a5 a6 b1 b2 b3.
(c1, c2, c3, c4, c5, c6)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> (c6, a6 -> ((p1, b1), (p2, b2), (p3, b3))))))))
ctxt63 (c1, c2, c3, c4, c5, c6)
c (p1, p2, p3)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3)
f 
scen64 :: ((c1, c2, c3, c4, c5, c6), (p1, p2, p3, p4),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (c6, a6 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))))
scen64 (c :: (c1, c2, c3, c4, c5, c6)
c,p :: (p1, p2, p3, p4)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3, b4)
f) = (c1, c2, c3, c4, c5, c6)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (c6, a6 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))))
forall c1 c2 c3 c4 c5 c6 p1 p2 p3 p4 a1 a2 a3 a4 a5 a6 b1 b2 b3 b4.
(c1, c2, c3, c4, c5, c6)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (c6, a6 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))))
ctxt64 (c1, c2, c3, c4, c5, c6)
c (p1, p2, p3, p4)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> (b1, b2, b3, b4)
f 
scen71 :: ((c1, c2, c3, c4, c5, c6, c7), p,
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> b)
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> (c5, a5 -> (c6, a6 -> (c7, a7 -> (p, b))))))))
scen71 (c :: (c1, c2, c3, c4, c5, c6, c7)
c,p :: p
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> b
f) = (c1, c2, c3, c4, c5, c6, c7)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> b)
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> (c5, a5 -> (c6, a6 -> (c7, a7 -> (p, b))))))))
forall c1 c2 c3 c4 c5 c6 c7 p a1 a2 a3 a4 a5 a6 a7 b.
(c1, c2, c3, c4, c5, c6, c7)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> b)
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3 -> (c4, a4 -> (c5, a5 -> (c6, a6 -> (c7, a7 -> (p, b))))))))
ctxt71 (c1, c2, c3, c4, c5, c6, c7)
c p
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> b
f 
scen72 :: ((c1, c2, c3, c4, c5, ctxa, ctxa), (ctxb, ctxb),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (ctxa, a6 -> (ctxa, a7 -> ((ctxb, b1), (ctxb, b2)))))))))
scen72 (c :: (c1, c2, c3, c4, c5, ctxa, ctxa)
c,p :: (ctxb, ctxb)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2)
f) = (c1, c2, c3, c4, c5, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (ctxa, a6 -> (ctxa, a7 -> ((ctxb, b1), (ctxb, b2)))))))))
forall c1 c2 c3 c4 c5 ctxa ctxb a1 a2 a3 a4 a5 a6 a7 b1 b2.
(c1, c2, c3, c4, c5, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (ctxa, a6 -> (ctxa, a7 -> ((ctxb, b1), (ctxb, b2)))))))))
ctxt72 (c1, c2, c3, c4, c5, ctxa, ctxa)
c (ctxb, ctxb)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2)
f 
scen73 :: ((c1, c2, c3, c4, c5, c6, c7), (p1, p2, p3),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (c6, a6 -> (c7, a7 -> ((p1, b1), (p2, b2), (p3, b3)))))))))
scen73 (c :: (c1, c2, c3, c4, c5, c6, c7)
c,p :: (p1, p2, p3)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3)
f) = (c1, c2, c3, c4, c5, c6, c7)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (c6, a6 -> (c7, a7 -> ((p1, b1), (p2, b2), (p3, b3)))))))))
forall c1 c2 c3 c4 c5 c6 c7 p1 p2 p3 a1 a2 a3 a4 a5 a6 a7 b1 b2 b3.
(c1, c2, c3, c4, c5, c6, c7)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5 -> (c6, a6 -> (c7, a7 -> ((p1, b1), (p2, b2), (p3, b3)))))))))
ctxt73 (c1, c2, c3, c4, c5, c6, c7)
c (p1, p2, p3)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3)
f 
scen74 :: ((c1, c2, c3, c4, c5, c6, c7), (p1, p2, p3, p4),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (c7, a7 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))))))
scen74 (c :: (c1, c2, c3, c4, c5, c6, c7)
c,p :: (p1, p2, p3, p4)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3, b4)
f) = (c1, c2, c3, c4, c5, c6, c7)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (c7, a7 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))))))
forall c1 c2 c3 c4 c5 c6 c7 p1 p2 p3 p4 a1 a2 a3 a4 a5 a6 a7 b1 b2
       b3 b4.
(c1, c2, c3, c4, c5, c6, c7)
-> (p1, p2, p3, p4)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (c7, a7 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4)))))))))
ctxt74 (c1, c2, c3, c4, c5, c6, c7)
c (p1, p2, p3, p4)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> (b1, b2, b3, b4)
f 
scen81 :: ((c1, c2, c3, c4, c5, c6, c7, c8), p,
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> b)
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> (c6, a6 -> (c7, a7 -> (c8, a8 -> (p, b)))))))))
scen81 (c :: (c1, c2, c3, c4, c5, c6, c7, c8)
c,p :: p
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> b
f) = (c1, c2, c3, c4, c5, c6, c7, c8)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> b)
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> (c6, a6 -> (c7, a7 -> (c8, a8 -> (p, b)))))))))
forall c1 c2 c3 c4 c5 c6 c7 c8 p a1 a2 a3 a4 a5 a6 a7 a8 b.
(c1, c2, c3, c4, c5, c6, c7, c8)
-> p
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> b)
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4 -> (c5, a5 -> (c6, a6 -> (c7, a7 -> (c8, a8 -> (p, b)))))))))
ctxt81 (c1, c2, c3, c4, c5, c6, c7, c8)
c p
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> b
f 
scen82 :: ((c1, c2, c3, c4, c5, c6, ctxa, ctxa), (ctxb, ctxb),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (ctxa, a7 -> (ctxa, a8 -> ((ctxb, b1), (ctxb, b2))))))))))
scen82 (c :: (c1, c2, c3, c4, c5, c6, ctxa, ctxa)
c,p :: (ctxb, ctxb)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2)
f) = (c1, c2, c3, c4, c5, c6, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (ctxa, a7 -> (ctxa, a8 -> ((ctxb, b1), (ctxb, b2))))))))))
forall c1 c2 c3 c4 c5 c6 ctxa ctxb a1 a2 a3 a4 a5 a6 a7 a8 b1 b2.
(c1, c2, c3, c4, c5, c6, ctxa, ctxa)
-> (ctxb, ctxb)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (ctxa, a7 -> (ctxa, a8 -> ((ctxb, b1), (ctxb, b2))))))))))
ctxt82 (c1, c2, c3, c4, c5, c6, ctxa, ctxa)
c (ctxb, ctxb)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2)
f 
scen83 :: ((c1, c2, c3, c4, c5, c6, c7, c8), (p1, p2, p3),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (c7, a7 -> (c8, a8 -> ((p1, b1), (p2, b2), (p3, b3))))))))))
scen83 (c :: (c1, c2, c3, c4, c5, c6, c7, c8)
c,p :: (p1, p2, p3)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3)
f) = (c1, c2, c3, c4, c5, c6, c7, c8)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (c7, a7 -> (c8, a8 -> ((p1, b1), (p2, b2), (p3, b3))))))))))
forall c1 c2 c3 c4 c5 c6 c7 c8 p1 p2 p3 a1 a2 a3 a4 a5 a6 a7 a8 b1
       b2 b3.
(c1, c2, c3, c4, c5, c6, c7, c8)
-> (p1, p2, p3)
-> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6 -> (c7, a7 -> (c8, a8 -> ((p1, b1), (p2, b2), (p3, b3))))))))))
ctxt83 (c1, c2, c3, c4, c5, c6, c7, c8)
c (p1, p2, p3)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3)
f 
scen84 :: ((c1, c2, c3, c4, c5, c6, c7, c8), (p1, p2, p3, p4),
 a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6
                        -> (c7,
                            a7 -> (c8, a8 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))))))
scen84 (c :: (c1, c2, c3, c4, c5, c6, c7, c8)
c,p :: (p1, p2, p3, p4)
p,f :: a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3, b4)
f) = (c1, c2, c3, c4, c5, c6, c7, c8)
-> (p1, p2, p3, p4)
-> (a1
    -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6
                        -> (c7,
                            a7 -> (c8, a8 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))))))
forall c1 c2 c3 c4 c5 c6 c7 c8 p1 p2 p3 p4 a1 a2 a3 a4 a5 a6 a7 a8
       b1 b2 b3 b4.
(c1, c2, c3, c4, c5, c6, c7, c8)
-> (p1, p2, p3, p4)
-> (a1
    -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3, b4))
-> (c1,
    a1
    -> (c2,
        a2
        -> (c3,
            a3
            -> (c4,
                a4
                -> (c5,
                    a5
                    -> (c6,
                        a6
                        -> (c7,
                            a7 -> (c8, a8 -> ((p1, b1), (p2, b2), (p3, b3), (p4, b4))))))))))
ctxt84 (c1, c2, c3, c4, c5, c6, c7, c8)
c (p1, p2, p3, p4)
p a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> (b1, b2, b3, b4)
f