typed-protocols: added PeerPipelined newtype wrapper

Author: coot

typed-protocols-examples/src/Network/TypedProtocol/Driver/Simple.hs

@@ -147,12 +147,12 @@ runPeer tracer codec channel peer =
 -- 'MonadSTM' constraint.
 --
 runPipelinedPeer
-  :: forall ps (st :: ps) pr failure bytes c m a.
+  :: forall ps (st :: ps) pr failure bytes m a.
      (MonadAsync m, MonadThrow m, Exception failure)
   => Tracer m (TraceSendRecv ps)
   -> Codec ps failure m bytes
   -> Channel m bytes
-  -> Peer ps pr ('Pipelined Z c) st m a
+  -> PeerPipelined ps pr st m a
   -> m (a, Maybe bytes)
 runPipelinedPeer tracer codec channel peer =
     runPipelinedPeerWithDriver driver peer
@@ -214,8 +214,8 @@ runConnectedPeersPipelined :: (MonadAsync m, MonadCatch m,
                            => m (Channel m bytes, Channel m bytes)
                            -> Tracer m (PeerRole, TraceSendRecv ps)
                            -> Codec ps failure m bytes
-                           -> Peer ps             pr  ('Pipelined Z c) st m a
-                           -> Peer ps (FlipAgency pr) 'NonPipelined    st m b
+                           -> PeerPipelined ps             pr                st m a
+                           -> Peer          ps (FlipAgency pr) 'NonPipelined st m b
                            -> m (a, b)
 runConnectedPeersPipelined createChannels tracer codec client server =
     createChannels >>= \(clientChannel, serverChannel) ->
@@ -240,8 +240,8 @@ runConnectedPeersAsymmetric
     -> Tracer m (Role, TraceSendRecv ps)
     -> Codec ps failure m bytes
     -> Codec ps failure m bytes
-    -> Peer ps             pr  ('Pipelined Z c) st m a
-    -> Peer ps (FlipAgency pr) 'NonPipelined    st m b
+    -> PeerPipelined ps             pr                st m a
+    -> Peer          ps (FlipAgency pr) 'NonPipelined st m b
     -> m (a, b)
 runConnectedPeersAsymmetric createChannels tracer codec codec' client server =
     createChannels >>= \(clientChannel, serverChannel) ->

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Client.hs

@@ -139,9 +139,9 @@ data PingPongClientIdle (n :: N) c m a where
 pingPongClientPeerPipelined
   :: Functor m
   => PingPongClientPipelined c m a
-  -> Client PingPong (Pipelined Z c) StIdle m a
+  -> ClientPipelined PingPong StIdle m a
 pingPongClientPeerPipelined (PingPongClientPipelined peer) =
-    pingPongClientPeerIdle peer
+    ClientPipelined $ pingPongClientPeerIdle peer
 
 
 pingPongClientPeerIdle

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Client.hs

@@ -84,12 +84,12 @@ requestOnce server req = (\(resp, _, _) -> resp)
 -- | A request-response client designed for running the 'ReqResp' protocol in
 -- a pipelined way.
 --
-data ReqRespClientPipelined req resp c m a where
+data ReqRespClientPipelined req resp m a where
   -- | A 'PingPongSender', but starting with zero outstanding pipelined
   -- responses, and for any internal collect type @c@.
   ReqRespClientPipelined ::
       ReqRespIdle            req resp Z c m a
-   -> ReqRespClientPipelined req resp   c m a
+   -> ReqRespClientPipelined req resp     m a
 
 
 data ReqRespIdle req resp n c m a where
@@ -117,10 +117,10 @@ data ReqRespIdle req resp n c m a where
 --
 reqRespClientPeerPipelined
   :: Functor m
-  => ReqRespClientPipelined req resp         c         m a
-  -> Client (ReqResp req resp) (Pipelined  Z c) StIdle m a
+  => ReqRespClientPipelined req resp           m a
+  -> ClientPipelined (ReqResp req resp) StIdle m a
 reqRespClientPeerPipelined (ReqRespClientPipelined peer) =
-    reqRespClientPeerIdle peer
+    ClientPipelined $ reqRespClientPeerIdle peer
 
 
 reqRespClientPeerIdle

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Examples.hs

@@ -68,7 +68,7 @@ reqRespClientMap = go []
 reqRespClientMapPipelined :: forall req resp m.
                              Monad m
                           => [req]
-                          -> ReqRespClientPipelined req resp resp m [resp]
+                          -> ReqRespClientPipelined req resp m [resp]
 reqRespClientMapPipelined reqs0 =
     ReqRespClientPipelined (go [] Zero reqs0)
   where

typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs

@@ -103,15 +103,15 @@ direct (SendMsgReq req kResp) ReqRespServer{recvMsgReq} = do
     direct client' server'
 
 
-directPipelined :: forall req resp c m a b. Monad m
-                => ReqRespClientPipelined req resp c m a
-                -> ReqRespServer          req resp   m b
+directPipelined :: Monad m
+                => ReqRespClientPipelined req resp m a
+                -> ReqRespServer          req resp m b
                 -> m (a, b)
 directPipelined (ReqRespClientPipelined client0) server0 =
     go EmptyQ client0 server0
   where
-    go :: forall n.
-          Queue n c
+    go :: Monad m
+       => Queue n c
        -> ReqRespIdle   req resp n c m a
        -> ReqRespServer req resp     m b
        -> m (a, b)

typed-protocols/src/Network/TypedProtocol/Driver.hs

@@ -156,12 +156,12 @@ runPeerWithDriver Driver{sendMessage, recvMessage, initialDState} =
 -- 'MonadAsync' constraint.
 --
 runPipelinedPeerWithDriver
-  :: forall ps (st :: ps) pr dstate c m a.
+  :: forall ps (st :: ps) pr dstate m a.
      MonadAsync m
   => Driver ps pr dstate m
-  -> Peer ps pr ('Pipelined Z c) st m a
+  -> PeerPipelined ps pr st m a
   -> m (a, dstate)
-runPipelinedPeerWithDriver driver@Driver{initialDState} peer = do
+runPipelinedPeerWithDriver driver@Driver{initialDState} (PeerPipelined peer) = do
     receiveQueue <- atomically newTQueue
     collectQueue <- atomically newTQueue
     a <- runPipelinedPeerReceiverQueue receiveQueue collectQueue driver

typed-protocols/src/Network/TypedProtocol/Peer.hs

@@ -17,6 +17,7 @@
 --
 module Network.TypedProtocol.Peer
   ( Peer (..)
+  , PeerPipelined (..)
   , Receiver (..)
   , Outstanding
   , N (..)
@@ -254,3 +255,11 @@ data Receiver ps pr st stdone m c where
                  -> Receiver ps pr st stdone m c
 
 deriving instance Functor m => Functor (Receiver ps pr st stdone m)
+
+-- | A description of a peer that engages in a protocol in a pipelined fashion.
+--
+data PeerPipelined ps pr (st :: ps) m a where
+    PeerPipelined :: { runPeerPipelined :: Peer ps pr (Pipelined Z c) st m a }
+                  -> PeerPipelined ps pr st m a
+
+deriving instance Functor m => Functor (PeerPipelined ps pr st m)

typed-protocols/src/Network/TypedProtocol/Peer/Client.hs

@@ -13,6 +13,8 @@
 --
 module Network.TypedProtocol.Peer.Client
   ( Client
+  , ClientPipelined
+  , TP.PeerPipelined(ClientPipelined, runClientPipelined)
   , pattern Effect
   , pattern Yield
   , pattern Await
@@ -46,6 +48,20 @@ type Client :: forall ps
 type Client ps pl st m a = Peer ps AsClient pl st m a
 
 
+-- | A description of a peer that engages in a protocol in a pipelined fashion.
+--
+type ClientPipelined  ps st m a = TP.PeerPipelined ps AsClient st m a
+
+pattern ClientPipelined :: forall ps st m a.
+                           ()
+                        => forall c.
+                           ()
+                        => Client ps (Pipelined Z c) st m a
+                        -> ClientPipelined ps st m a
+pattern ClientPipelined { runClientPipelined } = TP.PeerPipelined runClientPipelined
+
+{-# COMPLETE ClientPipelined #-}
+
 -- | Client role pattern for 'TP.Effect'.
 --
 pattern Effect :: forall ps pl st m a.

typed-protocols/src/Network/TypedProtocol/Peer/Server.hs

@@ -13,6 +13,8 @@
 --
 module Network.TypedProtocol.Peer.Server
   ( Server
+  , ServerPipelined
+  , TP.PeerPipelined(ServerPipelined, runServerPipelined)
   , pattern Effect
   , pattern Yield
   , pattern Await
@@ -46,6 +48,21 @@ type Server :: forall ps
 type Server ps pl st m a = Peer ps AsServer pl st m a
 
 
+-- | A description of a peer that engages in a protocol in a pipelined fashion.
+--
+type ServerPipelined  ps st m a = TP.PeerPipelined ps AsServer st m a
+
+pattern ServerPipelined :: forall ps st m a.
+                           ()
+                        => forall c.
+                           ()
+                        => Server ps (Pipelined Z c) st m a
+                        -> ServerPipelined ps st m a
+pattern ServerPipelined { runServerPipelined } = TP.PeerPipelined runServerPipelined
+
+{-# COMPLETE ServerPipelined #-}
+
+
 -- | Server role pattern for 'TP.Effect'.
 --
 pattern Effect :: forall ps pl st m a.

typed-protocols/src/Network/TypedProtocol/Proofs.hs

@@ -169,19 +169,19 @@ enqueue a (ConsQ b q) = ConsQ b (enqueue a q)
 -- us extra expressiveness or to break the protocol state machine.
 --
 forgetPipelined
-  :: forall ps (pr :: PeerRole) (st :: ps) c m a.
+  :: forall ps (pr :: PeerRole) (st :: ps) m a.
      Functor m
   => [Bool]
   -- ^ interleaving choices for pipelining allowed by
   -- `Collect` and `CollectSTM` primitive. False values or `[]` give no
   -- pipelining.  For the 'CollectSTM' primitive, the stm action must not
   -- block otherwise even if the choice is to pipeline more (a 'True' value),
   -- we'll actually collect a result.
-  -> Peer ps pr (Pipelined Z c) st m a
+  -> PeerPipelined ps pr st m a
   -> Peer ps pr  NonPipelined   st m a
-forgetPipelined = goSender EmptyQ
+forgetPipelined cs0 (PeerPipelined peer) = goSender EmptyQ cs0 peer
   where
-    goSender :: forall st' n.
+    goSender :: forall st' n c.
                 Queue n c
              -> [Bool]
              -> Peer ps pr ('Pipelined n c) st' m a
@@ -196,7 +196,7 @@ forgetPipelined = goSender EmptyQ
     goSender (ConsQ x q) (_:cs) (Collect _ k)        = goSender q cs (k x)
     goSender (ConsQ x q) cs@[]  (Collect _ k)        = goSender q cs (k x)
 
-    goReceiver :: forall stCurrent stNext n.
+    goReceiver :: forall stCurrent stNext n c.
                   Queue n c
                -> [Bool]
                -> Peer     ps pr ('Pipelined (S n) c) stNext m a
@@ -218,17 +218,19 @@ forgetPipelined = goSender EmptyQ
 -- using `connectPipelined` function.
 --
 promoteToPipelined
-  :: forall ps (pr :: PeerRole) st c m a.
+  :: forall ps (pr :: PeerRole) st m a.
      Functor m
-  => Peer ps pr 'NonPipelined    st m a
-  -> Peer ps pr ('Pipelined Z c) st m a
-promoteToPipelined (Effect k)         = Effect
-                                      $ promoteToPipelined <$> k
-promoteToPipelined (Yield refl msg k) = Yield refl msg
-                                      $ promoteToPipelined k
-promoteToPipelined (Await refl k)     = Await refl
-                                      $ promoteToPipelined . k
-promoteToPipelined (Done refl k)      = Done refl k
+  => Peer ps pr NonPipelined    st m a
+  -> PeerPipelined ps pr st m a
+promoteToPipelined p = PeerPipelined (go p)
+  where
+    go :: forall st' c.
+          Peer ps pr NonPipelined    st' m a
+       -> Peer ps pr (Pipelined Z c) st' m a
+    go (Effect k)         = Effect $ go <$> k
+    go (Yield refl msg k) = Yield refl msg (go k)
+    go (Await refl k)     = Await refl (go . k)
+    go (Done refl k)      = Done refl k
 
 
 -- | Analogous to 'connect' but also for pipelined peers.
@@ -243,11 +245,11 @@ promoteToPipelined (Done refl k)      = Done refl k
 --
 connectPipelined
   :: forall ps (pr :: PeerRole)
-               (st :: ps) c m a b.
+               (st :: ps) m a b.
        (Monad m, SingI pr)
     => [Bool]
-    -> Peer ps             pr  ('Pipelined Z c) st m a
-    -> Peer ps (FlipAgency pr) NonPipelined     st m b
+    -> PeerPipelined ps             pr               st m a
+    -> Peer          ps (FlipAgency pr) NonPipelined st m b
     -> m (a, b, TerminalStates ps)
 connectPipelined csA a b =
     connect (forgetPipelined csA a) b