Skip to content

Commit

Permalink
Merge pull request #61 from input-output-hk/coot/stateful
Browse files Browse the repository at this point in the history
Better stateful API
  • Loading branch information
coot authored Sep 26, 2024
2 parents cd80ff7 + dc0105c commit d127d3e
Show file tree
Hide file tree
Showing 18 changed files with 159 additions and 100 deletions.
5 changes: 3 additions & 2 deletions .github/workflows/github-page.yml
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
name: Haddocks

on:
schedule:
- cron: '0 0 * * *'
push:
branches:
- main
workflow_dispatch:

jobs:
Expand Down
16 changes: 8 additions & 8 deletions typed-protocols-cborg/typed-protocols-cborg.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
cabal-version: 3.0
cabal-version: 3.4
name: typed-protocols-cborg
version: 0.2.0.0
version: 0.3.0.0
synopsis: CBOR codecs for typed-protocols
-- description:
license: Apache-2.0
Expand All @@ -18,13 +18,13 @@ extra-source-files: CHANGELOG.md, README.md
library
exposed-modules: Network.TypedProtocol.Codec.CBOR

build-depends: base >=4.12 && <4.21,
bytestring >=0.10 && <0.13,
cborg >=0.2.1 && <0.3,
singletons,
build-depends: base >=4.12 && <4.21,
bytestring >=0.10 && <0.13,
cborg >=0.2.1 && <0.3,
singletons,

io-classes ^>=1.5,
typed-protocols
io-classes ^>=1.5,
typed-protocols ^>=0.3

hs-source-dirs: src
default-language: Haskell2010
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,12 +30,12 @@ reqRespClientPeer
-> Client (ReqResp req) StIdle State m a

reqRespClientPeer (SendMsgDone a) =
Yield StateDone MsgDone (Done a)
Yield StateIdle StateDone MsgDone (Done a)

