typed-protocols 1.1.0.1 → 1.2.0.0
raw patch · 8 files changed
+108/−21 lines, 8 filesdep +deepseqdep ~basedep ~io-classes
Dependencies added: deepseq
Dependency ranges changed: base, io-classes
Files
- CHANGELOG.md +5/−0
- examples/Network/TypedProtocol/Driver/Simple.hs +44/−9
- src/Network/TypedProtocol/Codec.hs +5/−0
- src/Network/TypedProtocol/Driver.hs +23/−5
- stateful/Network/TypedProtocol/Stateful/Driver.hs +9/−2
- test/Network/TypedProtocol/PingPong/Tests.hs +6/−1
- test/Network/TypedProtocol/ReqResp/Tests.hs +12/−3
- typed-protocols.cabal +4/−1
CHANGELOG.md view
@@ -1,5 +1,10 @@ # Revision history for typed-protocols +## 1.2.0.0 -- 2025-02-05++* Make `runPeerWithDriver` strict, it evaluates the result and `dstate` to+ normal form.+ ## 1.1.0.1 -- 2025-10-14 * Support QuickCheck <= 2.15
examples/Network/TypedProtocol/Driver/Simple.hs view
@@ -30,6 +30,7 @@ import Network.TypedProtocol.Driver import Network.TypedProtocol.Peer +import Control.DeepSeq (NFData, force) import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadThrow import Control.Tracer (Tracer (..), contramap, traceWith)@@ -72,7 +73,11 @@ driverSimple :: forall ps pr failure bytes m.- (MonadThrow m, Exception failure)+ ( MonadEvaluate m+ , MonadThrow m+ , Exception failure+ , NFData failure+ ) => Tracer m (TraceSendRecv ps) -> Codec ps failure m bytes -> Channel m bytes@@ -119,7 +124,12 @@ -- runPeer :: forall ps (st :: ps) pr failure bytes m a.- (MonadThrow m, Exception failure)+ ( MonadEvaluate m+ , MonadThrow m+ , Exception failure+ , NFData failure+ , NFData a+ ) => Tracer m (TraceSendRecv ps) -> Codec ps failure m bytes -> Channel m bytes@@ -140,7 +150,13 @@ -- runPipelinedPeer :: forall ps (st :: ps) pr failure bytes m a.- (MonadAsync m, MonadThrow m, Exception failure)+ ( MonadAsync m+ , MonadEvaluate m+ , MonadThrow m+ , Exception failure+ , NFData failure+ , NFData a+ ) => Tracer m (TraceSendRecv ps) -> Codec ps failure m bytes -> Channel m bytes@@ -159,7 +175,10 @@ -- | Run a codec incremental decoder 'DecodeStep' against a channel. It also -- takes any extra input data and returns any unused trailing data. ---runDecoderWithChannel :: Monad m+runDecoderWithChannel :: ( Monad m+ , MonadEvaluate m+ , NFData failure+ ) => Channel m bytes -> Maybe bytes -> DecodeStep bytes failure m a@@ -168,7 +187,7 @@ runDecoderWithChannel Channel{recv} = go where go _ (DecodeDone x trailing) = return (Right (x, trailing))- go _ (DecodeFail failure) = return (Left failure)+ go _ (DecodeFail failure) = Left <$> evaluate (force failure) go Nothing (DecodePartial k) = recv >>= k >>= go Nothing go (Just trailing) (DecodePartial k) = k (Just trailing) >>= go Nothing @@ -183,8 +202,14 @@ -- The first argument is expected to create two channels that are connected, -- for example 'createConnectedChannels'. ---runConnectedPeers :: (MonadAsync m, MonadCatch m,- Exception failure)+runConnectedPeers :: ( MonadAsync m+ , MonadCatch m+ , MonadEvaluate m+ , Exception failure+ , NFData failure+ , NFData a+ , NFData b+ ) => m (Channel m bytes, Channel m bytes) -> Tracer m (Role, TraceSendRecv ps) -> Codec ps failure m bytes@@ -201,8 +226,14 @@ tracerClient = contramap ((,) Client) tracer tracerServer = contramap ((,) Server) tracer -runConnectedPeersPipelined :: (MonadAsync m, MonadCatch m,- Exception failure)+runConnectedPeersPipelined :: ( MonadAsync m+ , MonadCatch m+ , MonadEvaluate m+ , Exception failure+ , NFData failure+ , NFData a+ , NFData b+ ) => m (Channel m bytes, Channel m bytes) -> Tracer m (PeerRole, TraceSendRecv ps) -> Codec ps failure m bytes@@ -225,8 +256,12 @@ -- runConnectedPeersAsymmetric :: ( MonadAsync m+ , MonadEvaluate m , MonadMask m , Exception failure+ , NFData failure+ , NFData a+ , NFData b ) => m (Channel m bytes, Channel m bytes) -> Tracer m (Role, TraceSendRecv ps)
src/Network/TypedProtocol/Codec.hs view
@@ -47,6 +47,7 @@ , SomeState (..) ) where +import Control.DeepSeq (NFData (..)) import Control.Exception (Exception) import Data.Kind (Type) @@ -315,6 +316,10 @@ data CodecFailure = CodecFailureOutOfInput | CodecFailure String deriving (Eq, Show)++instance NFData CodecFailure where+ rnf CodecFailureOutOfInput = ()+ rnf (CodecFailure failure) = rnf failure -- safe instance with @UndecidableInstances@ in scope instance Exception CodecFailure
src/Network/TypedProtocol/Driver.hs view
@@ -20,9 +20,11 @@ import Network.TypedProtocol.Peer import Control.Concurrent.Class.MonadSTM.TQueue+import Control.DeepSeq (NFData, force) import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadFork import Control.Monad.Class.MonadSTM+import Control.Monad.Class.MonadThrow -- $intro@@ -114,9 +116,18 @@ -- -- This runs the peer to completion (if the protocol allows for termination). --+-- The returned value `a` is evaluated to normal form, any pure exceptions will+-- be raised by `runPeerWithDriver`.+--+-- The returned `dstate` should be fed back into `runPeerWithDriver`, where it+-- will be evaluated incrementally.+-- runPeerWithDriver :: forall ps (st :: ps) pr dstate m a.- Monad m+ ( Monad m+ , MonadEvaluate m+ , NFData a+ ) => Driver ps pr dstate m -> Peer ps pr NonPipelined st m a -> m (a, dstate)@@ -128,7 +139,9 @@ -> Peer ps pr 'NonPipelined st' m a -> m (a, dstate) go dstate (Effect k) = k >>= go dstate- go dstate (Done _ x) = return (x, dstate)+ go dstate (Done _ x) = do+ x' <- evaluate (force x)+ return (x', dstate) go dstate (Yield refl msg k) = do sendMessage refl msg@@ -165,18 +178,23 @@ -- runPipelinedPeerWithDriver :: forall ps (st :: ps) pr dstate m a.- MonadAsync m+ ( MonadAsync m+ , MonadEvaluate m+ , NFData a+ ) => Driver ps pr dstate m -> PeerPipelined ps pr st m a -> m (a, dstate) runPipelinedPeerWithDriver driver@Driver{initialDState} (PeerPipelined peer) = do receiveQueue <- atomically newTQueue collectQueue <- atomically newTQueue- a <- runPipelinedPeerReceiverQueue receiveQueue collectQueue driver+ r@(a, _dstate) <- runPipelinedPeerReceiverQueue receiveQueue collectQueue driver `withAsyncLoop` runPipelinedPeerSender receiveQueue collectQueue driver peer initialDState- return a++ _ <- evaluate (force a)+ return r where withAsyncLoop :: m Void -> m x -> m x
stateful/Network/TypedProtocol/Stateful/Driver.hs view
@@ -11,7 +11,9 @@ , DecodeStep (..) ) where +import Control.DeepSeq (NFData, force) import Control.Monad.Class.MonadSTM+import Control.Monad.Class.MonadThrow import Data.Kind (Type) @@ -82,7 +84,10 @@ -- runPeerWithDriver :: forall ps (st :: ps) pr bytes failure dstate (f :: ps -> Type) m a.- MonadSTM m+ ( MonadEvaluate m+ , MonadSTM m+ , NFData a+ ) => Driver ps pr bytes failure dstate f m -> f st -> Peer ps pr st f m a@@ -100,7 +105,9 @@ -> m (a, dstate) go !dstate !f (Effect k) = k >>= go dstate f - go !dstate _ (Done _ x) = return (x, dstate)+ go !dstate _ (Done _ x) = do+ x' <- evaluate (force x)+ return (x', dstate) go !dstate _ (Yield refl !f !f' msg k) = do sendMessage refl f msg
test/Network/TypedProtocol/PingPong/Tests.hs view
@@ -290,7 +290,12 @@ -- | Run a non-pipelined client and server over a channel using a codec. ---prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m)+prop_channel :: ( MonadLabelledSTM m+ , MonadTraceSTM m+ , MonadAsync m+ , MonadCatch m+ , MonadEvaluate m+ ) => NonNegative Int -> m Bool prop_channel (NonNegative n) = do
test/Network/TypedProtocol/ReqResp/Tests.hs view
@@ -172,7 +172,12 @@ -- Properties using channels, codecs and drivers. -- -prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m)+prop_channel :: ( MonadLabelledSTM m+ , MonadTraceSTM m+ , MonadAsync m+ , MonadCatch m+ , MonadEvaluate m+ ) => (Int -> Int -> (Int, Int)) -> [Int] -> m Bool prop_channel f xs = do@@ -195,8 +200,12 @@ runSimOrThrow (prop_channel f xs) -prop_channelPipelined :: ( MonadLabelledSTM m, MonadAsync m, MonadCatch m- , MonadST m)+prop_channelPipelined :: ( MonadLabelledSTM m+ , MonadAsync m+ , MonadCatch m+ , MonadEvaluate m+ , MonadST m+ ) => (Int -> Int -> (Int, Int)) -> [Int] -> m Bool prop_channelPipelined f xs = do
typed-protocols.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.4 name: typed-protocols-version: 1.1.0.1+version: 1.2.0.0 synopsis: A framework for strongly typed protocols description: A robust session type framework which supports protocol pipelining. Haddocks are published [here](https://input-output-hk.github.io/typed-protocols/)@@ -43,6 +43,7 @@ , Network.TypedProtocol.Proofs other-modules: Network.TypedProtocol.Lemmas build-depends: base >=4.12 && <4.22,+ deepseq, io-classes:io-classes ^>= 1.8, singletons ^>= 3.0 hs-source-dirs: src@@ -84,6 +85,7 @@ , Network.TypedProtocol.Stateful.Proofs , Network.TypedProtocol.Stateful.Codec build-depends: base,+ deepseq, singletons, io-classes:io-classes, typed-protocols:typed-protocols@@ -139,6 +141,7 @@ build-depends: base, bytestring, cborg,+ deepseq, serialise, singletons, contra-tracer,