tracer-forwarder: Update to typed-protocols-0.3

trace-forward/src/Trace/Forward/Protocol/DataPoint/Acceptor.hs

@@ -14,7 +14,8 @@ module Trace.Forward.Protocol.DataPoint.Acceptor
   , dataPointAcceptorPeer
   ) where
 
-import           Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..), PeerRole (..))
+import           Network.TypedProtocol.Peer.Client
+-- import           Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..), PeerRole (..))
 
 import           Trace.Forward.Protocol.DataPoint.Type
 
@@ -33,15 +34,15 @@ data DataPointAcceptor m a where
 dataPointAcceptorPeer
   :: Monad m
   => DataPointAcceptor m a
-  -> Peer DataPointForward 'AsClient 'StIdle m a
+  -> Client DataPointForward 'NonPipelined 'StIdle m a
 dataPointAcceptorPeer = \case
   SendMsgDataPointsRequest request next ->
     -- Send our message (request for new 'DataPoint's from the forwarder).
-    Yield (ClientAgency TokIdle) (MsgDataPointsRequest request) $
+    Yield (MsgDataPointsRequest request) $
       -- We're now into the 'StBusy' state, and now we'll wait for a reply
       -- from the forwarder. It is assuming that the forwarder will reply
       -- immediately (even there are no 'DataPoint's).
-      Await (ServerAgency TokBusy) $ \(MsgDataPointsReply reply) ->
+      Await $ \(MsgDataPointsReply reply) ->
         Effect $
           dataPointAcceptorPeer <$> next reply
 
@@ -50,5 +51,5 @@ dataPointAcceptorPeer = \case
     -- 'StDone' state. Once in the 'StDone' state we can actually stop using
     -- 'done', with a return value.
     Effect $
-      Yield (ClientAgency TokIdle) MsgDone . Done TokDone
+      Yield MsgDone . Done 
         <$> getResult

trace-forward/src/Trace/Forward/Protocol/DataPoint/Codec.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -13,8 +14,9 @@ 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           Network.TypedProtocol.Codec (Codec, PeerHasAgency (..), PeerRole (..),
-                   SomeMessage (..))
+import           Network.TypedProtocol.Codec
+-- import           Network.TypedProtocol.Codec (Codec, PeerHasAgency (..), PeerRole (..),
+--                    SomeMessage (..))
 import           Network.TypedProtocol.Codec.CBOR (mkCodecCborLazyBS)
 import           Text.Printf (printf)
 
@@ -35,48 +37,46 @@ codecDataPointForward encodeRequest   decodeRequest
  where
   -- Encode messages.
   encode
-    :: forall (pr  :: PeerRole)
-              (st  :: DataPointForward)
+    :: forall (st  :: DataPointForward)
               (st' :: DataPointForward).
-       PeerHasAgency pr st
-    -> Message DataPointForward st st'
+       Message DataPointForward st st'
     -> CBOR.Encoding
 
-  encode (ClientAgency TokIdle) (MsgDataPointsRequest request) =
+  encode (MsgDataPointsRequest request) =
        CBOR.encodeListLen 2
     <> CBOR.encodeWord 1
     <> encodeRequest request
 
-  encode (ClientAgency TokIdle) MsgDone =
+  encode MsgDone =
        CBOR.encodeListLen 1
     <> CBOR.encodeWord 2
 
-  encode (ServerAgency TokBusy) (MsgDataPointsReply reply) =
+  encode (MsgDataPointsReply reply) =
        CBOR.encodeListLen 2
     <> CBOR.encodeWord 3
     <> encodeReplyList reply
 
   -- Decode messages
   decode
-    :: forall (pr :: PeerRole)
-              (st :: DataPointForward) s.
-       PeerHasAgency pr st
+    :: forall (st :: DataPointForward) s.
+       ActiveState st 
+    => StateToken st
     -> CBOR.Decoder s (SomeMessage st)
-  decode stok = do
+  decode stateToken = do
     len <- CBOR.decodeListLen
     key <- CBOR.decodeWord
-    case (key, len, stok) of
-      (1, 2, ClientAgency TokIdle) ->
+    case (key, len, stateToken) of
+      (1, 2, SingIdle) ->
         SomeMessage . MsgDataPointsRequest <$> decodeRequest
 
-      (2, 1, ClientAgency TokIdle) ->
+      (2, 1, SingIdle) ->
         return $ SomeMessage MsgDone
 
-      (3, 2, ServerAgency TokBusy) ->
+      (3, 2, SingBusy) ->
         SomeMessage . MsgDataPointsReply <$> decodeReplyList
 
       -- Failures per protocol state
-      (_, _, ClientAgency TokIdle) ->
-        fail (printf "codecDataPointForward (%s) unexpected key (%d, %d)" (show stok) key len)
-      (_, _, ServerAgency TokBusy) ->
-        fail (printf "codecDataPointForward (%s) unexpected key (%d, %d)" (show stok) key len)
+      (_, _, SingIdle) ->
+        fail (printf "codecDataPointForward (%s) unexpected key (%d, %d)" (show stateToken) key len)
+      (_, _, SingBusy) ->
+        fail (printf "codecDataPointForward (%s) unexpected key (%d, %d)" (show stateToken) key len)

trace-forward/src/Trace/Forward/Protocol/DataPoint/Forwarder.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
@@ -9,7 +10,7 @@ module Trace.Forward.Protocol.DataPoint.Forwarder
   , dataPointForwarderPeer
   ) where
 
