{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
module FRP.Yampa.InternalCore (
module Control.Arrow,
Time,
DTime,
SF(..),
SF'(..),
Transition,
sfTF',
sfId,
sfConst,
sfArrG,
sfSScan,
FunDesc(..),
fdFun,
arrPrim,
arrEPrim,
epPrim
) where
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative (Applicative(..))
#endif
import Control.Arrow
#if __GLASGOW_HASKELL__ >= 610
import qualified Control.Category (Category(..))
#endif
import FRP.Yampa.Diagnostics
import FRP.Yampa.Event
type Time = Double
type DTime = Double
data SF a b = SF {SF a b -> a -> Transition a b
sfTF :: a -> Transition a b}
data SF' a b where
SFArr :: !(DTime -> a -> Transition a b) -> !(FunDesc a b) -> SF' a b
SFSScan :: !(DTime -> a -> Transition a b)
-> !(c -> a -> Maybe (c, b)) -> !c -> b
-> SF' a b
SFEP :: !(DTime -> Event a -> Transition (Event a) b)
-> !(c -> a -> (c, b, b)) -> !c -> b
-> SF' (Event a) b
SFCpAXA :: !(DTime -> a -> Transition a d)
-> !(FunDesc a b) -> !(SF' b c) -> !(FunDesc c d)
-> SF' a d
SF' :: !(DTime -> a -> Transition a b) -> SF' a b
type Transition a b = (SF' a b, b)
sfTF' :: SF' a b -> (DTime -> a -> Transition a b)
sfTF' :: SF' a b -> DTime -> a -> Transition a b
sfTF' (SFArr DTime -> a -> Transition a b
tf FunDesc a b
_) = DTime -> a -> Transition a b
tf
sfTF' (SFSScan DTime -> a -> Transition a b
tf c -> a -> Maybe (c, b)
_ c
_ b
_) = DTime -> a -> Transition a b
tf
sfTF' (SFEP DTime -> Event a -> Transition (Event a) b
tf c -> a -> (c, b, b)
_ c
_ b
_) = DTime -> a -> Transition a b
DTime -> Event a -> Transition (Event a) b
tf
sfTF' (SFCpAXA DTime -> a -> Transition a b
tf FunDesc a b
_ SF' b c
_ FunDesc c b
_) = DTime -> a -> Transition a b
tf
sfTF' (SF' DTime -> a -> Transition a b
tf) = DTime -> a -> Transition a b
tf
sfArr :: FunDesc a b -> SF' a b
sfArr :: FunDesc a b -> SF' a b
sfArr FunDesc a b
FDI = SF' a b
forall a. SF' a a
sfId
sfArr (FDC b
b) = b -> SF' a b
forall b a. b -> SF' a b
sfConst b
b
sfArr (FDE Event a -> b
f b
fne) = (Event a -> b) -> b -> SF' (Event a) b
forall a b. (Event a -> b) -> b -> SF' (Event a) b
sfArrE Event a -> b
f b
fne
sfArr (FDG a -> b
f) = (a -> b) -> SF' a b
forall a b. (a -> b) -> SF' a b
sfArrG a -> b
f
sfId :: SF' a a
sfId :: SF' a a
sfId = SF' a a
forall a. SF' a a
sf
where
sf :: SF' b b
sf = (DTime -> b -> Transition b b) -> FunDesc b b -> SF' b b
forall a b.
(DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
SFArr (\DTime
_ b
a -> (SF' b b
sf, b
a)) FunDesc b b
forall a. FunDesc a a
FDI
sfConst :: b -> SF' a b
sfConst :: b -> SF' a b
sfConst b
b = SF' a b
sf
where
sf :: SF' a b
sf = (DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
forall a b.
(DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
SFArr (\DTime
_ a
_ -> (SF' a b
sf, b
b)) (b -> FunDesc a b
forall b a. b -> FunDesc a b
FDC b
b)
sfArrE :: (Event a -> b) -> b -> SF' (Event a) b
sfArrE :: (Event a -> b) -> b -> SF' (Event a) b
sfArrE Event a -> b
f b
fne = SF' (Event a) b
sf
where
sf :: SF' (Event a) b
sf = (DTime -> Event a -> Transition (Event a) b)
-> FunDesc (Event a) b -> SF' (Event a) b
forall a b.
(DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
SFArr (\DTime
_ Event a
ea -> (SF' (Event a) b
sf, case Event a
ea of Event a
NoEvent -> b
fne ; Event a
_ -> Event a -> b
f Event a
ea))
((Event a -> b) -> b -> FunDesc (Event a) b
forall a b. (Event a -> b) -> b -> FunDesc (Event a) b
FDE Event a -> b
f b
fne)
sfArrG :: (a -> b) -> SF' a b
sfArrG :: (a -> b) -> SF' a b
sfArrG a -> b
f = SF' a b
sf
where
sf :: SF' a b
sf = (DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
forall a b.
(DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
SFArr (\DTime
_ a
a -> (SF' a b
sf, a -> b
f a
a)) ((a -> b) -> FunDesc a b
forall a b. (a -> b) -> FunDesc a b
FDG a -> b
f)
epPrim :: (c -> a -> (c, b, b)) -> c -> b -> SF (Event a) b
epPrim :: (c -> a -> (c, b, b)) -> c -> b -> SF (Event a) b
epPrim c -> a -> (c, b, b)
f c
c b
bne = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: Event a -> Transition (Event a) b
sfTF = Event a -> Transition (Event a) b
tf0}
where
tf0 :: Event a -> Transition (Event a) b
tf0 Event a
NoEvent = ((c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP c -> a -> (c, b, b)
f c
c b
bne, b
bne)
tf0 (Event a
a) = let
(c
c', b
b, b
bne') = c -> a -> (c, b, b)
f c
c a
a
in
((c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP c -> a -> (c, b, b)
f c
c' b
bne', b
b)
sfEP :: (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP :: (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP c -> a -> (c, b, b)
f c
c b
bne = SF' (Event a) b
sf
where
sf :: SF' (Event a) b
sf = (DTime -> Event a -> Transition (Event a) b)
-> (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
forall a b c.
(DTime -> Event a -> Transition (Event a) b)
-> (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
SFEP (\DTime
_ Event a
ea -> case Event a
ea of
Event a
NoEvent -> (SF' (Event a) b
sf, b
bne)
Event a
a -> let
(c
c', b
b, b
bne') = c -> a -> (c, b, b)
f c
c a
a
in
((c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP c -> a -> (c, b, b)
f c
c' b
bne', b
b))
c -> a -> (c, b, b)
f
c
c
b
bne
data FunDesc a b where
FDI :: FunDesc a a
FDC :: b -> FunDesc a b
FDE :: (Event a -> b) -> b -> FunDesc (Event a) b
FDG :: (a -> b) -> FunDesc a b
fdFun :: FunDesc a b -> (a -> b)
fdFun :: FunDesc a b -> a -> b
fdFun FunDesc a b
FDI = a -> b
forall a. a -> a
id
fdFun (FDC b
b) = b -> a -> b
forall a b. a -> b -> a
const b
b
fdFun (FDE Event a -> b
f b
_) = a -> b
Event a -> b
f
fdFun (FDG a -> b
f) = a -> b
f
fdComp :: FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp :: FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc a b
FDI FunDesc b c
fd2 = FunDesc a c
FunDesc b c
fd2
fdComp FunDesc a b
fd1 FunDesc b c
FDI = FunDesc a b
FunDesc a c
fd1
fdComp (FDC b
b) FunDesc b c
fd2 = c -> FunDesc a c
forall b a. b -> FunDesc a b
FDC ((FunDesc b c -> b -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc b c
fd2) b
b)
fdComp FunDesc a b
_ (FDC c
c) = c -> FunDesc a c
forall b a. b -> FunDesc a b
FDC c
c
fdComp (FDE Event a -> b
f1 b
f1ne) FunDesc b c
fd2 = (Event a -> c) -> c -> FunDesc (Event a) c
forall a b. (Event a -> b) -> b -> FunDesc (Event a) b
FDE (b -> c
f2 (b -> c) -> (Event a -> b) -> Event a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Event a -> b
f1) (b -> c
f2 b
f1ne)
where
f2 :: b -> c
f2 = FunDesc b c -> b -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc b c
fd2
fdComp (FDG a -> b
f1) (FDE Event a -> c
f2 c
f2ne) = (a -> c) -> FunDesc a c
forall a b. (a -> b) -> FunDesc a b
FDG a -> c
f
where
f :: a -> c
f a
a = case a -> b
f1 a
a of
b
NoEvent -> c
f2ne
b
f1a -> Event a -> c
f2 b
Event a
f1a
fdComp (FDG a -> b
f1) FunDesc b c
fd2 = (a -> c) -> FunDesc a c
forall a b. (a -> b) -> FunDesc a b
FDG (FunDesc b c -> b -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc b c
fd2 (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f1)
fdPar :: FunDesc a b -> FunDesc c d -> FunDesc (a,c) (b,d)
fdPar :: FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar FunDesc a b
FDI FunDesc c d
FDI = FunDesc (a, c) (b, d)
forall a. FunDesc a a
FDI
fdPar FunDesc a b
FDI (FDC d
d) = ((a, c) -> (a, d)) -> FunDesc (a, c) (a, d)
forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
a, c
_)) -> (a
a, d
d))
fdPar FunDesc a b
FDI FunDesc c d
fd2 = ((a, c) -> (a, d)) -> FunDesc (a, c) (a, d)
forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
a, c
c)) -> (a
a, (FunDesc c d -> c -> d
forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd2) c
c))
fdPar (FDC b
b) FunDesc c d
FDI = ((a, c) -> (b, c)) -> FunDesc (a, c) (b, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
_, c
c)) -> (b
b, c
c))
fdPar (FDC b
b) (FDC d
d) = (b, d) -> FunDesc (a, c) (b, d)
forall b a. b -> FunDesc a b
FDC (b
b, d
d)
fdPar (FDC b
b) FunDesc c d
fd2 = ((a, c) -> (b, d)) -> FunDesc (a, c) (b, d)
forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
_, c
c)) -> (b
b, (FunDesc c d -> c -> d
forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd2) c
c))
fdPar FunDesc a b
fd1 FunDesc c d
fd2 = ((a, c) -> (b, d)) -> FunDesc (a, c) (b, d)
forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
a, c
c)) -> ((FunDesc a b -> a -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a, (FunDesc c d -> c -> d
forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd2) c
c))
fdFanOut :: FunDesc a b -> FunDesc a c -> FunDesc a (b,c)
fdFanOut :: FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
FDI FunDesc a c
FDI = (a -> (a, a)) -> FunDesc a (a, a)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
a, a
a))
fdFanOut FunDesc a b
FDI (FDC c
c) = (a -> (a, c)) -> FunDesc a (a, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
a, c
c))
fdFanOut FunDesc a b
FDI FunDesc a c
fd2 = (a -> (a, c)) -> FunDesc a (a, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
a, (FunDesc a c -> a -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a c
fd2) a
a))
fdFanOut (FDC b
b) FunDesc a c
FDI = (a -> (b, a)) -> FunDesc a (b, a)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (b
b, a
a))
fdFanOut (FDC b
b) (FDC c
c) = (b, c) -> FunDesc a (b, c)
forall b a. b -> FunDesc a b
FDC (b
b, c
c)
fdFanOut (FDC b
b) FunDesc a c
fd2 = (a -> (b, c)) -> FunDesc a (b, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (b
b, (FunDesc a c -> a -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a c
fd2) a
a))
fdFanOut (FDE Event a -> b
f1 b
f1ne) (FDE Event a -> c
f2 c
f2ne) = (Event a -> (b, c)) -> (b, c) -> FunDesc (Event a) (b, c)
forall a b. (Event a -> b) -> b -> FunDesc (Event a) b
FDE Event a -> (b, c)
f1f2 (b, c)
f1f2ne
where
f1f2 :: Event a -> (b, c)
f1f2 Event a
NoEvent = (b, c)
f1f2ne
f1f2 ea :: Event a
ea@(Event a
_) = (Event a -> b
f1 Event a
ea, Event a -> c
f2 Event a
Event a
ea)
f1f2ne :: (b, c)
f1f2ne = (b
f1ne, c
f2ne)
fdFanOut FunDesc a b
fd1 FunDesc a c
fd2 =
(a -> (b, c)) -> FunDesc a (b, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> ((FunDesc a b -> a -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a, (FunDesc a c -> a -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a c
fd2) a
a))
vfyNoEv :: Event a -> b -> b
vfyNoEv :: Event a -> b -> b
vfyNoEv Event a
NoEvent b
b = b
b
vfyNoEv Event a
_ b
_ =
String -> String -> String -> b
forall a. String -> String -> String -> a
usrErr
String
"AFRP"
String
"vfyNoEv"
String
"Assertion failed: Functions on events must not map NoEvent to Event."
#if __GLASGOW_HASKELL__ >= 610
instance Control.Category.Category SF where
. :: SF b c -> SF a b -> SF a c
(.) = (SF a b -> SF b c -> SF a c) -> SF b c -> SF a b -> SF a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip SF a b -> SF b c -> SF a c
forall a b c. SF a b -> SF b c -> SF a c
compPrim
id :: SF a a
id = (a -> Transition a a) -> SF a a
forall a b. (a -> Transition a b) -> SF a b
SF ((a -> Transition a a) -> SF a a)
-> (a -> Transition a a) -> SF a a
forall a b. (a -> b) -> a -> b
$ \a
x -> (SF' a a
forall a. SF' a a
sfId,a
x)
#endif
instance ArrowChoice SF where
SF b c
sfL +++ :: SF b c -> SF b' c' -> SF (Either b b') (Either c c')
+++ SF b' c'
sfR = (Either b b' -> Transition (Either b b') (Either c c'))
-> SF (Either b b') (Either c c')
forall a b. (a -> Transition a b) -> SF a b
SF ((Either b b' -> Transition (Either b b') (Either c c'))
-> SF (Either b b') (Either c c'))
-> (Either b b' -> Transition (Either b b') (Either c c'))
-> SF (Either b b') (Either c c')
forall a b. (a -> b) -> a -> b
$ \Either b b'
a ->
case Either b b'
a of
Left b
b -> let (SF' b c
sf', c
c) = SF b c -> b -> (SF' b c, c)
forall a b. SF a b -> a -> Transition a b
sfTF SF b c
sfL b
b
in (SF' b c -> SF b' c' -> SF' (Either b b') (Either c c')
forall a a a b. SF' a a -> SF a b -> SF' (Either a a) (Either a b)
chooseL SF' b c
sf' SF b' c'
sfR, c -> Either c c'
forall a b. a -> Either a b
Left c
c)
Right b'
d -> let (SF' b' c'
sf', c'
e) = SF b' c' -> b' -> (SF' b' c', c')
forall a b. SF a b -> a -> Transition a b
sfTF SF b' c'
sfR b'
d
in (SF b c -> SF' b' c' -> SF' (Either b b') (Either c c')
forall a a a b. SF a a -> SF' a b -> SF' (Either a a) (Either a b)
chooseR SF b c
sfL SF' b' c'
sf', c' -> Either c c'
forall a b. b -> Either a b
Right c'
e)
where
chooseL :: SF' a a -> SF a b -> SF' (Either a a) (Either a b)
chooseL SF' a a
sfCL SF a b
sfR = (DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' ((DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b))
-> (DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b)
forall a b. (a -> b) -> a -> b
$ \DTime
dt Either a a
a ->
case Either a a
a of
Left a
b -> let (SF' a a
sf', a
c) = SF' a a -> DTime -> a -> (SF' a a, a)
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a a
sfCL DTime
dt a
b
in (SF' a a -> SF a b -> SF' (Either a a) (Either a b)
chooseL SF' a a
sf' SF a b
sfR, a -> Either a b
forall a b. a -> Either a b
Left a
c)
Right a
d -> let (SF' a b
sf', b
e) = SF a b -> a -> (SF' a b, b)
forall a b. SF a b -> a -> Transition a b
sfTF SF a b
sfR a
d
in (SF' a a -> SF' a b -> SF' (Either a a) (Either a b)
forall a a a b. SF' a a -> SF' a b -> SF' (Either a a) (Either a b)
choose SF' a a
sfCL SF' a b
sf', b -> Either a b
forall a b. b -> Either a b
Right b
e)
chooseR :: SF a a -> SF' a b -> SF' (Either a a) (Either a b)
chooseR SF a a
sfL SF' a b
sfCR = (DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' ((DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b))
-> (DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b)
forall a b. (a -> b) -> a -> b
$ \DTime
dt Either a a
a ->
case Either a a
a of
Left a
b -> let (SF' a a
sf', a
c) = SF a a -> a -> (SF' a a, a)
forall a b. SF a b -> a -> Transition a b
sfTF SF a a
sfL a
b
in (SF' a a -> SF' a b -> SF' (Either a a) (Either a b)
forall a a a b. SF' a a -> SF' a b -> SF' (Either a a) (Either a b)
choose SF' a a
sf' SF' a b
sfCR, a -> Either a b
forall a b. a -> Either a b
Left a
c)
Right a
d -> let (SF' a b
sf', b
e) = SF' a b -> DTime -> a -> (SF' a b, b)
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sfCR DTime
dt a
d
in (SF a a -> SF' a b -> SF' (Either a a) (Either a b)
chooseR SF a a
sfL SF' a b
sf', b -> Either a b
forall a b. b -> Either a b
Right b
e)
choose :: SF' a a -> SF' a b -> SF' (Either a a) (Either a b)
choose SF' a a
sfCL SF' a b
sfCR = (DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' ((DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b))
-> (DTime -> Either a a -> Transition (Either a a) (Either a b))
-> SF' (Either a a) (Either a b)
forall a b. (a -> b) -> a -> b
$ \DTime
dt Either a a
a ->
case Either a a
a of
Left a
b -> let (SF' a a
sf', a
c) = SF' a a -> DTime -> a -> (SF' a a, a)
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a a
sfCL DTime
dt a
b
in (SF' a a -> SF' a b -> SF' (Either a a) (Either a b)
choose SF' a a
sf' SF' a b
sfCR, a -> Either a b
forall a b. a -> Either a b
Left a
c)
Right a
d -> let (SF' a b
sf', b
e) = SF' a b -> DTime -> a -> (SF' a b, b)
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sfCR DTime
dt a
d
in (SF' a a -> SF' a b -> SF' (Either a a) (Either a b)
choose SF' a a
sfCL SF' a b
sf', b -> Either a b
forall a b. b -> Either a b
Right b
e)
instance Arrow SF where
arr :: (b -> c) -> SF b c
arr = (b -> c) -> SF b c
forall b c. (b -> c) -> SF b c
arrPrim
first :: SF b c -> SF (b, d) (c, d)
first = SF b c -> SF (b, d) (c, d)
forall b c d. SF b c -> SF (b, d) (c, d)
firstPrim
second :: SF b c -> SF (d, b) (d, c)
second = SF b c -> SF (d, b) (d, c)
forall b c d. SF b c -> SF (d, b) (d, c)
secondPrim
*** :: SF b c -> SF b' c' -> SF (b, b') (c, c')
(***) = SF b c -> SF b' c' -> SF (b, b') (c, c')
forall b c b' c'. SF b c -> SF b' c' -> SF (b, b') (c, c')
parSplitPrim
&&& :: SF b c -> SF b c' -> SF b (c, c')
(&&&) = SF b c -> SF b c' -> SF b (c, c')
forall b c c'. SF b c -> SF b c' -> SF b (c, c')
parFanOutPrim
#if __GLASGOW_HASKELL__ >= 610
#else
(>>>) = compPrim
#endif
instance Functor (SF a) where
fmap :: (a -> b) -> SF a a -> SF a b
fmap a -> b
f = (SF a a -> SF a b -> SF a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (a -> b) -> SF a b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> b
f)
instance Applicative (SF a) where
pure :: a -> SF a a
pure a
x = (a -> a) -> SF a a
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (a -> a -> a
forall a b. a -> b -> a
const a
x)
SF a (a -> b)
f <*> :: SF a (a -> b) -> SF a a -> SF a b
<*> SF a a
x = (SF a (a -> b)
f SF a (a -> b) -> SF a a -> SF a (a -> b, a)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& SF a a
x) SF a (a -> b, a) -> SF (a -> b, a) b -> SF a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ((a -> b, a) -> b) -> SF (a -> b, a) b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((a -> b) -> a -> b) -> (a -> b, a) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($))
{-# NOINLINE arrPrim #-}
arrPrim :: (a -> b) -> SF a b
arrPrim :: (a -> b) -> SF a b
arrPrim a -> b
f = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: a -> Transition a b
sfTF = \a
a -> ((a -> b) -> SF' a b
forall a b. (a -> b) -> SF' a b
sfArrG a -> b
f, a -> b
f a
a)}
{-# RULES "arrPrim/arrEPrim" arrPrim = arrEPrim #-}
arrEPrim :: (Event a -> b) -> SF (Event a) b
arrEPrim :: (Event a -> b) -> SF (Event a) b
arrEPrim Event a -> b
f = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: Event a -> Transition (Event a) b
sfTF = \Event a
a -> ((Event a -> b) -> b -> SF' (Event a) b
forall a b. (Event a -> b) -> b -> SF' (Event a) b
sfArrE Event a -> b
f (Event a -> b
f Event a
forall a. Event a
NoEvent), Event a -> b
f Event a
a)}
compPrim :: SF a b -> SF b c -> SF a c
compPrim :: SF a b -> SF b c -> SF a c
compPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a b
tf10}) (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = b -> Transition b c
tf20}) = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: a -> Transition a c
sfTF = a -> Transition a c
tf0}
where
tf0 :: a -> Transition a c
tf0 a
a0 = (SF' a b -> SF' b c -> SF' a c
forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX SF' a b
sf1 SF' b c
sf2, c
c0)
where
(SF' a b
sf1, b
b0) = a -> Transition a b
tf10 a
a0
(SF' b c
sf2, c
c0) = b -> Transition b c
tf20 b
b0
cpXX :: SF' a b -> SF' b c -> SF' a c
cpXX :: SF' a b -> SF' b c -> SF' a c
cpXX (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) SF' b c
sf2 = FunDesc a b -> SF' b c -> SF' a c
forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd1 SF' b c
sf2
cpXX SF' a b
sf1 (SFArr DTime -> b -> Transition b c
_ FunDesc b c
fd2) = SF' a b -> FunDesc b c -> SF' a c
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' a b
sf1 FunDesc b c
fd2
cpXX (SFSScan DTime -> a -> Transition a b
_ c -> a -> Maybe (c, b)
f1 c
s1 b
b) (SFSScan DTime -> b -> Transition b c
_ c -> b -> Maybe (c, c)
f2 c
s2 c
c) =
((c, b, c, c) -> a -> Maybe ((c, b, c, c), c))
-> (c, b, c, c) -> c -> SF' a c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan (c, b, c, c) -> a -> Maybe ((c, b, c, c), c)
f (c
s1, b
b, c
s2, c
c) c
c
where
f :: (c, b, c, c) -> a -> Maybe ((c, b, c, c), c)
f (c
s1, b
b, c
s2, c
c) a
a =
let
(Bool
u, c
s1', b
b') = case c -> a -> Maybe (c, b)
f1 c
s1 a
a of
Maybe (c, b)
Nothing -> (Bool
True, c
s1, b
b)
Just (c
s1',b
b') -> (Bool
False, c
s1', b
b')
in
case c -> b -> Maybe (c, c)
f2 c
s2 b
b' of
Maybe (c, c)
Nothing | Bool
u -> Maybe ((c, b, c, c), c)
forall a. Maybe a
Nothing
| Bool
otherwise -> ((c, b, c, c), c) -> Maybe ((c, b, c, c), c)
forall a. a -> Maybe a
Just ((c
s1', b
b', c
s2, c
c), c
c)
Just (c
s2', c
c') -> ((c, b, c, c), c) -> Maybe ((c, b, c, c), c)
forall a. a -> Maybe a
Just ((c
s1', b
b', c
s2', c
c'), c
c')
cpXX (SFSScan DTime -> a -> Transition a b
_ c -> a -> Maybe (c, b)
f1 c
s1 b
eb) (SFEP DTime -> Event a -> Transition (Event a) c
_ c -> a -> (c, c, c)
f2 c
s2 c
cne) =
((c, Event a, c, c) -> a -> Maybe ((c, Event a, c, c), c))
-> (c, Event a, c, c) -> c -> SF' a c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan (c, Event a, c, c) -> a -> Maybe ((c, Event a, c, c), c)
f (c
s1, b
Event a
eb, c
s2, c
cne) c
cne
where
f :: (c, Event a, c, c) -> a -> Maybe ((c, Event a, c, c), c)
f (c
s1, Event a
eb, c
s2, c
cne) a
a =
case c -> a -> Maybe (c, b)
f1 c
s1 a
a of
Maybe (c, b)
Nothing ->
case Event a
eb of
Event a
NoEvent -> Maybe ((c, Event a, c, c), c)
forall a. Maybe a
Nothing
Event a
b ->
let (c
s2', c
c, c
cne') = c -> a -> (c, c, c)
f2 c
s2 a
b
in
((c, Event a, c, c), c) -> Maybe ((c, Event a, c, c), c)
forall a. a -> Maybe a
Just ((c
s1, Event a
eb, c
s2', c
cne'), c
c)
Just (c
s1', b
eb') ->
case b
eb' of
b
NoEvent -> ((c, b, c, c), c) -> Maybe ((c, b, c, c), c)
forall a. a -> Maybe a
Just ((c
s1', b
eb', c
s2, c
cne), c
cne)
Event b ->
let (c
s2', c
c, c
cne') = c -> a -> (c, c, c)
f2 c
s2 a
b
in
((c, b, c, c), c) -> Maybe ((c, b, c, c), c)
forall a. a -> Maybe a
Just ((c
s1', b
eb', c
s2', c
cne'), c
c)
cpXX (SFEP DTime -> Event a -> Transition (Event a) b
_ c -> a -> (c, b, b)
f1 c
s1 b
bne) (SFSScan DTime -> b -> Transition b c
_ c -> b -> Maybe (c, c)
f2 c
s2 c
c) =
((c, b, c, c) -> Event a -> Maybe ((c, b, c, c), c))
-> (c, b, c, c) -> c -> SF' (Event a) c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan (c, b, c, c) -> Event a -> Maybe ((c, b, c, c), c)
f (c
s1, b
bne, c
s2, c
c) c
c
where
f :: (c, b, c, c) -> Event a -> Maybe ((c, b, c, c), c)
f (c
s1, b
bne, c
s2, c
c) Event a
ea =
let (Bool
u, c
s1', b
b', b
bne') = case Event a
ea of
Event a
NoEvent -> (Bool
True, c
s1, b
bne, b
bne)
Event a
a ->
let (c
s1', b
b, b
bne') = c -> a -> (c, b, b)
f1 c
s1 a
a
in
(Bool
False, c
s1', b
b, b
bne')
in
case c -> b -> Maybe (c, c)
f2 c
s2 b
b' of
Maybe (c, c)
Nothing | Bool
u -> Maybe ((c, b, c, c), c)
forall a. Maybe a
Nothing
| Bool
otherwise -> ((c, b, c, c), c) -> Maybe ((c, b, c, c), c)
forall a. a -> Maybe a
Just (c -> (c, b, c, c) -> (c, b, c, c)
seq c
s1' (c
s1', b
bne', c
s2, c
c), c
c)
Just (c
s2', c
c') -> ((c, b, c, c), c) -> Maybe ((c, b, c, c), c)
forall a. a -> Maybe a
Just (c -> (c, b, c, c) -> (c, b, c, c)
seq c
s1' (c
s1', b
bne', c
s2', c
c'), c
c')
cpXX (SFEP DTime -> Event a -> Transition (Event a) b
_ c -> a -> (c, b, b)
f1 c
s1 b
bne) (SFEP DTime -> Event a -> Transition (Event a) c
_ c -> a -> (c, c, c)
f2 c
s2 c
cne) =
((c, c, c) -> a -> ((c, c, c), c, c))
-> (c, c, c) -> c -> SF' (Event a) c
forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP (c, c, c) -> a -> ((c, c, c), c, c)
f (c
s1, c
s2, c
cne) (Event a -> c -> c
forall a b. Event a -> b -> b
vfyNoEv b
Event a
bne c
cne)
where
f :: (c, c, c) -> a -> ((c, c, c), c, c)
f (c
s1, c
s2, c
cne) a
a =
case c -> a -> (c, b, b)
f1 c
s1 a
a of
(c
s1', b
NoEvent, b
NoEvent) -> ((c
s1', c
s2, c
cne), c
cne, c
cne)
(c
s1', Event b, b
NoEvent) ->
let (c
s2', c
c, c
cne') = c -> a -> (c, c, c)
f2 c
s2 a
b in ((c
s1', c
s2', c
cne'), c
c, c
cne')
(c, b, b)
_ -> String -> String -> String -> ((c, c, c), c, c)
forall a. String -> String -> String -> a
usrErr String
"AFRP" String
"cpXX" (String -> ((c, c, c), c, c)) -> String -> ((c, c, c), c, c)
forall a b. (a -> b) -> a -> b
$
String
"Assertion failed: Functions on events must not map "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"NoEvent to Event."
cpXX sf1 :: SF' a b
sf1@(SFEP{}) (SFCpAXA DTime -> b -> Transition b c
_ (FDE Event a -> b
f21 b
f21ne) SF' b c
sf22 FunDesc c c
fd23) =
SF' a b -> SF' b c -> SF' a c
forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (SF' a (Event a) -> (Event a -> b) -> b -> SF' a b
forall a b c. SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE SF' a b
SF' a (Event a)
sf1 Event a -> b
f21 b
f21ne) (SF' b c -> FunDesc c c -> SF' b c
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' b c
sf22 FunDesc c c
fd23)
cpXX sf1 :: SF' a b
sf1@(SFEP{}) (SFCpAXA DTime -> b -> Transition b c
_ (FDG b -> b
f21) SF' b c
sf22 FunDesc c c
fd23) =
SF' a b -> SF' b c -> SF' a c
forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (SF' a b -> (b -> b) -> SF' a b
forall a b c. SF' a b -> (b -> c) -> SF' a c
cpXG SF' a b
sf1 b -> b
f21) (SF' b c -> FunDesc c c -> SF' b c
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' b c
sf22 FunDesc c c
fd23)
cpXX (SFCpAXA DTime -> a -> Transition a b
_ FunDesc a b
fd11 SF' b c
sf12 (FDE Event a -> b
f13 b
f13ne)) sf2 :: SF' b c
sf2@(SFEP{}) =
SF' a c -> SF' c c -> SF' a c
forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (FunDesc a b -> SF' b c -> SF' a c
forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd11 SF' b c
sf12) ((Event a -> b) -> b -> SF' b c -> SF' (Event a) c
forall a b c. (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEX Event a -> b
f13 b
f13ne SF' b c
sf2)
cpXX (SFCpAXA DTime -> a -> Transition a b
_ FunDesc a b
fd11 SF' b c
sf12 FunDesc c b
fd13) (SFCpAXA DTime -> b -> Transition b c
_ FunDesc b b
fd21 SF' b c
sf22 FunDesc c c
fd23) =
FunDesc a b -> SF' b c -> FunDesc c c -> SF' a c
forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA FunDesc a b
fd11 (SF' b b -> SF' b c -> SF' b c
forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (SF' b c -> FunDesc c b -> SF' b b
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' b c
sf12 (FunDesc c b -> FunDesc b b -> FunDesc c b
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc c b
fd13 FunDesc b b
fd21)) SF' b c
sf22) FunDesc c c
fd23
cpXX SF' a b
sf1 SF' b c
sf2 = (DTime -> a -> Transition a c) -> SF' a c
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a c
tf
where
tf :: DTime -> a -> Transition a c
tf DTime
dt a
a = (SF' a b -> SF' b c -> SF' a c
forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX SF' a b
sf1' SF' b c
sf2', c
c)
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
(SF' b c
sf2', c
c) = (SF' b c -> DTime -> b -> Transition b c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt b
b
cpAXA :: FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA :: FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA FunDesc a b
FDI SF' b c
sf2 FunDesc c d
fd3 = SF' b c -> FunDesc c d -> SF' b d
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' b c
sf2 FunDesc c d
fd3
cpAXA FunDesc a b
fd1 SF' b c
sf2 FunDesc c d
FDI = FunDesc a b -> SF' b c -> SF' a c
forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd1 SF' b c
sf2
cpAXA (FDC b
b) SF' b c
sf2 FunDesc c d
fd3 = b -> SF' b c -> FunDesc c d -> SF' a d
forall b c d a. b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA b
b SF' b c
sf2 FunDesc c d
fd3
cpAXA FunDesc a b
_ SF' b c
_ (FDC d
d) = d -> SF' a d
forall b a. b -> SF' a b
sfConst d
d
cpAXA FunDesc a b
fd1 SF' b c
sf2 FunDesc c d
fd3 =
FunDesc a b
-> (a -> b) -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
forall a b c d.
FunDesc a b
-> (a -> b) -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpAXAAux FunDesc a b
fd1 (FunDesc a b -> a -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) FunDesc c d
fd3 (FunDesc c d -> c -> d
forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd3) SF' b c
sf2
where
cpAXAAux :: FunDesc a b -> (a -> b) -> FunDesc c d -> (c -> d)
-> SF' b c -> SF' a d
cpAXAAux :: FunDesc a b
-> (a -> b) -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpAXAAux FunDesc a b
fd1 a -> b
_ FunDesc c d
fd3 c -> d
_ (SFArr DTime -> b -> Transition b c
_ FunDesc b c
fd2) =
FunDesc a d -> SF' a d
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a c -> FunDesc c d -> FunDesc a d
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp (FunDesc a b -> FunDesc b c -> FunDesc a c
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc a b
fd1 FunDesc b c
fd2) FunDesc c d
fd3)
cpAXAAux FunDesc a b
fd1 a -> b
_ FunDesc c d
fd3 c -> d
_ sf2 :: SF' b c
sf2@(SFSScan {}) =
FunDesc a b -> SF' b d -> SF' a d
forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd1 (SF' b c -> FunDesc c d -> SF' b d
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' b c
sf2 FunDesc c d
fd3)
cpAXAAux FunDesc a b
fd1 a -> b
_ FunDesc c d
fd3 c -> d
_ sf2 :: SF' b c
sf2@(SFEP {}) =
FunDesc a b -> SF' b d -> SF' a d
forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd1 (SF' b c -> FunDesc c d -> SF' b d
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' b c
sf2 FunDesc c d
fd3)
cpAXAAux FunDesc a b
fd1 a -> b
_ FunDesc c d
fd3 c -> d
_ (SFCpAXA DTime -> b -> Transition b c
_ FunDesc b b
fd21 SF' b c
sf22 FunDesc c c
fd23) =
FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA (FunDesc a b -> FunDesc b b -> FunDesc a b
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc a b
fd1 FunDesc b b
fd21) SF' b c
sf22 (FunDesc c c -> FunDesc c d -> FunDesc c d
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc c c
fd23 FunDesc c d
fd3)
cpAXAAux FunDesc a b
fd1 a -> b
f1 FunDesc c d
fd3 c -> d
f3 SF' b c
sf2 = (DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
forall a d b c.
(DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
SFCpAXA DTime -> a -> Transition a d
tf FunDesc a b
fd1 SF' b c
sf2 FunDesc c d
fd3
where
tf :: DTime -> a -> Transition a d
tf DTime
dt a
a = (FunDesc a b
-> (a -> b) -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
forall a b c d.
FunDesc a b
-> (a -> b) -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpAXAAux FunDesc a b
fd1 a -> b
f1 FunDesc c d
fd3 c -> d
f3 SF' b c
sf2', c -> d
f3 c
c)
where
(SF' b c
sf2', c
c) = (SF' b c -> DTime -> b -> Transition b c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt (a -> b
f1 a
a)
cpAX :: FunDesc a b -> SF' b c -> SF' a c
cpAX :: FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
FDI SF' b c
sf2 = SF' a c
SF' b c
sf2
cpAX (FDC b
b) SF' b c
sf2 = b -> SF' b c -> SF' a c
forall b c a. b -> SF' b c -> SF' a c
cpCX b
b SF' b c
sf2
cpAX (FDE Event a -> b
f1 b
f1ne) SF' b c
sf2 = (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
forall a b c. (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEX Event a -> b
f1 b
f1ne SF' b c
sf2
cpAX (FDG a -> b
f1) SF' b c
sf2 = (a -> b) -> SF' b c -> SF' a c
forall a b c. (a -> b) -> SF' b c -> SF' a c
cpGX a -> b
f1 SF' b c
sf2
cpXA :: SF' a b -> FunDesc b c -> SF' a c
cpXA :: SF' a b -> FunDesc b c -> SF' a c
cpXA SF' a b
sf1 FunDesc b c
FDI = SF' a b
SF' a c
sf1
cpXA SF' a b
_ (FDC c
c) = c -> SF' a c
forall b a. b -> SF' a b
sfConst c
c
cpXA SF' a b
sf1 (FDE Event a -> c
f2 c
f2ne) = SF' a (Event a) -> (Event a -> c) -> c -> SF' a c
forall a b c. SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE SF' a b
SF' a (Event a)
sf1 Event a -> c
f2 c
f2ne
cpXA SF' a b
sf1 (FDG b -> c
f2) = SF' a b -> (b -> c) -> SF' a c
forall a b c. SF' a b -> (b -> c) -> SF' a c
cpXG SF' a b
sf1 b -> c
f2
cpCX :: b -> SF' b c -> SF' a c
cpCX :: b -> SF' b c -> SF' a c
cpCX b
b (SFArr DTime -> b -> Transition b c
_ FunDesc b c
fd2) = c -> SF' a c
forall b a. b -> SF' a b
sfConst ((FunDesc b c -> b -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc b c
fd2) b
b)
cpCX b
b (SFSScan DTime -> b -> Transition b c
_ c -> b -> Maybe (c, c)
f c
s c
c) = (c -> a -> Maybe (c, c)) -> c -> c -> SF' a c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan (\c
s a
_ -> c -> b -> Maybe (c, c)
f c
s b
b) c
s c
c
cpCX b
b (SFEP DTime -> Event a -> Transition (Event a) c
_ c -> a -> (c, c, c)
_ c
_ c
cne) = c -> SF' a c
forall b a. b -> SF' a b
sfConst (Event a -> c -> c
forall a b. Event a -> b -> b
vfyNoEv b
Event a
b c
cne)
cpCX b
b (SFCpAXA DTime -> b -> Transition b c
_ FunDesc b b
fd21 SF' b c
sf22 FunDesc c c
fd23) =
b -> SF' b c -> FunDesc c c -> SF' a c
forall b c d a. b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA ((FunDesc b b -> b -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc b b
fd21) b
b) SF' b c
sf22 FunDesc c c
fd23
cpCX b
b SF' b c
sf2 = (DTime -> a -> Transition a c)
-> FunDesc a b -> SF' b c -> FunDesc c c -> SF' a c
forall a d b c.
(DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
SFCpAXA DTime -> a -> Transition a c
tf (b -> FunDesc a b
forall b a. b -> FunDesc a b
FDC b
b) SF' b c
sf2 FunDesc c c
forall a. FunDesc a a
FDI
where
tf :: DTime -> a -> Transition a c
tf DTime
dt a
_ = (b -> SF' b c -> SF' a c
forall b c a. b -> SF' b c -> SF' a c
cpCX b
b SF' b c
sf2', c
c)
where
(SF' b c
sf2', c
c) = (SF' b c -> DTime -> b -> Transition b c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt b
b
cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA b
b SF' b c
sf2 FunDesc c d
FDI = b -> SF' b c -> SF' a c
forall b c a. b -> SF' b c -> SF' a c
cpCX b
b SF' b c
sf2
cpCXA b
_ SF' b c
_ (FDC d
c) = d -> SF' a d
forall b a. b -> SF' a b
sfConst d
c
cpCXA b
b SF' b c
sf2 FunDesc c d
fd3 = FunDesc a b -> b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
forall a b c d.
FunDesc a b -> b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpCXAAux (b -> FunDesc a b
forall b a. b -> FunDesc a b
FDC b
b) b
b FunDesc c d
fd3 (FunDesc c d -> c -> d
forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd3) SF' b c
sf2
where
cpCXAAux :: FunDesc a b -> b -> FunDesc c d -> (c -> d)
-> SF' b c -> SF' a d
cpCXAAux :: FunDesc a b -> b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpCXAAux FunDesc a b
_ b
b FunDesc c d
_ c -> d
f3 (SFArr DTime -> b -> Transition b c
_ FunDesc b c
fd2) = d -> SF' a d
forall b a. b -> SF' a b
sfConst (c -> d
f3 ((FunDesc b c -> b -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc b c
fd2) b
b))
cpCXAAux FunDesc a b
_ b
b FunDesc c d
_ c -> d
f3 (SFSScan DTime -> b -> Transition b c
_ c -> b -> Maybe (c, c)
f c
s c
c) = (c -> a -> Maybe (c, d)) -> c -> d -> SF' a d
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan c -> a -> Maybe (c, d)
f' c
s (c -> d
f3 c
c)
where
f' :: c -> a -> Maybe (c, d)
f' c
s a
_ = case c -> b -> Maybe (c, c)
f c
s b
b of
Maybe (c, c)
Nothing -> Maybe (c, d)
forall a. Maybe a
Nothing
Just (c
s', c
c') -> (c, d) -> Maybe (c, d)
forall a. a -> Maybe a
Just (c
s', c -> d
f3 c
c')
cpCXAAux FunDesc a b
_ b
b FunDesc c d
_ c -> d
f3 (SFEP DTime -> Event a -> Transition (Event a) c
_ c -> a -> (c, c, c)
_ c
_ c
cne) = d -> SF' a d
forall b a. b -> SF' a b
sfConst (c -> d
f3 (Event a -> c -> c
forall a b. Event a -> b -> b
vfyNoEv b
Event a
b c
cne))
cpCXAAux FunDesc a b
_ b
b FunDesc c d
fd3 c -> d
_ (SFCpAXA DTime -> b -> Transition b c
_ FunDesc b b
fd21 SF' b c
sf22 FunDesc c c
fd23) =
b -> SF' b c -> FunDesc c d -> SF' a d
forall b c d a. b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA ((FunDesc b b -> b -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc b b
fd21) b
b) SF' b c
sf22 (FunDesc c c -> FunDesc c d -> FunDesc c d
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc c c
fd23 FunDesc c d
fd3)
cpCXAAux FunDesc a b
fd1 b
b FunDesc c d
fd3 c -> d
f3 SF' b c
sf2 = (DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
forall a d b c.
(DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
SFCpAXA DTime -> a -> Transition a d
tf FunDesc a b
fd1 SF' b c
sf2 FunDesc c d
fd3
where
tf :: DTime -> a -> Transition a d
tf DTime
dt a
_ = (FunDesc a b -> b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
forall a b c d.
FunDesc a b -> b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpCXAAux FunDesc a b
fd1 b
b FunDesc c d
fd3 c -> d
f3 SF' b c
sf2', c -> d
f3 c
c)
where
(SF' b c
sf2', c
c) = (SF' b c -> DTime -> b -> Transition b c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt b
b
cpGX :: (a -> b) -> SF' b c -> SF' a c
cpGX :: (a -> b) -> SF' b c -> SF' a c
cpGX a -> b
f1 SF' b c
sf2 = FunDesc a b -> (a -> b) -> SF' b c -> SF' a c
forall a b c. FunDesc a b -> (a -> b) -> SF' b c -> SF' a c
cpGXAux ((a -> b) -> FunDesc a b
forall a b. (a -> b) -> FunDesc a b
FDG a -> b
f1) a -> b
f1 SF' b c
sf2
where
cpGXAux :: FunDesc a b -> (a -> b) -> SF' b c -> SF' a c
cpGXAux :: FunDesc a b -> (a -> b) -> SF' b c -> SF' a c
cpGXAux FunDesc a b
fd1 a -> b
_ (SFArr DTime -> b -> Transition b c
_ FunDesc b c
fd2) = FunDesc a c -> SF' a c
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc b c -> FunDesc a c
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc a b
fd1 FunDesc b c
fd2)
cpGXAux FunDesc a b
_ a -> b
f1 (SFSScan DTime -> b -> Transition b c
_ c -> b -> Maybe (c, c)
f c
s c
c) = (c -> a -> Maybe (c, c)) -> c -> c -> SF' a c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan (\c
s a
a -> c -> b -> Maybe (c, c)
f c
s (a -> b
f1 a
a)) c
s c
c
cpGXAux FunDesc a b
fd1 a -> b
_ (SFCpAXA DTime -> b -> Transition b c
_ FunDesc b b
fd21 SF' b c
sf22 FunDesc c c
fd23) =
FunDesc a b -> SF' b c -> FunDesc c c -> SF' a c
forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA (FunDesc a b -> FunDesc b b -> FunDesc a b
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc a b
fd1 FunDesc b b
fd21) SF' b c
sf22 FunDesc c c
fd23
cpGXAux FunDesc a b
fd1 a -> b
f1 SF' b c
sf2 = (DTime -> a -> Transition a c)
-> FunDesc a b -> SF' b c -> FunDesc c c -> SF' a c
forall a d b c.
(DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
SFCpAXA DTime -> a -> Transition a c
tf FunDesc a b
fd1 SF' b c
sf2 FunDesc c c
forall a. FunDesc a a
FDI
where
tf :: DTime -> a -> Transition a c
tf DTime
dt a
a = (FunDesc a b -> (a -> b) -> SF' b c -> SF' a c
forall a b c. FunDesc a b -> (a -> b) -> SF' b c -> SF' a c
cpGXAux FunDesc a b
fd1 a -> b
f1 SF' b c
sf2', c
c)
where
(SF' b c
sf2', c
c) = (SF' b c -> DTime -> b -> Transition b c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt (a -> b
f1 a
a)
cpXG :: SF' a b -> (b -> c) -> SF' a c
cpXG :: SF' a b -> (b -> c) -> SF' a c
cpXG SF' a b
sf1 b -> c
f2 = FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
forall b c a. FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
cpXGAux ((b -> c) -> FunDesc b c
forall a b. (a -> b) -> FunDesc a b
FDG b -> c
f2) b -> c
f2 SF' a b
sf1
where
cpXGAux :: FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
cpXGAux :: FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
cpXGAux FunDesc b c
fd2 b -> c
_ (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) = FunDesc a c -> SF' a c
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc b c -> FunDesc a c
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc a b
fd1 FunDesc b c
fd2)
cpXGAux FunDesc b c
_ b -> c
f2 (SFSScan DTime -> a -> Transition a b
_ c -> a -> Maybe (c, b)
f c
s b
b) = (c -> a -> Maybe (c, c)) -> c -> c -> SF' a c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan c -> a -> Maybe (c, c)
f' c
s (b -> c
f2 b
b)
where
f' :: c -> a -> Maybe (c, c)
f' c
s a
a = case c -> a -> Maybe (c, b)
f c
s a
a of
Maybe (c, b)
Nothing -> Maybe (c, c)
forall a. Maybe a
Nothing
Just (c
s', b
b') -> (c, c) -> Maybe (c, c)
forall a. a -> Maybe a
Just (c
s', b -> c
f2 b
b')
cpXGAux FunDesc b c
_ b -> c
f2 (SFEP DTime -> Event a -> Transition (Event a) b
_ c -> a -> (c, b, b)
f1 c
s b
bne) = (c -> a -> (c, c, c)) -> c -> c -> SF' (Event a) c
forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP c -> a -> (c, c, c)
f c
s (b -> c
f2 b
bne)
where
f :: c -> a -> (c, c, c)
f c
s a
a = let (c
s', b
b, b
bne') = c -> a -> (c, b, b)
f1 c
s a
a in (c
s', b -> c
f2 b
b, b -> c
f2 b
bne')
cpXGAux FunDesc b c
fd2 b -> c
_ (SFCpAXA DTime -> a -> Transition a b
_ FunDesc a b
fd11 SF' b c
sf12 FunDesc c b
fd22) =
FunDesc a b -> SF' b c -> FunDesc c c -> SF' a c
forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA FunDesc a b
fd11 SF' b c
sf12 (FunDesc c b -> FunDesc b c -> FunDesc c c
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc c b
fd22 FunDesc b c
fd2)
cpXGAux FunDesc b c
fd2 b -> c
f2 SF' a b
sf1 = (DTime -> a -> Transition a c)
-> FunDesc a a -> SF' a b -> FunDesc b c -> SF' a c
forall a d b c.
(DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
SFCpAXA DTime -> a -> Transition a c
tf FunDesc a a
forall a. FunDesc a a
FDI SF' a b
sf1 FunDesc b c
fd2
where
tf :: DTime -> a -> Transition a c
tf DTime
dt a
a = (FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
forall b c a. FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
cpXGAux FunDesc b c
fd2 b -> c
f2 SF' a b
sf1', b -> c
f2 b
b)
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
cpEX :: (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEX :: (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEX Event a -> b
f1 b
f1ne SF' b c
sf2 = FunDesc (Event a) b
-> (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
forall a b c.
FunDesc (Event a) b
-> (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEXAux ((Event a -> b) -> b -> FunDesc (Event a) b
forall a b. (Event a -> b) -> b -> FunDesc (Event a) b
FDE Event a -> b
f1 b
f1ne) Event a -> b
f1 b
f1ne SF' b c
sf2
where
cpEXAux :: FunDesc (Event a) b -> (Event a -> b) -> b
-> SF' b c -> SF' (Event a) c
cpEXAux :: FunDesc (Event a) b
-> (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEXAux FunDesc (Event a) b
fd1 Event a -> b
_ b
_ (SFArr DTime -> b -> Transition b c
_ FunDesc b c
fd2) = FunDesc (Event a) c -> SF' (Event a) c
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc (Event a) b -> FunDesc b c -> FunDesc (Event a) c
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc (Event a) b
fd1 FunDesc b c
fd2)
cpEXAux FunDesc (Event a) b
_ Event a -> b
f1 b
_ (SFSScan DTime -> b -> Transition b c
_ c -> b -> Maybe (c, c)
f c
s c
c) = (c -> Event a -> Maybe (c, c)) -> c -> c -> SF' (Event a) c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan (\c
s Event a
a -> c -> b -> Maybe (c, c)
f c
s (Event a -> b
f1 Event a
a)) c
s c
c
cpEXAux FunDesc (Event a) b
_ Event a -> b
f1 b
f1ne (SFEP DTime -> Event a -> Transition (Event a) c
_ c -> a -> (c, c, c)
f2 c
s c
cne) =
((c, c) -> a -> ((c, c), c, c)) -> (c, c) -> c -> SF' (Event a) c
forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP (c, c) -> a -> ((c, c), c, c)
f (c
s, c
cne) (Event a -> c -> c
forall a b. Event a -> b -> b
vfyNoEv b
Event a
f1ne c
cne)
where
f :: (c, c) -> a -> ((c, c), c, c)
f scne :: (c, c)
scne@(c
s, c
cne) a
a =
case Event a -> b
f1 (a -> Event a
forall a. a -> Event a
Event a
a) of
b
NoEvent -> ((c, c)
scne, c
cne, c
cne)
Event b ->
let (c
s', c
c, c
cne') = c -> a -> (c, c, c)
f2 c
s a
b in ((c
s', c
cne'), c
c, c
cne')
cpEXAux FunDesc (Event a) b
fd1 Event a -> b
_ b
_ (SFCpAXA DTime -> b -> Transition b c
_ FunDesc b b
fd21 SF' b c
sf22 FunDesc c c
fd23) =
FunDesc (Event a) b -> SF' b c -> FunDesc c c -> SF' (Event a) c
forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA (FunDesc (Event a) b -> FunDesc b b -> FunDesc (Event a) b
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc (Event a) b
fd1 FunDesc b b
fd21) SF' b c
sf22 FunDesc c c
fd23
cpEXAux FunDesc (Event a) b
fd1 Event a -> b
f1 b
f1ne SF' b c
sf2 = (DTime -> Event a -> Transition (Event a) c)
-> FunDesc (Event a) b -> SF' b c -> FunDesc c c -> SF' (Event a) c
forall a d b c.
(DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
SFCpAXA DTime -> Event a -> Transition (Event a) c
tf FunDesc (Event a) b
fd1 SF' b c
sf2 FunDesc c c
forall a. FunDesc a a
FDI
where
tf :: DTime -> Event a -> Transition (Event a) c
tf DTime
dt Event a
ea = (FunDesc (Event a) b
-> (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
forall a b c.
FunDesc (Event a) b
-> (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEXAux FunDesc (Event a) b
fd1 Event a -> b
f1 b
f1ne SF' b c
sf2', c
c)
where
(SF' b c
sf2', c
c) =
case Event a
ea of
Event a
NoEvent -> (SF' b c -> DTime -> b -> Transition b c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt b
f1ne
Event a
_ -> (SF' b c -> DTime -> b -> Transition b c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt (Event a -> b
f1 Event a
ea)
cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE SF' a (Event b)
sf1 Event b -> c
f2 c
f2ne = FunDesc (Event b) c
-> (Event b -> c) -> c -> SF' a (Event b) -> SF' a c
forall b c a.
FunDesc (Event b) c
-> (Event b -> c) -> c -> SF' a (Event b) -> SF' a c
cpXEAux ((Event b -> c) -> c -> FunDesc (Event b) c
forall a b. (Event a -> b) -> b -> FunDesc (Event a) b
FDE Event b -> c
f2 c
f2ne) Event b -> c
f2 c
f2ne SF' a (Event b)
sf1
where
cpXEAux :: FunDesc (Event b) c -> (Event b -> c) -> c
-> SF' a (Event b) -> SF' a c
cpXEAux :: FunDesc (Event b) c
-> (Event b -> c) -> c -> SF' a (Event b) -> SF' a c
cpXEAux FunDesc (Event b) c
fd2 Event b -> c
_ c
_ (SFArr DTime -> a -> Transition a (Event b)
_ FunDesc a (Event b)
fd1) = FunDesc a c -> SF' a c
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a (Event b) -> FunDesc (Event b) c -> FunDesc a c
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc a (Event b)
fd1 FunDesc (Event b) c
fd2)
cpXEAux FunDesc (Event b) c
_ Event b -> c
f2 c
f2ne (SFSScan DTime -> a -> Transition a (Event b)
_ c -> a -> Maybe (c, Event b)
f c
s Event b
eb) = (c -> a -> Maybe (c, c)) -> c -> c -> SF' a c
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan c -> a -> Maybe (c, c)
f' c
s (Event b -> c
f2 Event b
eb)
where
f' :: c -> a -> Maybe (c, c)
f' c
s a
a = case c -> a -> Maybe (c, Event b)
f c
s a
a of
Maybe (c, Event b)
Nothing -> Maybe (c, c)
forall a. Maybe a
Nothing
Just (c
s', Event b
NoEvent) -> (c, c) -> Maybe (c, c)
forall a. a -> Maybe a
Just (c
s', c
f2ne)
Just (c
s', Event b
eb') -> (c, c) -> Maybe (c, c)
forall a. a -> Maybe a
Just (c
s', Event b -> c
f2 Event b
eb')
cpXEAux FunDesc (Event b) c
_ Event b -> c
f2 c
f2ne (SFEP DTime -> Event a -> Transition (Event a) (Event b)
_ c -> a -> (c, Event b, Event b)
f1 c
s Event b
ebne) =
(c -> a -> (c, c, c)) -> c -> c -> SF' (Event a) c
forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP c -> a -> (c, c, c)
f c
s (Event b -> c -> c
forall a b. Event a -> b -> b
vfyNoEv Event b
ebne c
f2ne)
where
f :: c -> a -> (c, c, c)
f c
s a
a =
case c -> a -> (c, Event b, Event b)
f1 c
s a
a of
(c
s', Event b
NoEvent, Event b
NoEvent) -> (c
s', c
f2ne, c
f2ne)
(c
s', Event b
eb, Event b
NoEvent) -> (c
s', Event b -> c
f2 Event b
eb, c
f2ne)
(c, Event b, Event b)
_ -> String -> String -> String -> (c, c, c)
forall a. String -> String -> String -> a
usrErr String
"AFRP" String
"cpXEAux" (String -> (c, c, c)) -> String -> (c, c, c)
forall a b. (a -> b) -> a -> b
$
String
"Assertion failed: Functions on events must not "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"map NoEvent to Event."
cpXEAux FunDesc (Event b) c
fd2 Event b -> c
_ c
_ (SFCpAXA DTime -> a -> Transition a (Event b)
_ FunDesc a b
fd11 SF' b c
sf12 FunDesc c (Event b)
fd13) =
FunDesc a b -> SF' b c -> FunDesc c c -> SF' a c
forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA FunDesc a b
fd11 SF' b c
sf12 (FunDesc c (Event b) -> FunDesc (Event b) c -> FunDesc c c
forall a b c. FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FunDesc c (Event b)
fd13 FunDesc (Event b) c
fd2)
cpXEAux FunDesc (Event b) c
fd2 Event b -> c
f2 c
f2ne SF' a (Event b)
sf1 = (DTime -> a -> Transition a c)
-> FunDesc a a -> SF' a (Event b) -> FunDesc (Event b) c -> SF' a c
forall a d b c.
(DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
SFCpAXA DTime -> a -> Transition a c
tf FunDesc a a
forall a. FunDesc a a
FDI SF' a (Event b)
sf1 FunDesc (Event b) c
fd2
where
tf :: DTime -> a -> Transition a c
tf DTime
dt a
a = (FunDesc (Event b) c
-> (Event b -> c) -> c -> SF' a (Event b) -> SF' a c
forall b c a.
FunDesc (Event b) c
-> (Event b -> c) -> c -> SF' a (Event b) -> SF' a c
cpXEAux FunDesc (Event b) c
fd2 Event b -> c
f2 c
f2ne SF' a (Event b)
sf1',
case Event b
eb of Event b
NoEvent -> c
f2ne; Event b
_ -> Event b -> c
f2 Event b
eb)
where
(SF' a (Event b)
sf1', Event b
eb) = (SF' a (Event b) -> DTime -> a -> Transition a (Event b)
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a (Event b)
sf1) DTime
dt a
a
firstPrim :: SF a b -> SF (a,c) (b,c)
firstPrim :: SF a b -> SF (a, c) (b, c)
firstPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a b
tf10}) = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: (a, c) -> Transition (a, c) (b, c)
sfTF = (a, c) -> Transition (a, c) (b, c)
tf0}
where
tf0 :: (a, c) -> Transition (a, c) (b, c)
tf0 ~(a
a0, c
c0) = (SF' a b -> SF' (a, c) (b, c)
forall a b c. SF' a b -> SF' (a, c) (b, c)
fpAux SF' a b
sf1, (b
b0, c
c0))
where
(SF' a b
sf1, b
b0) = a -> Transition a b
tf10 a
a0
fpAux :: SF' a b -> SF' (a,c) (b,c)
fpAux :: SF' a b -> SF' (a, c) (b, c)
fpAux (SFArr DTime -> a -> Transition a b
_ FunDesc a b
FDI) = SF' (a, c) (b, c)
forall a. SF' a a
sfId
fpAux (SFArr DTime -> a -> Transition a b
_ (FDC b
b)) = ((a, c) -> (b, c)) -> SF' (a, c) (b, c)
forall a b. (a -> b) -> SF' a b
sfArrG (\(~(a
_, c
c)) -> (b
b, c
c))
fpAux (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) = ((a, c) -> (b, c)) -> SF' (a, c) (b, c)
forall a b. (a -> b) -> SF' a b
sfArrG (\(~(a
a, c
c)) -> ((FunDesc a b -> a -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a, c
c))
fpAux SF' a b
sf1 = (DTime -> (a, c) -> Transition (a, c) (b, c)) -> SF' (a, c) (b, c)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> Transition (a, c) (b, c)
tf
where
tf :: DTime -> (a, c) -> Transition (a, c) (b, c)
tf DTime
dt ~(a
a, c
c) = (SF' a b -> SF' (a, c) (b, c)
forall a b c. SF' a b -> SF' (a, c) (b, c)
fpAux SF' a b
sf1', (b
b, c
c))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
secondPrim :: SF a b -> SF (c,a) (c,b)
secondPrim :: SF a b -> SF (c, a) (c, b)
secondPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a b
tf10}) = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: (c, a) -> Transition (c, a) (c, b)
sfTF = (c, a) -> Transition (c, a) (c, b)
tf0}
where
tf0 :: (c, a) -> Transition (c, a) (c, b)
tf0 ~(c
c0, a
a0) = (SF' a b -> SF' (c, a) (c, b)
forall a b c. SF' a b -> SF' (c, a) (c, b)
spAux SF' a b
sf1, (c
c0, b
b0))
where
(SF' a b
sf1, b
b0) = a -> Transition a b
tf10 a
a0
spAux :: SF' a b -> SF' (c,a) (c,b)
spAux :: SF' a b -> SF' (c, a) (c, b)
spAux (SFArr DTime -> a -> Transition a b
_ FunDesc a b
FDI) = SF' (c, a) (c, b)
forall a. SF' a a
sfId
spAux (SFArr DTime -> a -> Transition a b
_ (FDC b
b)) = ((c, a) -> (c, b)) -> SF' (c, a) (c, b)
forall a b. (a -> b) -> SF' a b
sfArrG (\(~(c
c, a
_)) -> (c
c, b
b))
spAux (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) = ((c, a) -> (c, b)) -> SF' (c, a) (c, b)
forall a b. (a -> b) -> SF' a b
sfArrG (\(~(c
c, a
a)) -> (c
c, (FunDesc a b -> a -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a))
spAux SF' a b
sf1 = (DTime -> (c, a) -> Transition (c, a) (c, b)) -> SF' (c, a) (c, b)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (c, a) -> Transition (c, a) (c, b)
tf
where
tf :: DTime -> (c, a) -> Transition (c, a) (c, b)
tf DTime
dt ~(c
c, a
a) = (SF' a b -> SF' (c, a) (c, b)
forall a b c. SF' a b -> SF' (c, a) (c, b)
spAux SF' a b
sf1', (c
c, b
b))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
parSplitPrim :: SF a b -> SF c d -> SF (a,c) (b,d)
parSplitPrim :: SF a b -> SF c d -> SF (a, c) (b, d)
parSplitPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a b
tf10}) (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = c -> Transition c d
tf20}) = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: (a, c) -> Transition (a, c) (b, d)
sfTF = (a, c) -> Transition (a, c) (b, d)
tf0}
where
tf0 :: (a, c) -> Transition (a, c) (b, d)
tf0 ~(a
a0, c
c0) = (SF' a b -> SF' c d -> SF' (a, c) (b, d)
forall a b c d. SF' a b -> SF' c d -> SF' (a, c) (b, d)
psXX SF' a b
sf1 SF' c d
sf2, (b
b0, d
d0))
where
(SF' a b
sf1, b
b0) = a -> Transition a b
tf10 a
a0
(SF' c d
sf2, d
d0) = c -> Transition c d
tf20 c
c0
psXX :: SF' a b -> SF' c d -> SF' (a,c) (b,d)
psXX :: SF' a b -> SF' c d -> SF' (a, c) (b, d)
psXX (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) (SFArr DTime -> c -> Transition c d
_ FunDesc c d
fd2) = FunDesc (a, c) (b, d) -> SF' (a, c) (b, d)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar FunDesc a b
fd1 FunDesc c d
fd2)
psXX (SFArr DTime -> a -> Transition a b
_ FunDesc a b
FDI) SF' c d
sf2 = SF' c d -> SF' (a, c) (a, d)
forall a b c. SF' a b -> SF' (c, a) (c, b)
spAux SF' c d
sf2
psXX (SFArr DTime -> a -> Transition a b
_ (FDC b
b)) SF' c d
sf2 = b -> SF' c d -> SF' (a, c) (b, d)
forall b c d a. b -> SF' c d -> SF' (a, c) (b, d)
psCX b
b SF' c d
sf2
psXX (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) SF' c d
sf2 = (a -> b) -> SF' c d -> SF' (a, c) (b, d)
forall a b c d. (a -> b) -> SF' c d -> SF' (a, c) (b, d)
psAX (FunDesc a b -> a -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) SF' c d
sf2
psXX SF' a b
sf1 (SFArr DTime -> c -> Transition c d
_ FunDesc c d
FDI) = SF' a b -> SF' (a, c) (b, c)
forall a b c. SF' a b -> SF' (a, c) (b, c)
fpAux SF' a b
sf1
psXX SF' a b
sf1 (SFArr DTime -> c -> Transition c d
_ (FDC d
d)) = SF' a b -> d -> SF' (a, c) (b, d)
forall a b d c. SF' a b -> d -> SF' (a, c) (b, d)
psXC SF' a b
sf1 d
d
psXX SF' a b
sf1 (SFArr DTime -> c -> Transition c d
_ FunDesc c d
fd2) = SF' a b -> (c -> d) -> SF' (a, c) (b, d)
forall a b c d. SF' a b -> (c -> d) -> SF' (a, c) (b, d)
psXA SF' a b
sf1 (FunDesc c d -> c -> d
forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd2)
psXX SF' a b
sf1 SF' c d
sf2 = (DTime -> (a, c) -> Transition (a, c) (b, d)) -> SF' (a, c) (b, d)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> Transition (a, c) (b, d)
tf
where
tf :: DTime -> (a, c) -> Transition (a, c) (b, d)
tf DTime
dt ~(a
a, c
c) = (SF' a b -> SF' c d -> SF' (a, c) (b, d)
forall a b c d. SF' a b -> SF' c d -> SF' (a, c) (b, d)
psXX SF' a b
sf1' SF' c d
sf2', (b
b, d
d))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
(SF' c d
sf2', d
d) = (SF' c d -> DTime -> c -> Transition c d
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' c d
sf2) DTime
dt c
c
psCX :: b -> SF' c d -> SF' (a,c) (b,d)
psCX :: b -> SF' c d -> SF' (a, c) (b, d)
psCX b
b (SFArr DTime -> c -> Transition c d
_ FunDesc c d
fd2) = FunDesc (a, c) (b, d) -> SF' (a, c) (b, d)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar (b -> FunDesc a b
forall b a. b -> FunDesc a b
FDC b
b) FunDesc c d
fd2)
psCX b
b SF' c d
sf2 = (DTime -> (a, c) -> Transition (a, c) (b, d)) -> SF' (a, c) (b, d)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> Transition (a, c) (b, d)
tf
where
tf :: DTime -> (a, c) -> Transition (a, c) (b, d)
tf DTime
dt ~(a
_, c
c) = (b -> SF' c d -> SF' (a, c) (b, d)
forall b c d a. b -> SF' c d -> SF' (a, c) (b, d)
psCX b
b SF' c d
sf2', (b
b, d
d))
where
(SF' c d
sf2', d
d) = (SF' c d -> DTime -> c -> Transition c d
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' c d
sf2) DTime
dt c
c
psXC :: SF' a b -> d -> SF' (a,c) (b,d)
psXC :: SF' a b -> d -> SF' (a, c) (b, d)
psXC (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) d
d = FunDesc (a, c) (b, d) -> SF' (a, c) (b, d)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar FunDesc a b
fd1 (d -> FunDesc c d
forall b a. b -> FunDesc a b
FDC d
d))
psXC SF' a b
sf1 d
d = (DTime -> (a, c) -> Transition (a, c) (b, d)) -> SF' (a, c) (b, d)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> Transition (a, c) (b, d)
tf
where
tf :: DTime -> (a, c) -> Transition (a, c) (b, d)
tf DTime
dt ~(a
a, c
_) = (SF' a b -> d -> SF' (a, c) (b, d)
forall a b d c. SF' a b -> d -> SF' (a, c) (b, d)
psXC SF' a b
sf1' d
d, (b
b, d
d))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
psAX :: (a -> b) -> SF' c d -> SF' (a,c) (b,d)
psAX :: (a -> b) -> SF' c d -> SF' (a, c) (b, d)
psAX a -> b
f1 (SFArr DTime -> c -> Transition c d
_ FunDesc c d
fd2) = FunDesc (a, c) (b, d) -> SF' (a, c) (b, d)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar ((a -> b) -> FunDesc a b
forall a b. (a -> b) -> FunDesc a b
FDG a -> b
f1) FunDesc c d
fd2)
psAX a -> b
f1 SF' c d
sf2 = (DTime -> (a, c) -> Transition (a, c) (b, d)) -> SF' (a, c) (b, d)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> Transition (a, c) (b, d)
tf
where
tf :: DTime -> (a, c) -> Transition (a, c) (b, d)
tf DTime
dt ~(a
a, c
c) = ((a -> b) -> SF' c d -> SF' (a, c) (b, d)
forall a b c d. (a -> b) -> SF' c d -> SF' (a, c) (b, d)
psAX a -> b
f1 SF' c d
sf2', (a -> b
f1 a
a, d
d))
where
(SF' c d
sf2', d
d) = (SF' c d -> DTime -> c -> Transition c d
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' c d
sf2) DTime
dt c
c
psXA :: SF' a b -> (c -> d) -> SF' (a,c) (b,d)
psXA :: SF' a b -> (c -> d) -> SF' (a, c) (b, d)
psXA (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) c -> d
f2 = FunDesc (a, c) (b, d) -> SF' (a, c) (b, d)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar FunDesc a b
fd1 ((c -> d) -> FunDesc c d
forall a b. (a -> b) -> FunDesc a b
FDG c -> d
f2))
psXA SF' a b
sf1 c -> d
f2 = (DTime -> (a, c) -> Transition (a, c) (b, d)) -> SF' (a, c) (b, d)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> Transition (a, c) (b, d)
tf
where
tf :: DTime -> (a, c) -> Transition (a, c) (b, d)
tf DTime
dt ~(a
a, c
c) = (SF' a b -> (c -> d) -> SF' (a, c) (b, d)
forall a b c d. SF' a b -> (c -> d) -> SF' (a, c) (b, d)
psXA SF' a b
sf1' c -> d
f2, (b
b, c -> d
f2 c
c))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
parFanOutPrim :: SF a b -> SF a c -> SF a (b, c)
parFanOutPrim :: SF a b -> SF a c -> SF a (b, c)
parFanOutPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a b
tf10}) (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a c
tf20}) = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: a -> Transition a (b, c)
sfTF = a -> Transition a (b, c)
tf0}
where
tf0 :: a -> Transition a (b, c)
tf0 a
a0 = (SF' a b -> SF' a c -> SF' a (b, c)
forall a b c. SF' a b -> SF' a c -> SF' a (b, c)
pfoXX SF' a b
sf1 SF' a c
sf2, (b
b0, c
c0))
where
(SF' a b
sf1, b
b0) = a -> Transition a b
tf10 a
a0
(SF' a c
sf2, c
c0) = a -> Transition a c
tf20 a
a0
pfoXX :: SF' a b -> SF' a c -> SF' a (b ,c)
pfoXX :: SF' a b -> SF' a c -> SF' a (b, c)
pfoXX (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) (SFArr DTime -> a -> Transition a c
_ FunDesc a c
fd2) = FunDesc a (b, c) -> SF' a (b, c)
forall a b. FunDesc a b -> SF' a b
sfArr(FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
fd1 FunDesc a c
fd2)
pfoXX (SFArr DTime -> a -> Transition a b
_ FunDesc a b
FDI) SF' a c
sf2 = SF' a c -> SF' a (a, c)
forall a c. SF' a c -> SF' a (a, c)
pfoIX SF' a c
sf2
pfoXX (SFArr DTime -> a -> Transition a b
_ (FDC b
b)) SF' a c
sf2 = b -> SF' a c -> SF' a (b, c)
forall b a c. b -> SF' a c -> SF' a (b, c)
pfoCX b
b SF' a c
sf2
pfoXX (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) SF' a c
sf2 = (a -> b) -> SF' a c -> SF' a (b, c)
forall a b c. (a -> b) -> SF' a c -> SF' a (b, c)
pfoAX (FunDesc a b -> a -> b
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) SF' a c
sf2
pfoXX SF' a b
sf1 (SFArr DTime -> a -> Transition a c
_ FunDesc a c
FDI) = SF' a b -> SF' a (b, a)
forall a b. SF' a b -> SF' a (b, a)
pfoXI SF' a b
sf1
pfoXX SF' a b
sf1 (SFArr DTime -> a -> Transition a c
_ (FDC c
c)) = SF' a b -> c -> SF' a (b, c)
forall a b c. SF' a b -> c -> SF' a (b, c)
pfoXC SF' a b
sf1 c
c
pfoXX SF' a b
sf1 (SFArr DTime -> a -> Transition a c
_ FunDesc a c
fd2) = SF' a b -> (a -> c) -> SF' a (b, c)
forall a b c. SF' a b -> (a -> c) -> SF' a (b, c)
pfoXA SF' a b
sf1 (FunDesc a c -> a -> c
forall a b. FunDesc a b -> a -> b
fdFun FunDesc a c
fd2)
pfoXX SF' a b
sf1 SF' a c
sf2 = (DTime -> a -> Transition a (b, c)) -> SF' a (b, c)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a (b, c)
tf
where
tf :: DTime -> a -> Transition a (b, c)
tf DTime
dt a
a = (SF' a b -> SF' a c -> SF' a (b, c)
forall a b c. SF' a b -> SF' a c -> SF' a (b, c)
pfoXX SF' a b
sf1' SF' a c
sf2', (b
b, c
c))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
(SF' a c
sf2', c
c) = (SF' a c -> DTime -> a -> Transition a c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a c
sf2) DTime
dt a
a
pfoIX :: SF' a c -> SF' a (a ,c)
pfoIX :: SF' a c -> SF' a (a, c)
pfoIX (SFArr DTime -> a -> Transition a c
_ FunDesc a c
fd2) = FunDesc a (a, c) -> SF' a (a, c)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a a -> FunDesc a c -> FunDesc a (a, c)
forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a a
forall a. FunDesc a a
FDI FunDesc a c
fd2)
pfoIX SF' a c
sf2 = (DTime -> a -> Transition a (a, c)) -> SF' a (a, c)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a (a, c)
tf
where
tf :: DTime -> a -> Transition a (a, c)
tf DTime
dt a
a = (SF' a c -> SF' a (a, c)
forall a c. SF' a c -> SF' a (a, c)
pfoIX SF' a c
sf2', (a
a, c
c))
where
(SF' a c
sf2', c
c) = (SF' a c -> DTime -> a -> Transition a c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a c
sf2) DTime
dt a
a
pfoXI :: SF' a b -> SF' a (b ,a)
pfoXI :: SF' a b -> SF' a (b, a)
pfoXI (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) = FunDesc a (b, a) -> SF' a (b, a)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc a a -> FunDesc a (b, a)
forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
fd1 FunDesc a a
forall a. FunDesc a a
FDI)
pfoXI SF' a b
sf1 = (DTime -> a -> Transition a (b, a)) -> SF' a (b, a)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a (b, a)
tf
where
tf :: DTime -> a -> Transition a (b, a)
tf DTime
dt a
a = (SF' a b -> SF' a (b, a)
forall a b. SF' a b -> SF' a (b, a)
pfoXI SF' a b
sf1', (b
b, a
a))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
pfoCX :: b -> SF' a c -> SF' a (b ,c)
pfoCX :: b -> SF' a c -> SF' a (b, c)
pfoCX b
b (SFArr DTime -> a -> Transition a c
_ FunDesc a c
fd2) = FunDesc a (b, c) -> SF' a (b, c)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut (b -> FunDesc a b
forall b a. b -> FunDesc a b
FDC b
b) FunDesc a c
fd2)
pfoCX b
b SF' a c
sf2 = (DTime -> a -> Transition a (b, c)) -> SF' a (b, c)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a (b, c)
tf
where
tf :: DTime -> a -> Transition a (b, c)
tf DTime
dt a
a = (b -> SF' a c -> SF' a (b, c)
forall b a c. b -> SF' a c -> SF' a (b, c)
pfoCX b
b SF' a c
sf2', (b
b, c
c))
where
(SF' a c
sf2', c
c) = (SF' a c -> DTime -> a -> Transition a c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a c
sf2) DTime
dt a
a
pfoXC :: SF' a b -> c -> SF' a (b ,c)
pfoXC :: SF' a b -> c -> SF' a (b, c)
pfoXC (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) c
c = FunDesc a (b, c) -> SF' a (b, c)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
fd1 (c -> FunDesc a c
forall b a. b -> FunDesc a b
FDC c
c))
pfoXC SF' a b
sf1 c
c = (DTime -> a -> Transition a (b, c)) -> SF' a (b, c)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a (b, c)
tf
where
tf :: DTime -> a -> Transition a (b, c)
tf DTime
dt a
a = (SF' a b -> c -> SF' a (b, c)
forall a b c. SF' a b -> c -> SF' a (b, c)
pfoXC SF' a b
sf1' c
c, (b
b, c
c))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
pfoAX :: (a -> b) -> SF' a c -> SF' a (b ,c)
pfoAX :: (a -> b) -> SF' a c -> SF' a (b, c)
pfoAX a -> b
f1 (SFArr DTime -> a -> Transition a c
_ FunDesc a c
fd2) = FunDesc a (b, c) -> SF' a (b, c)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut ((a -> b) -> FunDesc a b
forall a b. (a -> b) -> FunDesc a b
FDG a -> b
f1) FunDesc a c
fd2)
pfoAX a -> b
f1 SF' a c
sf2 = (DTime -> a -> Transition a (b, c)) -> SF' a (b, c)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a (b, c)
tf
where
tf :: DTime -> a -> Transition a (b, c)
tf DTime
dt a
a = ((a -> b) -> SF' a c -> SF' a (b, c)
forall a b c. (a -> b) -> SF' a c -> SF' a (b, c)
pfoAX a -> b
f1 SF' a c
sf2', (a -> b
f1 a
a, c
c))
where
(SF' a c
sf2', c
c) = (SF' a c -> DTime -> a -> Transition a c
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a c
sf2) DTime
dt a
a
pfoXA :: SF' a b -> (a -> c) -> SF' a (b ,c)
pfoXA :: SF' a b -> (a -> c) -> SF' a (b, c)
pfoXA (SFArr DTime -> a -> Transition a b
_ FunDesc a b
fd1) a -> c
f2 = FunDesc a (b, c) -> SF' a (b, c)
forall a b. FunDesc a b -> SF' a b
sfArr (FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
fd1 ((a -> c) -> FunDesc a c
forall a b. (a -> b) -> FunDesc a b
FDG a -> c
f2))
pfoXA SF' a b
sf1 a -> c
f2 = (DTime -> a -> Transition a (b, c)) -> SF' a (b, c)
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a (b, c)
tf
where
tf :: DTime -> a -> Transition a (b, c)
tf DTime
dt a
a = (SF' a b -> (a -> c) -> SF' a (b, c)
forall a b c. SF' a b -> (a -> c) -> SF' a (b, c)
pfoXA SF' a b
sf1' a -> c
f2, (b
b, a -> c
f2 a
a))
where
(SF' a b
sf1', b
b) = (SF' a b -> DTime -> a -> Transition a b
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' a b
sf1) DTime
dt a
a
instance ArrowLoop SF where
loop :: SF (b, d) (c, d) -> SF b c
loop = SF (b, d) (c, d) -> SF b c
forall b d c. SF (b, d) (c, d) -> SF b c
loopPrim
loopPrim :: SF (a,c) (b,c) -> SF a b
loopPrim :: SF (a, c) (b, c) -> SF a b
loopPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = (a, c) -> Transition (a, c) (b, c)
tf10}) = SF :: forall a b. (a -> Transition a b) -> SF a b
SF {sfTF :: a -> Transition a b
sfTF = a -> Transition a b
tf0}
where
tf0 :: a -> Transition a b
tf0 a
a0 = (SF' (a, c) (b, c) -> SF' a b
forall a c b. SF' (a, c) (b, c) -> SF' a b
loopAux SF' (a, c) (b, c)
sf1, b
b0)
where
(SF' (a, c) (b, c)
sf1, (b
b0, c
c0)) = (a, c) -> Transition (a, c) (b, c)
tf10 (a
a0, c
c0)
loopAux :: SF' (a,c) (b,c) -> SF' a b
loopAux :: SF' (a, c) (b, c) -> SF' a b
loopAux (SFArr DTime -> (a, c) -> Transition (a, c) (b, c)
_ FunDesc (a, c) (b, c)
FDI) = SF' a b
forall a. SF' a a
sfId
loopAux (SFArr DTime -> (a, c) -> Transition (a, c) (b, c)
_ (FDC (b
b, c
_))) = b -> SF' a b
forall b a. b -> SF' a b
sfConst b
b
loopAux (SFArr DTime -> (a, c) -> Transition (a, c) (b, c)
_ FunDesc (a, c) (b, c)
fd1) =
(a -> b) -> SF' a b
forall a b. (a -> b) -> SF' a b
sfArrG (\a
a -> let (b
b,c
c) = (FunDesc (a, c) (b, c) -> (a, c) -> (b, c)
forall a b. FunDesc a b -> a -> b
fdFun FunDesc (a, c) (b, c)
fd1) (a
a,c
c) in b
b)
loopAux SF' (a, c) (b, c)
sf1 = (DTime -> a -> Transition a b) -> SF' a b
forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> Transition a b
tf
where
tf :: DTime -> a -> Transition a b
tf DTime
dt a
a = (SF' (a, c) (b, c) -> SF' a b
forall a c b. SF' (a, c) (b, c) -> SF' a b
loopAux SF' (a, c) (b, c)
sf1', b
b)
where
(SF' (a, c) (b, c)
sf1', (b
b, c
c)) = (SF' (a, c) (b, c) -> DTime -> (a, c) -> Transition (a, c) (b, c)
forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' (a, c) (b, c)
sf1) DTime
dt (a
a, c
c)
sfSScan :: (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan :: (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan c -> a -> Maybe (c, b)
f c
c b
b = SF' a b
sf
where
sf :: SF' a b
sf = (DTime -> a -> Transition a b)
-> (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
forall a b c.
(DTime -> a -> Transition a b)
-> (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
SFSScan DTime -> a -> Transition a b
tf c -> a -> Maybe (c, b)
f c
c b
b
tf :: DTime -> a -> Transition a b
tf DTime
_ a
a = case c -> a -> Maybe (c, b)
f c
c a
a of
Maybe (c, b)
Nothing -> (SF' a b
sf, b
b)
Just (c
c', b
b') -> ((c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
forall c a b. (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan c -> a -> Maybe (c, b)
f c
c' b
b', b
b')