From 9db65a0c28570fb988ae861e57031d4bafb3782c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Manuel=20B=C3=A4renz?= <programming@manuelbaerenz.de>
Date: Tue, 14 Nov 2023 15:48:14 +0100
Subject: [PATCH] WIP erase one clock

---
 rhine/src/FRP/Rhine/SN/Free.hs | 52 ++++++++++++++++++++++++++++------
 1 file changed, 44 insertions(+), 8 deletions(-)

diff --git a/rhine/src/FRP/Rhine/SN/Free.hs b/rhine/src/FRP/Rhine/SN/Free.hs
index 7ff4cf73..79c2ebe9 100644
--- a/rhine/src/FRP/Rhine/SN/Free.hs
+++ b/rhine/src/FRP/Rhine/SN/Free.hs
@@ -41,6 +41,8 @@ import Control.Monad.Schedule.Class (MonadSchedule)
 import Data.MonadicStreamFunction.Async (concatS)
 import Control.Monad.Trans.MSF (performOnFirstSample)
 import Control.Category (Category)
+import Data.Type.Equality ((:~:) (Refl))
+import Data.Typeable (cast, Typeable)
 
 -- Don't export Absent
 data At cl a = Present !a | Absent
@@ -73,18 +75,29 @@ instance Monad (At cl) where
 
 -- FIXME rewrite with prisms?
 class HasClock cl cls where
-  inject :: Proxy cl -> TimeInfo cl -> Tick cls
-  project :: Proxy cl -> Tick cls -> Maybe (TimeInfo cl)
+  position :: Position cl cls
 
 instance HasClock cl (cl ': cls) where
-  inject _ = Here
-  project _ (Here ti) = Just ti
-  project _ _ = Nothing
+  position = PHere
 
 instance {-# OVERLAPPABLE #-} (HasClock cl cls) => HasClock cl (cl' ': cls) where
-  inject proxy ti = There $ inject proxy ti
-  project _ (Here _) = Nothing
-  project proxy (There tick) = project proxy tick
+  position = PThere position
+
+inject :: forall cl cls . HasClock cl cls => Proxy cl -> TimeInfo cl -> Tick cls
+inject _ = injectPosition (position @cl @cls)
+
+injectPosition :: Position cl cls -> TimeInfo cl -> Tick cls
+injectPosition PHere ti = Here ti
+injectPosition (PThere pointer) ti = There $ injectPosition pointer ti
+
+project :: forall cl cls . HasClock cl cls => Proxy cl -> Tick cls -> Maybe (TimeInfo cl)
+project _ = projectPosition $ position @cl @cls
+
+projectPosition :: Position cl cls -> Tick cls -> Maybe (TimeInfo cl)
+projectPosition PHere (Here ti) = Just ti
+projectPosition (PThere position) (There tick) = projectPosition position tick
+projectPosition _ _ = Nothing
+
 
 type family HasClocksOrdered clA clB (cls :: [Type]) :: Constraint where
   HasClocksOrdered clA clB (clA ': cls) = HasClock clB cls
@@ -206,6 +219,24 @@ eraseClockFreeSN FreeSN {getFreeSN} = runA getFreeSN eraseClockSNComponent
 -- FIXME interesting idea: Erase only some clocks, e.g. the first one of the stack.
 -- Then I need a concept between FreeSN and MSF.
 -- The advantage would be higher flexibility, and I could maye also use MonadSchedule to make the data parts concurrent
+-- FIXME I should use a TL snoc list for the reader ticks to avoid confusion?
+eraseOneClock :: FreeSN (ReaderT (Tick (cl ': cls')) m) (cl ': cls) a b -> FreeSN (ReaderT (Tick (cl ': cls')) m) cls a b
+eraseOneClock = _
+-- FIXME who knows whether cls' will have the same order as cls? I should maybe write a TL prefix thingy
+eraseOneClockComponent :: (HasClock cl cls', Monad m) => SNComponent (ReaderT (Tick cls') m) (cl ': cls) a b -> SNComponent (ReaderT (Tick cls') m) cls a b
+eraseOneClockComponent component@(Synchronous clsf) = case positionClSF clsf component of
+  PHere -> Always $ readerS $ proc (tick, a) -> do
+    case (project (proxyFromClSF clsf) tick, a) of
+      (Nothing, _) -> returnA -< Absent
+      (Just ti, Present a) -> do
+        b <- runReaderS $ runReaderS clsf -< (tick, (ti, a))
+        returnA -< Present b
+      _ -> error "eraseClockSNComponent: Internal error (Synchronous)" -< ()
+  PThere _ -> Synchronous clsf -- FIXME I should probably put the position in the SN component and only require the type class when calling synchronous
+ where
+  positionClSF :: HasClock cl cls => ClSF m cl a b -> SNComponent m cls c d -> Position cl cls
+  positionClSF _ _ = position
+
 
 type family Map (f :: Type -> Type) (ts :: [Type]) :: [Type] where
   Map f '[] = '[]
@@ -218,6 +249,7 @@ data HTuple cls where
 data ClassyClock m td cl where
   ClassyClock :: (Clock m cl, Time cl ~ td) => cl -> ClassyClock m td cl
 
+-- FIXME I could also have a Nil constructor, an SN with no clocks is simply an MSF
 -- FIXME maybe put Clock constraints and time domain here?
 data Clocks m td cls where
   UnitClock :: (GetClockProxy cl, Clock m cl, Time cl ~ td) => cl -> Clocks m td '[cl]
@@ -226,6 +258,10 @@ data Clocks m td cls where
 -- FIXME This is
 -- newtype Clocks m td cls = Clocks {getClocks :: HTuple (Map (ClassyClock m td) cls)}
 
+data Position cl cls where
+  PHere :: Position cl (cl ': cls)
+  PThere :: Position cl cls -> Position cl (cl' ': cls)
+
 data Tags cls where
   TagHere :: Tag cl -> Tags (cl ': cls)
   TagThere :: Tags cls -> Tags (cl ': cls)