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

module Network.TypedProtocol.PingPong.Server where

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


data PingPongServer m a = PingPongServer {
    -- | The client sent us a ping message. We have no choices here, and
    -- the response is nullary, all we have are local effects.
    PingPongServer m a -> m (PingPongServer m a)
recvMsgPing  :: m (PingPongServer m a)

    -- | The client terminated. Here we have a pure return value, but we
    -- could have done another action in 'm' if we wanted to.
  , PingPongServer m a -> a
recvMsgDone  :: a
  }


-- | Interpret a particular server action sequence into the server side of the
-- 'PingPong' protocol.
--
pingPongServerPeer
  :: Monad m
  => PingPongServer m a
  -> Peer PingPong AsServer StIdle m a
pingPongServerPeer :: PingPongServer m a -> Peer PingPong 'AsServer 'StIdle m a
pingPongServerPeer PingPongServer{a
m (PingPongServer m a)
recvMsgDone :: a
recvMsgPing :: m (PingPongServer m a)
recvMsgDone :: forall (m :: * -> *) a. PingPongServer m a -> a
recvMsgPing :: forall (m :: * -> *) a.
PingPongServer m a -> m (PingPongServer m a)
..} =

    -- In the 'StIdle' the server is awaiting a request message
    TheyHaveAgency 'AsServer 'StIdle
-> (forall (st' :: PingPong).
    Message PingPong 'StIdle st' -> Peer PingPong 'AsServer st' m a)
-> Peer PingPong 'AsServer 'StIdle 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 (ClientHasAgency 'StIdle -> PeerHasAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
TokIdle) ((forall (st' :: PingPong).
  Message PingPong 'StIdle st' -> Peer PingPong 'AsServer st' m a)
 -> Peer PingPong 'AsServer 'StIdle m a)
-> (forall (st' :: PingPong).
    Message PingPong 'StIdle st' -> Peer PingPong 'AsServer st' m a)
-> Peer PingPong 'AsServer 'StIdle m a
forall a b. (a -> b) -> a -> b
$ \Message PingPong 'StIdle st'
req ->

    -- The client got to choose between two messages and we have to handle
    -- either of them
    case Message PingPong 'StIdle st'
req of

      -- The client sent the done transition, so we're in the 'StDone' state
      -- so all we can do is stop using 'done', with a return value.
      Message PingPong 'StIdle st'
MsgDone -> NobodyHasAgency 'StDone -> a -> Peer PingPong 'AsServer '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
recvMsgDone

      -- The client sent us a ping request, so now we're in the 'StBusy' state
      -- which means it's the server's turn to send.
      Message PingPong 'StIdle st'
MsgPing -> m (Peer PingPong 'AsServer 'StBusy m a)
-> Peer PingPong 'AsServer 'StBusy 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 'AsServer 'StBusy m a)
 -> Peer PingPong 'AsServer 'StBusy m a)
-> m (Peer PingPong 'AsServer 'StBusy m a)
-> Peer PingPong 'AsServer 'StBusy m a
forall a b. (a -> b) -> a -> b
$ do
        PingPongServer m a
next <- m (PingPongServer m a)
recvMsgPing
        Peer PingPong 'AsServer 'StBusy m a
-> m (Peer PingPong 'AsServer 'StBusy m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Peer PingPong 'AsServer 'StBusy m a
 -> m (Peer PingPong 'AsServer 'StBusy m a))
-> Peer PingPong 'AsServer 'StBusy m a
-> m (Peer PingPong 'AsServer 'StBusy m a)
forall a b. (a -> b) -> a -> b
$ WeHaveAgency 'AsServer 'StBusy
-> Message PingPong 'StBusy 'StIdle
-> Peer PingPong 'AsServer 'StIdle m a
-> Peer PingPong 'AsServer 'StBusy 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 (ServerHasAgency 'StBusy -> WeHaveAgency 'AsServer 'StBusy
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StBusy
TokBusy) Message PingPong 'StBusy 'StIdle
MsgPong (PingPongServer m a -> Peer PingPong 'AsServer 'StIdle m a
forall (m :: * -> *) a.
Monad m =>
PingPongServer m a -> Peer PingPong 'AsServer 'StIdle m a
pingPongServerPeer PingPongServer m a
next)