{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}

{- |
'Schedule's are the compatibility mechanism between two different clocks.
A schedule' implements the the universal clocks such that those two given clocks
are its subclocks.

This module defines the 'Schedule' type and certain general constructions of schedules,
such as lifting along monad morphisms or time domain morphisms.
It also supplies (sequential and parallel) compositions of clocks.

Specific implementations of schedules are found in submodules.
-}
module FRP.Rhine.Schedule where

-- transformers
import Control.Monad.Trans.Reader

-- dunai
import Data.MonadicStreamFunction

-- rhine
import FRP.Rhine.Clock
import FRP.Rhine.Schedule.Util

-- * The schedule type

{- | A schedule implements a combination of two clocks.
   It outputs a time stamp and an 'Either' value,
   which specifies which of the two subclocks has ticked.
-}
data Schedule m cl1 cl2 = (Time cl1 ~ Time cl2) =>
  Schedule
  { forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule ::
      cl1 ->
      cl2 ->
      RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
  }

-- The type constraint in the constructor is actually useful when pattern matching on 'Schedule',
-- which is interesting since a constraint like 'Monad m' is useful.
-- When reformulating as a GADT, it might get used,
-- but that would mean that we can't use record syntax.

-- * Utilities to create new schedules from existing ones

-- | Lift a schedule along a monad morphism.
hoistSchedule ::
  (Monad m1, Monad m2) =>
  (forall a. m1 a -> m2 a) ->
  Schedule m1 cl1 cl2 ->
  Schedule m2 cl1 cl2
hoistSchedule :: forall (m1 :: Type -> Type) (m2 :: Type -> Type) cl1 cl2.
(Monad m1, Monad m2) =>
(forall a. m1 a -> m2 a)
-> Schedule m1 cl1 cl2 -> Schedule m2 cl1 cl2
hoistSchedule forall a. m1 a -> m2 a
hoist Schedule {cl1
-> cl2
-> RunningClockInit m1 (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m1 (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..} = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule cl1
-> cl2
-> m2 (MSF m2 () (Time cl2, Either (Tag cl1) (Tag cl2)), Time cl2)
initSchedule'
  where
    initSchedule' :: cl1
-> cl2
-> m2 (MSF m2 () (Time cl2, Either (Tag cl1) (Tag cl2)), Time cl2)
initSchedule' cl1
cl1 cl2
cl2 =
      forall a. m1 a -> m2 a
hoist forall a b. (a -> b) -> a -> b
$
        forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall {a} {b}.
(forall a. m1 a -> m2 a) -> MSF m1 a b -> MSF m2 a b
hoistMSF forall a. m1 a -> m2 a
hoist) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> cl1
-> cl2
-> RunningClockInit m1 (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule cl1
cl1 cl2
cl2
    -- TODO This should be a dunai issue
    hoistMSF :: (forall a. m1 a -> m2 a) -> MSF m1 a b -> MSF m2 a b
hoistMSF = forall (m2 :: Type -> Type) (m1 :: Type -> Type) a b.
(Monad m2, Monad m1) =>
(forall c. m1 c -> m2 c) -> MSF m1 a b -> MSF m2 a b
morphS

-- | Swaps the clocks for a given schedule.
flipSchedule ::
  Monad m =>
  Schedule m cl1 cl2 ->
  Schedule m cl2 cl1
flipSchedule :: forall (m :: Type -> Type) cl1 cl2.
Monad m =>
Schedule m cl1 cl2 -> Schedule m cl2 cl1
flipSchedule Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..} = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule cl2
-> cl1
-> m (MSF m () (Time cl2, Either (Tag cl2) (Tag cl1)), Time cl2)
initSchedule_
  where
    initSchedule_ :: cl2
-> cl1
-> m (MSF m () (Time cl2, Either (Tag cl2) (Tag cl1)), Time cl2)
initSchedule_ cl2
cl2 cl1
cl1 = forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr (forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. Either a b -> Either b a
swapEither) forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
<<<) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule cl1
cl1 cl2
cl2