-import           Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..), PeerRole (..))
+import           Network.TypedProtocol.Peer.Server
 
 import           Trace.Forward.Protocol.DataPoint.Type
 
@@ -29,22 +30,21 @@ data DataPointForwarder m a = DataPointForwarder
 dataPointForwarderPeer
   :: Monad m
   => DataPointForwarder m a
-  -> Peer DataPointForward 'AsServer 'StIdle m a
+  -> Server DataPointForward 'NonPipelined 'StIdle m a
 dataPointForwarderPeer DataPointForwarder{recvMsgDataPointsRequest, recvMsgDone} = go
   where
     go =
       -- 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 'DataPoint's, so now we're
         -- in the 'StBusy' state which means it's the forwarder's turn to send
         -- a reply.
-        MsgDataPointsRequest request -> Effect $ do
+        MsgDataPointsRequest request -> Effect do
           reply <- recvMsgDataPointsRequest request
-          return $ Yield (ServerAgency TokBusy)
-                         (MsgDataPointsReply reply)
+          return $ Yield (MsgDataPointsReply reply)
                          go
 
         -- 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

trace-forward/src/Trace/Forward/Protocol/DataPoint/Type.hs

@@ -1,8 +1,10 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 
 -- | The type of the 'DataPoint' forwarding/accepting protocol.
@@ -14,16 +16,16 @@
   , DataPointValues
   , DataPointForward (..)
   , Message (..)
-  , ClientHasAgency (..)
-  , ServerHasAgency (..)
-  , NobodyHasAgency (..)
+  , SingDataPointForward (..)
   ) where
 
+import           Data.Singletons
+import           Network.TypedProtocol.Core
 import           Ouroboros.Network.Util.ShowProxy (ShowProxy (..))
 
 import qualified Data.ByteString.Lazy as LBS
+import           Data.Kind (Type)
 import           Data.Text (Text)
-import           Network.TypedProtocol.Core (Protocol (..))
 
 -- | A kind to identify our protocol, and the types of the states in the state
 -- transition diagram of the protocol.
@@ -62,6 +64,25 @@
 instance ShowProxy DataPointForward where
   showProxy _ = "DataPointForward"
 
+-- | Singleton type of DataPointForward. Same as:
+--
+-- @
+-- type SingDataPointForward :: DataPointForward -> Type
+-- type SingDataPointForward = TypeRep
+-- @
+type SingDataPointForward :: DataPointForward -> Type
+data SingDataPointForward dataPoint where
+  SingIdle :: SingDataPointForward 'StIdle
+  SingBusy :: SingDataPointForward 'StBusy
+  SingDone :: SingDataPointForward 'StDone
+
+type instance Sing = SingDataPointForward
+
+deriving instance Show (SingDataPointForward st)
+instance StateTokenI 'StIdle where stateToken = SingIdle
+instance StateTokenI 'StBusy where stateToken = SingBusy
+instance StateTokenI 'StDone where stateToken = SingDone
+
 instance Protocol DataPointForward where
 
   -- | The messages in the trace forwarding/accepting protocol.
