module Hydra.Network.Ouroboros.Server where

import Hydra.Prelude

import Hydra.Network.Ouroboros.Type (
  FireForget (StIdle),
  Message (MsgDone, MsgSend),
 )
import Network.TypedProtocol (
  IsPipelined (..),
  PeerRole (AsServer),
  ReflRelativeAgency (..),
 )

import Network.TypedProtocol.Peer (
  Peer (Await, Done, Effect),
 )

data FireForgetServer msg m a = FireForgetServer
  { forall msg (m :: * -> *) a.
FireForgetServer msg m a -> msg -> m (FireForgetServer msg m a)
recvMsg :: msg -> m (FireForgetServer msg m a)
  -- ^ The client sent us a message.
  -- There is no response and we must have effects.
  , forall msg (m :: * -> *) a. FireForgetServer msg m a -> m a
recvMsgDone :: 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.
  }

fireForgetServerPeer ::
  Monad m =>
  FireForgetServer msg m a ->
  Peer (FireForget msg) 'AsServer 'NonPipelined 'StIdle m a
fireForgetServerPeer :: forall (m :: * -> *) msg a.
Monad m =>
FireForgetServer msg m a
-> Peer (FireForget msg) 'AsServer 'NonPipelined 'StIdle m a
fireForgetServerPeer FireForgetServer{msg -> m (FireForgetServer msg m a)
$sel:recvMsg:FireForgetServer :: forall msg (m :: * -> *) a.
FireForgetServer msg m a -> msg -> m (FireForgetServer msg m a)
recvMsg :: msg -> m (FireForgetServer msg m a)
recvMsg, m a
$sel:recvMsgDone:FireForgetServer :: forall msg (m :: * -> *) a. FireForgetServer msg m a -> m a
recvMsgDone :: m a
recvMsgDone} =
  -- In the 'StIdle' the server is awaiting a request message
  TheyHaveAgencyProof 'AsServer 'StIdle
-> (forall {st' :: FireForget msg}.
    Message (FireForget msg) 'StIdle st'
    -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> Peer (FireForget msg) 'AsServer 'NonPipelined 'StIdle m a
forall ps (pr :: PeerRole) (pl :: IsPipelined) (st :: ps)
       (m :: * -> *) a.
(StateTokenI st, ActiveState st, Outstanding pl ~ 'Z) =>
TheyHaveAgencyProof pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr pl st' m a)
-> Peer ps pr pl st m a
Await TheyHaveAgencyProof 'AsServer 'StIdle
ReflRelativeAgency 'ClientAgency 'TheyHaveAgency 'TheyHaveAgency
forall (r :: RelativeAgency). ReflRelativeAgency 'ClientAgency r r
ReflClientAgency ((forall {st' :: FireForget msg}.
  Message (FireForget msg) 'StIdle st'
  -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
 -> Peer (FireForget msg) 'AsServer 'NonPipelined 'StIdle m a)
-> (forall {st' :: FireForget msg}.
    Message (FireForget msg) 'StIdle st'
    -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> Peer (FireForget msg) 'AsServer 'NonPipelined 'StIdle m a
forall a b. (a -> b) -> a -> b
$ \case
    -- The client got to choose between two messages and we have to handle
    -- either of them
    MsgSend msg1
payload -> m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a
forall ps (pr :: PeerRole) (pl :: IsPipelined) (st :: ps)
       (m :: * -> *) a.
m (Peer ps pr pl st m a) -> Peer ps pr pl st m a
Effect (m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
 -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a
forall a b. (a -> b) -> a -> b
$ FireForgetServer msg m a
-> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a
FireForgetServer msg m a
-> Peer (FireForget msg) 'AsServer 'NonPipelined 'StIdle m a
forall (m :: * -> *) msg a.
Monad m =>
FireForgetServer msg m a
-> Peer (FireForget msg) 'AsServer 'NonPipelined 'StIdle m a
fireForgetServerPeer (FireForgetServer msg m a
 -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> m (FireForgetServer msg m a)
-> m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> msg -> m (FireForgetServer msg m a)
recvMsg msg
msg1
payload
    Message (FireForget msg) 'StIdle st'
R:MessageFireForgetfromto (*) msg 'StIdle st'
MsgDone -> m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a
forall ps (pr :: PeerRole) (pl :: IsPipelined) (st :: ps)
       (m :: * -> *) a.
m (Peer ps pr pl st m a) -> Peer ps pr pl st m a
Effect (m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
 -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a
forall a b. (a -> b) -> a -> b
$ NobodyHasAgencyProof 'AsServer st'
-> a -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a
forall ps (pr :: PeerRole) (pl :: IsPipelined) (st :: ps)
       (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
NobodyHasAgencyProof pr st -> a -> Peer ps pr pl st m a
Done NobodyHasAgencyProof 'AsServer st'
ReflRelativeAgency 'NobodyAgency 'NobodyHasAgency 'NobodyHasAgency
forall (r :: RelativeAgency). ReflRelativeAgency 'NobodyAgency r r
ReflNobodyAgency (a -> Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
-> m a -> m (Peer (FireForget msg) 'AsServer 'NonPipelined st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
recvMsgDone