{- |
Combinators to create 'Rhine's (main programs) from basic components
such as 'ClSF's, clocks, 'ResamplingBuffer's and 'Schedule's.

The combinator names are often mixed of the symbols @, @*@ and @>@,
and several other symbols.
The general mnemonic for combinator names is:

* @ annotates a data processing unit such as a signal function, network or buffer
  with temporal information like a clock or a schedule.
* @*@ composes parallely.
* @>@ composes sequentially.
-}

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}

module FRP.Rhine.Reactimation.Combinators where


-- rhine
import FRP.Rhine.Clock
import FRP.Rhine.Clock.Proxy
import FRP.Rhine.ClSF.Core
import FRP.Rhine.ResamplingBuffer
import FRP.Rhine.Schedule
import FRP.Rhine.SN
import FRP.Rhine.SN.Combinators
import FRP.Rhine.Type


-- * Combinators and syntactic sugar for high-level composition of signal networks.


infix 5 @@
-- | Create a synchronous 'Rhine' by combining a clocked signal function with a matching clock.
--   Synchronicity is ensured by requiring that data enters (@In cl@)
--   and leaves (@Out cl@) the system at the same as it is processed (@cl@).
(@@) :: ( cl ~ In cl
        , cl ~ Out cl )
     => ClSF m cl a b -> cl -> Rhine m cl a b
@@ :: ClSF m cl a b -> cl -> Rhine m cl a b
(@@) = SN m cl a b -> cl -> Rhine m cl a b
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (SN m cl a b -> cl -> Rhine m cl a b)
-> (ClSF m cl a b -> SN m cl a b)
-> ClSF m cl a b
-> cl
-> Rhine m cl a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClSF m cl a b -> SN m cl a b
forall cl (m :: Type -> Type) a b.
(cl ~ In cl, cl ~ Out cl) =>
ClSF m cl a b -> SN m cl a b
Synchronous


-- | A point at which sequential asynchronous composition
--   ("resampling") of signal networks can happen.
data ResamplingPoint m cla clb a b = ResamplingPoint
  (ResamplingBuffer m (Out cla) (In clb) a b)
  (Schedule m cla clb)
-- TODO Make a record out of it?
-- TODO This is aesthetically displeasing.
--      For the buffer, the associativity doesn't matter, but for the Schedule,
--      we sometimes need to specify particular brackets in order for it to work.
--      This is confusing.
--      There would be a workaround if there were pullbacks of schedules...

-- | Syntactic sugar for 'ResamplingPoint'.
infix 8 -@-
(-@-) :: ResamplingBuffer m (Out cl1) (In cl2) a b
      -> Schedule         m      cl1      cl2
      -> ResamplingPoint  m      cl1      cl2  a b
-@- :: ResamplingBuffer m (Out cl1) (In cl2) a b
-> Schedule m cl1 cl2 -> ResamplingPoint m cl1 cl2 a b
(-@-) = ResamplingBuffer m (Out cl1) (In cl2) a b
-> Schedule m cl1 cl2 -> ResamplingPoint m cl1 cl2 a b
forall (m :: Type -> Type) cla clb a b.
ResamplingBuffer m (Out cla) (In clb) a b
-> Schedule m cla clb -> ResamplingPoint m cla clb a b
ResamplingPoint

-- | A purely syntactical convenience construction
--   enabling quadruple syntax for sequential composition, as described below.
infix 2 >--
data RhineAndResamplingPoint m cl1 cl2 a c = forall b.
     RhineAndResamplingPoint (Rhine m cl1 a b) (ResamplingPoint m cl1 cl2 b c)

-- | Syntactic sugar for 'RhineAndResamplingPoint'.
(>--) :: Rhine                   m cl1     a b
      -> ResamplingPoint         m cl1 cl2   b c
      -> RhineAndResamplingPoint m cl1 cl2 a   c
>-- :: Rhine m cl1 a b
-> ResamplingPoint m cl1 cl2 b c
-> RhineAndResamplingPoint m cl1 cl2 a c
(>--) = Rhine m cl1 a b
-> ResamplingPoint m cl1 cl2 b c
-> RhineAndResamplingPoint m cl1 cl2 a c
forall (m :: Type -> Type) cl1 cl2 a c b.
Rhine m cl1 a b
-> ResamplingPoint m cl1 cl2 b c
-> RhineAndResamplingPoint m cl1 cl2 a c
RhineAndResamplingPoint

