{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | The upstream side of LeiosNotify.
module Ouroboros.Consensus.MiniProtocol.LeiosNotify.Server
  ( ExnLeiosNotifyExcessiveRequests (..)
  , LeiosNotifyServerPeerLookahead
  , WhetherExcessiveRequests (..)
  , leiosNotifyServerPeerLookahead
  ) where

import Control.Monad.Class.MonadSTM
import Control.Monad.Class.MonadThrow
import Data.Functor ((<&>))
import GHC.Generics (Generic)
import Network.TypedProtocol.Codec (PeerRole (..))
import Network.TypedProtocol.Core
  ( IsPipelined (..)
  , N (..)
  , Nat (..)
  , ReflRelativeAgency (..)
  , SenderVariability (..)
  )
import Network.TypedProtocol.Peer
  ( Peer (..)
  , PeerLookaheadFixedSender (..)
  , Sender (..)
  )
import NoThunks.Class (NoThunks)
import Ouroboros.Consensus.MiniProtocol.LeiosNotify.Type
import Ouroboros.Consensus.Util.IOLike
  ( StrictTVar
  , newTVarIO
  , readTVar
  , writeTVar
  )

type LeiosNotifyServerPeerLookahead point announcement vote m =
  PeerLookaheadFixedSender (LeiosNotify point announcement vote) AsServer StIdle m ()

-- | Whether incrementing the count of outstanding LeiosNotify requests found the
-- peer already at its pipelining bound, i.e. requesting more than it is allowed.
data WhetherExcessiveRequests = ExcessiveRequests | NotExcessiveRequests

-- | Whether the client has sent 'MsgQuit'.
data WhetherQuitting = Quitting | NotYetQuitting
  deriving stock (forall x. WhetherQuitting -> Rep WhetherQuitting x)
-> (forall x. Rep WhetherQuitting x -> WhetherQuitting)
-> Generic WhetherQuitting
forall x. Rep WhetherQuitting x -> WhetherQuitting
forall x. WhetherQuitting -> Rep WhetherQuitting x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WhetherQuitting -> Rep WhetherQuitting x
from :: forall x. WhetherQuitting -> Rep WhetherQuitting x
$cto :: forall x. Rep WhetherQuitting x -> WhetherQuitting
to :: forall x. Rep WhetherQuitting x -> WhetherQuitting
Generic
  deriving anyclass Context -> WhetherQuitting -> IO (Maybe ThunkInfo)
Proxy WhetherQuitting -> String
(Context -> WhetherQuitting -> IO (Maybe ThunkInfo))
-> (Context -> WhetherQuitting -> IO (Maybe ThunkInfo))
-> (Proxy WhetherQuitting -> String)
-> NoThunks WhetherQuitting
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> WhetherQuitting -> IO (Maybe ThunkInfo)
noThunks :: Context -> WhetherQuitting -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> WhetherQuitting -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> WhetherQuitting -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy WhetherQuitting -> String
showTypeOf :: Proxy WhetherQuitting -> String
NoThunks

-- | Once the client sends 'MsgQuit', the server answers every outstanding
-- request with 'MsgCanceled', and then ends with 'MsgDone'.
leiosNotifyServerPeerLookahead ::
  forall m point announcement vote.
  (MonadThrow m, MonadSTM m) =>
  m WhetherExcessiveRequests ->
  -- | blocks until the next reply (announcement\/offer\/vote) is ready
  STM m (Message (LeiosNotify point announcement vote) StBusy StIdle) ->
  m (LeiosNotifyServerPeerLookahead point announcement vote m)
leiosNotifyServerPeerLookahead :: forall (m :: * -> *) point announcement vote.
(MonadThrow m, MonadSTM m) =>
m WhetherExcessiveRequests
-> STM
     m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle)
-> m (LeiosNotifyServerPeerLookahead point announcement vote m)
leiosNotifyServerPeerLookahead m WhetherExcessiveRequests
incr STM
  m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle)
next = do
  quitVar <- WhetherQuitting -> m (StrictTVar m WhetherQuitting)
