{-# 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 {k} {k1} {k2} (header :: k) (point :: k1) (tip :: k2).
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 [point1]
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]
[point1]
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 {k1} header1 tip1 (point :: k1) (any :: StNextKind).
header1
-> tip1
-> Message (ChainSync header1 point tip1) ('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 {k} point1 tip1 (header :: k) (any :: StNextKind).
point1
-> tip1
-> Message (ChainSync header point1 tip1) ('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 {k} point1 tip1 (header :: k).
point1
-> tip1
-> Message (ChainSync header point1 tip1) '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 {k} {k1} tip1 (header :: k) (point :: k1).
tip1 -> Message (ChainSync header point tip1) '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)