{- | The combinators for sequential composition allow for the following syntax:

@
rh1   :: Rhine            m      cl1           a b
rh1   =  ...

rh2   :: Rhine            m               cl2      c d
rh2   =  ...

rb    :: ResamplingBuffer m (Out cl1) (In cl2)   b c
rb    =  ...

sched :: Schedule         m      cl1      cl2
sched =  ...

rh    :: Rhine m (SequentialClock m cl1   cl2) a     d
rh    =  rh1 >-- rb -@- sched --> rh2
@
-}
infixr 1 -->
(-->) :: ( Clock m cl1
         , Clock m cl2
         , Time cl1 ~ Time cl2
         , Time (Out cl1) ~ Time cl1
         , Time (In  cl2) ~ Time cl2
         , Clock m (Out cl1), Clock m (Out cl2)
         , Clock m (In  cl1), Clock m (In  cl2)
         , GetClockProxy cl1, GetClockProxy cl2
         )
      => RhineAndResamplingPoint   m cl1 cl2  a b
      -> Rhine m                         cl2    b c
      -> Rhine m  (SequentialClock m cl1 cl2) a   c
RhineAndResamplingPoint (Rhine SN m cl1 a b
sn1 cl1
cl1) (ResamplingPoint ResamplingBuffer m (Out cl1) (In cl2) b b
rb Schedule m cl1 cl2
cc) --> :: RhineAndResamplingPoint m cl1 cl2 a b
-> Rhine m cl2 b c -> Rhine m (SequentialClock m cl1 cl2) a c
--> (Rhine SN m cl2 b c
sn2 cl2
cl2)
 = SN m (SequentialClock m cl1 cl2) a c
-> SequentialClock m cl1 cl2
-> Rhine m (SequentialClock m cl1 cl2) a c
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (SN m cl1 a b
-> ResamplingBuffer m (Out cl1) (In cl2) b b
-> SN m cl2 b c
-> SN m (SequentialClock m cl1 cl2) a c
forall (m :: Type -> Type) clab clcd a b c d.
(Clock m clab, Clock m clcd, Clock m (Out clab),
 Clock m (Out clcd), Clock m (In clab), Clock m (In clcd),
 GetClockProxy clab, GetClockProxy clcd, Time clab ~ Time clcd,
 Time clab ~ Time (Out clab), Time clcd ~ Time (In clcd)) =>
SN m clab a b
-> ResamplingBuffer m (Out clab) (In clcd) b c
-> SN m clcd c d
-> SN m (SequentialClock m clab clcd) a d
Sequential SN m cl1 a b
sn1 ResamplingBuffer m (Out cl1) (In cl2) b b
rb SN m cl2 b c
sn2) (cl1 -> cl2 -> Schedule m cl1 cl2 -> SequentialClock m cl1 cl2
forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
cl1 -> cl2 -> Schedule m cl1 cl2 -> SequentialClock m cl1 cl2
SequentialClock cl1
cl1 cl2
cl2 Schedule m cl1 cl2
cc)

-- | A purely syntactical convenience construction
--   allowing for ternary syntax for parallel composition, described below.
data RhineParallelAndSchedule m clL clR a b
  = RhineParallelAndSchedule (Rhine m clL a b) (Schedule m clL clR)

-- | Syntactic sugar for 'RhineParallelAndSchedule'.
infix 4 ++@
(++@)
  :: Rhine                    m clL     a b
  -> Schedule                 m clL clR
  -> RhineParallelAndSchedule m clL clR a b
++@ :: Rhine m clL a b
-> Schedule m clL clR -> RhineParallelAndSchedule m clL clR a b
(++@) = Rhine m clL a b
-> Schedule m clL clR -> RhineParallelAndSchedule m clL clR a b
forall (m :: Type -> Type) clL clR a b.
Rhine m clL a b
-> Schedule m clL clR -> RhineParallelAndSchedule m clL clR a b
RhineParallelAndSchedule

