Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Better stateful API #61

Merged
merged 5 commits into from
Sep 26, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading