@@ -33,6 +33,10 @@ module Network.TypedProtocol.Codec.Properties
3333 , SomeState (.. )
3434 ) where
3535
36+ import Control.Monad.Class.MonadST
37+ import Data.Maybe
38+ import Data.STRef
39+
3640import Network.TypedProtocol.Codec
3741import Network.TypedProtocol.Core
3842
@@ -161,28 +165,40 @@ prop_anncodec = prop_codecF runAnnotator
161165-- | A more general version of 'prop_codec_splitsM' for 'CodecF'.
162166--
163167prop_codecF_splitsM
164- :: forall ps failure m f bytes .
165- ( Monad m
166- , Eq (AnyMessage ps )
168+ :: forall ps failure m annotator f bytes channel .
169+ ( Eq (AnyMessage ps )
167170 , Show (AnyMessage ps )
168171 , Show failure
169- , Monoid bytes
172+ , MonadST m
170173 )
171- => (forall (st :: ps ). f st -> bytes -> SomeMessage st )
174+ => (forall (st :: ps ). annotator st -> f (SomeMessage st ))
175+ -> (m (Maybe bytes ) -> channel )
176+ -> (forall (st :: ps ).
177+ channel
178+ -> Maybe bytes
179+ -> DecodeStep bytes failure m (f (SomeMessage st ))
180+ -> m (Either failure (SomeMessage st )))
172181 -> (bytes -> [[bytes ]])
173182 -- ^ alternative re-chunkings of serialised form
174- -> CodecF ps failure m f bytes
183+ -> CodecF ps failure m annotator bytes
175184 -> AnyMessage ps
176185 -> m Property
177- prop_codecF_splitsM runF splits
186+ prop_codecF_splitsM conv mkChannel runDecoder' splits
178187 Codec {encode, decode} (AnyMessage (msg :: Message ps st st' )) = do
179188 property . foldMap Every <$> sequence
180- [ do r <- decode stateToken >>= runDecoder bytes'
181- case r :: Either failure (f st ) of
182- Right f -> case runF f (mconcat bytes') of
183- SomeMessage msg' ->
184- return $! AnyMessage msg' === AnyMessage msg
185- Left err -> return $ counterexample (show err) False
189+ [ do
190+ stateRef <- stToIO . newSTRef $ tail bytes'
191+ let channelAction = stToIO $ do
192+ chunksRemaining <- readSTRef stateRef
193+ modifySTRef' stateRef (drop 1 )
194+ return $! listToMaybe chunksRemaining
195+ channel = mkChannel channelAction
196+ decoder <- decode @ st stateToken
197+ r <- runDecoder' channel (listToMaybe bytes') (conv <$> decoder)
198+ case r of
199+ Right (SomeMessage msg') ->
200+ return $! AnyMessage msg' === AnyMessage msg
201+ Left err -> return $ counterexample (show err) False
186202
187203 | let bytes = encode msg
188204 , bytes' <- splits bytes ]
@@ -200,31 +216,42 @@ prop_codecF_splitsM runF splits
200216-- to be checked.
201217--
202218prop_codec_splitsM
203- :: forall ps failure m bytes .
204- ( Monad m
205- , Eq (AnyMessage ps )
219+ :: forall ps failure m f bytes channel .
220+ ( Eq (AnyMessage ps )
206221 , Show (AnyMessage ps )
207222 , Show failure
208- , Monoid bytes
223+ , Applicative f
224+ , MonadST m
209225 )
210- => (bytes -> [[bytes ]])
226+ => (m (Maybe bytes ) -> channel )
227+ -> (forall (st :: ps ).
228+ channel
229+ -> Maybe bytes
230+ -> DecodeStep bytes failure m (f (SomeMessage st ))
231+ -> m (Either failure (SomeMessage st )))
232+ -> (bytes -> [[bytes ]])
211233 -- ^ alternative re-chunkings of serialised form
212234 -> Codec ps failure m bytes
213235 -> AnyMessage ps
214236 -> m Property
215- prop_codec_splitsM = prop_codecF_splitsM const
237+ prop_codec_splitsM = prop_codecF_splitsM pure
216238
217239-- | A variant of 'prop_codec_splitsM' for 'AnnotatedCodec'.
218240--
219241prop_anncodec_splitsM
220- :: forall ps failure m bytes .
221- ( Monad m
222- , Eq (AnyMessage ps )
242+ :: forall ps failure m bytes channel .
243+ ( Eq (AnyMessage ps )
223244 , Show (AnyMessage ps )
224245 , Show failure
225- , Monoid bytes
246+ , MonadST m
226247 )
227- => (bytes -> [[bytes ]])
248+ => (m (Maybe bytes ) -> channel )
249+ -> (forall (st :: ps ).
250+ channel
251+ -> Maybe bytes
252+ -> DecodeStep bytes failure m (bytes -> SomeMessage st )
253+ -> m (Either failure (SomeMessage st )))
254+ -> (bytes -> [[bytes ]])
228255 -- ^ alternative re-chunkings of serialised form
229256 -> AnnotatedCodec ps failure m bytes
230257 -> AnyMessage ps
@@ -235,51 +262,67 @@ prop_anncodec_splitsM = prop_codecF_splitsM runAnnotator
235262-- | A more general version of 'prop_codec_splits' for 'CodecF'.
236263--
237264prop_codecF_splits
238- :: forall ps failure m f bytes .
239- ( Monad m
240- , Eq (AnyMessage ps )
265+ :: forall ps failure m annotator f bytes channel .
266+ ( Eq (AnyMessage ps )
241267 , Show (AnyMessage ps )
242268 , Show failure
243- , Monoid bytes
269+ , MonadST m
244270 )
245- => (forall (st :: ps ). f st -> bytes -> SomeMessage st )
271+ => (forall (st :: ps ). annotator st -> f (SomeMessage st ))
272+ -> (m (Maybe bytes ) -> channel )
273+ -> (forall (st :: ps ).
274+ channel
275+ -> Maybe bytes
276+ -> DecodeStep bytes failure m (f (SomeMessage st ))
277+ -> m (Either failure (SomeMessage st )))
246278 -> (bytes -> [[bytes ]])
247279 -- ^ alternative re-chunkings of serialised form
248280 -> (forall a . m a -> a )
249- -> CodecF ps failure m f bytes
281+ -> CodecF ps failure m annotator bytes
250282 -> AnyMessage ps
251283 -> Property
252- prop_codecF_splits runF splits runM codec msg =
253- runM $ prop_codecF_splitsM runF splits codec msg
284+ prop_codecF_splits runF mkChannel runDecoder' splits runM codec msg =
285+ runM $ prop_codecF_splitsM runF mkChannel runDecoder' splits codec msg
254286
255287-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
256288--
257289prop_codec_splits
258- :: forall ps failure m bytes .
259- ( Monad m
260- , Eq (AnyMessage ps )
290+ :: forall ps failure m f bytes channel .
291+ ( Eq (AnyMessage ps )
261292 , Show (AnyMessage ps )
262293 , Show failure
263- , Monoid bytes
294+ , Applicative f
295+ , MonadST m
264296 )
265- => (bytes -> [[bytes ]])
297+ => (m (Maybe bytes ) -> channel )
298+ -> (forall (st :: ps ).
299+ channel
300+ -> Maybe bytes
301+ -> DecodeStep bytes failure m (f (SomeMessage st ))
302+ -> m (Either failure (SomeMessage st )))
303+ -> (bytes -> [[bytes ]])
266304 -- ^ alternative re-chunkings of serialised form
267305 -> (forall a . m a -> a )
268306 -> Codec ps failure m bytes
269307 -> AnyMessage ps
270308 -> Property
271- prop_codec_splits = prop_codecF_splits const
309+ prop_codec_splits = prop_codecF_splits pure
272310
273311-- | Like 'prop_codec_splits' but for 'AnnotatorCodec'.
274312prop_anncodec_splits
275- :: forall ps failure m bytes .
276- ( Monad m
277- , Eq (AnyMessage ps )
313+ :: forall ps failure m bytes channel .
314+ ( Eq (AnyMessage ps )
278315 , Show (AnyMessage ps )
279316 , Show failure
280- , Monoid bytes
317+ , MonadST m
281318 )
282- => (bytes -> [[bytes ]])
319+ => (m (Maybe bytes ) -> channel )
320+ -> (forall (st :: ps ).
321+ channel
322+ -> Maybe bytes
323+ -> DecodeStep bytes failure m (bytes -> SomeMessage st )
324+ -> m (Either failure (SomeMessage st )))
325+ -> (bytes -> [[bytes ]])
283326 -- ^ alternative re-chunkings of serialised form
284327 -> (forall a . m a -> a )
285328 -> AnnotatedCodec ps failure m bytes
0 commit comments