{- | The combinators for parallel composition allow for the following syntax:

@
rh1   :: Rhine    m                clL      a         b
rh1   =  ...

rh2   :: Rhine    m                    clR  a           c
rh2   =  ...

sched :: Schedule m                clL clR
sched =  ...

rh    :: Rhine    m (ParallelClock clL clR) a (Either b c)
rh    =  rh1 ++\@ sched \@++ rh2
@
-}
infix 3 @++
(@++)
  :: ( Monad m, Clock m clL, Clock m clR
     , Clock m (Out clL), Clock m (Out clR)
     , GetClockProxy clL, GetClockProxy clR
     , Time clL ~ Time (Out clL), Time clR ~ Time (Out clR)
     , Time clL ~ Time (In  clL), Time clR ~ Time (In  clR)
     , Time clL ~ Time clR
     )
       => RhineParallelAndSchedule m clL clR  a b
       -> Rhine                    m     clR  a c
       -> Rhine m (ParallelClock   m clL clR) a (Either b c)
RhineParallelAndSchedule (Rhine SN m clL a b
sn1 clL
clL) Schedule m clL clR
schedule @++ :: RhineParallelAndSchedule m clL clR a b
-> Rhine m clR a c
-> Rhine m (ParallelClock m clL clR) a (Either b c)
@++ (Rhine SN m clR a c
sn2 clR
clR)
  = SN m (ParallelClock m clL clR) a (Either b c)
-> ParallelClock m clL clR
-> Rhine m (ParallelClock m clL clR) a (Either b c)
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (SN m clL a b
sn1 SN m clL a b
-> SN m clR a c -> SN m (ParallelClock m clL clR) a (Either b c)
forall (m :: Type -> Type) clL clR a b c.
(Monad m, Clock m clL, Clock m clR, Clock m (Out clL),
 Clock m (Out clR), GetClockProxy clL, GetClockProxy clR,
 Time clL ~ Time clR, Time clL ~ Time (Out clL),
 Time clL ~ Time (In clL), Time clR ~ Time (Out clR),
 Time clR ~ Time (In clR)) =>
SN m clL a b
-> SN m clR a c -> SN m (ParClock m clL clR) a (Either b c)
++++ SN m clR a c
sn2) (clL -> clR -> Schedule m clL clR -> ParallelClock m clL clR
forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
cl1 -> cl2 -> Schedule m cl1 cl2 -> ParallelClock m cl1 cl2
ParallelClock clL
clL clR
clR Schedule m clL clR
schedule)

-- | Further syntactic sugar for 'RhineParallelAndSchedule'.
infix 4 ||@
(||@)
  :: Rhine                    m clL     a b
  -> Schedule                 m clL clR
  -> RhineParallelAndSchedule m clL clR a b
||@ :: Rhine m clL a b
-> Schedule m clL clR -> RhineParallelAndSchedule m clL clR a b
(||@) = Rhine m clL a b
-> Schedule m clL clR -> RhineParallelAndSchedule m clL clR a b
forall (m :: Type -> Type) clL clR a b.
Rhine m clL a b
-> Schedule m clL clR -> RhineParallelAndSchedule m clL clR a b
RhineParallelAndSchedule

{- | The combinators for parallel composition allow for the following syntax:

@
rh1   :: Rhine    m                clL      a b
rh1   =  ...

rh2   :: Rhine    m                    clR  a b
rh2   =  ...

sched :: Schedule m                clL clR
sched =  ...

rh    :: Rhine    m (ParallelClock clL clR) a b
rh    =  rh1 ||\@ sched \@|| rh2
@
-}
infix 3 @||
(@||)
  :: ( Monad m, Clock m clL, Clock m clR
     , Clock m (Out clL), Clock m (Out clR)
     , GetClockProxy clL, GetClockProxy clR
     , Time clL ~ Time (Out clL), Time clR ~ Time (Out clR)
     , Time clL ~ Time (In  clL), Time clR ~ Time (In  clR)
     , Time clL ~ Time clR
     )
       => RhineParallelAndSchedule m clL clR  a b
       -> Rhine                    m     clR  a b
       -> Rhine m (ParallelClock   m clL clR) a b
RhineParallelAndSchedule (Rhine SN m clL a b
sn1 clL
clL) Schedule m clL clR
schedule @|| :: RhineParallelAndSchedule m clL clR a b
-> Rhine m clR a b -> Rhine m (ParallelClock m clL clR) a b
@|| (Rhine SN m clR a b
sn2 clR
clR)
  = SN m (ParallelClock m clL clR) a b
