{-# LANGUAGE CPP   #-}
{-# LANGUAGE GADTs #-}
-- |
-- Module      : FRP.Yampa
-- Copyright   : (c) Ivan Perez, 2014-2022
--               (c) George Giorgidze, 2007-2012
--               (c) Henrik Nilsson, 2005-2006
--               (c) Antony Courtney and Henrik Nilsson, Yale University, 2003-2004
-- License     : BSD-style (see the LICENSE file in the distribution)
--
-- Maintainer  : ivan.perez@keera.co.uk
-- Stability   : provisional
-- Portability : non-portable (GHC extensions)
--
-- Domain-specific language embedded in Haskell for programming hybrid (mixed
-- discrete-time and continuous-time) systems. Yampa is based on the concepts of
-- Functional Reactive Programming (FRP) and is structured using arrow
-- combinators.
--
-- You can find examples, tutorials and documentation on Yampa here:
--
-- <www.haskell.org/haskellwiki/Yampa>
--
-- Structuring a hybrid system in Yampa is done based on two main concepts:
--
-- * Signal Functions: 'SF'. Yampa is based on the concept of Signal Functions,
-- which are functions from a typed input signal to a typed output signal.
-- Conceptually, signals are functions from Time to Value, where time are the
-- real numbers and, computationally, a very dense approximation (Double) is
-- used.
--
-- * Events: 'Event'. Values that may or may not occur (and would probably occur
-- rarely). It is often used for incoming network messages, mouse clicks, etc.
-- Events are used as values carried by signals.
--
-- A complete Yampa system is defined as one Signal Function from some type @a@
-- to a type @b@. The execution of this signal transformer with specific input
-- can be accomplished by means of two functions: 'reactimate' (which needs an
-- initialization action, an input sensing action and an actuation/consumer
-- action and executes until explicitly stopped), and 'react' (which executes
-- only one cycle).
--
-- Apart from using normal functions and arrow syntax to define 'SF's, you can
-- also use several combinators. See [<#g:4>] for basic signals combinators,
-- [<#g:11>] for ways of switching from one signal transformation to another,
-- and [<#g:16>] for ways of transforming Event-carrying signals into continuous
-- signals, [<#g:19>] for ways of delaying signals, and [<#g:21>] for ways to
-- feed a signal back to the same signal transformer.
--
-- Ways to define Event-carrying signals are given in [<#g:7>], and
-- "FRP.Yampa.Event" defines events and event-manipulation functions.
--
-- Finally, see [<#g:26>] for sources of randomness (useful in games).
module FRP.Yampa.InternalCore
    ( module Control.Arrow

      -- * Basic definitions
      -- ** Time
    , Time
    , DTime

      -- ** Signal Functions
    , SF(..)

      -- ** Future Signal Function
    , SF'(..)
    , Transition
    , sfTF'
    , sfId
    , sfConst
    , sfArrG

      -- ** Function descriptions
    , FunDesc(..)
    , fdFun

      -- ** Lifting
    , arrPrim
    , arrEPrim
    , epPrim

      -- *** Scanning
    , sfSScan
    )
  where

-- External imports
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative (Applicative(..))
#endif

import Control.Arrow (Arrow (..), ArrowChoice (..), ArrowLoop (..), (>>>))

#if __GLASGOW_HASKELL__ >= 610
import qualified Control.Category (Category(..))
#endif

-- Internal imports
import FRP.Yampa.Diagnostics (usrErr)
import FRP.Yampa.Event       (Event (..))

-- * Basic type definitions with associated utilities

-- | Time is used both for time intervals (duration), and time w.r.t. some
-- agreed reference point in time.

--  Conceptually, Time = R, i.e. time can be 0 -- or even negative.
type Time = Double      -- [s]

-- | DTime is the time type for lengths of sample intervals. Conceptually,
-- DTime = R+ = { x in R | x > 0 }. Don't assume Time and DTime have the
-- same representation.
type DTime = Double     -- [s]

-- | Signal function that transforms a signal carrying values of some type 'a'
-- into a signal carrying values of some type 'b'. You can think of it as
-- (Signal a -> Signal b). A signal is, conceptually, a function from 'Time' to
-- value.
data SF a b = SF {forall a b. SF a b -> a -> Transition a b
sfTF :: a -> Transition a b}

-- | Signal function in "running" state.
--
-- It can also be seen as a Future Signal Function, meaning, an SF that, given a
-- time delta or a time in the future, it will be an SF.
data SF' a b where
  SFArr :: !(DTime -> a -> Transition a b) -> !(FunDesc a b) -> SF' a b

  -- The b is intentionally unstrict as the initial output sometimes is
  -- undefined (e.g. when defining pre). In any case, it isn't necessarily used
  -- and should thus not be forced.
  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

-- | A transition is a pair of the next state (in the form of a future signal
-- function) and the output at the present time step.
type Transition a b = (SF' a b, b)

-- | Obtain the function that defines a running SF.
sfTF' :: SF' a b -> (DTime -> a -> Transition a b)
sfTF' :: forall a b. 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

-- | Constructor for a lifted structured function.
sfArr :: FunDesc a b -> SF' a b
sfArr :: forall a b. FunDesc a b -> SF' a b
sfArr FunDesc a b
FDI         = SF' a a
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

-- | SF constructor for the identity function.
sfId :: SF' a a
sfId :: forall a. 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

-- | SF constructor for the constant function.
sfConst :: b -> SF' a b
sfConst :: forall b a. 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)

-- Assumption: fne = f NoEvent
sfArrE :: (Event a -> b) -> b -> SF' (Event a) b
sfArrE :: forall a b. (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 c b. (Event c -> b) -> b -> FunDesc (Event c) b
FDE Event a -> b
f b
fne)

-- | SF constructor for a general function.
sfArrG :: (a -> b) -> SF' a b
sfArrG :: forall a b. (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)

-- ** Function descriptions

-- | Structured function definition.
--
-- This type represents functions with a bit more structure, providing specific
-- constructors for the identity, constant and event-based functions, helping
-- optimise arrow combinators for special cases.
data FunDesc a b where
  FDI :: FunDesc a a                                  -- Identity function
  FDC :: b -> FunDesc a b                             -- Constant function
  FDE :: (Event a -> b) -> b -> FunDesc (Event a) b   -- Event-processing fun
  FDG :: (a -> b) -> FunDesc a b                      -- General function

-- | Turns a function into a structured function.
fdFun :: FunDesc a b -> (a -> b)
fdFun :: forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
FDI       = a -> a
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

-- | Composition for structured functions.
fdComp :: FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp :: forall a b c. 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 c b. (Event c -> b) -> b -> FunDesc (Event c) 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
Event a
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)

-- | Parallel application of structured functions.
fdPar :: FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar :: forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar FunDesc a b
FDI     FunDesc c d
FDI     = FunDesc (a, c) (a, c)
FunDesc (a, c) (b, d)
forall a. FunDesc a a
FDI
fdPar FunDesc a b
FDI     (FDC d
d) = ((a, c) -> (b, d)) -> FunDesc (a, c) (b, d)
forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
a, c
_)) -> (a
b
a, d
d))
fdPar FunDesc a b
FDI     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)) -> (a
b
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, d)) -> FunDesc (a, c) (b, d)
forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
_, c
c)) -> (b
b, c
d
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))

