{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | The upstream side of LeiosFetch.
module Ouroboros.Consensus.MiniProtocol.LeiosFetch.Server
  ( ExnLeiosInvalidRequest (..)
  , LeiosFetchRequestHandler (..)
  , LeiosFetchServerPeer
  , leiosFetchServerPeer
  ) where

import Control.Monad.Class.MonadThrow (Exception)
import Network.TypedProtocol.Codec (PeerRole (..))
import Network.TypedProtocol.Core
  ( IsPipelined (..)
  , ReflRelativeAgency (..)
  )
import Network.TypedProtocol.Peer (Peer (..))
import Ouroboros.Consensus.Leios.Types (LeiosPoint)
import Ouroboros.Consensus.MiniProtocol.LeiosFetch.Type
  ( LeiosFetch (..)
  , Message (..)
  )

type LeiosFetchServerPeer point eb tx m a =
  Peer (LeiosFetch point eb tx) AsServer NonPipelined StIdle m a

-- | How a server answers each request.
newtype LeiosFetchRequestHandler point eb tx m
  = MkLeiosFetchRequestHandler
      ( forall st.
        Message (LeiosFetch point eb tx) StIdle (StBusy st) ->
        m (Message (LeiosFetch point eb tx) (StBusy st) StIdle)
      )

-- | A server that answers each request with the handler, and ends when the
-- client sends 'MsgDone'.
leiosFetchServerPeer ::
  forall point eb tx m.
  Functor m =>
  LeiosFetchRequestHandler point eb tx m ->
  LeiosFetchServerPeer point eb tx m ()
leiosFetchServerPeer :: forall point eb tx (m :: * -> *).
Functor m =>
LeiosFetchRequestHandler point eb tx m
-> LeiosFetchServerPeer point eb tx m ()
leiosFetchServerPeer (MkLeiosFetchRequestHandler forall (st :: LeiosFetchBusy point eb tx).
Message (LeiosFetch point eb tx) 'StIdle ('StBusy st)
-> m (Message (LeiosFetch point eb tx) ('StBusy st) 'StIdle)
answer) = LeiosFetchServerPeer point eb tx m ()
go
 where
  go :: LeiosFetchServerPeer point eb tx m ()
  go :: LeiosFetchServerPeer point eb tx m ()
go = TheyHaveAgencyProof 'AsServer 'StIdle
-> (forall (st' :: LeiosFetch point eb tx).
    Message (LeiosFetch point eb tx) 'StIdle st'
    -> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> LeiosFetchServerPeer point eb tx m ()
forall ps (pr :: PeerRole) (pl :: IsPipelined ps) (st :: ps)
       (m :: * -> *) a.
(StateTokenI st, ActiveState st, Outstanding pl ~ 'Z,
 OutstandingSenders 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 ReflRelativeAgency 'ClientAgency 'TheyHaveAgency 'TheyHaveAgency
TheyHaveAgencyProof 'AsServer 'StIdle
forall (r :: RelativeAgency). ReflRelativeAgency 'ClientAgency r r
ReflClientAgency ((forall (st' :: LeiosFetch point eb tx).
  Message (LeiosFetch point eb tx) 'StIdle st'
  -> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
 -> LeiosFetchServerPeer point eb tx m ())
-> (forall (st' :: LeiosFetch point eb tx).
    Message (LeiosFetch point eb tx) 'StIdle st'
    -> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> LeiosFetchServerPeer point eb tx m ()
forall a b. (a -> b) -> a -> b
$ \case
    Message (LeiosFetch point eb tx) 'StIdle st'
R:MessageLeiosFetchfromto point eb tx 'StIdle st'
MsgDone -> NobodyHasAgencyProof 'AsServer st'
-> ()
-> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ()
forall ps (pr :: PeerRole) (pl :: IsPipelined ps) (st :: ps)
       (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) =>
NobodyHasAgencyProof pr st -> a -> Peer ps pr pl st m a
Done ReflRelativeAgency 'NobodyAgency 'NobodyHasAgency 'NobodyHasAgency
NobodyHasAgencyProof 'AsServer st'
forall (r :: RelativeAgency). ReflRelativeAgency 'NobodyAgency r r
ReflNobodyAgency ()
    request :: Message (LeiosFetch point eb tx) 'StIdle st'
request@MsgLeiosBlockRequest{} ->
      m (Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ()
forall ps (pr :: PeerRole) (pl :: IsPipelined ps) (st :: ps)
       (m :: * -> *) a.
m (Peer ps pr pl st m a) -> Peer ps pr pl st m a
Effect (m (Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
 -> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> m (Peer
        (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ()
forall a b. (a -> b) -> a -> b
$ (\Message (LeiosFetch point eb tx) st' 'StIdle
response -> WeHaveAgencyProof 'AsServer st'
-> Message (LeiosFetch point eb tx) st' 'StIdle
-> LeiosFetchServerPeer point eb tx m ()
-> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ()
forall ps (pr :: PeerRole) (pl :: IsPipelined ps) (st :: ps)
       (st' :: ps) (m :: * -> *) a.
(StateTokenI st, StateTokenI st', ActiveState st,
 Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) =>
WeHaveAgencyProof pr st
-> Message ps st st'
-> Peer ps pr pl st' m a
-> Peer ps pr pl st m a
Yield ReflRelativeAgency 'ServerAgency 'WeHaveAgency 'WeHaveAgency
WeHaveAgencyProof 'AsServer st'
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency Message (LeiosFetch point eb tx) st' 'StIdle
response LeiosFetchServerPeer point eb tx m ()
go) (Message (LeiosFetch point eb tx) st' 'StIdle
 -> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> m (Message (LeiosFetch point eb tx) st' 'StIdle)
-> m (Peer
        (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Message (LeiosFetch point eb tx) 'StIdle ('StBusy 'StBlock)
-> m (Message (LeiosFetch point eb tx) ('StBusy 'StBlock) 'StIdle)
forall (st :: LeiosFetchBusy point eb tx).
Message (LeiosFetch point eb tx) 'StIdle ('StBusy st)
-> m (Message (LeiosFetch point eb tx) ('StBusy st) 'StIdle)
answer Message (LeiosFetch point eb tx) 'StIdle st'
Message (LeiosFetch point eb tx) 'StIdle ('StBusy 'StBlock)
request
    request :: Message (LeiosFetch point eb tx) 'StIdle st'
request@MsgLeiosBlockTxsRequest{} ->
      m (Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ()
forall ps (pr :: PeerRole) (pl :: IsPipelined ps) (st :: ps)
       (m :: * -> *) a.
m (Peer ps pr pl st m a) -> Peer ps pr pl st m a
Effect (m (Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
 -> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> m (Peer
        (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ()
forall a b. (a -> b) -> a -> b
$ (\Message (LeiosFetch point eb tx) st' 'StIdle
response -> WeHaveAgencyProof 'AsServer st'
-> Message (LeiosFetch point eb tx) st' 'StIdle
-> LeiosFetchServerPeer point eb tx m ()
-> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ()
forall ps (pr :: PeerRole) (pl :: IsPipelined ps) (st :: ps)
       (st' :: ps) (m :: * -> *) a.
(StateTokenI st, StateTokenI st', ActiveState st,
 Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) =>
WeHaveAgencyProof pr st
-> Message ps st st'
-> Peer ps pr pl st' m a
-> Peer ps pr pl st m a
Yield ReflRelativeAgency 'ServerAgency 'WeHaveAgency 'WeHaveAgency
WeHaveAgencyProof 'AsServer st'
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency Message (LeiosFetch point eb tx) st' 'StIdle
response LeiosFetchServerPeer point eb tx m ()
go) (Message (LeiosFetch point eb tx) st' 'StIdle
 -> Peer (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
-> m (Message (LeiosFetch point eb tx) st' 'StIdle)
-> m (Peer
        (LeiosFetch point eb tx) 'AsServer 'NonPipelined st' m ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Message (LeiosFetch point eb tx) 'StIdle ('StBusy 'StBlockTxs)
-> m (Message
        (LeiosFetch point eb tx) ('StBusy 'StBlockTxs) 'StIdle)
forall (st :: LeiosFetchBusy point eb tx).
Message (LeiosFetch point eb tx) 'StIdle ('StBusy st)
-> m (Message (LeiosFetch point eb tx) ('StBusy st) 'StIdle)
answer Message (LeiosFetch point eb tx) 'StIdle st'
Message (LeiosFetch point eb tx) 'StIdle ('StBusy 'StBlockTxs)
request

-- | Thrown by the node's LeiosFetch server, which disconnects a client that
-- requests what the node does not hold.
data ExnLeiosInvalidRequest
  = -- | An endorser block whose body the node does not hold.
    ExnLeiosUnknownBlockRequested !LeiosPoint
  | -- | Offsets into an endorser block that it does not have, or whose
    -- transactions the node does not hold.
    ExnLeiosUnknownTxsRequested !LeiosPoint ![Int]
  deriving Int -> ExnLeiosInvalidRequest -> ShowS
[ExnLeiosInvalidRequest] -> ShowS
ExnLeiosInvalidRequest -> String
(Int -> ExnLeiosInvalidRequest -> ShowS)
-> (ExnLeiosInvalidRequest -> String)
-> ([ExnLeiosInvalidRequest] -> ShowS)
-> Show ExnLeiosInvalidRequest
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExnLeiosInvalidRequest -> ShowS
showsPrec :: Int -> ExnLeiosInvalidRequest -> ShowS
$cshow :: ExnLeiosInvalidRequest -> String
show :: ExnLeiosInvalidRequest -> String
$cshowList :: [ExnLeiosInvalidRequest] -> ShowS
showList :: [ExnLeiosInvalidRequest] -> ShowS
Show

instance Exception ExnLeiosInvalidRequest