-- TODO I originally wanted to rescale a schedule and its clocks at the same time.
-- That's rescaleSequentialClock.

{- | If a schedule works for two clocks, a rescaling of the clocks
   also applies to the schedule.
-}
rescaledSchedule ::
  Monad m =>
  Schedule m cl1 cl2 ->
  Schedule m (RescaledClock cl1 time) (RescaledClock cl2 time)
rescaledSchedule :: forall (m :: Type -> Type) cl1 cl2 time.
Monad m =>
Schedule m cl1 cl2
-> Schedule m (RescaledClock cl1 time) (RescaledClock cl2 time)
rescaledSchedule Schedule m cl1 cl2
schedule = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule RescaledClock cl1 time
-> RescaledClock cl2 time
-> RunningClockInit
     m
     (Time (RescaledClockS m cl1 time (Tag cl1)))
     (Either
        (Tag (RescaledClockS m cl1 time (Tag cl1)))
        (Tag (RescaledClockS m cl2 time (Tag cl2))))
initSchedule'
  where
    initSchedule' :: RescaledClock cl1 time
-> RescaledClock cl2 time
-> RunningClockInit
     m
     (Time (RescaledClockS m cl1 time (Tag cl1)))
     (Either
        (Tag (RescaledClockS m cl1 time (Tag cl1)))
        (Tag (RescaledClockS m cl2 time (Tag cl2))))
initSchedule' RescaledClock cl1 time
cl1 RescaledClock cl2 time
cl2 = forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule (forall (m :: Type -> Type) cl1 cl2 time tag1 tag2.
Monad m =>
Schedule m cl1 cl2
-> Schedule
     m (RescaledClockS m cl1 time tag1) (RescaledClockS m cl2 time tag2)
rescaledScheduleS Schedule m cl1 cl2
schedule) (forall (m :: Type -> Type) cl time.
Monad m =>
RescaledClock cl time -> RescaledClockS m cl time (Tag cl)
rescaledClockToS RescaledClock cl1 time
cl1) (forall (m :: Type -> Type) cl time.
Monad m =>
RescaledClock cl time -> RescaledClockS m cl time (Tag cl)
rescaledClockToS RescaledClock cl2 time
cl2)

-- | As 'rescaledSchedule', with a stateful rescaling
rescaledScheduleS ::
  Monad m =>
  Schedule m cl1 cl2 ->
  Schedule m (RescaledClockS m cl1 time tag1) (RescaledClockS m cl2 time tag2)
rescaledScheduleS :: forall (m :: Type -> Type) cl1 cl2 time tag1 tag2.
Monad m =>
Schedule m cl1 cl2
-> Schedule
     m (RescaledClockS m cl1 time tag1) (RescaledClockS m cl2 time tag2)
rescaledScheduleS Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..} = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule RescaledClockS m cl1 time tag1
-> RescaledClockS m cl2 time tag2
-> m (MSF m () (time, Either tag1 tag2), time)
initSchedule'
  where
    initSchedule' :: RescaledClockS m cl1 time tag1