@@ -95,27 +116,11 @@
   -- 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 (Message DataPointForward from to) where
-  show MsgDataPointsRequest{} = "MsgDataPointsRequest"
-  show MsgDataPointsReply{}   = "MsgDataPointsReply"
-  show MsgDone{}              = "MsgDone"
+  type StateAgency 'StIdle = 'ClientAgency
+  type StateAgency 'StBusy = 'ServerAgency
+  type StateAgency 'StDone = 'NobodyAgency
 
-instance Show (ClientHasAgency (st :: DataPointForward)) where
-  show TokIdle = "TokIdle"
+  type StateToken = SingDataPointForward
 
-instance Show (ServerHasAgency (st :: DataPointForward)) where
-  show TokBusy{} = "TokBusy"
+deriving 
+  instance Show (Message DataPointForward from to)

trace-forward/src/Trace/Forward/Protocol/TraceObject/Acceptor.hs

@@ -1,8 +1,10 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 
 -- | A view of the trace forwarding/accepting protocol
 --   from the point of view of the client.
@@ -14,10 +16,12 @@ module Trace.Forward.Protocol.TraceObject.Acceptor
   , traceObjectAcceptorPeer
   ) where
 
-import           Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..), PeerRole (..))
+import           Data.Kind (Type)
 
+import           Network.TypedProtocol.Peer.Client
 import           Trace.Forward.Protocol.TraceObject.Type
 
+type TraceObjectAcceptor :: Type -> (Type -> Type) -> Type -> Type
 data TraceObjectAcceptor lo m a where
   SendMsgTraceObjectsRequest
     :: TokBlockingStyle blocking
@@ -34,31 +38,31 @@ data TraceObjectAcceptor lo m a where
 traceObjectAcceptorPeer
   :: Monad m
   => TraceObjectAcceptor lo m a
-  -> Peer (TraceObjectForward lo) 'AsClient 'StIdle m a
+  -> Client (TraceObjectForward lo) 'NonPipelined 'StIdle m a
 traceObjectAcceptorPeer = \case
   SendMsgTraceObjectsRequest TokBlocking request next ->
     -- Send our message (request for new 'TraceObject's from the forwarder).
-    Yield (ClientAgency TokIdle) (MsgTraceObjectsRequest TokBlocking request) $
+    Yield (MsgTraceObjectsRequest TokBlocking request) do
       -- We're now into the 'StBusy' state, and now we'll wait for a reply
       -- from the forwarder.
-      Await (ServerAgency (TokBusy TokBlocking)) $ \(MsgTraceObjectsReply reply) ->
-        Effect $
+      Await \(MsgTraceObjectsReply reply) ->
+        Effect do
           traceObjectAcceptorPeer <$> next reply
 
   SendMsgTraceObjectsRequest TokNonBlocking request next ->
     -- Send our message (request for new 'TraceObject's from the forwarder).
-    Yield (ClientAgency TokIdle) (MsgTraceObjectsRequest TokNonBlocking request) $
+    Yield (MsgTraceObjectsRequest TokNonBlocking request) do
       -- We're now into the 'StBusy' state, and now we'll wait for a reply
       -- from the forwarder. It is assuming that the forwarder will reply
       -- immediately (even there are no 'TraceObject's).
-      Await (ServerAgency (TokBusy TokNonBlocking)) $ \(MsgTraceObjectsReply reply) ->
-        Effect $
+      Await \(MsgTraceObjectsReply reply) ->
+        Effect do
           traceObjectAcceptorPeer <$> next reply
 
   SendMsgDone getResult ->
     -- We do an actual transition using 'yield', to go from the 'StIdle' to
     -- 'StDone' state. Once in the 'StDone' state we can actually stop using
     -- 'done', with a return value.
-    Effect $
-      Yield (ClientAgency TokIdle) MsgDone . Done TokDone
+    Effect do
+      Yield MsgDone . Done
         <$> getResult