@@ -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,41 @@ 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+ let stateM = newSTRef $ tail bytes'
191+ channelAction = stToIO $ do
192+ stateRef <- stateM
193+ chunksRemaining <- readSTRef stateRef
194+ modifySTRef' stateRef (drop 1 )
195+ return $! listToMaybe chunksRemaining
196+ channel = mkChannel channelAction
197+ decoder <- decode @ st stateToken
198+ r <- runDecoder' channel (listToMaybe bytes') (conv <$> decoder)
199+ case r of
200+ Right (SomeMessage msg') ->
201+ return $! AnyMessage msg' === AnyMessage msg
202+ Left err -> return $ counterexample (show err) False
186203
187204 | let bytes = encode msg
188205 , bytes' <- splits bytes ]
@@ -200,31 +217,42 @@ prop_codecF_splitsM runF splits
200217-- to be checked.
201218--
202219prop_codec_splitsM
203- :: forall ps failure m bytes .
204- ( Monad m
205- , Eq (AnyMessage ps )
220+ :: forall ps failure m f bytes channel .
221+ ( Eq (AnyMessage ps )
206222 , Show (AnyMessage ps )
207223 , Show failure
208- , Monoid bytes
224+ , Applicative f
225+ , MonadST m
209226 )
210- => (bytes -> [[bytes ]])
227+ => (m (Maybe bytes ) -> channel )
228+ -> (forall (st :: ps ).
229+ channel
230+ -> Maybe bytes
231+ -> DecodeStep bytes failure m (f (SomeMessage st ))
232+ -> m (Either failure (SomeMessage st )))
233+ -> (bytes -> [[bytes ]])
211234 -- ^ alternative re-chunkings of serialised form
212235 -> Codec ps failure m bytes
213236 -> AnyMessage ps
214237 -> m Property
215- prop_codec_splitsM = prop_codecF_splitsM const
238+ prop_codec_splitsM = prop_codecF_splitsM pure
216239
217240-- | A variant of 'prop_codec_splitsM' for 'AnnotatedCodec'.
218241--
219242prop_anncodec_splitsM
220- :: forall ps failure m bytes .
221- ( Monad m
222- , Eq (AnyMessage ps )
243+ :: forall ps failure m bytes channel .
244+ ( Eq (AnyMessage ps )
223245 , Show (AnyMessage ps )
224246 , Show failure
225- , Monoid bytes
247+ , MonadST m
226248 )
227- => (bytes -> [[bytes ]])
249+ => (m (Maybe bytes ) -> channel )
250+ -> (forall (st :: ps ).
251+ channel
252+ -> Maybe bytes
253+ -> DecodeStep bytes failure m (bytes -> SomeMessage st )
254+ -> m (Either failure (SomeMessage st )))
255+ -> (bytes -> [[bytes ]])
228256 -- ^ alternative re-chunkings of serialised form
229257 -> AnnotatedCodec ps failure m bytes
230258 -> AnyMessage ps
@@ -235,51 +263,67 @@ prop_anncodec_splitsM = prop_codecF_splitsM runAnnotator
235263-- | A more general version of 'prop_codec_splits' for 'CodecF'.
236264--
237265prop_codecF_splits
238- :: forall ps failure m f bytes .
239- ( Monad m
240- , Eq (AnyMessage ps )
266+ :: forall ps failure m annotator f bytes channel .
267+ ( Eq (AnyMessage ps )
241268 , Show (AnyMessage ps )
242269 , Show failure
243- , Monoid bytes
270+ , MonadST m
244271 )
245- => (forall (st :: ps ). f st -> bytes -> SomeMessage st )
272+ => (forall (st :: ps ). annotator st -> f (SomeMessage st ))
273+ -> (m (Maybe bytes ) -> channel )
274+ -> (forall (st :: ps ).
275+ channel
276+ -> Maybe bytes
277+ -> DecodeStep bytes failure m (f (SomeMessage st ))
278+ -> m (Either failure (SomeMessage st )))
246279 -> (bytes -> [[bytes ]])
247280 -- ^ alternative re-chunkings of serialised form
248281 -> (forall a . m a -> a )
249- -> CodecF ps failure m f bytes
282+ -> CodecF ps failure m annotator bytes
250283 -> AnyMessage ps
251284 -> Property
252- prop_codecF_splits runF splits runM codec msg =
253- runM $ prop_codecF_splitsM runF splits codec msg
285+ prop_codecF_splits runF mkChannel runDecoder' splits runM codec msg =
286+ runM $ prop_codecF_splitsM runF mkChannel runDecoder' splits codec msg
254287
255288-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
256289--
257290prop_codec_splits
258- :: forall ps failure m bytes .
259- ( Monad m
260- , Eq (AnyMessage ps )
291+ :: forall ps failure m f bytes channel .
292+ ( Eq (AnyMessage ps )
261293 , Show (AnyMessage ps )
262294 , Show failure
263- , Monoid bytes
295+ , Applicative f
296+ , MonadST m
264297 )
265- => (bytes -> [[bytes ]])
298+ => (m (Maybe bytes ) -> channel )
299+ -> (forall (st :: ps ).
300+ channel
301+ -> Maybe bytes
302+ -> DecodeStep bytes failure m (f (SomeMessage st ))
303+ -> m (Either failure (SomeMessage st )))
304+ -> (bytes -> [[bytes ]])
266305 -- ^ alternative re-chunkings of serialised form
267306 -> (forall a . m a -> a )
268307 -> Codec ps failure m bytes
269308 -> AnyMessage ps
270309 -> Property
271- prop_codec_splits = prop_codecF_splits const
310+ prop_codec_splits = prop_codecF_splits pure
272311
273312-- | Like 'prop_codec_splits' but for 'AnnotatorCodec'.
274313prop_anncodec_splits
275- :: forall ps failure m bytes .
276- ( Monad m
277- , Eq (AnyMessage ps )
314+ :: forall ps failure m bytes channel .
315+ ( Eq (AnyMessage ps )
278316 , Show (AnyMessage ps )
279317 , Show failure
280- , Monoid bytes
318+ , MonadST m
281319 )
282- => (bytes -> [[bytes ]])
320+ => (m (Maybe bytes ) -> channel )
321+ -> (forall (st :: ps ).
322+ channel
323+ -> Maybe bytes
324+ -> DecodeStep bytes failure m (bytes -> SomeMessage st )
325+ -> m (Either failure (SomeMessage st )))
326+ -> (bytes -> [[bytes ]])
283327 -- ^ alternative re-chunkings of serialised form
284328 -> (forall a . m a -> a )
285329 -> AnnotatedCodec ps failure m bytes
0 commit comments