{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

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

import           Network.TypedProtocol.Core
import           Network.TypedProtocol.Peer.Client
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
  :: Functor m
  => PingPongClient m a
  -> Client PingPong NonPipelined StIdle m a

pingPongClientPeer :: forall (m :: * -> *) a.
Functor m =>
PingPongClient m a -> Client PingPong 'NonPipelined '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.
    Message PingPong 'StIdle 'StDone
-> Client PingPong 'NonPipelined 'StDone m a
-> Client PingPong 'NonPipelined 'StIdle m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield Message PingPong 'StIdle 'StDone
MsgDone (a -> Client PingPong 'NonPipelined 'StDone m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
a -> Client ps pl st m a
Done a
result)

pingPongClientPeer (SendMsgPing m (PingPongClient m a)
next) =

    -- Send our message.
    Message PingPong 'StIdle 'StBusy
-> Client PingPong 'NonPipelined 'StBusy m a
-> Client PingPong 'NonPipelined 'StIdle m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield Message PingPong 'StIdle 'StBusy
MsgPing (Client PingPong 'NonPipelined 'StBusy m a
 -> Client PingPong 'NonPipelined 'StIdle m a)
-> Client PingPong 'NonPipelined 'StBusy m a
-> Client PingPong 'NonPipelined '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.
    (forall (st' :: PingPong).
 Message PingPong 'StBusy st'
 -> Client PingPong 'NonPipelined st' m a)
-> Client PingPong 'NonPipelined 'StBusy m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Client ps pl st' m a)
-> Client ps pl st m a
Await ((forall (st' :: PingPong).
  Message PingPong 'StBusy st'
  -> Client PingPong 'NonPipelined st' m a)
 -> Client PingPong 'NonPipelined 'StBusy m a)
-> (forall (st' :: PingPong).
    Message PingPong 'StBusy st'
    -> Client PingPong 'NonPipelined st' m a)
-> Client PingPong 'NonPipelined 'StBusy m a
forall a b. (a -> b) -> a -> b
$ \Message PingPong 'StBusy st'
R:MessagePingPongfromto '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 (Client PingPong 'NonPipelined st' m a)
-> Client PingPong 'NonPipelined st' m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client PingPong 'NonPipelined st' m a)
 -> Client PingPong 'NonPipelined st' m a)
-> m (Client PingPong 'NonPipelined st' m a)
-> Client PingPong 'NonPipelined st' m a
forall a b. (a -> b) -> a -> b
$ PingPongClient m a -> Client PingPong 'NonPipelined st' m a
PingPongClient m a -> Client PingPong 'NonPipelined 'StIdle m a
forall (m :: * -> *) a.
Functor m =>
PingPongClient m a -> Client PingPong 'NonPipelined 'StIdle m a
pingPongClientPeer (PingPongClient m a -> Client PingPong 'NonPipelined st' m a)
-> m (PingPongClient m a)
-> m (Client PingPong 'NonPipelined st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (PingPongClient m a)
next


--
-- Pipelined client
--

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


data PingPongClientIdle (n :: N) c m a where
  -- | Send a `Ping` message but alike in `PingPongClient` do not await for the
  -- response, instead supply a monadic action which will run on a received
  -- `Pong` message.
  --
  SendMsgPingPipelined
    :: m c
    -> PingPongClientIdle (S n) c m a -- continuation
    -> PingPongClientIdle    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, which allows to run a monadic action
  --   when 'MsgPong' is received.
  --
  -- 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 (PingPongClientIdle (S n) c m a)
    -> (c -> (PingPongClientIdle    n  c m a))
    ->        PingPongClientIdle (S n) c m a

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



-- | Interpret a pipelined client as a pipelined 'Peer' on the client side of
-- the 'PingPong' protocol.
--
pingPongClientPeerPipelined
  :: Functor m
  => PingPongClientPipelined c m a
  -> ClientPipelined PingPong StIdle m a
pingPongClientPeerPipelined :: forall (m :: * -> *) c a.
Functor m =>
PingPongClientPipelined c m a
-> ClientPipelined PingPong 'StIdle m a
pingPongClientPeerPipelined (PingPongClientPipelined PingPongClientIdle 'Z c m a
peer) =
    Client PingPong ('Pipelined 'Z c) 'StIdle m a
-> ClientPipelined PingPong 'StIdle m a
forall ps (st :: ps) (m :: * -> *) a c.
Client ps ('Pipelined 'Z c) st m a -> ClientPipelined ps st m a
ClientPipelined (Client PingPong ('Pipelined 'Z c) 'StIdle m a
 -> ClientPipelined PingPong 'StIdle m a)
-> Client PingPong ('Pipelined 'Z c) 'StIdle m a
-> ClientPipelined PingPong 'StIdle m a
forall a b. (a -> b) -> a -> b
$ PingPongClientIdle 'Z c m a
-> Client PingPong ('Pipelined 'Z c) 'StIdle m a
forall (n :: N) c (m :: * -> *) a.
Functor m =>
PingPongClientIdle n c m a
-> Client PingPong ('Pipelined n c) 'StIdle m a
pingPongClientPeerIdle PingPongClientIdle 'Z c m a
peer


pingPongClientPeerIdle
  :: forall (n :: N) c m a. Functor m
  => PingPongClientIdle         n c         m a
  -> Client PingPong (Pipelined n c) StIdle m a
pingPongClientPeerIdle :: forall (n :: N) c (m :: * -> *) a.
Functor m =>
PingPongClientIdle n c m a
-> Client PingPong ('Pipelined n c) 'StIdle m a
pingPongClientPeerIdle = PingPongClientIdle n c m a
-> Client PingPong ('Pipelined n c) 'StIdle m a
forall (n' :: N).
PingPongClientIdle n' c m a
-> Client PingPong ('Pipelined n' c) 'StIdle m a
go
  where
    go :: forall (n' :: N).
          PingPongClientIdle         n' c         m a
       -> Client PingPong (Pipelined n' c) StIdle m a

    go :: forall (n' :: N).
PingPongClientIdle n' c m a
-> Client PingPong ('Pipelined n' c) 'StIdle m a
go (SendMsgPingPipelined m c
receive PingPongClientIdle ('S n') c m a
next) =
      -- Pipelined yield: send `MsgPing`, immediately follow with the next step.
      Message PingPong 'StIdle 'StBusy
-> Receiver PingPong 'StBusy 'StIdle m c
-> Client PingPong ('Pipelined ('S n') c) 'StIdle m a
-> Client PingPong ('Pipelined n' c) 'StIdle m a
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
       (st'' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
YieldPipelined
        Message PingPong 'StIdle 'StBusy
MsgPing
        ((forall (st' :: PingPong).
 Message PingPong 'StBusy st' -> Receiver PingPong st' 'StIdle m c)
-> Receiver PingPong 'StBusy 'StIdle m c
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
(StateTokenI st, ActiveState st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 Message ps st st' -> Receiver ps st' stdone m c)
-> Receiver ps st stdone m c
ReceiverAwait ((forall (st' :: PingPong).
  Message PingPong 'StBusy st' -> Receiver PingPong st' 'StIdle m c)
 -> Receiver PingPong 'StBusy 'StIdle m c)
-> (forall (st' :: PingPong).
    Message PingPong 'StBusy st' -> Receiver PingPong st' 'StIdle m c)
-> Receiver PingPong 'StBusy 'StIdle m c
forall a b. (a -> b) -> a -> b
$ \Message PingPong 'StBusy st'
R:MessagePingPongfromto 'StBusy st'
MsgPong ->
            m (Receiver PingPong st' 'StIdle m c)
-> Receiver PingPong st' 'StIdle m c
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
m (Receiver ps st stdone m c) -> Receiver ps st stdone m c
ReceiverEffect (m (Receiver PingPong st' 'StIdle m c)
 -> Receiver PingPong st' 'StIdle m c)
-> m (Receiver PingPong st' 'StIdle m c)
-> Receiver PingPong st' 'StIdle m c
forall a b. (a -> b) -> a -> b
$ c -> Receiver PingPong st' st' m c
c -> Receiver PingPong st' 'StIdle m c
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (c -> Receiver PingPong st' 'StIdle m c)
-> m c -> m (Receiver PingPong st' 'StIdle m c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m c
receive)
        (PingPongClientIdle ('S n') c m a
-> Client PingPong ('Pipelined ('S n') c) 'StIdle m a
forall (n' :: N).
PingPongClientIdle n' c m a
-> Client PingPong ('Pipelined n' c) 'StIdle m a
go PingPongClientIdle ('S n') c m a
next)

    go (CollectPipelined Maybe (PingPongClientIdle ('S n) c m a)
mNone c -> PingPongClientIdle n c m a
collect) =
      Maybe (Client PingPong ('Pipelined ('S n) c) 'StIdle m a)
-> (c -> Client PingPong ('Pipelined n c) 'StIdle m a)
-> Client PingPong ('Pipelined ('S n) c) 'StIdle m a
forall ps (st :: ps) (n :: N) c (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Client ps ('Pipelined ('S n) c) st m a)
-> (c -> Client ps ('Pipelined n c) st m a)
-> Client ps ('Pipelined ('S n) c) st m a
Collect
        (PingPongClientIdle ('S n) c m a
-> Client PingPong ('Pipelined ('S n) c) 'StIdle m a
forall (n' :: N).
PingPongClientIdle n' c m a
-> Client PingPong ('Pipelined n' c) 'StIdle m a
go (PingPongClientIdle ('S n) c m a
 -> Client PingPong ('Pipelined ('S n) c) 'StIdle m a)
-> Maybe (PingPongClientIdle ('S n) c m a)
-> Maybe (Client PingPong ('Pipelined ('S n) c) 'StIdle m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (PingPongClientIdle ('S n) c m a)
mNone)
        (PingPongClientIdle n c m a
-> Client PingPong ('Pipelined n c) 'StIdle m a
forall (n' :: N).
PingPongClientIdle n' c m a
-> Client PingPong ('Pipelined n' c) 'StIdle m a
go (PingPongClientIdle n c m a
 -> Client PingPong ('Pipelined n c) 'StIdle m a)
-> (c -> PingPongClientIdle n c m a)
-> c
-> Client PingPong ('Pipelined n c) 'StIdle m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> PingPongClientIdle n c m a
collect)

    go (SendMsgDonePipelined a
result) =
      -- Send `MsgDone` and complete the protocol
      Message PingPong 'StIdle 'StDone
-> Client PingPong ('Pipelined n' c) 'StDone m a
-> Client PingPong ('Pipelined n' c) 'StIdle m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield
        Message PingPong 'StIdle 'StDone
MsgDone
        (a -> Client PingPong ('Pipelined n' c) 'StDone m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
a -> Client ps pl st m a
Done a
result)