{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

module Network.TypedProtocol.PingPong.Client (
    -- * Normal client
    PingPongClient(..),
    pingPongClientPeer,
    -- * Pipelined client
    PingPongClientPipelined(..),
    PingPongSender(..),
    pingPongClientPeerPipelined,
  ) where

import           Network.TypedProtocol.Core
import           Network.TypedProtocol.Pipelined
import           Network.TypedProtocol.PingPong.Type

-- | A ping-pong client, on top of some effect 'm'.
--
-- At each step the client has a choice: ping or stop.
--
-- This type encodes the pattern of state transitions the client can go through.
-- For the ping\/pong case this is trivial. We start from one main state,
-- issue a ping and move into a state where we expect a single response,
-- bringing us back to the same main state.
--
-- If we had another state in which a different set of options were available
-- then we would need a second type like this. The two would be mutually
-- recursive if we can get in both directions, or perhaps just one way such
-- as a special initialising state or special terminating state.
--
data PingPongClient m a where
  -- | Choose to go for sending a ping message. The ping has no body so
  -- all we have to provide here is a continuation for the single legal
  -- reply message.
  --
  SendMsgPing    :: m (PingPongClient m a) -- continuation for Pong response
                 -> PingPongClient m a

  -- | Choose to terminate the protocol. This is an actual but nullary message,
  -- we terminate with the local result value. So this ends up being much like
  -- 'return' in this case, but in general the termination is a message that
  -- can communicate final information.
  --
  SendMsgDone    :: a -> PingPongClient m a


-- | Interpret a particular client action sequence into the client side of the
-- 'PingPong' protocol.
--
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) =
    -- We do an actual transition using 'yield', to go from the 'StIdle' to
    -- 'StDone' state. Once in the 'StDone' state we can actually stop using
    -- 'done', with a return value.
    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) =

    -- Send our message.
    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
$

    -- The type of our protocol means that we're now into the 'StBusy' state
    -- and the only thing we can do next is local effects or wait for a reply.
    -- We'll wait for a reply.
    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 ->

    -- Now in this case there is only one possible response, and we have
    -- one corresponding continuation 'kPong' to handle that response.
    -- The pong reply has no content so there's nothing to pass to our
    -- continuation, but if there were we would.
      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


--
-- Pipelined client
--

-- | A ping-pong client designed for running the 'PingPong' protocol in
-- a pipelined way.
--
data PingPongClientPipelined m a where
  -- | A 'PingPongSender', but starting with zero outstanding pipelined
  -- responses, and for any internal collect type @c@.
  PingPongClientPipelined ::
      PingPongSender      Z c m a
   -> PingPongClientPipelined m a


data PingPongSender n c m a where
  -- | 
  -- Send a `Ping` message but alike in `PingPongClient` do not await for the
  -- resopnse, instead supply a monadic action which will run on a received
  -- `Pong` message.
  SendMsgPingPipelined
    :: m c                        -- pong receive action
    -> PingPongSender (S n) c m a -- continuation
    -> PingPongSender    n  c m a

  -- | Collect the result of a previous pipelined receive action.
  --
  -- This (optionally) provides two choices:
  --
  -- * Continue without a pipelined result
  -- * Continue with a pipelined result
  --
  -- Since presenting the first choice is optional, this allows expressing
  -- both a blocking collect and a non-blocking collect. This allows
  -- implementations to express policies such as sending a short sequence
  -- of messages and then waiting for all replies, but also a maximum pipelining
  -- policy that keeps a large number of messages in flight but collects results
  -- eagerly.
  -- 
  CollectPipelined
    :: Maybe (PingPongSender (S n) c m a)
    -> (c ->  PingPongSender    n  c m a)
    ->        PingPongSender (S n) c m a

  -- | Termination of the ping-pong protocol.
  --
  -- Note that all pipelined results must be collected before terminating.
  --
  SendMsgDonePipelined
    :: a -> PingPongSender Z c m a



-- | Interpret a pipelined client as a 'PeerPipelined' on the client side of
-- the 'PingPong' protocol.
--
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) =
  -- Send `MsgDone` and complete the protocol
  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) =
  -- Pipelined yield: send `MsgPing`, immediately follow with the next step.
  -- Await for a response in a continuation.
  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
    -- response handler
    (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))
    -- run the next step of the ping-pong protocol.
    (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)