{-# 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

      -- *** Scanning
    , sfSScan

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

      -- ** Lifting
    , 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

-- * 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 -> 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         = forall a. SF' a a
sfId
sfArr (FDC b
b)     = forall b a. b -> SF' a b
sfConst b
b
sfArr (FDE Event a -> b
f b
fne) = forall a b. (Event a -> b) -> b -> SF' (Event a) b
sfArrE Event a -> b
f b
fne
sfArr (FDG a -> b
f)     = 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 = forall a. SF' a a
sf
  where
    sf :: SF' b b
sf = forall a b.
(DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
SFArr (\DTime
_ b
a -> (SF' b b
sf, b
a)) 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 = forall a b.
(DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
SFArr (\DTime
_ a
_ -> (SF' a b
sf, b
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  = 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))
                (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 = 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)) (forall a b. (a -> b) -> FunDesc a b
FDG a -> b
f)

-- | 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   = (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 (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)

-- | 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 = 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 (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

-- | 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       = forall a. a -> a
id
fdFun (FDC b
b)   = forall a b. a -> b -> a
const b
b
fdFun (FDE Event a -> b
f 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 b c
fd2
fdComp FunDesc a b
fd1           FunDesc b c
FDI     = FunDesc a b
fd1
fdComp (FDC b
b)       FunDesc b c
fd2     = forall b a. b -> FunDesc a b
FDC ((forall a b. FunDesc a b -> a -> b
fdFun FunDesc b c
fd2) b
b)
fdComp FunDesc a b
_             (FDC c
c) = forall b a. b -> FunDesc a b
FDC c
c
fdComp (FDE Event a -> b
f1 b
f1ne) FunDesc b c
fd2     = forall c b. (Event c -> b) -> b -> FunDesc (Event c) b
FDE (b -> c
f2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Event a -> b
f1) (b -> c
f2 b
f1ne)
  where
    f2 :: b -> c
f2 = 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) = 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
f1a
fdComp (FDG a -> b
f1) FunDesc b c
fd2 = forall a b. (a -> b) -> FunDesc a b
FDG (forall a b. FunDesc a b -> a -> b
fdFun FunDesc b c
fd2 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     = forall a. FunDesc a a
FDI
fdPar FunDesc a b
FDI     (FDC d
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     = forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
a, c
c)) -> (a
a, (forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd2) c
c))
fdPar (FDC b
b) FunDesc c d
FDI     = forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
_, c
c)) -> (b
b, c
c))
fdPar (FDC b
b) (FDC d
d) = forall b a. b -> FunDesc a b
FDC (b
b, d
d)
fdPar (FDC b
b) FunDesc c d
fd2     = forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
_, c
c)) -> (b
b, (forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd2) c
c))
fdPar FunDesc a b
fd1     FunDesc c d
fd2     = forall a b. (a -> b) -> FunDesc a b
FDG (\(~(a
a, c
c)) -> ((forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a, (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     = forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
a, a
a))
fdFanOut FunDesc a b
FDI     (FDC c
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     = forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (a
a, (forall a b. FunDesc a b -> a -> b
fdFun FunDesc a c
fd2) a
a))
fdFanOut (FDC b
b) FunDesc a c
FDI     = forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (b
b, a
a))
fdFanOut (FDC b
b) (FDC c
c) = forall b a. b -> FunDesc a b
FDC (b
b, c
c)
fdFanOut (FDC b
b) FunDesc a c
fd2     = forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> (b
b, (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) = 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
ea)

    f1f2ne :: (b, c)
f1f2ne = (b
f1ne, c
f2ne)
fdFanOut FunDesc a b
fd1 FunDesc a c
fd2 =
  forall a b. (a -> b) -> FunDesc a b
FDG (\a
a -> ((forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a, (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
_  =
  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
(.) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b c. SF a b -> SF b c -> SF a c
compPrim
  id :: forall a. SF a a
id = forall a b. (a -> Transition a b) -> SF a b
SF forall a b. (a -> b) -> a -> b
$ \a
x -> (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 = forall a b. (a -> Transition a b) -> SF a b
SF 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) = forall a b. SF a b -> a -> Transition a b
sfTF SF b c
sfL b
b
                   in (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, forall a b. a -> Either a b
Left c
c)
        Right b'
d -> let (SF' b' c'
sf', c'
e) = forall a b. SF a b -> a -> Transition a b
sfTF SF b' c'
sfR b'
d
                   in (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', 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 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' 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) = 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, forall a b. a -> Either a b
Left a
c)
          Right a
d -> let (SF' a b
sf', b
e) = forall a b. SF a b -> a -> Transition a b
sfTF SF a b
sfR a
d
                     in (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', 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 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' 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) = forall a b. SF a b -> a -> Transition a b
sfTF SF a a
sfL a
b
                     in (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, forall a b. a -> Either a b
Left a
c)
          Right a
d -> let (SF' a b
sf', b
e) = 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', 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 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' 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) = 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, forall a b. a -> Either a b
Left a
c)
          Right a
d -> let (SF' a b
sf', b
e) = 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', 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    = forall b c. (b -> c) -> SF b c
arrPrim
  first :: forall b c d. SF b c -> SF (b, d) (c, d)
first  = 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 = 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')
(***)  = 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')
(&&&)  = 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 = (forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a 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 = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (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 forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& SF a a
x) forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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 -> (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 -> (forall a b. (Event a -> b) -> b -> SF' (Event a) b
sfArrE Event a -> b
f (Event a -> b
f forall a. Event a
NoEvent), Event a -> b
f Event a
a)}

-- * 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 = (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               = 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)     = 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) =
    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         -> forall a. Maybe a
Nothing
                     | Bool
otherwise -> forall a. a -> Maybe a
Just ((c
s1', b
b', c
s2, c
c), c
c)
             Just (c
s2', 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) =
    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
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 -> 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 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 -> forall a. a -> Maybe a
Just ((c
s1', b
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 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) =
    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         -> forall a. Maybe a
Nothing
                   | Bool
otherwise -> forall a. a -> Maybe a
Just (seq :: forall a b. a -> b -> b
seq c
s1' (c
s1', b
bne', c
s2, c
c), c
c)
           Just (c
s2', c
c') -> forall a. a -> Maybe a
Just (seq :: forall a b. a -> b -> b
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) =
    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) (forall a b. Event a -> b -> b
vfyNoEv b
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)
_ -> forall a. String -> String -> String -> a
usrErr String
"Yampa" String
"cpXX" forall a b. (a -> b) -> a -> b
$
               String
"Assertion failed: Functions on events must not map "
               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) =
  forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (forall a b c. SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE SF' a b
sf1 Event a -> b
f21 b
f21ne) (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) =
  forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (forall a b c. SF' a b -> (b -> c) -> SF' a c
cpXG SF' a b
sf1 b -> b
f21) (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{}) =
  forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd11 SF' b c
sf12) (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.
  forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA FunDesc a b
fd11 (forall a b c. SF' a b -> SF' b c -> SF' a c
cpXX (forall a b c. SF' a b -> FunDesc b c -> SF' a c
cpXA SF' b c
sf12 (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 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a c, c)
tf --  False
  where
    tf :: DTime -> a -> (SF' a c, c)
tf DTime
dt a
a = (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) = (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) = (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     = 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     = 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     = 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) = forall b a. b -> SF' a b
sfConst d
d
cpAXA FunDesc a b
fd1     SF' b c
sf2 FunDesc c d
fd3     =
    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 (forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) FunDesc c d
fd3 (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) =
      forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c. 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
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 {}) =
      forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd1 (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 {}) =
      forall a b c. FunDesc a b -> SF' b c -> SF' a c
cpAX FunDesc a b
fd1 (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) =
      forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA (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 (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 = 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 -> (SF' a d, d)
tf FunDesc a b
fd1 SF' b c
sf2 FunDesc c d
fd3

      where
        tf :: DTime -> a -> (SF' a d, d)
tf DTime
dt a
a = (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) = (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' b c
sf2
cpAX (FDC b
b)       SF' b c
sf2 = 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 = 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 = 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
sf1
cpXA SF' a b
_   (FDC c
c)       = forall b a. b -> SF' a b
sfConst c
c
cpXA SF' a b
sf1 (FDE Event a -> c
f2 c
f2ne) = forall a b c. SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE SF' a b
sf1 Event a -> c
f2 c
f2ne
cpXA SF' a b
sf1 (FDG b -> c
f2)      = 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) = forall b a. b -> SF' a b
sfConst ((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) = 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) = forall b a. b -> SF' a b
sfConst (forall a b. Event a -> b -> b
vfyNoEv b
b c
cne)
cpCX b
b (SFCpAXA DTime -> b -> Transition b c
_ FunDesc b b
fd21 SF' b c
sf22 FunDesc c c
fd23) =
  forall b c d a. b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA ((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 = 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 -> (SF' a c, c)
tf (forall b a. b -> FunDesc a b
FDC b
b) SF' b c
sf2 forall a. FunDesc a a
FDI
  where
    tf :: DTime -> a -> (SF' a c, c)
tf DTime
dt a
_ = (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) = (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     = 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) = forall b a. b -> SF' a b
sfConst d
c
cpCXA b
b SF' b c
sf2 FunDesc c d
fd3     = forall a b c d.
FunDesc a b -> b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpCXAAux (forall b a. b -> FunDesc a b
FDC b
b) b
b FunDesc c d
fd3 (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)     = forall b a. b -> SF' a b
sfConst (c -> d
f3 ((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) = 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 -> forall a. Maybe a
Nothing
                   Just (c
s', c
c') -> 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) = forall b a. b -> SF' a b
sfConst (c -> d
f3 (forall a b. Event a -> b -> b
vfyNoEv b
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) =
      forall b c d a. b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA ((forall a b. FunDesc a b -> a -> b
fdFun FunDesc b b
fd21) b
b) SF' b c
sf22 (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 = 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 -> (SF' a d, d)
tf FunDesc a b
fd1 SF' b c
sf2 FunDesc c d
fd3
      where
        tf :: DTime -> a -> (SF' a d, d)
tf DTime
dt a
_ = (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) = (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 = forall a b c. FunDesc a b -> (a -> b) -> SF' b c -> SF' a c
cpGXAux (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) = forall a b. FunDesc a b -> SF' a b
sfArr (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) = 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) =
      forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA (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 = 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 -> (SF' a c, c)
tf FunDesc a b
fd1 SF' b c
sf2 forall a. FunDesc a a
FDI
      where
        tf :: DTime -> a -> (SF' a c, c)
tf DTime
dt a
a = (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) = (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 = forall b c a. FunDesc b c -> (b -> c) -> SF' a b -> SF' a c
cpXGAux (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) = forall a b. FunDesc a b -> SF' a b
sfArr (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) = 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 -> forall a. Maybe a
Nothing
                   Just (c
s', b
b') -> 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) = 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) =
      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 (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 = 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 -> (SF' a c, c)
tf forall a. FunDesc a a
FDI SF' a b
sf1 FunDesc b c
fd2
      where
        tf :: DTime -> a -> (SF' a c, c)
tf DTime
dt a
a = (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) = (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 = forall a b c.
FunDesc (Event a) b
-> (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEXAux (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) = forall a b. FunDesc a b -> SF' a b
sfArr (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) = 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) =
        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) (forall a b. Event a -> b -> b
vfyNoEv b
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 (forall a. a -> Event a
Event a
a) of
            b
Event a
NoEvent -> ((c, c)
scne, c
cne, c
cne)
            Event a
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) =
      forall a b c d. FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA (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 = 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 -> (SF' (Event a) c, c)
tf FunDesc (Event a) b
fd1 SF' b c
sf2 forall a. FunDesc a a
FDI
      where
        tf :: DTime -> Event a -> (SF' (Event a) c, c)
tf DTime
dt Event a
ea = (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 -> (forall a b. SF' a b -> DTime -> a -> Transition a b
sfTF' SF' b c
sf2) DTime
dt b
f1ne
                Event a
_       -> (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 = forall b c a.
FunDesc (Event b) c
-> (Event b -> c) -> c -> SF' a (Event b) -> SF' a c
cpXEAux (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) = forall a b. FunDesc a b -> SF' a b
sfArr (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) = 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 -> forall a. Maybe a
Nothing
                   Just (c
s', Event b
NoEvent) -> forall a. a -> Maybe a
Just (c
s', c
f2ne)
                   Just (c
s', Event b
eb')     -> 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) =
        forall c a b. (c -> a -> (c, b, b)) -> c -> b -> SF' (Event a) b
sfEP c -> a -> (c, c, c)
f c
s (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)
_ -> forall a. String -> String -> String -> a
usrErr String
"Yampa" String
"cpXEAux" forall a b. (a -> b) -> a -> b
$
                   String
"Assertion failed: Functions on events must not "
                   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) =
      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 (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 = 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 -> (SF' a c, c)
tf forall a. FunDesc a a
FDI SF' a (Event b)
sf1 FunDesc (Event b) c
fd2
      where
        tf :: DTime -> a -> (SF' a c, c)
tf DTime
dt a
a = ( 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) = (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) = (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)       = forall a. SF' a a
sfId                        -- New
fpAux (SFArr DTime -> a -> Transition a b
_ (FDC b
b))   = 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)       = forall a b. (a -> b) -> SF' a b
sfArrG (\(~(a
a, c
c)) -> ((forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a, c
c))
fpAux SF' a b
sf1 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> (SF' (a, c) (b, c), (b, c))
tf
  where
    tf :: DTime -> (a, c) -> (SF' (a, c) (b, c), (b, c))
tf DTime
dt ~(a
a, c
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) = (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) = (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)       = forall a. SF' a a
sfId                        -- New
spAux (SFArr DTime -> a -> Transition a b
_ (FDC b
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)       = forall a b. (a -> b) -> SF' a b
sfArrG (\(~(c
c, a
a)) -> (c
c, (forall a b. FunDesc a b -> a -> b
fdFun FunDesc a b
fd1) a
a))
spAux SF' a b
sf1 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (c, a) -> (SF' (c, a) (c, b), (c, b))
tf
  where
    tf :: DTime -> (c, a) -> (SF' (c, a) (c, b), (c, b))
tf DTime
dt ~(c
c, a
a) = (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) = (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) = (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)       = forall a b. FunDesc a b -> SF' a b
sfArr (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                 = 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                 = 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                 = forall a b c d. (a -> b) -> SF' c d -> SF' (a, c) (b, d)
psAX (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)       = 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))   = 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)       = forall a b c d. SF' a b -> (c -> d) -> SF' (a, c) (b, d)
psXA SF' a b
sf1 (forall a b. FunDesc a b -> a -> b
fdFun FunDesc c d
fd2)
    psXX SF' a b
sf1 SF' c d
sf2 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf
      where
        tf :: DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf DTime
dt ~(a
a, c
c) = (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) = (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) = (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)       = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar (forall b a. b -> FunDesc a b
FDC b
b) FunDesc c d
fd2)
    psCX b
b SF' c d
sf2                 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf
      where
        tf :: DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf DTime
dt ~(a
_, c
c) = (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) = (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 = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar FunDesc a b
fd1 (forall b a. b -> FunDesc a b
FDC d
d))
    psXC SF' a b
sf1                 d
d = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf
      where
        tf :: DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf DTime
dt ~(a
a, c
_) = (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) = (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)       = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar (forall a b. (a -> b) -> FunDesc a b
FDG a -> b
f1) FunDesc c d
fd2)
    psAX a -> b
f1 SF' c d
sf2                 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf
      where
        tf :: DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf DTime
dt ~(a
a, c
c) = (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) = (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 = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c d. FunDesc a b -> FunDesc c d -> FunDesc (a, c) (b, d)
fdPar FunDesc a b
fd1 (forall a b. (a -> b) -> FunDesc a b
FDG c -> d
f2))
    psXA SF' a b
sf1                 c -> d
f2 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf
      where
        tf :: DTime -> (a, c) -> (SF' (a, c) (b, d), (b, d))
tf DTime
dt ~(a
a, c
c) = (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) = (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 = (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)       = forall a b. FunDesc a b -> SF' a b
sfArr(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                 = 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                 = 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                 = forall a b c. (a -> b) -> SF' a c -> SF' a (b, c)
pfoAX (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)       = 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))   = 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)       = forall a b c. SF' a b -> (a -> c) -> SF' a (b, c)
pfoXA SF' a b
sf1 (forall a b. FunDesc a b -> a -> b
fdFun FunDesc a c
fd2)
    pfoXX SF' a b
sf1 SF' a c
sf2 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a (b, c), (b, c))
tf
      where
        tf :: DTime -> a -> (SF' a (b, c), (b, c))
tf DTime
dt a
a = (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) = (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) = (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) = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut forall a. FunDesc a a
FDI FunDesc a c
fd2)
    pfoIX SF' a c
sf2 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a (a, c), (a, c))
tf
      where
        tf :: DTime -> a -> (SF' a (a, c), (a, c))
tf DTime
dt a
a = (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) = (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) = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
fd1 forall a. FunDesc a a
FDI)
    pfoXI SF' a b
sf1 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a (b, a), (b, a))
tf
      where
        tf :: DTime -> a -> (SF' a (b, a), (b, a))
tf DTime
dt a
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) = (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) = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut (forall b a. b -> FunDesc a b
FDC b
b) FunDesc a c
fd2)
    pfoCX b
b SF' a c
sf2 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a (b, c), (b, c))
tf
      where
        tf :: DTime -> a -> (SF' a (b, c), (b, c))
tf DTime
dt a
a = (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) = (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 = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
fd1 (forall b a. b -> FunDesc a b
FDC c
c))
    pfoXC SF' a b
sf1 c
c = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a (b, c), (b, c))
tf
      where
        tf :: DTime -> a -> (SF' a (b, c), (b, c))
tf DTime
dt a
a = (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) = (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) = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut (forall a b. (a -> b) -> FunDesc a b
FDG a -> b
f1) FunDesc a c
fd2)
    pfoAX a -> b
f1 SF' a c
sf2 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a (b, c), (b, c))
tf
      where
        tf :: DTime -> a -> (SF' a (b, c), (b, c))
tf DTime
dt a
a = (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) = (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 = forall a b. FunDesc a b -> SF' a b
sfArr (forall a b c. FunDesc a b -> FunDesc a c -> FunDesc a (b, c)
fdFanOut FunDesc a b
fd1 (forall a b. (a -> b) -> FunDesc a b
FDG a -> c
f2))
    pfoXA SF' a b
sf1 a -> c
f2 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a (b, c), (b, c))
tf
      where
        tf :: DTime -> a -> (SF' a (b, c), (b, c))
tf DTime
dt a
a = (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) = (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 = 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 = (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) = forall a. SF' a a
sfId
    loopAux (SFArr DTime -> (a, c) -> Transition (a, c) (b, c)
_ (FDC (b
b, c
_))) = 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) =
      forall a b. (a -> b) -> SF' a b
sfArrG (\a
a -> let (b
b,c
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 = forall a b. (DTime -> a -> Transition a b) -> SF' a b
SF' DTime -> a -> (SF' a b, b)
tf
      where
        tf :: DTime -> a -> (SF' a b, b)
tf DTime
dt a
a = (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)) = (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 = 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') -> (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')