{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

-- | A view of the chain synchronisation protocol from the point of view of the
-- server.
--
-- This provides a view that uses less complex types and should be easier to
-- use than the underlying typed protocol itself.
--
-- For execution, a conversion into the typed protocol is provided.
--
module Ouroboros.Network.Protocol.ChainSync.Server
  ( -- * Protocol type for the server
    -- | The protocol states from the point of view of the server.
    ChainSyncServer (..)
  , ServerStIdle (..)
  , ServerStNext (..)
  , ServerStIntersect (..)
    -- * Execution as a typed protocol
  , chainSyncServerPeer
  ) where

import Data.Singletons

import Network.TypedProtocol.Core
import Network.TypedProtocol.Peer.Server

import Ouroboros.Network.Protocol.ChainSync.Type


-- | A chain sync protocol server, on top of some effect 'm'.
--
newtype ChainSyncServer header point tip m a = ChainSyncServer {
    forall header point tip (m :: * -> *) a.
ChainSyncServer header point tip m a
-> m (ServerStIdle header point tip m a)
runChainSyncServer :: m (ServerStIdle header point tip m a)
  }


-- | In the 'StIdle' protocol state, the server does not have agency. Instead
-- it is waiting for:
--
--  * a next update request
--  * a find intersection request
--  * a termination messge
--
-- It must be prepared to handle either.
--
data ServerStIdle header point tip m a = ServerStIdle {

       forall header point tip (m :: * -> *) a.
ServerStIdle header point tip m a
-> m (Either
        (ServerStNext header point tip m a)
        (m (ServerStNext header point tip m a)))
recvMsgRequestNext   :: m (Either (ServerStNext header point tip m a)
                                      (m (ServerStNext header point tip m a))),

       forall header point tip (m :: * -> *) a.
ServerStIdle header point tip m a
-> [point] -> m (ServerStIntersect header point tip m a)
recvMsgFindIntersect :: [point]
                            -> m (ServerStIntersect header point tip m a),

       forall header point tip (m :: * -> *) a.
ServerStIdle header point tip m a -> m a
recvMsgDoneClient :: m a
     }

-- | In the 'StNext' protocol state, the server has agency and must send either:
--
--  * a roll forward
--  * a roll back message
--  * a termination message
--
data ServerStNext header point tip m a where
  SendMsgRollForward  :: header -> tip
                      -> ChainSyncServer header point tip m a
                      -> ServerStNext header point tip m a

  SendMsgRollBackward :: point -> tip
                      -> ChainSyncServer header point tip m a
                      -> ServerStNext header point tip m a

-- | In the 'StIntersect' protocol state, the server has agency and must send
-- either:
--
--  * an intersection improved,
--  * unchanged message,
--  * termination message
--
data ServerStIntersect header point tip m a where
  SendMsgIntersectFound     :: point -> tip
                            -> ChainSyncServer header point tip m a
                            -> ServerStIntersect header point tip m a

  SendMsgIntersectNotFound  :: tip
                            -> ChainSyncServer header point tip m a
                            -> ServerStIntersect header point tip m a


-- | Interpret a 'ChainSyncServer' action sequence as a 'Peer' on the server
-- side of the 'ChainSyncProtocol'.
--
chainSyncServerPeer
  :: forall header point tip m a.
     Monad m
  => ChainSyncServer header point tip m a
  -> Server (ChainSync header point tip) NonPipelined StIdle m a
chainSyncServerPeer :: forall header point tip (m :: * -> *) a.
Monad m =>
ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
chainSyncServerPeer (ChainSyncServer m (ServerStIdle header point tip m a)
mterm) = m (Server (ChainSync header point tip) 'NonPipelined 'StIdle m a)
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Server ps pl st m a) -> Server ps pl st m a
Effect (m (Server (ChainSync header point tip) 'NonPipelined 'StIdle m a)
 -> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a)
-> m (Server
        (ChainSync header point tip) 'NonPipelined 'StIdle m a)
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall a b. (a -> b) -> a -> b
$ m (ServerStIdle header point tip m a)
mterm m (ServerStIdle header point tip m a)
-> (ServerStIdle header point tip m a
    -> m (Server
            (ChainSync header point tip) 'NonPipelined 'StIdle m a))