-> RescaledClockS m cl2 time tag2
-> m (MSF m () (time, Either tag1 tag2), time)
initSchedule' (RescaledClockS cl1
cl1 RescalingSInit m cl1 time tag1
rescaleS1) (RescaledClockS cl2
cl2 RescalingSInit m cl2 time tag2
rescaleS2) = do
      (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningSchedule, Time cl2
initTime) <- cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule cl1
cl1 cl2
cl2
      (MSF m (Time cl2, Tag cl1) (time, tag1)
rescaling1, time
initTime') <- RescalingSInit m cl1 time tag1
rescaleS1 Time cl2
initTime
      (MSF m (Time cl2, Tag cl2) (time, tag2)
rescaling2, time
_) <- RescalingSInit m cl2 time tag2
rescaleS2 Time cl2
initTime
      let runningSchedule' :: MSF m () (time, Either tag1 tag2)
runningSchedule' =
            MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningSchedule forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> proc (Time cl2
time, Either (Tag cl1) (Tag cl2)
tag12) -> case Either (Tag cl1) (Tag cl2)
tag12 of
              Left Tag cl1
tag1 -> do
                (time
time', tag1
tag1') <- MSF m (Time cl2, Tag cl1) (time, tag1)
rescaling1 -< (Time cl2
time, Tag cl1
tag1)
                forall (a :: Type -> Type -> Type) b. Arrow a => a b b
returnA -< (time
time', forall a b. a -> Either a b
Left tag1
tag1')
              Right Tag cl2
tag2 -> do
                (time
time', tag2
tag2') <- MSF m (Time cl2, Tag cl2) (time, tag2)
rescaling2 -< (Time cl2
time, Tag cl2
tag2)
                forall (a :: Type -> Type -> Type) b. Arrow a => a b b
returnA -< (time
time', forall a b. b -> Either a b
Right tag2
tag2')
      forall (m :: Type -> Type) a. Monad m => a -> m a
return (MSF m () (time, Either tag1 tag2)
runningSchedule', time
initTime')

-- TODO What's the most general way we can lift a schedule this way?

{- | Lifts a schedule into the 'ReaderT' transformer,
   supplying the same environment to its scheduled clocks.
-}
readerSchedule ::
  ( Monad m
  , Clock (ReaderT r m) cl1
  , Clock (ReaderT r m) cl2
  , Time cl1 ~ Time cl2
  ) =>
  Schedule
    m
    (HoistClock (ReaderT r m) m cl1)
    (HoistClock (ReaderT r m) m cl2) ->
  Schedule (ReaderT r m) cl1 cl2
readerSchedule :: forall (m :: Type -> Type) r cl1 cl2.
(Monad m, Clock (ReaderT r m) cl1, Clock (ReaderT r m) cl2,
 Time cl1 ~ Time cl2) =>
Schedule
  m (HoistClock (ReaderT r m) m cl1) (HoistClock (ReaderT r m) m cl2)
-> Schedule (ReaderT r m) cl1 cl2
readerSchedule Schedule {HoistClock (ReaderT r m) m cl1
-> HoistClock (ReaderT r m) m cl2
-> RunningClockInit
     m
     (Time (HoistClock (ReaderT r m) m cl1))
     (Either
        (Tag (HoistClock (ReaderT r m) m cl1))
        (Tag (HoistClock (ReaderT r m) m cl2)))
initSchedule :: HoistClock (ReaderT r m) m cl1
-> HoistClock (ReaderT r m) m cl2
-> RunningClockInit
     m
     (Time (HoistClock (ReaderT r m) m cl1))
     (Either
        (Tag (HoistClock (ReaderT r m) m cl1))
        (Tag (HoistClock (ReaderT r m) m cl2)))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..} =
  forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule forall a b. (a -> b) -> a -> b
$ \cl1
cl1 cl2
cl2 -> forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \r
r ->
    forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a
       b.
(MonadTrans t, Monad m, Monad (t m)) =>
MSF m a b -> MSF (t m) a b
liftTransS
      forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> HoistClock (ReaderT r m) m cl1
-> HoistClock (ReaderT r m) m cl2
-> RunningClockInit
     m
     (Time (HoistClock (ReaderT r m) m cl1))
     (Either
        (Tag (HoistClock (ReaderT r m) m cl1))
        (Tag (HoistClock (ReaderT r m) m cl2)))
initSchedule
        (forall (m1 :: Type -> Type) (m2 :: Type -> Type) cl.
cl -> (forall a. m1 a -> m2 a) -> HoistClock m1 m2 cl
HoistClock cl1
cl1 forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT r
r)
        (forall (m1 :: Type -> Type) (m2 :: Type -> Type) cl.
cl -> (forall a. m1 a -> m2 a) -> HoistClock m1 m2 cl
HoistClock cl2
cl2 forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT r
r)

-- * Composite clocks

-- ** Sequentially combined clocks

{- | Two clocks can be combined with a schedule as a clock
   for an asynchronous sequential composition of signal networks.
-}
data SequentialClock m cl1 cl2 = Time cl1 ~ Time cl2 =>
  SequentialClock
  { forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl1
sequentialCl1 :: cl1
  , forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl2
sequentialCl2 :: cl2
  , forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> Schedule m cl1 cl2
sequentialSchedule :: Schedule m cl1 cl2
  }

-- | Abbrevation synonym.
type SeqClock m cl1 cl2 = SequentialClock m cl1 cl2

instance
  (Monad m, Clock m cl1, Clock m cl2) =>
  Clock m (SequentialClock m cl1 cl2)
  where
  type Time (SequentialClock m cl1 cl2) = Time cl1
  type Tag (SequentialClock m cl1 cl2) = Either (Tag cl1) (Tag cl2)
  initClock :: SequentialClock m cl1 cl2
-> RunningClockInit
     m
     (Time (SequentialClock m cl1 cl2))
     (Tag (SequentialClock m cl1 cl2))
initClock SequentialClock {cl1
cl2
Schedule m cl1 cl2
sequentialSchedule :: Schedule m cl1 cl2
sequentialCl2 :: cl2
sequentialCl1 :: cl1
sequentialSchedule :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> Schedule m cl1 cl2
sequentialCl2 :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl2
sequentialCl1 :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl1
..} =
    forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule Schedule m cl1 cl2
sequentialSchedule cl1
sequentialCl1 cl2
sequentialCl2

{- | @cl1@ is a subclock of @SequentialClock m cl1 cl2@,
   therefore it is always possible to schedule these two clocks deterministically.
   The left subclock of the combined clock always ticks instantly after @cl1@.
-}
schedSeq1 :: (Monad m, Semigroup cl1) => Schedule m cl1 (SequentialClock m cl1 cl2)
schedSeq1 :: forall (m :: Type -> Type) cl1 cl2.
(Monad m, Semigroup cl1) =>
Schedule m cl1 (SequentialClock m cl1 cl2)
schedSeq1 = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule forall a b. (a -> b) -> a -> b
$ \cl1
cl1 SequentialClock {sequentialSchedule :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> Schedule m cl1 cl2
sequentialSchedule = Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..}, cl1
cl2
sequentialCl2 :: cl2
sequentialCl1 :: cl1
sequentialCl2 :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl2
sequentialCl1 :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl1
..} -> do
  (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime) <- cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule (cl1
cl1 forall a. Semigroup a => a -> a -> a
<> cl1
sequentialCl1) cl2
sequentialCl2
  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Type -> Type) time a b.
Monad m =>
MSF m () (time, Either a b)
-> MSF m () (time, Either a (Either a b))
duplicateSubtick MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime)

{- | As 'schedSeq1', but for the right subclock.
   The right subclock of the combined clock always ticks instantly before @cl2@.
-}
schedSeq2 :: (Monad m, Semigroup cl2, Time cl1 ~ Time cl2) => Schedule m (SequentialClock m cl1 cl2) cl2
schedSeq2 :: forall (m :: Type -> Type) cl2 cl1.
(Monad m, Semigroup cl2, Time cl1 ~ Time cl2) =>
Schedule m (SequentialClock m cl1 cl2) cl2
schedSeq2 = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule forall a b. (a -> b) -> a -> b
$ \SequentialClock {sequentialSchedule :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> Schedule m cl1 cl2
sequentialSchedule = Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..}, cl2
cl1
sequentialCl2 :: cl2
sequentialCl1 :: cl1
sequentialCl2 :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl2
sequentialCl1 :: forall (m :: Type -> Type) cl1 cl2.
SequentialClock m cl1 cl2 -> cl1
..} cl2
cl2 -> do
  (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime) <- cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule cl1
sequentialCl1 (cl2
sequentialCl2 forall a. Semigroup a => a -> a -> a
<> cl2
cl2)
  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Type -> Type) time a b.
Monad m =>
MSF m () (time, Either a b)
-> MSF m () (time, Either a (Either a b))
duplicateSubtick (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr forall a b. Either a b -> Either b a
swapEither)) forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr forall {b} {b} {a}. Either b (Either b a) -> Either (Either a b) b
remap), Time cl2
initTime)
  where
    remap :: Either b (Either b a) -> Either (Either a b) b
