Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
39 commits
Select commit Hold shift + click to select a range
08ee7c4
typed-protocols: new API
coot Jul 25, 2024
81f2fbe
typed-protocols: Peer pattern synonyms
coot Jul 25, 2024
fe36759
typed-protocols-examples: updated
coot Jul 25, 2024
88d246f
typed-protocols: ActiveAgency
coot Sep 6, 2021
b121a80
typed-protocols: simplify runPeerWithDriver
coot Mar 27, 2022
bdf8100
typed-protocols: internal lemmas module
coot May 23, 2022
564da48
typed-protocols: provide ReflRelativeAgency type aliases
coot Jul 13, 2022
6f5ce41
typed-protocols-examples: socketAsChannel
coot Sep 4, 2021
c69993a
typed-protocols-examples: ReqResp2 example
coot Sep 17, 2021
e4bcf98
typed-protocols-examples: Wedge
coot Sep 18, 2021
86d007a
typed-protocols-examples: requestOnce
coot Sep 28, 2021
b4070d4
typed-protocols-examples: fixed cborg tests
coot Oct 2, 2021
74a64f2
typed-protocols-examples: pipelined tests
coot Oct 2, 2021
5ef5f2d
typed-protocols-examples: unbounded buffered channel
coot Mar 27, 2022
ce833a9
typed-protocols-examples: added runConnectedPeersAsymetric
coot Mar 27, 2022
1ca4aa7
typed-protocols: simplify evidence of termination in a terminal state
coot May 13, 2022
558a9fc
typed-protocols: added StateToken type family to Protocol type class
coot Jun 23, 2022
03270e4
typed-protocols: renamed Pipelined kind to IsPipelined
coot Jul 13, 2022
6b6118d
typed-protocols: added AnyMessageAndAgency pattern synonym
coot Sep 8, 2023
abecdaf
typed-protocols: added application specific singletons for protocol s…
coot Sep 26, 2023
a81caa1
typed-protocols-examples: relaxed constraint in PingPong client
coot Jul 1, 2022
166f5af
typed-protocols-examples: fixed a socket test on macos
coot Aug 17, 2022
f5ccedd
typed-protocols: bump version to `0.2.0.0`
coot Aug 25, 2023
148a91b
Added CHANGELOG and bumped versions of the packages
coot May 17, 2022
6c6a8ce
typed-protocols: moved outstanding counter into IsPipelined kind
coot Jul 23, 2024
d2f1e74
typed-protocols-stateful: non-pipelined stateful Peer
coot Jul 24, 2024
0d9cb77
typed-protocols: moved types to `Core` module
coot Jul 24, 2024
5ec9a8c
typed-protocols: connectPipelined type signature
coot Jul 24, 2024
8d31814
typed-protocols: added PeerPipelined newtype wrapper
coot Jul 24, 2024
b3ba779
Support io-classes-1.7
coot Jul 26, 2024
b23f327
typed-protocols: added haddocks
coot Aug 19, 2024
72a799c
disabled `typed-protocols-doc` in GHA
coot Aug 22, 2024
5cf79f3
stylish-haskell: fixes
coot Aug 22, 2024
b9e71bb
typed-protocols: removed unused extensions
coot Aug 23, 2024
20aa2fe
Improved haddocks, removed unused pragmas (extensions)
coot Aug 23, 2024
bdcf30a
Core module cannot be checked with stylish-haskell
coot Aug 23, 2024
0042b72
Removed Stateful PingPong example
coot Sep 4, 2024
b195c92
Stateful RPC example
coot Sep 5, 2024
f451040
typed-protocols: fixed typos
coot Sep 14, 2024
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
Prev Previous commit
Next Next commit
Stateful RPC example
  • Loading branch information