-- | Parallel application with broadcasting for structured functions.
fdFanOut :: FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut :: forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
FDI           FunDesc a c
FDI           = (a -> (b, c)) -> FunDesc a (b, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
b
a, a
c
a))
fdFanOut FunDesc a b
FDI           (FDC c
c)       = (a -> (b, c)) -> FunDesc a (b, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
b
a, c
c))
fdFanOut FunDesc a b
FDI           FunDesc a c
fd2           = (a -> (b, c)) -> FunDesc a (b, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
b
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, c)) -> FunDesc a (b, c)
forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (b
b, a
c
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 c b. (Event c -> b) -> b -> FunDesc (Event c) 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))

-- | Verifies that the first argument is NoEvent. Returns the value of the
-- second argument that is the case. Raises an error otherwise. Used to check
-- that functions on events do not map NoEvent to Event wherever that assumption
-- is exploited.
vfyNoEv :: Event a -> b -> b
vfyNoEv :: forall a b. 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
"Yampa"
    String
"vfyNoEv"
    String
"Assertion failed: Functions on events must not map NoEvent to Event."

-- * Arrow instance and implementation

#if __GLASGOW_HASKELL__ >= 610
-- | Composition and identity for SFs.
instance Control.Category.Category SF where
  . :: forall b c a. 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 :: forall a. 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

-- | Choice of which SF to run based on the value of a signal.
instance ArrowChoice SF where
  -- (+++) :: forall b c b' c'
  --       .  SF b c -> SF d e -> SF (Either b d) (Either c e)
  SF b c