reqRespClientPeer (SendMsgReq req next) =
Yield (StateBusy req)
Yield StateIdle (StateBusy req)
(MsgReq req) $
Await $ \_ (MsgResp _ resp) ->
Await $ \_ (MsgResp resp) ->
let client = next resp
in ( Effect $ reqRespClientPeer <$> client
, StateIdle
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,12 @@ codecReqResp
codecReqResp encodeReq decodeReq encodeResp decodeResp =
Codec { encode, decode }
where
encode :: State st'
encode :: State st
-> Message (ReqResp req) st st'
-> String
encode _ (MsgReq req) = "MsgReq " ++ encodeReq req ++ "\n"
encode _ MsgDone = "MsgDone\n"
encode _ (MsgResp req resp) = "MsgResp " ++ encodeResp req resp ++ "\n"
encode (StateBusy req) (MsgResp resp) = "MsgResp " ++ encodeResp req resp ++ "\n"

decode :: forall (st :: ReqResp req).
ActiveState st
Expand All @@ -60,7 +60,7 @@ codecReqResp encodeReq decodeReq encodeResp decodeResp =
(SingBusy, StateBusy req, ("MsgResp", str'))
-- note that we need `req` to decode response of the given type
| Just resp <- decodeResp req str'
-> DecodeDone (SomeMessage (MsgResp req resp)) trailing
-> DecodeDone (SomeMessage (MsgResp resp)) trailing
(_, _, _) -> DecodeFail failure
where failure = CodecFailure ("unexpected server message: " ++ str)

Expand Down Expand Up @@ -106,7 +106,7 @@ codecReqRespId eqRespTypes = Codec { encode, decode }

msgRespType :: forall resp. Message (ReqResp FileAPI) (StBusy resp) StIdle
-> Proxy resp
msgRespType (MsgResp _ _) = Proxy
msgRespType (MsgResp _) = Proxy

reqRespType :: forall resp. FileAPI resp -> Proxy resp
reqRespType _ = Proxy
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ reqRespServerPeer ReqRespServer { reqRespServerDone = a,
MsgDone -> (Done a, StateDone)
MsgReq req ->
( Effect $
(\(resp, k') -> Yield StateIdle (MsgResp req resp) (reqRespServerPeer k'))
(\(resp, k') -> Yield (StateBusy req) StateIdle (MsgResp resp) (reqRespServerPeer k'))
<$> k req
, StateBusy req
)
Original file line number Diff line number Diff line change
Expand Up @@ -54,12 +54,7 @@ instance Protocol (ReqResp req) where
-- promoted to the state `StBusy` state.
-> Message (ReqResp req) StIdle (StBusy resp)
MsgResp :: Typeable resp
=> req resp -- ^ request, not sent over the wire, just useful in the
-- codec.
--
-- TODO: https://github.com/input-output-hk/typed-protocols/issues/59

-> resp -- ^ respond
=> resp -- ^ respond
-> Message (ReqResp req) (StBusy resp) StIdle
MsgDone :: Message (ReqResp req) StIdle StDone

Expand Down
6 changes: 3 additions & 3 deletions typed-protocols-examples/typed-protocols-examples.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
cabal-version: 3.0
cabal-version: 3.4
name: typed-protocols-examples
version: 0.4.0.0
version: 0.5.0.0
synopsis: Examples and tests for the typed-protocols framework
-- description:
license: Apache-2.0
Expand Down Expand Up @@ -63,7 +63,7 @@ library
si-timers,
network,
time,
typed-protocols ^>= 0.2,
typed-protocols ^>= 0.3,
typed-protocols-cborg,
typed-protocols-stateful

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ mkCodecCborStrictBS
=> (forall (st :: ps) (st' :: ps).
StateTokenI st
=>ActiveState st
=> f st' -> Message ps st st' -> CBOR.Encoding)
=> f st -> Message ps st st' -> CBOR.Encoding)
-- ^ cbor encoder

-> (forall (st :: ps) s.
Expand Down Expand Up @@ -90,7 +90,7 @@ mkCodecCborLazyBS
=> (forall (st :: ps) (st' :: ps).
StateTokenI st
=> ActiveState st
=> f st'
=> f st
-> Message ps st st' -> CBOR.Encoding)
-- ^ cbor encoder

Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
cabal-version: 3.0
cabal-version: 3.4
name: typed-protocols-stateful-cborg
version: 0.2.0.0
version: 0.3.0.0
synopsis: CBOR codecs for typed-protocols
-- description:
license: Apache-2.0
Expand All @@ -25,7 +25,7 @@ library
singletons,

io-classes,
typed-protocols,
typed-protocols ^>= 0.3,
typed-protocols-cborg,
typed-protocols-stateful

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,8 @@ module Network.TypedProtocol.Stateful.Codec
-- * CodecFailure
, CodecFailure (..)
-- * Testing codec properties
, AnyMessage (..)
, pattern AnyMessageAndAgency
, AnyMessage (.., AnyMessageAndAgency)
, showAnyMessage
, prop_codecM
, prop_codec
, prop_codec_splitsM
Expand All @@ -59,7 +59,7 @@ import Network.TypedProtocol.Codec (CodecFailure (..),
DecodeStep (..), SomeMessage (..), hoistDecodeStep,
isoDecodeStep, mapFailureDecodeStep, runDecoder,
runDecoderPure)
import qualified Network.TypedProtocol.Codec as TP
import qualified Network.TypedProtocol.Codec as TP hiding (AnyMessageAndAgency)


-- | A stateful codec.
Expand All @@ -68,14 +68,23 @@ data Codec ps failure (f :: ps -> Type) m bytes = Codec {
encode :: forall (st :: ps) (st' :: ps).
StateTokenI st
=> ActiveState st
=> f st'
=> f st
-- local state, which contain extra context for the encoding
-- process.
--
-- TODO: input-output-hk/typed-protocols#57
-> Message ps st st'
-- message to be encoded
-> bytes,

decode :: forall (st :: ps).
ActiveState st
=> StateToken st
-> f st
-- local state, which can contain extra context from the
-- previous message.
--
-- TODO: input-output-hk/typed-protocols#57
-> m (DecodeStep bytes failure m (SomeMessage st))
}

Expand Down Expand Up @@ -130,22 +139,32 @@ data AnyMessage ps (f :: ps -> Type) where
, ActiveState st
)
=> f st
-> f st'
-- ^ local state
-> Message ps (st :: ps) (st' :: ps)
-- ^ protocol messsage
-> AnyMessage ps f

instance ( forall (st :: ps) (st' :: ps). Show (Message ps st st')
, forall (st :: ps). Show (f st)
)
=> Show (AnyMessage ps f) where
show (AnyMessage st st' msg) = concat [ "AnyMessage "
, show st
, " "
, show st'
, " "
, show msg
]

-- | `showAnyMessage` is can be used to provide `Show` instance for
-- `AnyMessage` if showing `Message` is independent of the state or one accepts
-- showing only partial information included in message constructors or accepts
-- message constructors to carry `Show` instances for its arguments. Note that
-- the proper solution is to define a custom `Show (AnyMessage ps f)` instance
-- for a protocol `ps`, which give access to the state functor `f` in scope of
-- `show`.
--
showAnyMessage :: forall ps f.
( forall st st'. Show (Message ps st st')
, forall st. Show (f st)
)
=> AnyMessage ps f
-> String
showAnyMessage (AnyMessage st msg) =
concat [ "AnyMessage "
, show st
, " "
, show msg
]


-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the
Expand All @@ -156,10 +175,9 @@ pattern AnyMessageAndAgency :: forall ps f. ()
(StateTokenI st, ActiveState st)
=> StateToken st
-> f st
-> f st'
-> Message ps st st'
-> AnyMessage ps f
pattern AnyMessageAndAgency stateToken f f' msg <- AnyMessage f f' (getAgency -> (msg, stateToken))
pattern AnyMessageAndAgency stateToken f msg <- AnyMessage f (getAgency -> (msg, stateToken))
where
AnyMessageAndAgency _ msg = AnyMessage msg
{-# COMPLETE AnyMessageAndAgency #-}
Expand All @@ -169,28 +187,29 @@ pattern AnyMessageAndAgency stateToken f f' msg <- AnyMessage f f' (getAgency ->
getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st)
getAgency msg = (msg, stateToken)


-- | The 'Codec' round-trip property: decode after encode gives the same
-- message. Every codec must satisfy this property.
--
prop_codecM
:: forall ps failure f m bytes.
( Monad m
, Eq (TP.AnyMessage ps)
, Eq (AnyMessage ps f)
)
=> Codec ps failure f m bytes
-> AnyMessage ps f
-> m Bool
prop_codecM Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st')) = do
r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f' msg]
prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg]
case r :: Either failure (SomeMessage st) of
Right (SomeMessage msg') -> return $ TP.AnyMessage msg' == TP.AnyMessage msg
Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
Left _ -> return False

-- | The 'Codec' round-trip property in a pure monad.
--
prop_codec
:: forall ps failure f m bytes.
(Monad m, Eq (TP.AnyMessage ps))
(Monad m, Eq (AnyMessage ps f))
=> (forall a. m a -> a)
-> Codec ps failure f m bytes
-> AnyMessage ps f
Expand All @@ -212,28 +231,28 @@ prop_codec runM codec msg =
--
prop_codec_splitsM
:: forall ps failure f m bytes.
(Monad m, Eq (TP.AnyMessage ps))
(Monad m, Eq (AnyMessage ps f))
=> (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form
-> Codec ps failure f m bytes
-> AnyMessage ps f
-> m Bool
prop_codec_splitsM splits
Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st')) = do
Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
and <$> sequence
[ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes'
case r :: Either failure (SomeMessage st) of
Right (SomeMessage msg') -> return $ TP.AnyMessage msg' == TP.AnyMessage msg
Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
Left _ -> return False

| let bytes = encode f' msg
| let bytes = encode f msg
, bytes' <- splits bytes ]


-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
--
prop_codec_splits
:: forall ps failure f m bytes.
(Monad m, Eq (TP.AnyMessage ps))
(Monad m, Eq (AnyMessage ps f))
=> (bytes -> [[bytes]])
-> (forall a. m a -> a)
-> Codec ps failure f m bytes
Expand All @@ -250,30 +269,30 @@ prop_codec_splits splits runM codec msg =
prop_codecs_compatM
:: forall ps failure f m bytes.
( Monad m
, Eq (TP.AnyMessage ps)
, Eq (AnyMessage ps f)
, forall a. Monoid a => Monoid (m a)
)
=> Codec ps failure f m bytes
-> Codec ps failure f m bytes
-> AnyMessage ps f
-> m Bool
prop_codecs_compatM codecA codecB
(AnyMessage f f' (msg :: Message ps st st')) =
getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f' msg]
a@(AnyMessage f (msg :: Message ps st st')) =
getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg]
case r :: Either failure (SomeMessage st) of
Right (SomeMessage msg') -> return $ All $ TP.AnyMessage msg' == TP.AnyMessage msg
Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
Left _ -> return $ All False
<> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f' msg]
<> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg]
case r :: Either failure (SomeMessage st) of
Right (SomeMessage msg') -> return $ All $ TP.AnyMessage msg' == TP.AnyMessage msg
Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
Left _ -> return $ All False

-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
--
prop_codecs_compat
:: forall ps failure f m bytes.
( Monad m
, Eq (TP.AnyMessage ps)
, Eq (AnyMessage ps f)
, forall a. Monoid a => Monoid (m a)
)
=> (forall a. m a -> a)
Expand Down
Loading

0 comments on commit d127d3e

Please sign in to comment.