coot committed Sep 16, 2024
commit b195c921250444399522980bf086010af47018cc
Original file line number Diff line number Diff line change
Expand Up @@ -39,12 +39,12 @@ codecReqResp =
decodeTerminatedFrame '\n' $ \str trailing ->
case (stok, break (==' ') str) of
(SingIdle, ("MsgReq", str'))
| Just resp <- readMaybe str'
-> DecodeDone (SomeMessage (MsgReq resp)) trailing
| Just req <- readMaybe str'
-> DecodeDone (SomeMessage (MsgReq req)) trailing
(SingIdle, ("MsgDone", ""))
-> DecodeDone (SomeMessage MsgDone) trailing
(SingBusy, ("MsgResp", str'))
| Just resp <- readMaybe str'
| Just resp <- readMaybe str'
-> DecodeDone (SomeMessage (MsgResp resp)) trailing

(_ , _ ) -> DecodeFail failure
Expand Down
Original file line number Diff line number Diff line change
@@ -1,52 +1,42 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Network.TypedProtocol.Stateful.ReqResp.Client
( -- * Non-Pipelined Client
ReqRespClient (..)
( ReqRespClient (..)
, reqRespClientPeer
) where

import Data.Kind (Type)

import Network.TypedProtocol.ReqResp.Type
import Data.Typeable
import Network.TypedProtocol.Stateful.Peer.Client
import Network.TypedProtocol.Stateful.ReqResp.Type

data ReqRespClient req m a where
SendMsgReq :: Typeable resp
=> req resp
-> (resp -> m (ReqRespClient req m a))
-> ReqRespClient req m a

data ReqRespClient req resp (f :: ReqResp req resp -> Type) m a where
SendMsgReq :: f StBusy
-> req
-> (f StBusy -> resp -> ( m (ReqRespClient req resp f m a)
, f StIdle
))
-> ReqRespClient req resp f m a

SendMsgDone :: f StDone
-> m a
-> ReqRespClient req resp f m a
SendMsgDone :: a
-> ReqRespClient req m a


reqRespClientPeer
:: Monad m
=> ReqRespClient req resp f m a
-> Client (ReqResp req resp) StIdle f m a

reqRespClientPeer (SendMsgDone f result) =
Effect $ do
r <- result
return $ Yield f MsgDone (Done r)

reqRespClientPeer (SendMsgReq f req next) =
Yield f (MsgReq req) $
Await $ \f' (MsgResp resp) ->
case next f' resp of
(client, f'') ->
( Effect $ reqRespClientPeer <$> client
, f''
)
=> ReqRespClient req m a
-> Client (ReqResp req) StIdle State m a

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

reqRespClientPeer (SendMsgReq req next) =
Yield (StateBusy req)
(MsgReq req) $
Await $ \_ (MsgResp resp) ->
let client = next resp
in ( Effect $ reqRespClientPeer <$> client
, StateIdle
)
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Network.TypedProtocol.Stateful.ReqResp.Codec where

import Data.Kind (Type)
import Data.Singletons.Decide
import Data.Typeable
import Network.TypedProtocol.Core
import Network.TypedProtocol.PingPong.Codec (decodeTerminatedFrame)
import Network.TypedProtocol.Stateful.Codec
import Network.TypedProtocol.Stateful.ReqResp.Type

data Some (f :: k -> Type) where
Some :: Typeable a => f a -> Some f


-- | Codec polymorphic in the RPC (e.g. `req` type)
--
codecReqResp
:: forall req m. Monad m
=> (forall resp. req resp -> String)
-- ^ encode `req resp`
-> (String -> Maybe (Some req))
-- ^ decode `req resp`
-> (forall resp. resp -> String)
-- ^ encode resp
-> (forall resp. req resp -> String -> Maybe resp)
-- ^ decode resp
-> Codec (ReqResp req) CodecFailure State m String
codecReqResp encodeReq decodeReq encodeResp decodeResp =
Codec { encode, decode }
where
encode :: State st'
-> Message (ReqResp req) st st'
-> String
encode _ (MsgReq req) = "MsgReq " ++ encodeReq req ++ "\n"
encode _ MsgDone = "MsgDone\n"
encode _ (MsgResp resp) = "MsgResp " ++ encodeResp resp ++ "\n"

decode :: forall (st :: ReqResp req).
ActiveState st
=> StateToken st
-> State st
-> m (DecodeStep String CodecFailure m (SomeMessage st))
decode stok state =
decodeTerminatedFrame '\n' $ \str trailing ->
case (stok, state, break (==' ') str) of
(SingIdle, StateIdle, ("MsgReq", str'))
| Just (Some req) <- decodeReq str'
-> DecodeDone (SomeMessage (MsgReq req)) trailing
(SingIdle, StateIdle, ("MsgDone", ""))
-> DecodeDone (SomeMessage MsgDone) trailing
(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 resp)) trailing
(_, _, _) -> DecodeFail failure
where failure = CodecFailure ("unexpected server message: " ++ str)


data Bytes where
Bytes :: Message (ReqResp FileAPI) st st' -> Bytes

-- | An identity codec which wraps messages into `AnyMessage`.
--
codecReqRespId
:: forall m.
Applicative m
=> (forall (res1 :: Type) (res2 :: Type).
(Typeable res1, Typeable res2)
=> Proxy res1
-> Proxy res2
-> Maybe (res1 :~: res2)
)
-> Codec FileRPC String State m Bytes
codecReqRespId eqRespTypes = Codec { encode, decode }
where
encode _ = Bytes

decode :: forall (st :: ReqResp FileAPI).
ActiveState st
=> StateToken st
-> State st
-> m (DecodeStep Bytes String m (SomeMessage st))
decode stok state = pure $ DecodePartial $ \bytes -> pure $
case (stok, state, bytes) of
(SingIdle, StateIdle, Just (Bytes msg@MsgDone))
-> DecodeDone (SomeMessage msg) Nothing
(SingIdle, StateIdle, Just (Bytes msg@MsgReq{}))
-> DecodeDone (SomeMessage msg) Nothing
(SingBusy, StateBusy req, Just (Bytes msg@(MsgResp _)))
-- the codec needs to verify that response type of `req` and `msg` agrees
| Just Refl <- eqRespTypes (reqRespType req) (msgRespType msg)
-> DecodeDone (SomeMessage msg) Nothing

(SingDone, _, _) -> notActiveState stok
(_, _, Nothing) -> DecodeFail "no bytes"
(_, _, _) -> DecodeFail "no matching message"

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

reqRespType :: forall resp. FileAPI resp -> Proxy resp
reqRespType _ = Proxy


Original file line number Diff line number Diff line change
Expand Up @@ -2,49 +2,32 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Network.TypedProtocol.Stateful.ReqResp.Examples
( ReqRespStateCallbacks (..)
, reqRespClientMap
) where
module Network.TypedProtocol.Stateful.ReqResp.Examples where

import Data.Kind (Type)
import Network.TypedProtocol.Stateful.ReqResp.Server
import Network.TypedProtocol.Stateful.ReqResp.Type

import Network.TypedProtocol.ReqResp.Type
import Network.TypedProtocol.Stateful.ReqResp.Client

fileRPCServer :: Monad m
=> (forall resp. FileAPI resp -> m resp)
-- ^ execute `FileAPI` locally
-> ReqRespServer FileAPI m ()
fileRPCServer run = ReqRespServer {
reqRespServerDone = (),
reqRespHandleReq = \req -> do
resp <- run req
return (resp, fileRPCServer run)
}

data ReqRespStateCallbacks (f :: ReqResp req resp -> Type) =
ReqRespStateCallbacks {
rrBusyToIdle :: f StBusy -> f StIdle
, rrBusyToBusy :: f StBusy -> f StBusy
, rrBusyToDone :: f StBusy -> f StDone
}
-- | Example of a file API
--
simpleFileAPI :: Monad m => FileAPI resp -> m resp
simpleFileAPI (ReadFile filepath) = return filepath
simpleFileAPI (WriteFile _ _) = return ()

reqRespClientMap
:: forall req resp f m.
Monad m
=> ReqRespStateCallbacks f
-> f StBusy
-> [req]
-> ReqRespClient req resp f m ([resp], f StDone)
reqRespClientMap ReqRespStateCallbacks
{ rrBusyToIdle
, rrBusyToBusy
, rrBusyToDone
} = go []
where
go :: [resp]
-> f StBusy
-> [req]
-> ReqRespClient req resp f m ([resp], f StDone)
go resps f [] = SendMsgDone f' (pure (reverse resps, f'))
where
f' = rrBusyToDone f
go resps f (req:reqs) =
SendMsgReq f req $ \f' resp ->
( return (go (resp:resps) (rrBusyToBusy f') reqs)
, rrBusyToIdle f'
)
simpleFileRPCServer :: Monad m => ReqRespServer FileAPI m ()
simpleFileRPCServer = fileRPCServer simpleFileAPI

Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Network.TypedProtocol.Stateful.ReqResp.Server
( ReqRespServer (..)
, reqRespServerPeer
) where

import Data.Typeable
import Network.TypedProtocol.Stateful.Peer.Server
import Network.TypedProtocol.Stateful.ReqResp.Type


data ReqRespServer req m a = ReqRespServer {
reqRespServerDone :: a,
reqRespHandleReq :: forall resp. Typeable resp => req resp -> m (resp, ReqRespServer req m a)
}

reqRespServerPeer :: Functor m
=> ReqRespServer req m a
-> Server (ReqResp req) StIdle State m a
reqRespServerPeer ReqRespServer { reqRespServerDone = a,
reqRespHandleReq = k } =
Await $ \_ -> \case
MsgDone -> (Done a, StateDone)
MsgReq req ->
( Effect $
(\(resp, k') -> Yield StateIdle (MsgResp resp) (reqRespServerPeer k'))
<$> k req
, StateBusy req
)
Loading