remap (Left b
tag2) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right b
tag2
    remap (Right (Left b
tag2)) = forall a b. b -> Either a b
Right b
tag2
    remap (Right (Right a
tag1)) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
tag1

-- TODO Why did I need the constraint on the time domains here, but not in schedSeq1?
--      Same for schedPar2

-- ** Parallelly combined clocks

{- | Two clocks can be combined with a schedule as a clock
   for an asynchronous parallel composition of signal networks.
-}
data ParallelClock m cl1 cl2 = Time cl1 ~ Time cl2 =>
  ParallelClock
  { forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl1
parallelCl1 :: cl1
  , forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl2
parallelCl2 :: cl2
  , forall (m :: Type -> Type) cl1 cl2.
ParallelClock m cl1 cl2 -> Schedule m cl1 cl2
parallelSchedule :: Schedule m cl1 cl2
  }

-- | Abbrevation synonym.
type ParClock m cl1 cl2 = ParallelClock m cl1 cl2

instance
  (Monad m, Clock m cl1, Clock m cl2) =>
  Clock m (ParallelClock m cl1 cl2)
  where
  type Time (ParallelClock m cl1 cl2) = Time cl1
  type Tag (ParallelClock m cl1 cl2) = Either (Tag cl1) (Tag cl2)
  initClock :: ParallelClock m cl1 cl2
