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

{- |
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.
-}
module FRP.Rhine.Reactimation.Combinators where

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

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

infix 5 @@

{- FOURMOLU_DISABLE -}
{- | 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
@@ :: forall cl (m :: Type -> Type) a b.
(cl ~ In cl, cl ~ Out cl) =>
ClSF 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
-@- :: forall (m :: Type -> Type) 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) cl1 cl2 a b.
ResamplingBuffer m (Out cl1) (In cl2) a b
-> Schedule m cl1 cl2 -> ResamplingPoint m cl1 cl2 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
>-- :: forall (m :: Type -> Type) cl1 a b cl2 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) --> :: forall (m :: Type -> Type) cl1 cl2 a b c.
(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
--> (Rhine SN m cl2 b c
sn2 cl2
cl2)
 = forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (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) (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
++@ :: forall (m :: Type -> Type) clL a b clR.
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 @++ :: 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 (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)
@++ (Rhine SN m clR a c
sn2 clR
clR)
  = 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 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) (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
||@ :: forall (m :: Type -> Type) clL a b clR.
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 @|| :: 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 (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
@|| (Rhine SN m clR a b
sn2 clR
clR)
  = 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 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) (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 @>>^ :: forall (m :: Type -> Type) cl a b c.
Monad m =>
Rhine m cl a b -> (b -> c) -> Rhine m cl a c
@>>^ b -> c
f = 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 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 ^>>@ :: forall (m :: Type -> Type) a b cl c.
Monad m =>
(a -> b) -> Rhine m cl b c -> Rhine m cl a c
^>>@ Rhine SN m cl b c
sn cl
cl = forall (m :: Type -> Type) cl a b.
SN m cl a b -> cl -> Rhine m cl a b
Rhine (a -> b
f 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 @>-^ :: forall (m :: Type -> Type) cl a b c.
(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
@>-^ ClSF m (Out cl) b c
clsf = 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 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 ^->@ :: forall (m :: Type -> Type) cl a b c.
(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
^->@ Rhine SN m cl b c
sn cl
cl = 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 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
{- FOURMOLU_ENABLE -}