@@ -41,8 +41,8 @@ module Network.TypedProtocol.Stateful.Codec
41
41
-- * CodecFailure
42
42
, CodecFailure (.. )
43
43
-- * Testing codec properties
44
- , AnyMessage (.. )
45
- , pattern AnyMessageAndAgency
44
+ , AnyMessage (.. , AnyMessageAndAgency )
45
+ , showAnyMessage
46
46
, prop_codecM
47
47
, prop_codec
48
48
, prop_codec_splitsM
@@ -59,7 +59,7 @@ import Network.TypedProtocol.Codec (CodecFailure (..),
59
59
DecodeStep (.. ), SomeMessage (.. ), hoistDecodeStep ,
60
60
isoDecodeStep , mapFailureDecodeStep , runDecoder ,
61
61
runDecoderPure )
62
- import qualified Network.TypedProtocol.Codec as TP
62
+ import qualified Network.TypedProtocol.Codec as TP hiding ( AnyMessageAndAgency )
63
63
64
64
65
65
-- | A stateful codec.
@@ -68,14 +68,23 @@ data Codec ps failure (f :: ps -> Type) m bytes = Codec {
68
68
encode :: forall (st :: ps ) (st' :: ps ).
69
69
StateTokenI st
70
70
=> ActiveState st
71
- => f st'
71
+ => f st
72
+ -- local state, which contain extra context for the encoding
73
+ -- process.
74
+ --
75
+ -- TODO: input-output-hk/typed-protocols#57
72
76
-> Message ps st st'
77
+ -- message to be encoded
73
78
-> bytes ,
74
79
75
80
decode :: forall (st :: ps ).
76
81
ActiveState st
77
82
=> StateToken st
78
83
-> f st
84
+ -- local state, which can contain extra context from the
85
+ -- previous message.
86
+ --
87
+ -- TODO: input-output-hk/typed-protocols#57
79
88
-> m (DecodeStep bytes failure m (SomeMessage st ))
80
89
}
81
90
@@ -130,22 +139,32 @@ data AnyMessage ps (f :: ps -> Type) where
130
139
, ActiveState st
131
140
)
132
141
=> f st
133
- -> f st'
142
+ -- ^ local state
134
143
-> Message ps (st :: ps ) (st' :: ps )
144
+ -- ^ protocol messsage
135
145
-> AnyMessage ps f
136
146
137
- instance ( forall (st :: ps ) (st' :: ps ). Show (Message ps st st' )
138
- , forall (st :: ps ). Show (f st )
139
- )
140
- => Show (AnyMessage ps f ) where
141
- show (AnyMessage st st' msg) = concat [ " AnyMessage "
142
- , show st
143
- , " "
144
- , show st'
145
- , " "
146
- , show msg
147
- ]
148
147
148
+ -- | `showAnyMessage` is can be used to provide `Show` instance for
149
+ -- `AnyMessage` if showing `Message` is independent of the state or one accepts
150
+ -- showing only partial information included in message constructors or accepts
151
+ -- message constructors to carry `Show` instances for its arguments. Note that
152
+ -- the proper solution is to define a custom `Show (AnyMessage ps f)` instance
153
+ -- for a protocol `ps`, which give access to the state functor `f` in scope of
154
+ -- `show`.
155
+ --
156
+ showAnyMessage :: forall ps f .
157
+ ( forall st st' . Show (Message ps st st' )
158
+ , forall st . Show (f st )
159
+ )
160
+ => AnyMessage ps f
161
+ -> String
162
+ showAnyMessage (AnyMessage st msg) =
163
+ concat [ " AnyMessage "
164
+ , show st
165
+ , " "
166
+ , show msg
167
+ ]
149
168
150
169
151
170
-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the
@@ -156,10 +175,9 @@ pattern AnyMessageAndAgency :: forall ps f. ()
156
175
(StateTokenI st, ActiveState st)
157
176
=> StateToken st
158
177
-> f st
159
- -> f st'
160
178
-> Message ps st st'
161
179
-> AnyMessage ps f
162
- pattern AnyMessageAndAgency stateToken f f' msg <- AnyMessage f f' (getAgency -> (msg, stateToken))
180
+ pattern AnyMessageAndAgency stateToken f msg <- AnyMessage f (getAgency -> (msg, stateToken))
163
181
where
164
182
AnyMessageAndAgency _ msg = AnyMessage msg
165
183
{-# COMPLETE AnyMessageAndAgency #-}
@@ -169,28 +187,29 @@ pattern AnyMessageAndAgency stateToken f f' msg <- AnyMessage f f' (getAgency ->
169
187
getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st' , StateToken st )
170
188
getAgency msg = (msg, stateToken)
171
189
190
+
172
191
-- | The 'Codec' round-trip property: decode after encode gives the same
173
192
-- message. Every codec must satisfy this property.
174
193
--
175
194
prop_codecM
176
195
:: forall ps failure f m bytes .
177
196
( Monad m
178
- , Eq (TP. AnyMessage ps )
197
+ , Eq (AnyMessage ps f )
179
198
)
180
199
=> Codec ps failure f m bytes
181
200
-> AnyMessage ps f
182
201
-> m Bool
183
- prop_codecM Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st' )) = do
184
- r <- decode (stateToken :: StateToken st ) f >>= runDecoder [encode f' msg]
202
+ prop_codecM Codec {encode, decode} a @ (AnyMessage f (msg :: Message ps st st' )) = do
203
+ r <- decode (stateToken :: StateToken st ) f >>= runDecoder [encode f msg]
185
204
case r :: Either failure (SomeMessage st ) of
186
- Right (SomeMessage msg') -> return $ TP. AnyMessage msg' == TP. AnyMessage msg
205
+ Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
187
206
Left _ -> return False
188
207
189
208
-- | The 'Codec' round-trip property in a pure monad.
190
209
--
191
210
prop_codec
192
211
:: forall ps failure f m bytes .
193
- (Monad m , Eq (TP. AnyMessage ps ))
212
+ (Monad m , Eq (AnyMessage ps f ))
194
213
=> (forall a . m a -> a )
195
214
-> Codec ps failure f m bytes
196
215
-> AnyMessage ps f
@@ -212,28 +231,28 @@ prop_codec runM codec msg =
212
231
--
213
232
prop_codec_splitsM
214
233
:: forall ps failure f m bytes .
215
- (Monad m , Eq (TP. AnyMessage ps ))
234
+ (Monad m , Eq (AnyMessage ps f ))
216
235
=> (bytes -> [[bytes ]]) -- ^ alternative re-chunkings of serialised form
217
236
-> Codec ps failure f m bytes
218
237
-> AnyMessage ps f
219
238
-> m Bool
220
239
prop_codec_splitsM splits
221
- Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st' )) = do
240
+ Codec {encode, decode} a @ (AnyMessage f (msg :: Message ps st st' )) = do
222
241
and <$> sequence
223
242
[ do r <- decode (stateToken :: StateToken st ) f >>= runDecoder bytes'
224
243
case r :: Either failure (SomeMessage st ) of
225
- Right (SomeMessage msg') -> return $ TP. AnyMessage msg' == TP. AnyMessage msg
244
+ Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
226
245
Left _ -> return False
227
246
228
- | let bytes = encode f' msg
247
+ | let bytes = encode f msg
229
248
, bytes' <- splits bytes ]
230
249
231
250
232
251
-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
233
252
--
234
253
prop_codec_splits
235
254
:: forall ps failure f m bytes .
236
- (Monad m , Eq (TP. AnyMessage ps ))
255
+ (Monad m , Eq (AnyMessage ps f ))
237
256
=> (bytes -> [[bytes ]])
238
257
-> (forall a . m a -> a )
239
258
-> Codec ps failure f m bytes
@@ -250,30 +269,30 @@ prop_codec_splits splits runM codec msg =
250
269
prop_codecs_compatM
251
270
:: forall ps failure f m bytes .
252
271
( Monad m
253
- , Eq (TP. AnyMessage ps )
272
+ , Eq (AnyMessage ps f )
254
273
, forall a . Monoid a => Monoid (m a )
255
274
)
256
275
=> Codec ps failure f m bytes
257
276
-> Codec ps failure f m bytes
258
277
-> AnyMessage ps f
259
278
-> m Bool
260
279
prop_codecs_compatM codecA codecB
261
- (AnyMessage f f' (msg :: Message ps st st' )) =
262
- getAll <$> do r <- decode codecB (stateToken :: StateToken st ) f >>= runDecoder [encode codecA f' msg]
280
+ a @ (AnyMessage f (msg :: Message ps st st' )) =
281
+ getAll <$> do r <- decode codecB (stateToken :: StateToken st ) f >>= runDecoder [encode codecA f msg]
263
282
case r :: Either failure (SomeMessage st ) of
264
- Right (SomeMessage msg') -> return $ All $ TP. AnyMessage msg' == TP. AnyMessage msg
283
+ Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
265
284
Left _ -> return $ All False
266
- <> do r <- decode codecA (stateToken :: StateToken st ) f >>= runDecoder [encode codecB f' msg]
285
+ <> do r <- decode codecA (stateToken :: StateToken st ) f >>= runDecoder [encode codecB f msg]
267
286
case r :: Either failure (SomeMessage st ) of
268
- Right (SomeMessage msg') -> return $ All $ TP. AnyMessage msg' == TP. AnyMessage msg
287
+ Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
269
288
Left _ -> return $ All False
270
289
271
290
-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
272
291
--
273
292
prop_codecs_compat
274
293
:: forall ps failure f m bytes .
275
294
( Monad m
276
- , Eq (TP. AnyMessage ps )
295
+ , Eq (AnyMessage ps f )
277
296
, forall a . Monoid a => Monoid (m a )
278
297
)
279
298
=> (forall a . m a -> a )
0 commit comments