Updated against type-protocols changes

cabal.project

@@ -1,4 +1,4 @@
-index-state: 2021-10-01T00:00:00Z
+index-state: 2022-02-18T00:00:00Z
 
 packages:
     ./*.cabal
@@ -30,10 +30,28 @@ package ouroboros-network
 source-repository-package
   type: git
   location: https://github.com/input-output-hk/cardano-prelude
-  tag: ee4e7b547a991876e6b05ba542f4e62909f4a571
-  --sha256: 0dg6ihgrn5mgqp95c4f11l6kh9k3y75lwfqf47hdp554w7wyvaw6
+  tag: bb4ed71ba8e587f672d06edf9d2e376f4b055555
+  --sha256: 00h10l5mmiza9819p9v5q5749nb9pzgi20vpzpy1d34zmh6gf1cj
   subdir:
     cardano-prelude
+    cardano-prelude-test
+
+source-repository-package
+  type: git
+  location: https://github.com/input-output-hk/cardano-base
+  tag: 631cb6cf1fa01ab346233b610a38b3b4cba6e6ab
+  --sha256: 0944wg2nqazmhlmsynwgdwxxj6ay0hb9qig9l128isb2cjia0hlp
+  subdir:
+    base-deriving-via
+    binary
+    binary/test
+    cardano-crypto-class
+    cardano-crypto-praos
+    cardano-crypto-tests
+    measures
+    orphans-deriving-via
+    slotting
+    strict-containers
 
 source-repository-package
   type: git
@@ -51,16 +69,35 @@ source-repository-package
 
 source-repository-package
   type: git
-  location: https://github.com/input-output-hk/ouroboros-network
-  tag: 94782e5ca52f234ff8eeddc6322a46cca0b69c0e
-  --sha256: 1da3pka4pn6sjf6w19d957aryjc9ip1a3g0vz7jz66pjri3v2n0j
+  location: https://github.com/input-output-hk/io-sim
+  tag: 606de33fa2f467d108fb1efb86daeb3348bf34e3
+  --sha256: 048djqfdkzrbmdz670knbkjy12wddpvsmhm4x5yldg3w9lwqi1yx
   subdir:
-    io-sim
     io-classes
+    io-sim
+    strict-stm
+
+source-repository-package
+  type: git
+  location: https://github.com/input-output-hk/typed-protocols
+  tag: 932ff9676b57c34b188af44aa47a3ca3afbc72d9
+  --sha256: 0hnlx7ar2y9wki5qaj5pscdysqzg8pxwxfhgc2w0i7if6ly464m6
+  subdir:
+    typed-protocols
+    typed-protocols-cborg
+    typed-protocols-stateful
+    typed-protocols-stateful-cborg
+    typed-protocols-examples
+
+source-repository-package
+  type: git
+  location: https://github.com/input-output-hk/ouroboros-network
+  tag: 5dc41d7f3f138e45cae9eb5a8c2be5c2da539291
+  --sha256: 14kmaflaqjrb4101gs8kvgkazzc5cna5zmz2kygqr1g1dwmbf34b
+  -- pull only the packages which are necessary
+  subdir:
     monoidal-synchronisation
     network-mux
+    ouroboros-network
     ouroboros-network-framework
     ouroboros-network-testing
-    typed-protocols
-    typed-protocols-cborg
-    typed-protocols-examples

ekg-forward.cabal

@@ -65,6 +65,7 @@ library
                        , io-classes
                        , network
                        , ouroboros-network-framework
+                       , singletons >= 3.0.0
                        , serialise
                        , stm
                        , text

src/System/Metrics/Protocol/Acceptor.hs

@@ -12,8 +12,8 @@ module System.Metrics.Protocol.Acceptor (
   , ekgAcceptorPeer
   ) where
 
-import           Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..),
-                                             PeerRole (..))
+import           Network.TypedProtocol.Core
+import           Network.TypedProtocol.Peer.Client
 
 import           System.Metrics.Protocol.Type
 
@@ -36,14 +36,14 @@ data EKGAcceptor req resp m a where
 ekgAcceptorPeer
   :: Monad m
   => EKGAcceptor req resp m a
-  -> Peer (EKGForward req resp) 'AsClient 'StIdle m a
+  -> Client (EKGForward req resp) 'NonPipelined 'Empty 'StIdle m stm a
 ekgAcceptorPeer = \case
   SendMsgReq req next ->
     -- Send our message (request for the new metrics from the forwarder).
-    Yield (ClientAgency TokIdle) (MsgReq req) $
+    Yield (MsgReq req) $
       -- We're now into the 'StBusy' state, and now we'll wait for a reply
       -- from the forwarder.
-      Await (ServerAgency TokBusy) $ \(MsgResp resp) ->
+      Await $ \(MsgResp resp) ->
         Effect $
           ekgAcceptorPeer <$> next resp
 
@@ -53,4 +53,4 @@ ekgAcceptorPeer = \case
       -- 'done', with a return value.
       Effect $ do
         r <- getResult
-        return $ Yield (ClientAgency TokIdle) MsgDone (Done TokDone r)
+        return $ Yield MsgDone (Done r)

src/System/Metrics/Protocol/Codec.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -13,10 +14,11 @@ import qualified Codec.CBOR.Encoding as CBOR
 import           Codec.CBOR.Read (DeserialiseFailure)
 import           Control.Monad.Class.MonadST (MonadST)
 import qualified Data.ByteString.Lazy as LBS
+import           Data.Singletons
 import           Text.Printf (printf)
-import           Network.TypedProtocol.Codec.CBOR (Codec, PeerHasAgency (..),
-                                                   PeerRole (..), SomeMessage (..),
-                                                   mkCodecCborLazyBS)
+import           Network.TypedProtocol.Core
+import           Network.TypedProtocol.Codec (Codec, SomeMessage (..))
+import           Network.TypedProtocol.Codec.CBOR (mkCodecCborLazyBS)
 
 import           System.Metrics.Protocol.Type
 
@@ -34,47 +36,46 @@ codecEKGForward encodeReq  decodeReq
   mkCodecCborLazyBS encode decode
  where
   -- Encode messages.
-  encode :: forall (pr  :: PeerRole)
-                   (st  :: EKGForward req resp)
+  encode :: forall (st  :: EKGForward req resp)
                    (st' :: EKGForward req resp).
-            PeerHasAgency pr st
-         -> Message (EKGForward req resp) st st'
+            Message (EKGForward req resp) st st'
          -> CBOR.Encoding
 
-  encode (ClientAgency TokIdle) (MsgReq req) =
+  encode (MsgReq req) =
     CBOR.encodeListLen 2
       <> CBOR.encodeWord 0
       <> encodeReq req
 
-  encode (ClientAgency TokIdle) MsgDone =
+  encode MsgDone =
     CBOR.encodeListLen 1
       <> CBOR.encodeWord 1
 
-  encode (ServerAgency TokBusy) (MsgResp resp) =
+  encode (MsgResp resp) =
     CBOR.encodeListLen 2
       <> CBOR.encodeWord 1
       <> encodeResp resp
 
   -- Decode messages
-  decode :: forall (pr :: PeerRole)
-                   (st :: EKGForward req resp) s.
-            PeerHasAgency pr st
+  decode :: forall (st :: EKGForward req resp) s.
+            ActiveState st
+         => Sing st
          -> CBOR.Decoder s (SomeMessage st)
   decode stok = do
     len <- CBOR.decodeListLen
     key <- CBOR.decodeWord
     case (key, len, stok) of
-      (0, 2, ClientAgency TokIdle) ->
+      (0, 2, SingIdle) ->
         SomeMessage . MsgReq <$> decodeReq
 
-      (1, 1, ClientAgency TokIdle) ->
+      (1, 1, SingIdle) ->
         return $ SomeMessage MsgDone
 
-      (1, 2, ServerAgency TokBusy) ->
+      (1, 2, SingBusy) ->
         SomeMessage . MsgResp <$> decodeResp
 
       -- Failures per protocol state
-      (_, _, ClientAgency TokIdle) ->
+      (_, _, SingIdle) ->
         fail (printf "codecEKGForward (%s) unexpected key (%d, %d)" (show stok) key len)
-      (_, _, ServerAgency TokBusy) ->
+      (_, _, SingBusy) ->
         fail (printf "codecEKGForward (%s) unexpected key (%d, %d)" (show stok) key len)
+      (_, _, SingDone) -> notActiveState stok

src/System/Metrics/Protocol/Forwarder.hs

@@ -8,8 +8,8 @@ module System.Metrics.Protocol.Forwarder (
   , ekgForwarderPeer
   ) where
 
-import           Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..),
-                                             PeerRole (..))
+import           Network.TypedProtocol.Core
+import           Network.TypedProtocol.Peer.Server
 
 import           System.Metrics.Protocol.Type
 
@@ -34,18 +34,18 @@ data EKGForwarder req resp m a = EKGForwarder {
 ekgForwarderPeer
   :: Monad m
   => EKGForwarder req resp m a
-  -> Peer (EKGForward req resp) 'AsServer 'StIdle m a
+  -> Server (EKGForward req resp) 'NonPipelined 'Empty 'StIdle m stm a
 ekgForwarderPeer EKGForwarder{..} =
   -- In the 'StIdle' state the forwarder is awaiting a request message
   -- from the acceptor.
-  Await (ClientAgency TokIdle) $ \case
+  Await $ \case
     -- The acceptor sent us a request for new metrics, so now we're
     -- in the 'StBusy' state which means it's the forwarder's turn to send
     -- a reply.
     MsgReq req -> Effect $ do
       (resp, next) <- recvMsgReq req
-      return $ Yield (ServerAgency TokBusy) (MsgResp resp) (ekgForwarderPeer next)
+      return $ Yield (MsgResp resp) (ekgForwarderPeer next)
 
     -- The acceptor sent the done transition, so we're in the 'StDone' state
     -- so all we can do is stop using 'done', with a return value.
-    MsgDone -> Effect $ Done TokDone <$> recvMsgDone
+    MsgDone -> Effect $ Done <$> recvMsgDone

src/System/Metrics/Protocol/Type.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 
 -- | The type of the EKG forwarding/accepting protocol.
@@ -13,14 +14,12 @@
 
 module System.Metrics.Protocol.Type
   ( EKGForward (..)
+  , SingEKGForward (..)
   , Message (..)
-  , ClientHasAgency (..)
-  , ServerHasAgency (..)
-  , NobodyHasAgency (..)
   ) where
 
-import           Data.Proxy (Proxy(..))
-import           Network.TypedProtocol.Core (Protocol (..))
+import           Data.Singletons
+import           Network.TypedProtocol.Core
 import           Ouroboros.Network.Util.ShowProxy (ShowProxy(..))
 
 -- | A kind to identify our protocol, and the types of the states in the state
@@ -69,6 +68,17 @@ instance (ShowProxy req, ShowProxy resp)
     , ")"
     ]
 
+data SingEKGForward (st :: EKGForward req resp) where
+  SingIdle :: SingEKGForward 'StIdle
+  SingBusy :: SingEKGForward 'StBusy
+  SingDone :: SingEKGForward 'StDone
+
+deriving instance Show (SingEKGForward st)
+type instance Sing = SingEKGForward
+instance SingI 'StIdle where sing = SingIdle
+instance SingI 'StBusy where sing = SingBusy
+instance SingI 'StDone where sing = SingDone
+
 instance Protocol (EKGForward req resp) where
 
   -- | The messages in the EKG forwarding/accepting protocol.
@@ -91,32 +101,10 @@ instance Protocol (EKGForward req resp) where
   -- 2. When both peers are in Busy state, the forwarder is expected to send
   --    a reply to the acceptor (list of new metrics).
   --
-  -- So we assume that, from __interaction__ point of view:
-  -- 1. ClientHasAgency (from 'Network.TypedProtocol.Core') corresponds to acceptor's agency.
-  -- 3. ServerHasAgency (from 'Network.TypedProtocol.Core') corresponds to forwarder's agency.
-  --
-  data ClientHasAgency st where
-    TokIdle :: ClientHasAgency 'StIdle
-
-  data ServerHasAgency st where
-    TokBusy :: ServerHasAgency 'StBusy
-
-  data NobodyHasAgency st where
-    TokDone :: NobodyHasAgency 'StDone
-
-  -- | Impossible cases.
-  exclusionLemma_ClientAndServerHaveAgency TokIdle tok = case tok of {}
-  exclusionLemma_NobodyAndClientHaveAgency TokDone tok = case tok of {}
-  exclusionLemma_NobodyAndServerHaveAgency TokDone tok = case tok of {}
-
-instance (Show req, Show resp)
-      => Show (Message (EKGForward req resp) from to) where
-  show MsgReq{}  = "MsgReq"
-  show MsgResp{} = "MsgResp"
-  show MsgDone{} = "MsgDone"
+  type StateAgency 'StIdle = 'ClientAgency
+  type StateAgency 'StBusy = 'ServerAgency
+  type StateAgency 'StDone = 'NobodyAgency
 
-instance Show (ClientHasAgency (st :: EKGForward req resp)) where
-  show TokIdle = "TokIdle"
 
-instance Show (ServerHasAgency (st :: EKGForward req resp)) where
-  show TokBusy = "TokBusy"
+deriving instance (Show req, Show resp)
+               => Show (Message (EKGForward req resp) from to)