WIP typed-prototols update

hydra-node/src/Hydra/Network/Ouroboros/Type.hs

@@ -3,9 +3,11 @@ module Hydra.Network.Ouroboros.Type where
 import Hydra.Prelude
 
 import Cardano.Binary qualified as CBOR
+import Network.TypedProtocol.Codec
 import Codec.CBOR.Read qualified as CBOR
 import GHC.Show (Show (show))
 import Network.TypedProtocol.Core (ReflRelativeAgency (ReflClientAgency))
+import Network.TypedProtocol.Core 
 import Network.TypedProtocol (Protocol (..))
 import Network.TypedProtocol.Codec (Codec)
 import Network.TypedProtocol.Codec.CBOR (mkCodecCborLazyBS)
@@ -22,6 +24,17 @@ data FireForget msg where
   StIdle :: FireForget msg
   StDone :: FireForget msg
 
+data SFireForget (st :: FireForget msg) where
+  SingIdle :: SFireForget StIdle
+  SingDone :: SFireForget StDone
+
+deriving instance Show (SFireForget st)
+
+instance StateTokenI StIdle where
+    stateToken = SingIdle
+instance StateTokenI StDone where
+    stateToken = SingDone
+
 instance ShowProxy (FireForget msg) where
   showProxy _ = "FireForget"
 
@@ -35,35 +48,44 @@ instance Protocol (FireForget msg) where
     MsgSend :: msg -> Message (FireForget msg) 'StIdle 'StIdle
     MsgDone :: Message (FireForget msg) 'StIdle 'StDone
 
-  -- We have to explain to the framework what our states mean, in terms of
-  -- who is expected to send and receive in the different states.
-  --
-  -- Idle states are where it is for the client to send a message.
-  data ClientHasAgency st where
-    TokIdle :: ClientHasAgency 'StIdle
-
-  -- In our protocol the server is always receiving, thus in no state the server
-  -- has agency.
-  data ServerHasAgency st
-
-  -- In the done state neither client nor server can send messages.
-  data NobodyHasAgency st where
-    TokDone :: NobodyHasAgency 'StDone
+  type StateAgency StIdle = ClientAgency
+  type StateAgency StDone = NobodyAgency
 
-  exclusionLemma_ClientAndServerHaveAgency TokIdle tok = case tok of {}
-  exclusionLemma_NobodyAndClientHaveAgency TokDone tok = case tok of {}
-  exclusionLemma_NobodyAndServerHaveAgency TokDone tok = case tok of {}
+  type StateToken = SFireForget
 
 deriving stock instance Show msg => Show (Message (FireForget msg) from to)
 
 deriving stock instance Eq msg => Eq (Message (FireForget msg) from to)
 
-instance Show (ClientHasAgency (st :: FireForget msg)) where
-  show TokIdle = "TokIdle"
+codecFireForget
+  :: forall m msg. Monad m
+  => Codec (FireForget msg) CodecFailure m String
+codecFireForget = undefined
+{--
+    Codec{encode, decode}
+  where
+    encode :: forall (st :: FireForget msg) (st' :: FireForget msg).
+              Message (FireForget msg) st st'
+           -> String
+    encode MsgSend = "ping\n"
+    encode MsgDone = "done\n"
 
-instance Show (ServerHasAgency (st :: FireForget msg)) where
-  show _ = error "absurd"
+    decode :: forall (st :: FireForget msg).
+              ActiveState st
+           => StateToken st
+           -> m (DecodeStep String CodecFailure m (SomeMessage st))
+    decode stok =
+      decodeTerminatedFrame '\n' $ \str trailing ->
+        case (stok, str) of
+          (SingIdle, "idle") ->
+            DecodeDone (SomeMessage MsgPong) trailing
+          (SingDone, "done") ->
+            DecodeDone (SomeMessage MsgDone) trailing
 
+          (_       , _     ) -> DecodeFail failure
+            where failure = CodecFailure ("unexpected server message: " ++ str)
+--}
+{--
 codecFireForget ::
   forall a m.
   ( MonadST m
@@ -94,3 +116,4 @@ codecFireForget = mkCodecCborLazyBS encodeMsg decodeMsg
         SomeMessage . MsgSend <$> fromCBOR
       (ReflClientAgency TokIdle, _) ->
         fail "codecFireForget.StIdle: unexpected key"
+--}