-> m (Server
        (ChainSync header point tip) 'NonPipelined 'StIdle m a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    \(ServerStIdle{m (Either
     (ServerStNext header point tip m a)
     (m (ServerStNext header point tip m a)))
recvMsgRequestNext :: forall header point tip (m :: * -> *) a.
ServerStIdle header point tip m a
-> m (Either
        (ServerStNext header point tip m a)
        (m (ServerStNext header point tip m a)))
recvMsgRequestNext :: m (Either
     (ServerStNext header point tip m a)
     (m (ServerStNext header point tip m a)))
recvMsgRequestNext, [point] -> m (ServerStIntersect header point tip m a)
recvMsgFindIntersect :: forall header point tip (m :: * -> *) a.
ServerStIdle header point tip m a
-> [point] -> m (ServerStIntersect header point tip m a)
recvMsgFindIntersect :: [point] -> m (ServerStIntersect header point tip m a)
recvMsgFindIntersect, m a
recvMsgDoneClient :: forall header point tip (m :: * -> *) a.
ServerStIdle header point tip m a -> m a
recvMsgDoneClient :: m a
recvMsgDoneClient}) ->

    Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
-> m (Server
        (ChainSync header point tip) 'NonPipelined 'StIdle m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
 -> m (Server
         (ChainSync header point tip) 'NonPipelined 'StIdle m a))
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
-> m (Server
        (ChainSync header point tip) 'NonPipelined 'StIdle m a)
forall a b. (a -> b) -> a -> b
$ (forall (st' :: ChainSync header point tip).
 Message (ChainSync header point tip) 'StIdle st'
 -> Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Server ps pl st' m a)
-> Server ps pl st m a
Await ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) 'StIdle st'
  -> Server (ChainSync header point tip) 'NonPipelined st' m a)
 -> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) 'StIdle st'
    -> Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall a b. (a -> b) -> a -> b
$ \Message (ChainSync header point tip) 'StIdle st'
req ->
    case Message (ChainSync header point tip) 'StIdle st'
req of
      Message (ChainSync header point tip) 'StIdle st'
R:MessageChainSyncfromto header point tip 'StIdle st'
MsgRequestNext -> m (Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Server ps pl st m a) -> Server ps pl st m a
Effect (m (Server (ChainSync header point tip) 'NonPipelined st' m a)
 -> Server (ChainSync header point tip) 'NonPipelined st' m a)
-> m (Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall a b. (a -> b) -> a -> b
$ do
        mresp <- m (Either
     (ServerStNext header point tip m a)
     (m (ServerStNext header point tip m a)))
recvMsgRequestNext
        pure $ case mresp of
          Left  ServerStNext header point tip m a
resp    -> SingNextKind 'StCanAwait
-> ServerStNext header point tip m a
-> Server
     (ChainSync header point tip)
     'NonPipelined
     ('StNext 'StCanAwait)
     m
     a
forall (nextKind :: StNextKind).
SingI nextKind =>
SingNextKind nextKind
-> ServerStNext header point tip m a
-> Server
     (ChainSync header point tip) 'NonPipelined ('StNext nextKind) m a
handleStNext SingNextKind 'StCanAwait
SingCanAwait ServerStNext header point tip m a
resp
          Right m (ServerStNext header point tip m a)
waiting -> Message (ChainSync header point tip) st' ('StNext 'StMustReply)
-> Server
     (ChainSync header point tip)
     'NonPipelined
     ('StNext 'StMustReply)
     m
     a
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Server ps pl st' m a -> Server ps pl st m a
Yield Message (ChainSync header point tip) st' ('StNext 'StMustReply)
Message
  (ChainSync header point tip)
  ('StNext 'StCanAwait)
  ('StNext 'StMustReply)
forall header point tip.
Message
  (ChainSync header point tip)
  ('StNext 'StCanAwait)
  ('StNext 'StMustReply)
MsgAwaitReply (Server
   (ChainSync header point tip)
   'NonPipelined
   ('StNext 'StMustReply)
   m
   a
 -> Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server
     (ChainSync header point tip)
     'NonPipelined
     ('StNext 'StMustReply)
     m
     a
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall a b. (a -> b) -> a -> b
$ m (Server
     (ChainSync header point tip)
     'NonPipelined
     ('StNext 'StMustReply)
     m
     a)
-> Server
     (ChainSync header point tip)
     'NonPipelined
     ('StNext 'StMustReply)
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Server ps pl st m a) -> Server ps pl st m a
Effect (m (Server
      (ChainSync header point tip)
      'NonPipelined
      ('StNext 'StMustReply)
      m
      a)
 -> Server
      (ChainSync header point tip)
      'NonPipelined
      ('StNext 'StMustReply)
      m
      a)
-> m (Server
        (ChainSync header point tip)
        'NonPipelined
        ('StNext 'StMustReply)
        m
        a)
-> Server
     (ChainSync header point tip)
     'NonPipelined
     ('StNext 'StMustReply)
     m
     a
forall a b. (a -> b) -> a -> b
$ do
                             resp <- m (ServerStNext header point tip m a)
waiting
                             pure $ handleStNext SingMustReply resp

      MsgFindIntersect [point]
points -> m (Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Server ps pl st m a) -> Server ps pl st m a
Effect (m (Server (ChainSync header point tip) 'NonPipelined st' m a)
 -> Server (ChainSync header point tip) 'NonPipelined st' m a)
