Updated against type-protocols changes

ekg-forward.cabal

@@ -64,9 +64,8 @@ library
                        , ekg-core
                        , io-classes >= 0.3
                        , network
-                       , ouroboros-network-api
-                       -- The API has changed in 0.6 so don't use it.
-                       , ouroboros-network-framework < 0.6
+                       , 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,12 @@ 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 {}
+  type StateAgency 'StIdle = 'ClientAgency
+  type StateAgency 'StBusy = 'ServerAgency
+  type StateAgency 'StDone = 'NobodyAgency
 
-instance (Show req, Show resp)
-      => Show (Message (EKGForward req resp) from to) where
-  show MsgReq{}  = "MsgReq"
-  show MsgResp{} = "MsgResp"
-  show MsgDone{} = "MsgDone"
+  type StateToken = SingEKGForward
 
-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)