-> RunningClockInit
     m (Time (ParallelClock m cl1 cl2)) (Tag (ParallelClock m cl1 cl2))
initClock ParallelClock {cl1
cl2
Schedule m cl1 cl2
parallelSchedule :: Schedule m cl1 cl2
parallelCl2 :: cl2
parallelCl1 :: cl1
parallelSchedule :: forall (m :: Type -> Type) cl1 cl2.
ParallelClock m cl1 cl2 -> Schedule m cl1 cl2
parallelCl2 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl2
parallelCl1 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl1
..} =
    forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule Schedule m cl1 cl2
parallelSchedule cl1
parallelCl1 cl2
parallelCl2

{- | Like 'schedSeq1', but for parallel clocks.
   The left subclock of the combined clock always ticks instantly after @cl1@.
-}
schedPar1 :: (Monad m, Semigroup cl1) => Schedule m cl1 (ParallelClock m cl1 cl2)
schedPar1 :: forall (m :: Type -> Type) cl1 cl2.
(Monad m, Semigroup cl1) =>
Schedule m cl1 (ParallelClock m cl1 cl2)
schedPar1 = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule forall a b. (a -> b) -> a -> b
$ \cl1
cl1 ParallelClock {parallelSchedule :: forall (m :: Type -> Type) cl1 cl2.
ParallelClock m cl1 cl2 -> Schedule m cl1 cl2
parallelSchedule = Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..}, cl1
cl2
parallelCl2 :: cl2
parallelCl1 :: cl1
parallelCl2 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl2
parallelCl1 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl1
..} -> do
  (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime) <- cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule (cl1
cl1 forall a. Semigroup a => a -> a -> a
<> cl1
parallelCl1) cl2
parallelCl2
  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Type -> Type) time a b.
Monad m =>
MSF m () (time, Either a b)
-> MSF m () (time, Either a (Either a b))
duplicateSubtick MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime)