forall (m :: * -> *) a.
(HasCallStack, MonadSTM m, NoThunks a) =>
a -> m (StrictTVar m a)
newTVarIO WhetherQuitting
NotYetQuitting
  pure $ PeerLookaheadFixedSender (responder quitVar) (start quitVar)
 where
  responder ::
    StrictTVar m WhetherQuitting ->
    Sender (LeiosNotify point announcement vote) AsServer VariableSender StBusy StIdle m
  responder :: StrictTVar m WhetherQuitting
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m
responder StrictTVar m WhetherQuitting
quitVar =
    m (Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m)
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (stdone :: ps).
m (Sender ps pr 'VariableSender st stdone m)
-> Sender ps pr 'VariableSender st stdone m
SenderEffect (m (Sender
      (LeiosNotify point announcement vote)
      'AsServer
      'VariableSender
      'StBusy
      'StIdle
      m)
 -> Sender
      (LeiosNotify point announcement vote)
      'AsServer
      'VariableSender
      'StBusy
      'StIdle
      m)
-> m (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m
forall a b. (a -> b) -> a -> b
$
      STM
  m
  (Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m)
-> m (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM
   m
   (Sender
      (LeiosNotify point announcement vote)
      'AsServer
      'VariableSender
      'StBusy
      'StIdle
      m)
 -> m (Sender
         (LeiosNotify point announcement vote)
         'AsServer
         'VariableSender
         'StBusy
         'StIdle
         m))
-> STM
     m
     (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
-> m (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
forall a b. (a -> b) -> a -> b
$
        STM
  m
  (Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m)
-> STM
     m
     (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
-> STM
     m
     (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
forall a. STM m a -> STM m a -> STM m a
forall (m :: * -> *) a. MonadSTM m => STM m a -> STM m a -> STM m a
orElse
          ( StrictTVar m WhetherQuitting -> STM m WhetherQuitting
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m WhetherQuitting
quitVar STM m WhetherQuitting
-> (WhetherQuitting
    -> STM
         m
         (Sender
            (LeiosNotify point announcement vote)
            'AsServer
            'VariableSender
            'StBusy
            'StIdle
            m))
-> STM
     m
     (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
forall a b. STM m a -> (a -> STM m b) -> STM m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              WhetherQuitting
Quitting -> Sender
  (LeiosNotify point announcement vote)
  'AsServer
  'VariableSender
  'StBusy
  'StIdle
  m
-> STM
     m
     (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
forall a. a -> STM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sender
   (LeiosNotify point announcement vote)
   'AsServer
   'VariableSender
   'StBusy
   'StIdle
   m
 -> STM
      m
      (Sender
         (LeiosNotify point announcement vote)
         'AsServer
         'VariableSender
         'StBusy
         'StIdle
         m))
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m
-> STM
     m
     (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
forall a b. (a -> b) -> a -> b
$ WeHaveAgencyProof 'AsServer 'StBusy
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StIdle
     'StIdle
     m
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m
forall ps (st :: ps) (st' :: ps) (pr :: PeerRole) (stdone :: ps)
       (m :: * -> *).
(StateTokenI st, StateTokenI st', ActiveState st) =>
WeHaveAgencyProof pr st
-> Message ps st st'
-> Sender ps pr 'VariableSender st' stdone m
-> Sender ps pr 'VariableSender st stdone m
SenderYield ReflRelativeAgency 'ServerAgency 'WeHaveAgency 'WeHaveAgency
WeHaveAgencyProof 'AsServer 'StBusy
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
MsgCanceled Sender
  (LeiosNotify point announcement vote)
  'AsServer
  'VariableSender
  'StIdle
  'StIdle
  m
forall ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
Sender ps pr 'VariableSender st st m
SenderDone
              WhetherQuitting
NotYetQuitting -> STM
  m
  (Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m)
forall a. STM m a
forall (m :: * -> *) a. MonadSTM m => STM m a
retry
          )
          (STM
  m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle)
next STM
  m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle)
-> (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
    -> Sender
         (LeiosNotify point announcement vote)
         'AsServer
         'VariableSender
         'StBusy
         'StIdle
         m)
-> STM
     m
     (Sender
        (LeiosNotify point announcement vote)
        'AsServer
        'VariableSender
        'StBusy
        'StIdle
        m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg -> WeHaveAgencyProof 'AsServer 'StBusy
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StIdle
     'StIdle
     m
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     'VariableSender
     'StBusy
     'StIdle
     m
forall ps (st :: ps) (st' :: ps) (pr :: PeerRole) (stdone :: ps)
       (m :: * -> *).
(StateTokenI st, StateTokenI st', ActiveState st) =>
WeHaveAgencyProof pr st
-> Message ps st st'
-> Sender ps pr 'VariableSender st' stdone m
-> Sender ps pr 'VariableSender st stdone m
SenderYield ReflRelativeAgency 'ServerAgency 'WeHaveAgency 'WeHaveAgency
WeHaveAgencyProof 'AsServer 'StBusy
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg Sender
  (LeiosNotify point announcement vote)
  'AsServer
  'VariableSender
  'StIdle
  'StIdle
  m
forall ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
Sender ps pr 'VariableSender st st m
SenderDone)

  -- StIdle with nothing outstanding: receive the first request (or quit). A
  -- plain 'Await' is required here; 'AwaitLookahead' defers the StBusy->StIdle
  -- send, so it is only usable once we hold a request (i.e. are at StBusy).
  start ::
    StrictTVar m WhetherQuitting ->
    Peer
      (LeiosNotify point announcement vote)
      AsServer
      (Lookahead Z (FixedSender StBusy StIdle))
      StIdle
      m
      ()
  start :: StrictTVar m WhetherQuitting
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     'StIdle
     m
     ()
start StrictTVar m WhetherQuitting
quitVar =
    TheyHaveAgencyProof 'AsServer 'StIdle
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StIdle st'
    -> Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
         st'
         m
         ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     'StIdle
     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' :: LeiosNotify point announcement vote).
  Message (LeiosNotify point announcement vote) 'StIdle st'
  -> Peer
       (LeiosNotify point announcement vote)
       'AsServer
       ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
       st'
       m
       ())
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
      'StIdle
      m
      ())
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StIdle st'
    -> Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
         st'
         m
         ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     'StIdle
     m
     ()
forall a b. (a -> b) -> a -> b
$ \case
      Message (LeiosNotify point announcement vote) 'StIdle st'
R:MessageLeiosNotifyfromto point announcement vote 'StIdle st'
MsgQuit -> m (Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     st'
     m
     ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     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
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
      st'
      m
      ())
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
      st'
      m
      ())
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
        st'
        m
        ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     st'
     m
     ()
forall a b. (a -> b) -> a -> b
$ do
        STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m WhetherQuitting -> WhetherQuitting -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m WhetherQuitting
quitVar WhetherQuitting
Quitting
        Peer
  (LeiosNotify point announcement vote)
  'AsServer
  ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
  st'
  m
  ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
        st'
        m
        ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Peer
   (LeiosNotify point announcement vote)
   'AsServer
   ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
   st'
   m
   ()
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
         st'
         m
         ()))
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     st'
     m
     ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
        st'
        m
        ())
forall a b. (a -> b) -> a -> b
$ WeHaveAgencyProof 'AsServer st'
-> Message (LeiosNotify point announcement vote) st' 'StDone
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     'StDone
     m
     ()
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     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 (LeiosNotify point announcement vote) st' 'StDone
Message (LeiosNotify point announcement vote) 'StQuit 'StDone
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StQuit 'StDone
MsgDone (Peer
   (LeiosNotify point announcement vote)
   'AsServer
   ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
   'StDone
   m
   ()
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
      st'
      m
      ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     'StDone
     m
     ()
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     st'
     m
     ()
forall a b. (a -> b) -> a -> b
$ NobodyHasAgencyProof 'AsServer 'StDone
-> ()
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     'StDone
     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 'StDone
forall (r :: RelativeAgency). ReflRelativeAgency 'NobodyAgency r r
ReflNobodyAgency ()
      Message (LeiosNotify point announcement vote) 'StIdle st'
R:MessageLeiosNotifyfromto point announcement vote 'StIdle st'
MsgLeiosNotificationRequestNext ->
        m (Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     st'
     m
     ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     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
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
      st'
      m
      ())
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
      st'
      m
      ())
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
        st'
        m
        ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     st'
     m
     ()
forall a b. (a -> b) -> a -> b
$ do
          m WhetherExcessiveRequests
incr m WhetherExcessiveRequests
-> (WhetherExcessiveRequests -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            WhetherExcessiveRequests
ExcessiveRequests -> ExnLeiosNotifyExcessiveRequests -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwIO ExnLeiosNotifyExcessiveRequests
ExnLeiosNotifyExcessiveRequests
            WhetherExcessiveRequests
NotExcessiveRequests -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Peer
  (LeiosNotify point announcement vote)
  'AsServer
  ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
  st'
  m
  ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
        st'
        m
        ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Peer
   (LeiosNotify point announcement vote)
   'AsServer
   ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
   st'
   m
   ()
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
         st'
         m
         ()))
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     st'
     m
     ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
        st'
        m
        ())
forall a b. (a -> b) -> a -> b
$ StrictTVar m WhetherQuitting
-> Nat 'Z
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead 'Z ('FixedSender 'StBusy 'StIdle))
     'StBusy
     m
     ()
forall (n :: N).
StrictTVar m WhetherQuitting
-> Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StBusy
     m
     ()
busy StrictTVar m WhetherQuitting
quitVar Nat 'Z
forall (n :: N). ('Z ~ n) => Nat n
Zero

  -- StBusy with @n@ deferred sends outstanding: hand this reply off to the
  -- responder and look ahead to the next request (or done) in one step.
  busy ::
    forall n.
    StrictTVar m WhetherQuitting ->
    Nat n ->
    Peer
      (LeiosNotify point announcement vote)
      AsServer
      (Lookahead n (FixedSender StBusy StIdle))
      StBusy
      m
      ()
  busy :: forall (n :: N).
StrictTVar m WhetherQuitting
-> Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StBusy
     m
     ()
busy StrictTVar m WhetherQuitting
quitVar Nat n
n =
    TheyHaveAgencyProof 'AsServer 'StIdle
-> Sender
     (LeiosNotify point announcement vote)
     'AsServer
     ('FixedSender 'StBusy 'StIdle)
     'StBusy
     'StIdle
     m
-> (forall (st'' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StIdle st''
    -> Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
         st''
         m
         ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StBusy
     m
     ()
forall ps (pr :: PeerRole) (sv :: SenderVariability ps) (st :: ps)
       (st' :: ps) (n :: N) (m :: * -> *) a.
(StateTokenI st, StateTokenI st', ActiveState st,
 ActiveState st') =>
TheyHaveAgencyProof pr st'
-> Sender ps pr sv st st' m
-> (forall (st'' :: ps).
    Message ps st' st'' -> Peer ps pr ('Lookahead ('S n) sv) st'' m a)
-> Peer ps pr ('Lookahead n sv) st m a
AwaitLookahead ReflRelativeAgency 'ClientAgency 'TheyHaveAgency 'TheyHaveAgency
TheyHaveAgencyProof 'AsServer 'StIdle
forall (r :: RelativeAgency). ReflRelativeAgency 'ClientAgency r r
ReflClientAgency Sender
  (LeiosNotify point announcement vote)
  'AsServer
  ('FixedSender 'StBusy 'StIdle)
  'StBusy
  'StIdle
  m
forall ps (pr :: PeerRole) (st :: ps) (stdone :: ps) (m :: * -> *).
Sender ps pr ('FixedSender st stdone) st stdone m
TheSender ((forall (st'' :: LeiosNotify point announcement vote).
  Message (LeiosNotify point announcement vote) 'StIdle st''
  -> Peer
       (LeiosNotify point announcement vote)
       'AsServer
       ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
       st''
       m
       ())
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead n ('FixedSender 'StBusy 'StIdle))
      'StBusy
      m
      ())
-> (forall (st'' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StIdle st''
    -> Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
         st''
         m
         ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StBusy
     m
     ()
forall a b. (a -> b) -> a -> b
$ \case
      Message (LeiosNotify point announcement vote) 'StIdle st''
R:MessageLeiosNotifyfromto point announcement vote 'StIdle st''
MsgQuit -> m (Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     st''
     m
     ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     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
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
      st''
      m
      ())
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
      st''
      m
      ())
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
        st''
        m
        ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     st''
     m
     ()
forall a b. (a -> b) -> a -> b
$ do
        STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (StrictTVar m WhetherQuitting -> WhetherQuitting -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m WhetherQuitting
quitVar WhetherQuitting
Quitting)
        Peer
  (LeiosNotify point announcement vote)
  'AsServer
  ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
  st''
  m
  ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
        st''
        m
        ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Peer
   (LeiosNotify point announcement vote)
   'AsServer
   ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
   st''
   m
   ()
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
         st''
         m
         ()))
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     st''
     m
     ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
        st''
        m
        ())
forall a b. (a -> b) -> a -> b
$ Nat ('S n)
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
forall (n :: N).
Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
drain (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
n)
      Message (LeiosNotify point announcement vote) 'StIdle st''
R:MessageLeiosNotifyfromto point announcement vote 'StIdle st''
MsgLeiosNotificationRequestNext ->
        m (Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     st''
     m
     ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     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
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
      st''
      m
      ())
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
      st''
      m
      ())
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
        st''
        m
        ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     st''
     m
     ()
forall a b. (a -> b) -> a -> b
$ do
          m WhetherExcessiveRequests
incr m WhetherExcessiveRequests
-> (WhetherExcessiveRequests -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            WhetherExcessiveRequests
ExcessiveRequests -> ExnLeiosNotifyExcessiveRequests -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwIO ExnLeiosNotifyExcessiveRequests
ExnLeiosNotifyExcessiveRequests
            WhetherExcessiveRequests
NotExcessiveRequests -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Peer
  (LeiosNotify point announcement vote)
  'AsServer
  ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
  st''
  m
  ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
        st''
        m
        ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Peer
   (LeiosNotify point announcement vote)
   'AsServer
   ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
   st''
   m
   ()
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsServer
         ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
         st''
         m
         ()))
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     st''
     m
     ()
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsServer
        ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
        st''
        m
        ())
forall a b. (a -> b) -> a -> b
$ StrictTVar m WhetherQuitting
-> Nat ('S n)
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     'StBusy
     m
     ()
forall (n :: N).
StrictTVar m WhetherQuitting
-> Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StBusy
     m
     ()
busy StrictTVar m WhetherQuitting
quitVar (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
n)

  -- on termination, flush the sends we've spawned, then send MsgDone.
  --
  -- Those sends are unblocked because the MsgQuit handler which lead us to this
  -- already set the quitVar flag.
  drain ::
    forall n.
    Nat n ->
    Peer
      (LeiosNotify point announcement vote)
      AsServer
      (Lookahead n (FixedSender StBusy StIdle))
      StQuit
      m
      ()
  drain :: forall (n :: N).
Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
drain = \case
    Nat n
Zero -> WeHaveAgencyProof 'AsServer 'StQuit
-> Message (LeiosNotify point announcement vote) 'StQuit 'StDone
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StDone
     m
     ()
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StQuit
     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 'StQuit
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency Message (LeiosNotify point announcement vote) 'StQuit 'StDone
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StQuit 'StDone
MsgDone (Peer
   (LeiosNotify point announcement vote)
   'AsServer
   ('Lookahead n ('FixedSender 'StBusy 'StIdle))
   'StDone
   m
   ()
 -> Peer
      (LeiosNotify point announcement vote)
      'AsServer
      ('Lookahead n ('FixedSender 'StBusy 'StIdle))
      'StQuit
      m
      ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StDone
     m
     ()
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
forall a b. (a -> b) -> a -> b
$ NobodyHasAgencyProof 'AsServer 'StDone
-> ()
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StDone
     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 'StDone
forall (r :: RelativeAgency). ReflRelativeAgency 'NobodyAgency r r
ReflNobodyAgency ()
    Succ Nat n
j -> Maybe
  (Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
forall ps (pr :: PeerRole) (n :: N) (sv :: SenderVariability ps)
       (st :: ps) (m :: * -> *) a.
StateTokenI st =>
Maybe (Peer ps pr ('Lookahead ('S n) sv) st m a)
-> Peer ps pr ('Lookahead n sv) st m a
-> Peer ps pr ('Lookahead ('S n) sv) st m a
FlushSender Maybe
  (Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead ('S n) ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ())
forall a. Maybe a
Nothing (Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
forall (n :: N).
Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsServer
     ('Lookahead n ('FixedSender 'StBusy 'StIdle))
     'StQuit
     m
     ()
drain Nat n
j)

data ExnLeiosNotifyExcessiveRequests = ExnLeiosNotifyExcessiveRequests
  deriving Int -> ExnLeiosNotifyExcessiveRequests -> ShowS
[ExnLeiosNotifyExcessiveRequests] -> ShowS
ExnLeiosNotifyExcessiveRequests -> String
(Int -> ExnLeiosNotifyExcessiveRequests -> ShowS)
-> (ExnLeiosNotifyExcessiveRequests -> String)
-> ([ExnLeiosNotifyExcessiveRequests] -> ShowS)
-> Show ExnLeiosNotifyExcessiveRequests
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExnLeiosNotifyExcessiveRequests -> ShowS
showsPrec :: Int -> ExnLeiosNotifyExcessiveRequests -> ShowS
$cshow :: ExnLeiosNotifyExcessiveRequests -> String
show :: ExnLeiosNotifyExcessiveRequests -> String
$cshowList :: [ExnLeiosNotifyExcessiveRequests] -> ShowS
showList :: [ExnLeiosNotifyExcessiveRequests] -> ShowS
Show

instance Exception ExnLeiosNotifyExcessiveRequests