-> ParallelClock m clL clR -> Rhine m (ParallelClock m clL clR) a b
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (SN m clL a b
sn1 SN m clL a b -> SN m clR a b -> SN m (ParallelClock m clL clR) a b
forall (m :: Type -> Type) clL clR a b.
(Monad m, Clock m clL, Clock m clR, Clock m (Out clL),
 Clock m (Out clR), GetClockProxy clL, GetClockProxy clR,
 Time clL ~ Time clR, Time clL ~ Time (Out clL),
 Time clL ~ Time (In clL), Time clR ~ Time (Out clR),
 Time clR ~ Time (In clR)) =>
SN m clL a b -> SN m clR a b -> SN m (ParClock m clL clR) a b
|||| SN m clR a b
sn2) (clL -> clR -> Schedule m clL clR -> ParallelClock m clL clR
forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
cl1 -> cl2 -> Schedule m cl1 cl2 -> ParallelClock m cl1 cl2
ParallelClock clL
clL clR
clR Schedule m clL clR
schedule)


-- | Postcompose a 'Rhine' with a pure function.
(@>>^)
  :: Monad m
  => Rhine m cl a b
  ->             (b -> c)
  -> Rhine m cl a      c
Rhine SN m cl a b
sn cl
cl @>>^ :: Rhine m cl a b -> (b -> c) -> Rhine m cl a c
@>>^ b -> c
f = SN m cl a c -> cl -> Rhine m cl a c
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (SN m cl a b
sn SN m cl a b -> (b -> c) -> SN m cl a c
forall (m :: Type -> Type) cl a b c.
Monad m =>
SN m cl a b -> (b -> c) -> SN m cl a c
>>>^ b -> c
f) cl
cl

-- | Precompose a 'Rhine' with a pure function.
(^>>@)
  :: Monad m
  =>           (a -> b)
  -> Rhine m cl      b c
  -> Rhine m cl a      c
a -> b
f ^>>@ :: (a -> b) -> Rhine m cl b c -> Rhine m cl a c
^>>@ Rhine SN m cl b c
sn cl
cl = SN m cl a c -> cl -> Rhine m cl a c
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (a -> b
f (a -> b) -> SN m cl b c -> SN m cl a c
forall (m :: Type -> Type) a b cl c.
Monad m =>
(a -> b) -> SN m cl b c -> SN m cl a c
^>>> SN m cl b c
sn) cl
cl

-- | Postcompose a 'Rhine' with a 'ClSF'.
(@>-^)
  :: ( Clock m (Out cl)
     , Time cl ~ Time (Out cl)
     )
  => Rhine m      cl  a b
  -> ClSF  m (Out cl)   b c
  -> Rhine m      cl  a   c
Rhine SN m cl a b
sn cl
cl @>-^ :: Rhine m cl a b -> ClSF m (Out cl) b c -> Rhine m cl a c
@>-^ ClSF m (Out cl) b c
clsf = SN m cl a c -> cl -> Rhine m cl a c
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (SN m cl a b
sn SN m cl a b -> ClSF m (Out cl) b c -> SN m cl a c
forall (m :: Type -> Type) cl a b c.
(Clock m (Out cl), Time cl ~ Time (Out cl)) =>
SN m cl a b -> ClSF m (Out cl) b c -> SN m cl a c
>--^ ClSF m (Out cl) b c
clsf) cl
cl

-- | Precompose a 'Rhine' with a 'ClSF'.
(^->@)
  :: ( Clock m (In cl)
     , Time cl ~ Time (In cl)
     )
  => ClSF  m (In cl) a b
  -> Rhine m     cl    b c
  -> Rhine m     cl  a   c
ClSF m (In cl) a b
clsf ^->@ :: ClSF m (In cl) a b -> Rhine m cl b c -> Rhine m cl a c
^->@ Rhine SN m cl b c
sn cl
cl = SN m cl a c -> cl -> Rhine m cl a c
forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (ClSF m (In cl) a b
clsf ClSF m (In cl) a b -> SN m cl b c -> SN m cl a c
forall (m :: Type -> Type) cl a b c.
(Clock m (In cl), Time cl ~ Time (In cl)) =>
ClSF m (In cl) a b -> SN m cl b c -> SN m cl a c
^--> SN m cl b c
sn) cl
cl