{- | Like 'schedPar1',
   but the left subclock of the combined clock always ticks instantly /before/ @cl1@.
-}
schedPar1' :: (Monad m, Semigroup cl1) => Schedule m cl1 (ParallelClock m cl1 cl2)
schedPar1' :: forall (m :: Type -> Type) cl1 cl2.
(Monad m, Semigroup cl1) =>
Schedule m cl1 (ParallelClock m cl1 cl2)
schedPar1' = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule forall a b. (a -> b) -> a -> b
$ \cl1
cl1 ParallelClock {parallelSchedule :: forall (m :: Type -> Type) cl1 cl2.
ParallelClock m cl1 cl2 -> Schedule m cl1 cl2
parallelSchedule = Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..}, cl1
cl2
parallelCl2 :: cl2
parallelCl1 :: cl1
parallelCl2 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl2
parallelCl1 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl1
..} -> do
  (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime) <- cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule (cl1
parallelCl1 forall a. Semigroup a => a -> a -> a
<> cl1
cl1) cl2
parallelCl2
  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Type -> Type) time a b.
Monad m =>
MSF m () (time, Either a b)
-> MSF m () (time, Either a (Either a b))
duplicateSubtick MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr (forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall {a} {b}. Either a (Either a b) -> Either a (Either a b)
remap), Time cl2
initTime)
  where
    remap :: Either a (Either a b) -> Either a (Either a b)
remap (Left a
tag1) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
tag1
    remap (Right (Left a
tag1)) = forall a b. a -> Either a b
Left a
tag1
    remap Either a (Either a b)
tag = Either a (Either a b)
tag

{- | Like 'schedPar1', but for the right subclock.
   The right subclock of the combined clock always ticks instantly before @cl2@.
-}
schedPar2 :: (Monad m, Semigroup cl2, Time cl1 ~ Time cl2) => Schedule m (ParallelClock m cl1 cl2) cl2
schedPar2 :: forall (m :: Type -> Type) cl2 cl1.
(Monad m, Semigroup cl2, Time cl1 ~ Time cl2) =>
Schedule m (ParallelClock m cl1 cl2) cl2
schedPar2 = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule forall a b. (a -> b) -> a -> b
$ \ParallelClock {parallelSchedule :: forall (m :: Type -> Type) cl1 cl2.
ParallelClock m cl1 cl2 -> Schedule m cl1 cl2
parallelSchedule = Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..}, cl2
cl1
parallelCl2 :: cl2
parallelCl1 :: cl1
parallelCl2 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl2
parallelCl1 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl1
..} cl2
cl2 -> do
  (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime) <- cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule cl1
parallelCl1 (cl2
parallelCl2 forall a. Semigroup a => a -> a -> a
<> cl2
cl2)
  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Type -> Type) time a b.
Monad m =>
MSF m () (time, Either a b)
-> MSF m () (time, Either a (Either a b))
duplicateSubtick (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr forall a b. Either a b -> Either b a
swapEither)) forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr forall {b} {b} {a}. Either b (Either b a) -> Either (Either a b) b
remap), Time cl2
initTime)
  where
    remap :: Either b (Either b a) -> Either (Either a b) b
remap (Left b
tag2) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right b
tag2
    remap (Right (Left b
tag2)) = forall a b. b -> Either a b
Right b
tag2
    remap (Right (Right a
tag1)) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
tag1

{- | Like 'schedPar1',
   but the right subclock of the combined clock always ticks instantly /after/ @cl2@.
-}
schedPar2' :: (Monad m, Semigroup cl2, Time cl1 ~ Time cl2) => Schedule m (ParallelClock m cl1 cl2) cl2
schedPar2' :: forall (m :: Type -> Type) cl2 cl1.
(Monad m, Semigroup cl2, Time cl1 ~ Time cl2) =>
Schedule m (ParallelClock m cl1 cl2) cl2
schedPar2' = forall (m :: Type -> Type) cl1 cl2.
(Time cl1 ~ Time cl2) =>
(cl1
 -> cl2
 -> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2)))
