typed-protocols: connectPipelined type signature

Author: coot

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

@@ -211,9 +211,9 @@ connect_pipelined :: PingPongClientPipelined Int Identity [Either Int Int]
                   -> (Int, [Either Int Int])
 connect_pipelined client cs =
   case runIdentity
-         (connectPipelined cs []
+         (connectPipelined cs
             (pingPongClientPeerPipelined client)
-            (promoteToPipelined $ pingPongServerPeer pingPongServerCount))
+            (pingPongServerPeer pingPongServerCount))
     of (reqResps, n, TerminalStates SingDone SingDone) ->
          (n, reqResps)
 

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

@@ -165,9 +165,9 @@ prop_connect f xs =
 prop_connectPipelined :: [Bool] -> (Int -> Int -> (Int, Int)) -> [Int] -> Bool
 prop_connectPipelined cs f xs =
     case runIdentity
-           (connectPipelined cs []
+           (connectPipelined cs
              (reqRespClientPeerPipelined (reqRespClientMapPipelined xs))
-             (promoteToPipelined $ reqRespServerPeer
+             (reqRespServerPeer
                (reqRespServerMapAccumL (\a -> pure . f a) 0)))
 
       of (c, s, TerminalStates SingDone SingDone) ->

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

@@ -243,16 +243,14 @@ promoteToPipelined (Done refl k)      = Done refl k
 --
 connectPipelined
   :: forall ps (pr :: PeerRole)
-               (st :: ps) c c' m a b.
+               (st :: ps) c m a b.
        (Monad m, SingI pr)
     => [Bool]
-    -> [Bool]
-    -> Peer ps             pr  ('Pipelined Z c)  st m a
-    -> Peer ps (FlipAgency pr) ('Pipelined Z c') st m b
+    -> Peer ps             pr  ('Pipelined Z c) st m a
+    -> Peer ps (FlipAgency pr) NonPipelined     st m b
     -> m (a, b, TerminalStates ps)
-connectPipelined csA csB a b =
-    connect (forgetPipelined csA a)
-            (forgetPipelined csB b)
+connectPipelined csA a b =
+    connect (forgetPipelined csA a) b
 
 -- | A reference specification for interleaving of requests and responses
 -- with pipelining, where the environment can choose whether a response is