sfL +++ :: forall b c b' c'.
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

      -- (+++) for an initialized SF and an SF
      --
      -- chooseL :: SF' b c -> SF d e -> SF' (Either b d) (Either c e)
      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)

      -- (+++) for an SF and an initialized SF
      --
      -- chooseR :: SF b c -> SF' d e -> SF' (Either b d) (Either c 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)

      -- (+++) for initialized SFs
      --
      -- choose :: SF' b c -> SF' d e -> SF' (Either b d) (Either c 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)

-- | Signal Functions as Arrows. See "The Yampa Arcade", by Courtney, Nilsson
-- and Peterson.
instance Arrow SF where
  arr :: forall b c. (b -> c) -> SF b c
arr    = (b -> c) -> SF b c
forall b c. (b -> c) -> SF b c
arrPrim
  first :: forall b c d. 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 :: forall b c d. 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
  *** :: forall b c b' c'. 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
  &&& :: forall b c c'. 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

-- | Functor instance for applied SFs.
instance Functor (SF a) where
  fmap :: forall a b. (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 b c. (b -> c) -> SF b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> b
f)

-- | Applicative Functor instance (allows classic-frp style signals and
-- composition using applicative style).
instance Applicative (SF a) where
  pure :: forall a. a -> SF a a
pure a
x  = (a -> a) -> SF a a
forall b c. (b -> c) -> SF b c
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 <*> :: forall a b. 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 b c c'. SF b c -> SF b c' -> SF b (c, c')
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 b c. (b -> c) -> SF b c
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
($))

-- * Lifting.

-- | Lifts a pure function into a signal function (applied pointwise).
{-# NOINLINE arrPrim #-}
arrPrim :: (a -> b) -> SF a b
arrPrim :: forall b c. (b -> c) -> SF b c
arrPrim a -> b
f = 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)}

-- | Lifts a pure function into a signal function applied to events
--   (applied pointwise).
{-# RULES "arrPrim/arrEPrim" arrPrim = arrEPrim #-}
arrEPrim :: (Event a -> b) -> SF (Event a) b
arrEPrim :: forall a b. (Event a -> b) -> SF (Event a) b
arrEPrim Event a -> b
f = 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)}