-> Schedule m cl1 cl2
Schedule forall a b. (a -> b) -> a -> b
$ \ParallelClock {parallelSchedule :: forall (m :: Type -> Type) cl1 cl2.
ParallelClock m cl1 cl2 -> Schedule m cl1 cl2
parallelSchedule = Schedule {cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule :: forall (m :: Type -> Type) cl1 cl2.
Schedule m cl1 cl2
-> cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
..}, cl2
cl1
parallelCl2 :: cl2
parallelCl1 :: cl1
parallelCl2 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl2
parallelCl1 :: forall (m :: Type -> Type) cl1 cl2. ParallelClock m cl1 cl2 -> cl1
..} cl2
cl2 -> do
  (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock, Time cl2
initTime) <- cl1
-> cl2
-> RunningClockInit m (Time cl1) (Either (Tag cl1) (Tag cl2))
initSchedule cl1
parallelCl1 (cl2
parallelCl2 forall a. Semigroup a => a -> a -> a
<> cl2
cl2)
  forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Type -> Type) time a b.
Monad m =>
MSF m () (time, Either a b)
-> MSF m () (time, Either a (Either a b))
duplicateSubtick (MSF m () (Time cl2, Either (Tag cl1) (Tag cl2))
runningClock forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr forall a b. Either a b -> Either b a
swapEither)) forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr forall {b} {b} {a}. Either b (Either b a) -> Either (Either a b) b
remap), Time cl2
initTime)
  where
    remap :: Either b (Either b a) -> Either (Either a b) b
remap (Left b
tag2) = forall a b. b -> Either a b
Right b
tag2
    remap (Right (Left b
tag2)) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right b
tag2
    remap (Right (Right a
tag1)) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
tag1

-- * Navigating the clock tree

-- | The clock that represents the rate at which data enters the system.
type family In cl where
  In (SequentialClock m cl1 cl2) = In cl1
  In (ParallelClock m cl1 cl2) = ParallelClock m (In cl1) (In cl2)
  In cl = cl

-- | The clock that represents the rate at which data leaves the system.
type family Out cl where
  Out (SequentialClock m cl1 cl2) = Out cl2
  Out (ParallelClock m cl1 cl2) = ParallelClock m (Out cl1) (Out cl2)
  Out cl = cl

{- | A tree representing possible last times to which
   the constituents of a clock may have ticked.
-}
data LastTime cl where
  SequentialLastTime ::
    LastTime cl1 ->
    LastTime cl2 ->
    LastTime (SequentialClock m cl1 cl2)
  ParallelLastTime ::
    LastTime cl1 ->
    LastTime cl2 ->
    LastTime (ParallelClock m cl1 cl2)
  LeafLastTime :: Time cl -> LastTime cl

-- | An inclusion of a clock into a tree of parallel compositions of clocks.
data ParClockInclusion clS cl where
  ParClockInL ::
    ParClockInclusion (ParallelClock m clL clR) cl ->
    ParClockInclusion clL cl
  ParClockInR ::
    ParClockInclusion (ParallelClock m clL clR) cl ->
    ParClockInclusion clR cl
  ParClockRefl :: ParClockInclusion cl cl

{- | Generates a tag for the composite clock from a tag of a leaf clock,
   given a parallel clock inclusion.
-}
parClockTagInclusion :: ParClockInclusion clS cl -> Tag clS -> Tag cl
parClockTagInclusion :: forall clS cl. ParClockInclusion clS cl -> Tag clS -> Tag cl
parClockTagInclusion (ParClockInL ParClockInclusion (ParallelClock m clS clR) cl
parClockInL) Tag clS
tag = forall clS cl. ParClockInclusion clS cl -> Tag clS -> Tag cl
parClockTagInclusion ParClockInclusion (ParallelClock m clS clR) cl
parClockInL forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Tag clS
tag
parClockTagInclusion (ParClockInR ParClockInclusion (ParallelClock m clL clS) cl
parClockInR) Tag clS
tag = forall clS cl. ParClockInclusion clS cl -> Tag clS -> Tag cl
parClockTagInclusion ParClockInclusion (ParallelClock m clL clS) cl
parClockInR forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Tag clS
tag
parClockTagInclusion ParClockInclusion clS cl
ParClockRefl Tag clS
tag = Tag clS
tag