{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module Network.TypedProtocol.PingPong.Client (
PingPongClient(..),
pingPongClientPeer,
PingPongClientPipelined(..),
PingPongSender(..),
pingPongClientPeerPipelined,
) where
import Network.TypedProtocol.Core
import Network.TypedProtocol.Pipelined
import Network.TypedProtocol.PingPong.Type
data PingPongClient m a where
SendMsgPing :: m (PingPongClient m a)
-> PingPongClient m a
SendMsgDone :: a -> PingPongClient m a
pingPongClientPeer
:: Monad m
=> PingPongClient m a
-> Peer PingPong AsClient StIdle m a
pingPongClientPeer :: PingPongClient m a -> Peer PingPong 'AsClient 'StIdle m a
pingPongClientPeer (SendMsgDone a
result) =
WeHaveAgency 'AsClient 'StIdle
-> Message PingPong 'StIdle 'StDone
-> Peer PingPong 'AsClient 'StDone m a
-> Peer PingPong 'AsClient 'StIdle m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
TokIdle) Message PingPong 'StIdle 'StDone
MsgDone (NobodyHasAgency 'StDone -> a -> Peer PingPong 'AsClient 'StDone m a
forall ps (st :: ps) a (pr :: PeerRole) (m :: * -> *).
NobodyHasAgency st -> a -> Peer ps pr st m a
Done NobodyHasAgency 'StDone
TokDone a
result)
pingPongClientPeer (SendMsgPing m (PingPongClient m a)
next) =
WeHaveAgency 'AsClient 'StIdle
-> Message PingPong 'StIdle 'StBusy
-> Peer PingPong 'AsClient 'StBusy m a
-> Peer PingPong 'AsClient 'StIdle m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
TokIdle) Message PingPong 'StIdle 'StBusy
MsgPing (Peer PingPong 'AsClient 'StBusy m a
-> Peer PingPong 'AsClient 'StIdle m a)
-> Peer PingPong 'AsClient 'StBusy m a
-> Peer PingPong 'AsClient 'StIdle m a
forall a b. (a -> b) -> a -> b
$
TheyHaveAgency 'AsClient 'StBusy
-> (forall (st' :: PingPong).
Message PingPong 'StBusy st' -> Peer PingPong 'AsClient st' m a)
-> Peer PingPong 'AsClient 'StBusy m a
forall (pr :: PeerRole) ps (st :: ps) (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr st' m a)
-> Peer ps pr st m a
Await (ServerHasAgency 'StBusy -> PeerHasAgency 'AsServer 'StBusy
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StBusy
TokBusy) ((forall (st' :: PingPong).
Message PingPong 'StBusy st' -> Peer PingPong 'AsClient st' m a)
-> Peer PingPong 'AsClient 'StBusy m a)
-> (forall (st' :: PingPong).
Message PingPong 'StBusy st' -> Peer PingPong 'AsClient st' m a)
-> Peer PingPong 'AsClient 'StBusy m a
forall a b. (a -> b) -> a -> b
$ \Message PingPong 'StBusy st'
MsgPong ->
m (Peer PingPong 'AsClient 'StIdle m a)
-> Peer PingPong 'AsClient 'StIdle m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer PingPong 'AsClient 'StIdle m a)
-> Peer PingPong 'AsClient 'StIdle m a)
-> m (Peer PingPong 'AsClient 'StIdle m a)
-> Peer PingPong 'AsClient 'StIdle m a
forall a b. (a -> b) -> a -> b
$ do
PingPongClient m a
client <- m (PingPongClient m a)
next
Peer PingPong 'AsClient 'StIdle m a
-> m (Peer PingPong 'AsClient 'StIdle m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Peer PingPong 'AsClient 'StIdle m a
-> m (Peer PingPong 'AsClient 'StIdle m a))
-> Peer PingPong 'AsClient 'StIdle m a
-> m (Peer PingPong 'AsClient 'StIdle m a)
forall a b. (a -> b) -> a -> b
$ PingPongClient m a -> Peer PingPong 'AsClient 'StIdle m a
forall (m :: * -> *) a.
Monad m =>
PingPongClient m a -> Peer PingPong 'AsClient 'StIdle m a
pingPongClientPeer PingPongClient m a
client
data PingPongClientPipelined m a where
PingPongClientPipelined ::
PingPongSender Z c m a
-> PingPongClientPipelined m a
data PingPongSender n c m a where
SendMsgPingPipelined
:: m c
-> PingPongSender (S n) c m a
-> PingPongSender n c m a
CollectPipelined
:: Maybe (PingPongSender (S n) c m a)
-> (c -> PingPongSender n c m a)
-> PingPongSender (S n) c m a
SendMsgDonePipelined
:: a -> PingPongSender Z c m a
pingPongClientPeerPipelined
:: Monad m
=> PingPongClientPipelined m a
-> PeerPipelined PingPong AsClient StIdle m a
pingPongClientPeerPipelined :: PingPongClientPipelined m a
-> PeerPipelined PingPong 'AsClient 'StIdle m a
pingPongClientPeerPipelined (PingPongClientPipelined PingPongSender 'Z c m a
peer) =
PeerSender PingPong 'AsClient 'StIdle 'Z c m a
-> PeerPipelined PingPong 'AsClient 'StIdle m a
forall ps (pr :: PeerRole) (st :: ps) c (m :: * -> *) a.
PeerSender ps pr st 'Z c m a -> PeerPipelined ps pr st m a
PeerPipelined (PingPongSender 'Z c m a
-> PeerSender PingPong 'AsClient 'StIdle 'Z c m a
forall (m :: * -> *) (n :: N) c a.
Monad m =>
PingPongSender n c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a
pingPongClientPeerSender PingPongSender 'Z c m a
peer)
pingPongClientPeerSender
:: Monad m
=> PingPongSender n c m a
-> PeerSender PingPong AsClient StIdle n c m a
pingPongClientPeerSender :: PingPongSender n c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a
pingPongClientPeerSender (SendMsgDonePipelined a
result) =
WeHaveAgency 'AsClient 'StIdle
-> Message PingPong 'StIdle 'StDone
-> PeerSender PingPong 'AsClient 'StDone 'Z c m a
-> PeerSender PingPong 'AsClient 'StIdle 'Z c m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) c (m :: * -> *)
a.
WeHaveAgency pr st
-> Message ps st st'
-> PeerSender ps pr st' 'Z c m a
-> PeerSender ps pr st 'Z c m a
SenderYield
(ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
TokIdle)
Message PingPong 'StIdle 'StDone
MsgDone
(NobodyHasAgency 'StDone
-> a -> PeerSender PingPong 'AsClient 'StDone 'Z c m a
forall ps (st :: ps) a (pr :: PeerRole) c (m :: * -> *).
NobodyHasAgency st -> a -> PeerSender ps pr st 'Z c m a
SenderDone NobodyHasAgency 'StDone
TokDone a
result)
pingPongClientPeerSender (SendMsgPingPipelined m c
receive PingPongSender ('S n) c m a
next) =
WeHaveAgency 'AsClient 'StIdle
-> Message PingPong 'StIdle 'StBusy
-> PeerReceiver PingPong 'AsClient 'StBusy 'StIdle m c
-> PeerSender PingPong 'AsClient 'StIdle ('S n) c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (st'' :: ps)
(m :: * -> *) c (n :: N) a.
WeHaveAgency pr st
-> Message ps st st'
-> PeerReceiver ps pr st' st'' m c
-> PeerSender ps pr st'' ('S n) c m a
-> PeerSender ps pr st n c m a
SenderPipeline
(ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
TokIdle)
Message PingPong 'StIdle 'StBusy
MsgPing
(TheyHaveAgency 'AsClient 'StBusy
-> (forall (st' :: PingPong).
Message PingPong 'StBusy st'
-> PeerReceiver PingPong 'AsClient st' 'StIdle m c)
-> PeerReceiver PingPong 'AsClient 'StBusy 'StIdle m c
forall (pr :: PeerRole) ps (st :: ps) (stdone :: ps) (m :: * -> *)
c.
TheyHaveAgency pr st
-> (forall (st' :: ps).
Message ps st st' -> PeerReceiver ps pr st' stdone m c)
-> PeerReceiver ps pr st stdone m c
ReceiverAwait (ServerHasAgency 'StBusy -> PeerHasAgency 'AsServer 'StBusy
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StBusy
TokBusy) ((forall (st' :: PingPong).
Message PingPong 'StBusy st'
-> PeerReceiver PingPong 'AsClient st' 'StIdle m c)
-> PeerReceiver PingPong 'AsClient 'StBusy 'StIdle m c)
-> (forall (st' :: PingPong).
Message PingPong 'StBusy st'
-> PeerReceiver PingPong 'AsClient st' 'StIdle m c)
-> PeerReceiver PingPong 'AsClient 'StBusy 'StIdle m c
forall a b. (a -> b) -> a -> b
$ \Message PingPong 'StBusy st'
MsgPong ->
m (PeerReceiver PingPong 'AsClient st' st' m c)
-> PeerReceiver PingPong 'AsClient st' st' m c
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (stdone :: ps)
c.
m (PeerReceiver ps pr st stdone m c)
-> PeerReceiver ps pr st stdone m c
ReceiverEffect (m (PeerReceiver PingPong 'AsClient st' st' m c)
-> PeerReceiver PingPong 'AsClient st' st' m c)
-> m (PeerReceiver PingPong 'AsClient st' st' m c)
-> PeerReceiver PingPong 'AsClient st' st' m c
forall a b. (a -> b) -> a -> b
$ do
c
x <- m c
receive
PeerReceiver PingPong 'AsClient st' st' m c
-> m (PeerReceiver PingPong 'AsClient st' st' m c)
forall (m :: * -> *) a. Monad m => a -> m a
return (c -> PeerReceiver PingPong 'AsClient st' st' m c
forall c ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
c -> PeerReceiver ps pr st st m c
ReceiverDone c
x))
(PingPongSender ('S n) c m a
-> PeerSender PingPong 'AsClient 'StIdle ('S n) c m a
forall (m :: * -> *) (n :: N) c a.
Monad m =>
PingPongSender n c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a
pingPongClientPeerSender PingPongSender ('S n) c m a
next)
pingPongClientPeerSender (CollectPipelined Maybe (PingPongSender ('S n) c m a)
mNone c -> PingPongSender n c m a
collect) =
Maybe (PeerSender PingPong 'AsClient 'StIdle ('S n) c m a)
-> (c -> PeerSender PingPong 'AsClient 'StIdle n c m a)
-> PeerSender PingPong 'AsClient 'StIdle ('S n) c m a
forall ps (pr :: PeerRole) (st :: ps) (n1 :: N) c (m :: * -> *) a.
Maybe (PeerSender ps pr st ('S n1) c m a)
-> (c -> PeerSender ps pr st n1 c m a)
-> PeerSender ps pr st ('S n1) c m a
SenderCollect
((PingPongSender ('S n) c m a
-> PeerSender PingPong 'AsClient 'StIdle ('S n) c m a)
-> Maybe (PingPongSender ('S n) c m a)
-> Maybe (PeerSender PingPong 'AsClient 'StIdle ('S n) c m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PingPongSender ('S n) c m a
-> PeerSender PingPong 'AsClient 'StIdle ('S n) c m a
forall (m :: * -> *) (n :: N) c a.
Monad m =>
PingPongSender n c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a
pingPongClientPeerSender Maybe (PingPongSender ('S n) c m a)
mNone)
(PingPongSender n c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a
forall (m :: * -> *) (n :: N) c a.
Monad m =>
PingPongSender n c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a
pingPongClientPeerSender (PingPongSender n c m a
-> PeerSender PingPong 'AsClient 'StIdle n c m a)
-> (c -> PingPongSender n c m a)
-> c
-> PeerSender PingPong 'AsClient 'StIdle n c m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> PingPongSender n c m a
collect)