-> m (Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall a b. (a -> b) -> a -> b
$ do
        resp <- [point] -> m (ServerStIntersect header point tip m a)
recvMsgFindIntersect [point]
points
        pure $ handleStIntersect resp

      Message (ChainSync header point tip) 'StIdle st'
R:MessageChainSyncfromto header point tip 'StIdle st'
MsgDone -> m (Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Server ps pl st m a) -> Server ps pl st m a
Effect (m (Server (ChainSync header point tip) 'NonPipelined st' m a)
 -> Server (ChainSync header point tip) 'NonPipelined st' m a)
-> m (Server (ChainSync header point tip) 'NonPipelined st' m a)
-> Server (ChainSync header point tip) 'NonPipelined st' m a
forall a b. (a -> b) -> a -> b
$ a -> Server (ChainSync header point tip) 'NonPipelined st' m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
a -> Server ps pl st m a
Done (a -> Server (ChainSync header point tip) 'NonPipelined st' m a)
-> m a
-> m (Server (ChainSync header point tip) 'NonPipelined st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
recvMsgDoneClient

  where
    handleStNext
      :: SingI nextKind
      => SingNextKind nextKind
      -> ServerStNext header point tip m a
      -> Server (ChainSync header point tip) NonPipelined (StNext nextKind) m a

    handleStNext :: forall (nextKind :: StNextKind).
SingI nextKind =>
SingNextKind nextKind
-> ServerStNext header point tip m a
-> Server
     (ChainSync header point tip) 'NonPipelined ('StNext nextKind) m a
handleStNext SingNextKind nextKind
_ (SendMsgRollForward  header
header tip
tip ChainSyncServer header point tip m a
next) =
      Message (ChainSync header point tip) ('StNext nextKind) 'StIdle
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
-> Server
     (ChainSync header point tip) 'NonPipelined ('StNext nextKind) m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Server ps pl st' m a -> Server ps pl st m a
Yield (header
-> tip
-> Message (ChainSync header point tip) ('StNext nextKind) 'StIdle
forall header tip point (any :: StNextKind).
header
-> tip
-> Message (ChainSync header point tip) ('StNext any) 'StIdle
MsgRollForward header
header tip
tip)
            (ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall header point tip (m :: * -> *) a.
Monad m =>
ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
chainSyncServerPeer ChainSyncServer header point tip m a
next)

    handleStNext SingNextKind nextKind
_ (SendMsgRollBackward point
pIntersect tip
tip ChainSyncServer header point tip m a
next) =
      Message (ChainSync header point tip) ('StNext nextKind) 'StIdle
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
-> Server
     (ChainSync header point tip) 'NonPipelined ('StNext nextKind) m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Server ps pl st' m a -> Server ps pl st m a
Yield (point
-> tip
-> Message (ChainSync header point tip) ('StNext nextKind) 'StIdle
forall point tip header (any :: StNextKind).
point
-> tip
-> Message (ChainSync header point tip) ('StNext any) 'StIdle
MsgRollBackward point
pIntersect tip
tip)
            (ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall header point tip (m :: * -> *) a.
Monad m =>
ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
chainSyncServerPeer ChainSyncServer header point tip m a
next)


    handleStIntersect
      :: ServerStIntersect header point tip m a
      -> Server (ChainSync header point tip) NonPipelined StIntersect m a

    handleStIntersect :: ServerStIntersect header point tip m a
-> Server
     (ChainSync header point tip) 'NonPipelined 'StIntersect m a
handleStIntersect (SendMsgIntersectFound point
pIntersect tip
tip ChainSyncServer header point tip m a
next) =
      Message (ChainSync header point tip) 'StIntersect 'StIdle
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
-> Server
     (ChainSync header point tip) 'NonPipelined 'StIntersect m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Server ps pl st' m a -> Server ps pl st m a
Yield (point
-> tip -> Message (ChainSync header point tip) 'StIntersect 'StIdle
forall point tip header.
point
-> tip -> Message (ChainSync header point tip) 'StIntersect 'StIdle
MsgIntersectFound point
pIntersect tip
tip)
            (ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall header point tip (m :: * -> *) a.
Monad m =>
ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
chainSyncServerPeer ChainSyncServer header point tip m a
next)

    handleStIntersect (SendMsgIntersectNotFound tip
tip ChainSyncServer header point tip m a
next) =
      Message (ChainSync header point tip) 'StIntersect 'StIdle
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
-> Server
     (ChainSync header point tip) 'NonPipelined 'StIntersect m a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Server ps pl st' m a -> Server ps pl st m a
Yield (tip -> Message (ChainSync header point tip) 'StIntersect 'StIdle
forall tip header point.
tip -> Message (ChainSync header point tip) 'StIntersect 'StIdle
MsgIntersectNotFound tip
tip)
            (ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
forall header point tip (m :: * -> *) a.
Monad m =>
ChainSyncServer header point tip m a
-> Server (ChainSync header point tip) 'NonPipelined 'StIdle m a
chainSyncServerPeer ChainSyncServer header point tip m a
next)