-- | Versatile zero-order hold SF' with folding.
--
-- This function returns an SF that, if there is an input, runs it through the
-- given function and returns part of its output and, if not, returns the last
-- known output.
--
-- The auxiliary function returns the value of the current output and the future
-- held output, thus making it possible to have to distinct outputs for the
-- present and the future.
epPrim :: (c -> a -> (c, b, b)) -> c -> b -> SF (Event a) b
epPrim :: forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF (Event a) b
epPrim c -> a -> (c, b, b)
f c
c b
bne = 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) = ((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)
      where
        (c
c', b
b, b
bne') = c -> a -> (c, b, b)
f c
c a
a

-- | Constructor for a zero-order hold SF' with folding.
--
-- This function returns a running SF that, if there is an input, runs it
-- through the given function and returns part of its output and, if not,
-- returns the last known output.
--
-- The auxiliary function returns the value of the current output and the future
-- held output, thus making it possible to have to distinct outputs for the
-- present and the future.
sfEP :: (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP :: 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 = 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 c b c.
(DTime -> Event c -> Transition (Event c) b)
-> (c -> c -> (c, b, b)) -> c -> b -> SF' (Event c) 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

-- * Composition.

-- | SF Composition.
--
-- The definition exploits the following identities:
--     sf         >>> identity   = sf                           -- New
--     identity   >>> sf         = sf                           -- New
--     sf         >>> constant c = constant c
--     constant c >>> arr f      = constant (f c)
--     arr f      >>> arr g      = arr (g . f)
compPrim :: SF a b -> SF b c -> SF a c
compPrim :: forall a b c. 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 {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

-- The following defs are not local to compPrim because cpAXA needs to be
-- called from parSplitPrim.
-- Naming convention: cp<X><Y> where  <X> and <Y> is one of:
-- X - arbitrary signal function
-- A - arbitrary pure arrow
-- C - constant arrow
-- E - event-processing arrow
-- G - arrow known not to be identity, constant (C) or
--     event-processing (E).

cpXX :: SF' a b -> SF' b c -> SF' a c
cpXX :: forall a b c. 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 =
        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')
      where
        (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')
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
Event a
NoEvent -> ((c, Event a, c, c), c) -> Maybe ((c, Event a, c, c), c)
forall a. a -> Maybe a
Just ((c
s1', b
Event a
eb', c
s2, c
cne), c
cne)
            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', b
Event a
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) -> 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)
(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 =
        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)
forall a b. a -> b -> b
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)
forall a b. a -> b -> b
seq c
s1' (c
s1', b
bne', c
s2', c
c'), c
c')
      where
        (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')
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
    -- The function "f" is invoked whenever an event is to be processed. It then
    -- computes the output, the new state, and the new NoEvent output.  However,
    -- when sequencing event processors, the ones in the latter part of the
    -- chain may not get invoked since previous ones may decide not to "fire".
    -- But a "new" NoEvent output still has to be produced, i.e. the old one
    -- retained. Since it cannot be computed by invoking the last
    -- event-processing function in the chain, it has to be remembered. Since
    -- the composite event-processing function remains constant/unchanged, the
    -- NoEvent output has to be part of the state.  An alternative would be to
    -- make the event-processing function take an extra argument. But that is
    -- likely to make the simple case more expensive. See note at sfEP.
    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
Event a
NoEvent, b
Event a
NoEvent) -> ((c
s1', c
s2, c
cne), c
cne, c
cne)
        (c
s1', Event a
b, b
Event a
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
"Yampa" 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) =
  -- Termination: The first argument to cpXX is no larger than the current first
  -- argument, and the second is smaller.
  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 --  False
  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
-- Termination: cpAX/cpXA, via cpCX, cpEX etc. only call cpAXA if sf2 is
-- SFCpAXA, and then on the embedded sf and hence on a smaller arg.
cpAXA :: forall a b c d. 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' a c -> FunDesc c d -> SF' a d
forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' a c
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 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
SF' b d
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
    -- Really: cpAXAAux :: SF' b c -> SF' a d. Note: Event cases are not
    -- optimized (EXA etc.)
    cpAXAAux :: FunDesc a b
             -> (a -> b)
             -> FunDesc c d
             -> (c -> d)
             -> SF' b c
             -> SF' a d
    cpAXAAux :: 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
_ 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 c c.
(DTime -> a -> Transition a d)
-> FunDesc a c -> SF' c 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 :: forall a b c. 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 :: forall a b c. 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

-- The remaining signal function, if it is SF', later could turn into something
-- else, like SFId.
cpCX :: b -> SF' b c -> SF' a c
cpCX :: forall b c a. 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 c c.
(DTime -> a -> Transition a d)
-> FunDesc a c -> SF' c 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 :: 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
FDI     = b -> SF' b d -> SF' a d
forall b c a. b -> SF' b c -> SF' a c
cpCX b
b SF' b c
SF' b d
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
    -- Really: SF' b c -> SF' a d
    cpCXAAux :: FunDesc a b
             -> b
             -> FunDesc c d
             -> (c -> d)
             -> SF' b c
             -> SF' a d
    cpCXAAux :: forall a b c d.
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 c c.
(DTime -> a -> Transition a d)
-> FunDesc a c -> SF' c 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 :: forall a b c. (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 :: forall a b c. 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)
    -- We actually do know that (fdComp (FDG f1) fd21) is going to result in an
    -- FDG. So we *could* call a cpGXA here. But the price is "inlining" of part
    -- of fdComp.
    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
    -- We really shouldn't see an EP here, as that would mean an arrow
    -- INTRODUCING events ...
    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 c c.
(DTime -> a -> Transition a d)
-> FunDesc a c -> SF' c 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 :: forall a b c. 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
    -- Really: cpXGAux :: SF' a b -> SF' a c
    cpXGAux :: FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
    cpXGAux :: forall b c a. 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 = (c
s', b -> c
f2 b
b, b -> c
f2 b
bne')
          where
            (c
s', b
b, b
bne') = c -> a -> (c, b, b)
f1 c
s a
a

    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 c c.
(DTime -> a -> Transition a d)
-> FunDesc a c -> SF' c 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 :: 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 = 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 c b. (Event c -> b) -> b -> FunDesc (Event c) 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 :: 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
_ 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
    -- We must not capture cne in the f closure since cne can change! See cpXX
    -- the SFEP/SFEP case for a similar situation. However, FDE represent a
    -- state-less signal function, so *its* NoEvent value never changes. Hence
    -- we only need to verify that it is NoEvent once.
    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
Event a
NoEvent -> ((c, c)
scne, c
cne, c
cne)
            Event a
b -> ((c
s', c
cne'), c
c, c
cne')
              where
                (c
s', c
c, c
cne') = c -> a -> (c, c, c)
f2 c
s a
b

    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
    -- The rationale for the following is that the case analysis is typically
    -- not going to be more expensive than applying the function and possibly a
    -- bit cheaper. Thus if events are sparse, we might win, and if not, we
    -- don't loose to much.
    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 c c.
(DTime -> a -> Transition a d)
-> FunDesc a c -> SF' c 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 :: forall a b c. 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 c b. (Event c -> b) -> b -> FunDesc (Event c) 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 :: 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
_ 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
"Yampa" 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 c c.
(DTime -> a -> Transition a d)
-> FunDesc a c -> SF' c 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

-- * Widening.

-- | Widening.
--
-- The definition exploits the following identities:
--     first identity     = identity                            -- New
--     first (constant b) = arr (\(_, c) -> (b, c))
--     (first (arr f))    = arr (\(a, c) -> (f a, c))
firstPrim :: SF a b -> SF (a, c) (b, c)
firstPrim :: forall b c d. SF b c -> SF (b, d) (c, d)
firstPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a b
tf10}) = 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 :: forall a b c. SF' a b -> SF' (a, c) (b, c)
fpAux (SFArr DTime -> a -> Transition a b
_ FunDesc a b
FDI)     = SF' (a, c) (a, c)
SF' (a, c) (b, c)
forall a. SF' a a
sfId                        -- New
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

-- Mirror image of first.
secondPrim :: SF a b -> SF (c, a) (c, b)
secondPrim :: forall b c d. SF b c -> SF (d, b) (d, c)
secondPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = a -> Transition a b
tf10}) = 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 :: forall a b c. SF' a b -> SF' (c, a) (c, b)
spAux (SFArr DTime -> a -> Transition a b
_ FunDesc a b
FDI)     = SF' (c, a) (c, a)
SF' (c, a) (c, b)
forall a. SF' a a
sfId                        -- New
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

-- * Parallel composition.

-- The definition exploits the following identities (that hold for SF):
--     identity   *** identity   = identity             -- New
--     sf         *** identity   = first sf             -- New
--     identity   *** sf         = second sf            -- New
--     constant b *** constant d = constant (b, d)
--     constant b *** arr f2     = arr (\(_, c) -> (b, f2 c)
--     arr f1     *** constant d = arr (\(a, _) -> (f1 a, d)
--     arr f1     *** arr f2     = arr (\(a, b) -> (f1 a, f2 b)
parSplitPrim :: SF a b -> SF c d -> SF (a, c) (b, d)
parSplitPrim :: forall b c b' c'. SF b c -> SF b' c' -> SF (b, b') (c, c')
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 {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

    -- Naming convention: ps<X><Y> where  <X> and <Y> is one of:
    -- X - arbitrary signal function
    -- A - arbitrary pure arrow
    -- C - constant arrow

    psXX :: SF' a b -> SF' c d -> SF' (a, c) (b, d)
    psXX :: forall a b c d. 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        -- New
    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        -- New
    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 :: forall b c d a. 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 :: forall a b d c. 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 :: forall a b c d. (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 :: forall a b c d. 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 :: forall b c c'. SF b c -> SF b c' -> SF b (c, 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 {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

    -- Naming convention: pfo<X><Y> where  <X> and <Y> is one of:
    -- X - arbitrary signal function
    -- A - arbitrary pure arrow
    -- I - identity arrow
    -- C - constant arrow

    pfoXX :: SF' a b -> SF' a c -> SF' a (b, c)
    pfoXX :: forall a b c. 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 :: forall a c. 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 :: forall a b. 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 :: forall b a c. 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 :: forall a b c. 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 :: forall a b c. (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 :: forall a b c. 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

-- * ArrowLoop instance and implementation

-- | Creates a feedback loop without delay.
instance ArrowLoop SF where
  loop :: forall b d c. 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 :: forall b d c. SF (b, d) (c, d) -> SF b c
loopPrim (SF {sfTF :: forall a b. SF a b -> a -> Transition a b
sfTF = (a, c) -> Transition (a, c) (b, c)
tf10}) = 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 :: forall a c b. 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 a
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)

-- * Scanning

-- | Constructor for a zero-order hold with folding.
--
-- This function returns a running SF that takes an input, runs it through a
-- function and, if there is an output, returns it, otherwise, returns the
-- previous value. Additionally, an accumulator or folded value is kept
-- internally.
sfSScan :: (c -> a -> Maybe (c, b)) -> c -> b -> SF' a b
sfSScan :: 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 = 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')