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

-- | The downstream side of LeiosNotify.
module Ouroboros.Consensus.MiniProtocol.LeiosNotify.Client
  ( ExnLeiosNotifyUnexpectedCancel (..)
  , LeiosNotifyClientPeerPipelined
  , awaitImmTipCanForecastNow
  , leiosNotifyClientPeerHandlingReplies
  , leiosNotifyClientPeerPipelined
  , toLeiosNotifyClientPeerPipelined
  ) where

import Control.Monad (join)
import Control.Monad.Class.MonadSTM
import Control.Monad.Class.MonadThrow
import Control.Monad.Except (runExcept)
import Control.Monad.Primitive (PrimMonad, PrimState)
import Data.Primitive.MutVar (MutVar)
import qualified Data.Primitive.MutVar as Prim
import Network.TypedProtocol.Codec (PeerRole (..))
import Network.TypedProtocol.Core
  ( IsPipelined (..)
  , N (..)
  , Nat (..)
  , ReflRelativeAgency (..)
  , natToInt
  )
import Network.TypedProtocol.Peer
  ( Peer (..)
  , PeerPipelined (..)
  , Receiver (..)
  )
import Ouroboros.Consensus.BlockchainTime (CurrentSlot (..))
import Ouroboros.Consensus.Config (TopLevelConfig, configLedger)
import Ouroboros.Consensus.Forecast (forecastFor)
import Ouroboros.Consensus.Ledger.Extended (ExtLedgerState, ledgerState)
import Ouroboros.Consensus.Ledger.SupportsProtocol (LedgerSupportsProtocol (..))
import Ouroboros.Consensus.MiniProtocol.LeiosNotify.Type
import Ouroboros.Consensus.Util.IOLike
  ( StrictTVar
  , modifyTVar
  , newTVarIO
  , readTVar
  )
import Ouroboros.Network.ControlMessage (ControlMessage (..), ControlMessageSTM)

-- | Retry until the immutable tip's ledger state can forecast to the current
-- slot.
--
-- A LeiosNotify client judges the replies it receives by forecasting from the
-- immutable tip. Until that tip reaches approximately now, a fresh reply would
-- be beyond the forecast horizon, and a reply the client cannot judge is no
-- grounds to disconnect the peer. So a client sends no request until then.
--
-- The current slot comes from the volatile tip, whose horizon reaches further,
-- so gating on it alone would send requests too soon.
awaitImmTipCanForecastNow ::
  (MonadSTM m, LedgerSupportsProtocol blk) =>
  TopLevelConfig blk ->
  -- | the immutable tip's ledger state
  STM m (ExtLedgerState blk mk) ->
  STM m CurrentSlot ->
  STM m ()
awaitImmTipCanForecastNow :: forall (m :: * -> *) blk (mk :: MapKind).
(MonadSTM m, LedgerSupportsProtocol blk) =>
TopLevelConfig blk
-> STM m (ExtLedgerState blk mk) -> STM m CurrentSlot -> STM m ()
awaitImmTipCanForecastNow TopLevelConfig blk
cfg STM m (ExtLedgerState blk mk)
readImmutableLedger STM m CurrentSlot
readCurrentSlot =
  STM m CurrentSlot
readCurrentSlot STM m CurrentSlot -> (CurrentSlot -> STM m ()) -> STM 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
    CurrentSlot
CurrentSlotUnknown -> STM m ()
forall a. STM m a
forall (m :: * -> *) a. MonadSTM m => STM m a
retry
    CurrentSlot SlotNo
slot -> do
      immLedger <- STM m (ExtLedgerState blk mk)
readImmutableLedger
      case runExcept $
        forecastFor
          (ledgerViewForecastAt (configLedger cfg) (ledgerState immLedger))
          slot of
        Left OutsideForecastRange
_outsideRange -> STM m ()
forall a. STM m a
forall (m :: * -> *) a. MonadSTM m => STM m a
retry
        Right LedgerView (BlockProtocol blk)
_view -> () -> STM m ()
forall a. a -> STM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | A client that keeps @depth@ requests outstanding until the control message
-- says to terminate, passing each reply to @handleReply@. It sends no request
-- while @gate@ blocks; see 'awaitImmTipCanForecastNow'. It disconnects a peer
-- that cancels a request before the client has sent 'MsgQuit'.
leiosNotifyClientPeerHandlingReplies ::
  (PrimMonad m, MonadSTM m, MonadThrow m) =>
  Int ->
  -- | blocks until the client may send requests
  STM m () ->
  ControlMessageSTM m ->
  -- | throws to disconnect the peer
  (Message (LeiosNotify point announcement vote) StBusy StIdle -> m ()) ->
  LeiosNotifyClientPeerPipelined point announcement vote m ()
leiosNotifyClientPeerHandlingReplies :: forall (m :: * -> *) point announcement vote.
(PrimMonad m, MonadSTM m, MonadThrow m) =>
Int
-> STM m ()
-> ControlMessageSTM m
-> (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
    -> m ())
-> LeiosNotifyClientPeerPipelined point announcement vote m ()
leiosNotifyClientPeerHandlingReplies Int
depth STM m ()
gate ControlMessageSTM m
controlMessageSTM Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> m ()
handleReply =
  Peer
  (LeiosNotify point announcement vote)
  'AsClient
  ('Pipelined 'Z C)
  'StIdle
  m
  ()
-> LeiosNotifyClientPeerPipelined point announcement vote m ()
forall point announcement vote (m :: * -> *) a.
Peer
  (LeiosNotify point announcement vote)
  'AsClient
  ('Pipelined 'Z C)
  'StIdle
  m
  a
-> LeiosNotifyClientPeerPipelined point announcement vote m a
toLeiosNotifyClientPeerPipelined (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined 'Z C)
   'StIdle
   m
   ()
 -> LeiosNotifyClientPeerPipelined point announcement vote m ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined 'Z C)
     'StIdle
     m
     ()
-> LeiosNotifyClientPeerPipelined point announcement vote m ()
forall a b. (a -> b) -> a -> b
$
    STM m (Either () Int)
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined 'Z C)
     'StIdle
     m
     ()
forall (m :: * -> *) point announcement vote a.
(PrimMonad m, MonadSTM m) =>
STM m (Either a Int)
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined 'Z C)
     'StIdle
     m
     a
leiosNotifyClientPeerPipelined
      ( ControlMessageSTM m
controlMessageSTM ControlMessageSTM m
-> (ControlMessage -> STM m (Either () Int))
-> STM m (Either () Int)
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
          ControlMessage
Continue -> Int -> Either () Int
forall a b. b -> Either a b
Right Int
depth Either () Int -> STM m () -> STM m (Either () Int)
forall a b. a -> STM m b -> STM m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ STM m ()
gate
          -- Only warm mini-protocols receive this, and LeiosNotify is hot.
          ControlMessage
Quiesce -> Int -> Either () Int
forall a b. b -> Either a b
Right Int
depth Either () Int -> STM m () -> STM m (Either () Int)
forall a b. a -> STM m b -> STM m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ STM m ()
gate
          ControlMessage
Terminate -> Either () Int -> STM m (Either () Int)
forall a. a -> STM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Either () Int
forall a b. a -> Either a b
Left ())
      )
      ( (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
 -> m ())
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
  -> m ())
 -> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
       -> m ()))
-> (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
    -> m ())
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
forall a b. (a -> b) -> a -> b
$ \case
          Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
R:MessageLeiosNotifyfromto point announcement vote 'StBusy 'StIdle
MsgCanceled -> ExnLeiosNotifyUnexpectedCancel -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwIO ExnLeiosNotifyUnexpectedCancel
ExnLeiosNotifyUnexpectedCancel
          Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg -> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> m ()
handleReply Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg
      )

-- | The peer sent 'MsgCanceled' although the client had not sent 'MsgQuit'.
data ExnLeiosNotifyUnexpectedCancel = ExnLeiosNotifyUnexpectedCancel
  deriving Int -> ExnLeiosNotifyUnexpectedCancel -> ShowS
[ExnLeiosNotifyUnexpectedCancel] -> ShowS
ExnLeiosNotifyUnexpectedCancel -> String
(Int -> ExnLeiosNotifyUnexpectedCancel -> ShowS)
-> (ExnLeiosNotifyUnexpectedCancel -> String)
-> ([ExnLeiosNotifyUnexpectedCancel] -> ShowS)
-> Show ExnLeiosNotifyUnexpectedCancel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExnLeiosNotifyUnexpectedCancel -> ShowS
showsPrec :: Int -> ExnLeiosNotifyUnexpectedCancel -> ShowS
$cshow :: ExnLeiosNotifyUnexpectedCancel -> String
show :: ExnLeiosNotifyUnexpectedCancel -> String
$cshowList :: [ExnLeiosNotifyUnexpectedCancel] -> ShowS
showList :: [ExnLeiosNotifyUnexpectedCancel] -> ShowS
Show

instance Exception ExnLeiosNotifyUnexpectedCancel

-- | Merely an abbreviation local to this module
type X point announcement vote st m a n =
  Peer (LeiosNotify point announcement vote) AsClient (Pipelined n C) st m a

type LeiosNotifyClientPeerPipelined point announcement vote m a =
  PeerPipelined (LeiosNotify point announcement vote) AsClient StIdle m a

toLeiosNotifyClientPeerPipelined ::
  Peer (LeiosNotify point announcement vote) AsClient (Pipelined Z C) StIdle m a ->
  LeiosNotifyClientPeerPipelined point announcement vote m a
toLeiosNotifyClientPeerPipelined :: forall point announcement vote (m :: * -> *) a.
Peer
  (LeiosNotify point announcement vote)
  'AsClient
  ('Pipelined 'Z C)
  'StIdle
  m
  a
-> LeiosNotifyClientPeerPipelined point announcement vote m a
toLeiosNotifyClientPeerPipelined = Peer
  (LeiosNotify point announcement vote)
  'AsClient
  ('Pipelined 'Z C)
  'StIdle
  m
  a
-> PeerPipelined
     (LeiosNotify point announcement vote) 'AsClient 'StIdle m a
forall ps (pr :: PeerRole) c (st :: ps) (m :: * -> *) a.
Peer ps pr ('Pipelined 'Z c) st m a -> PeerPipelined ps pr st m a
PeerPipelined

data C = MkC

data WhetherDraining = AlreadyDraining | NotYetDraining

leiosNotifyClientPeerPipelined ::
  forall m point announcement vote a.
  (PrimMonad m, MonadSTM m) =>
  -- | either the return value or else the current max pipelining depth
  STM m (Either a Int) ->
  -- | INVARIANT: this will only be 'MsgCanceled' if the peer sent that before
  -- we sent 'MsgQuit'
  m (Message (LeiosNotify point announcement vote) StBusy StIdle -> m ()) ->
  Peer (LeiosNotify point announcement vote) AsClient (Pipelined Z C) StIdle m a
leiosNotifyClientPeerPipelined :: forall (m :: * -> *) point announcement vote a.
(PrimMonad m, MonadSTM m) =>
STM m (Either a Int)
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined 'Z C)
     'StIdle
     m
     a
leiosNotifyClientPeerPipelined STM m (Either a Int)
checkDone m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
   -> m ())
k0 =
  m (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined 'Z C)
     'StIdle
     m
     a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined 'Z C)
     'StIdle
     m
     a
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)
      'AsClient
      ('Pipelined 'Z C)
      'StIdle
      m
      a)
 -> Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined 'Z C)
      'StIdle
      m
      a)
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined 'Z C)
        'StIdle
        m
        a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined 'Z C)
     'StIdle
     m
     a
forall a b. (a -> b) -> a -> b
$ do
    stop <- WhetherDraining -> m (MutVar (PrimState m) WhetherDraining)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
Prim.newMutVar WhetherDraining
NotYetDraining
    arrived <- newTVarIO 0
    pure $ go stop arrived Zero
 where
  go ::
    MutVar (PrimState m) WhetherDraining ->
    StrictTVar m Int ->
    Nat n ->
    X point announcement vote StIdle m a n
  go :: forall (n :: N).
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat n
-> X point announcement vote 'StIdle m a n
go MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived !Nat n
n =
    m (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
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)
      'AsClient
      ('Pipelined n C)
      'StIdle
      m
      a)
 -> Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined n C)
      'StIdle
      m
      a)
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined n C)
        'StIdle
        m
        a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. Monad m => m (m a) -> m a
join @m (m (m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StIdle
         m
         a))
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StIdle
         m
         a))
-> m (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined n C)
           'StIdle
           m
           a))
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined n C)
        'StIdle
        m
        a)
forall a b. (a -> b) -> a -> b
$
        STM
  m
  (m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined n C)
        'StIdle
        m
        a))
-> m (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined n C)
           'StIdle
           m
           a))
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM
   m
   (m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StIdle
         m
         a))
 -> m (m (Peer
            (LeiosNotify point announcement vote)
            'AsClient
            ('Pipelined n C)
            'StIdle
            m
            a)))
-> STM
     m
     (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined n C)
           'StIdle
           m
           a))
-> m (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined n C)
           'StIdle
           m
           a))
forall a b. (a -> b) -> a -> b
$
          STM m (Either a Int)
checkDone STM m (Either a Int)
-> (Either a Int
    -> STM
         m
         (m (Peer
               (LeiosNotify point announcement vote)
               'AsClient
               ('Pipelined n C)
               'StIdle
               m
               a)))
-> STM
     m
     (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined n C)
           'StIdle
           m
           a))
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
            Left a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure @(STM m) (m (Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined n C)
      'StIdle
      m
      a)
 -> STM
      m
      (m (Peer
            (LeiosNotify point announcement vote)
            'AsClient
            ('Pipelined n C)
            'StIdle
            m
            a)))
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined n C)
        'StIdle
        m
        a)
-> STM
     m
     (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined n C)
           'StIdle
           m
           a))
forall a b. (a -> b) -> a -> b
$ do
              MutVar (PrimState m) WhetherDraining -> WhetherDraining -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
Prim.writeMutVar MutVar (PrimState m) WhetherDraining
stop WhetherDraining
AlreadyDraining
              forall (f :: * -> *) a. Applicative f => a -> f a
pure @m (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined n C)
   'StIdle
   m
   a
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StIdle
         m
         a))
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined n C)
        'StIdle
        m
        a)
forall a b. (a -> b) -> a -> b
$ case Nat n
n of
                Nat n
Zero ->
                  WeHaveAgencyProof 'AsClient 'StIdle
-> Message (LeiosNotify point announcement vote) 'StIdle 'StQuit
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StQuit
     m
     a
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
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 'ClientAgency 'WeHaveAgency 'WeHaveAgency
WeHaveAgencyProof 'AsClient 'StIdle
forall (r :: RelativeAgency). ReflRelativeAgency 'ClientAgency r r
ReflClientAgency Message (LeiosNotify point announcement vote) 'StIdle 'StQuit
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StIdle 'StQuit
MsgQuit (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined n C)
   'StQuit
   m
   a
 -> Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined n C)
      'StIdle
      m
      a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StQuit
     m
     a
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
forall a b. (a -> b) -> a -> b
$
                    TheyHaveAgencyProof 'AsClient 'StQuit
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StQuit st'
    -> Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         st'
         m
         a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StQuit
     m
     a
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 'ServerAgency 'TheyHaveAgency 'TheyHaveAgency
TheyHaveAgencyProof 'AsClient 'StQuit
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency ((forall (st' :: LeiosNotify point announcement vote).
  Message (LeiosNotify point announcement vote) 'StQuit st'
  -> Peer
       (LeiosNotify point announcement vote)
       'AsClient
       ('Pipelined n C)
       st'
       m
       a)
 -> Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined n C)
      'StQuit
      m
      a)
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StQuit st'
    -> Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         st'
         m
         a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StQuit
     m
     a
forall a b. (a -> b) -> a -> b
$ \Message (LeiosNotify point announcement vote) 'StQuit st'
R:MessageLeiosNotifyfromto point announcement vote 'StQuit st'
MsgDone ->
                      NobodyHasAgencyProof 'AsClient st'
-> a
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     st'
     m
     a
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 'AsClient st'
forall (r :: RelativeAgency). ReflRelativeAgency 'NobodyAgency r r
ReflNobodyAgency a
x
                Succ Nat n
_ ->
                  WeHaveAgencyProof 'AsClient 'StIdle
-> Message (LeiosNotify point announcement vote) 'StIdle 'StQuit
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StQuit 'StQuit m C
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S ('S n)) C)
     'StQuit
     m
     a
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
forall ps (pr :: PeerRole) (st :: ps) (st' :: ps) c (n :: N)
       (st'' :: ps) (m :: * -> *) a.
(StateTokenI st, StateTokenI st', ActiveState st) =>
WeHaveAgencyProof pr st
-> Message ps st st'
-> Receiver ps pr st' st'' m c
-> Peer ps pr ('Pipelined ('S n) c) st'' m a
-> Peer ps pr ('Pipelined n c) st m a
YieldPipelined
                    ReflRelativeAgency 'ClientAgency 'WeHaveAgency 'WeHaveAgency
WeHaveAgencyProof 'AsClient 'StIdle
forall (r :: RelativeAgency). ReflRelativeAgency 'ClientAgency r r
ReflClientAgency
                    Message (LeiosNotify point announcement vote) 'StIdle 'StQuit
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StIdle 'StQuit
MsgQuit
                    (C
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StQuit 'StQuit m C
forall c ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
c -> Receiver ps pr st st m c
ReceiverDone C
MkC) -- note that this Receiver doesn't await the MsgDone response
                    (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined ('S ('S n)) C)
   'StQuit
   m
   a
 -> Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined ('S n) C)
      'StIdle
      m
      a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S ('S n)) C)
     'StQuit
     m
     a
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
forall a b. (a -> b) -> a -> b
$ a
-> Nat ('S ('S n))
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S ('S n)) C)
     'StQuit
     m
     a
forall (n :: N).
a -> Nat n -> X point announcement vote 'StQuit m a n
drainThePipe a
x (Nat n -> Nat ('S ('S n))
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
n)
            Right Int
maxDepth ->
              case Nat n
n of
                Nat n
Zero -> forall (f :: * -> *) a. Applicative f => a -> f a
pure @(STM m) (m (Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined n C)
      'StIdle
      m
      a)
 -> STM
      m
      (m (Peer
            (LeiosNotify point announcement vote)
            'AsClient
            ('Pipelined n C)
            'StIdle
            m
            a)))
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined n C)
        'StIdle
        m
        a)
-> STM
     m
     (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined n C)
           'StIdle
           m
           a))
forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure @m (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined n C)
   'StIdle
   m
   a
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StIdle
         m
         a))
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined n C)
        'StIdle
        m
        a)
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
forall (n :: N).
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat n
-> X point announcement vote 'StIdle m a n
sendAnother MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived Nat n
n
                Succ Nat n
p
                  | Nat n -> Int
forall (n :: N). Nat n -> Int
natToInt Nat n
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxDepth ->
                      forall (f :: * -> *) a. Applicative f => a -> f a
pure @(STM m) (m (Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined ('S n) C)
      'StIdle
      m
      a)
 -> STM
      m
      (m (Peer
            (LeiosNotify point announcement vote)
            'AsClient
            ('Pipelined ('S n) C)
            'StIdle
            m
            a)))
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined ('S n) C)
        'StIdle
        m
        a)
-> STM
     m
     (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined ('S n) C)
           'StIdle
           m
           a))
forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure @m (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined ('S n) C)
   'StIdle
   m
   a
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined ('S n) C)
         'StIdle
         m
         a))
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined ('S n) C)
        'StIdle
        m
        a)
forall a b. (a -> b) -> a -> b
$ Maybe
  (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a)
-> (C
    -> Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StIdle
         m
         a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
forall ps (pr :: PeerRole) c (n :: N) (st :: ps) (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Peer ps pr ('Pipelined ('S n) c) st m a)
-> (c -> Peer ps pr ('Pipelined n c) st m a)
-> Peer ps pr ('Pipelined ('S n) c) st m a
Collect (Peer
  (LeiosNotify point announcement vote)
  'AsClient
  ('Pipelined ('S n) C)
  'StIdle
  m
  a
-> Maybe
     (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined ('S n) C)
        'StIdle
        m
        a)
forall a. a -> Maybe a
Just (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined ('S n) C)
   'StIdle
   m
   a
 -> Maybe
      (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined ('S n) C)
         'StIdle
         m
         a))
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
-> Maybe
     (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined ('S n) C)
        'StIdle
        m
        a)
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat ('S n)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
forall (n :: N).
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat n
-> X point announcement vote 'StIdle m a n
sendAnother MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived Nat n
Nat ('S n)
n) (Nat n
-> C
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
forall (p :: N).
Nat p -> C -> X point announcement vote 'StIdle m a p
collectOne Nat n
p)
                  | Bool
otherwise -> do
                      StrictTVar m Int -> STM m Int
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Int
arrived STM m Int -> (Int -> STM m ()) -> STM 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
>>= Bool -> STM m ()
forall (m :: * -> *). MonadSTM m => Bool -> STM m ()
check (Bool -> STM m ()) -> (Int -> Bool) -> Int -> STM m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
                      -- We can only call Collect if it would only block
                      -- ephemerally. That way we're always able to send MsgQuit as
                      -- soon as the Diffusion Layer commands us to.
                      --
                      -- This STM noise should be upstreamed into a CollectSTM that
                      -- runs handles whichever happens first: the continuation
                      -- becomes known or a pipelined request's reply arrives.
                      forall (f :: * -> *) a. Applicative f => a -> f a
pure @(STM m) (m (Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined ('S n) C)
      'StIdle
      m
      a)
 -> STM
      m
      (m (Peer
            (LeiosNotify point announcement vote)
            'AsClient
            ('Pipelined ('S n) C)
            'StIdle
            m
            a)))
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined ('S n) C)
        'StIdle
        m
        a)
-> STM
     m
     (m (Peer
           (LeiosNotify point announcement vote)
           'AsClient
           ('Pipelined ('S n) C)
           'StIdle
           m
           a))
forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure @m (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined ('S n) C)
   'StIdle
   m
   a
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined ('S n) C)
         'StIdle
         m
         a))
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined ('S n) C)
        'StIdle
        m
        a)
forall a b. (a -> b) -> a -> b
$ Maybe
  (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a)
-> (C
    -> Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StIdle
         m
         a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
forall ps (pr :: PeerRole) c (n :: N) (st :: ps) (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Peer ps pr ('Pipelined ('S n) c) st m a)
-> (c -> Peer ps pr ('Pipelined n c) st m a)
-> Peer ps pr ('Pipelined ('S n) c) st m a
Collect Maybe
  (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a)
forall a. Maybe a
Nothing (Nat n
-> C
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
forall (p :: N).
Nat p -> C -> X point announcement vote 'StIdle m a p
collectOne Nat n
p)
   where
    collectOne :: Nat p -> C -> X point announcement vote StIdle m a p
    collectOne :: forall (p :: N).
Nat p -> C -> X point announcement vote 'StIdle m a p
collectOne Nat p
p C
MkC = m (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined p C)
     'StIdle
     m
     a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined p C)
     'StIdle
     m
     a
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)
      'AsClient
      ('Pipelined p C)
      'StIdle
      m
      a)
 -> Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined p C)
      'StIdle
      m
      a)
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined p C)
        'StIdle
        m
        a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined p C)
     'StIdle
     m
     a
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 Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
arrived (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1)
      Peer
  (LeiosNotify point announcement vote)
  'AsClient
  ('Pipelined p C)
  'StIdle
  m
  a
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined p C)
        'StIdle
        m
        a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Peer
   (LeiosNotify point announcement vote)
   'AsClient
   ('Pipelined p C)
   'StIdle
   m
   a
 -> m (Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined p C)
         'StIdle
         m
         a))
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined p C)
     'StIdle
     m
     a
-> m (Peer
        (LeiosNotify point announcement vote)
        'AsClient
        ('Pipelined p C)
        'StIdle
        m
        a)
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat p
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined p C)
     'StIdle
     m
     a
forall (n :: N).
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat n
-> X point announcement vote 'StIdle m a n
go MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived Nat p
p

  sendAnother ::
    MutVar (PrimState m) WhetherDraining ->
    StrictTVar m Int ->
    Nat n ->
    X point announcement vote StIdle m a n
  sendAnother :: forall (n :: N).
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat n
-> X point announcement vote 'StIdle m a n
sendAnother MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived !Nat n
n =
    WeHaveAgencyProof 'AsClient 'StIdle
-> Message (LeiosNotify point announcement vote) 'StIdle 'StBusy
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StBusy 'StIdle m C
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StIdle
     m
     a
forall ps (pr :: PeerRole) (st :: ps) (st' :: ps) c (n :: N)
       (st'' :: ps) (m :: * -> *) a.
(StateTokenI st, StateTokenI st', ActiveState st) =>
WeHaveAgencyProof pr st
-> Message ps st st'
-> Receiver ps pr st' st'' m c
-> Peer ps pr ('Pipelined ('S n) c) st'' m a
-> Peer ps pr ('Pipelined n c) st m a
YieldPipelined
      ReflRelativeAgency 'ClientAgency 'WeHaveAgency 'WeHaveAgency
WeHaveAgencyProof 'AsClient 'StIdle
forall (r :: RelativeAgency). ReflRelativeAgency 'ClientAgency r r
ReflClientAgency
      Message (LeiosNotify point announcement vote) 'StIdle 'StBusy
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StIdle 'StBusy
MsgLeiosNotificationRequestNext
      (MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StBusy 'StIdle m C
receiver MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived)
      (MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat ('S n)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
forall (n :: N).
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Nat n
-> X point announcement vote 'StIdle m a n
go MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived (Nat ('S n)
 -> Peer
      (LeiosNotify point announcement vote)
      'AsClient
      ('Pipelined ('S n) C)
      'StIdle
      m
      a)
-> Nat ('S n)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StIdle
     m
     a
forall a b. (a -> b) -> a -> b
$ Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
n)

  receiver ::
    MutVar (PrimState m) WhetherDraining ->
    StrictTVar m Int ->
    Receiver (LeiosNotify point announcement vote) AsClient StBusy StIdle m C
  receiver :: MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StBusy 'StIdle m C
receiver MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived =
    TheyHaveAgencyProof 'AsClient 'StBusy
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StBusy st'
    -> Receiver
         (LeiosNotify point announcement vote) 'AsClient st' 'StIdle m C)
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StBusy 'StIdle m C
forall ps (st :: ps) (pr :: PeerRole) (stdone :: ps) (m :: * -> *)
       c.
(StateTokenI st, ActiveState st) =>
TheyHaveAgencyProof pr st
-> (forall (st' :: ps).
    Message ps st st' -> Receiver ps pr st' stdone m c)
-> Receiver ps pr st stdone m c
ReceiverAwait ReflRelativeAgency 'ServerAgency 'TheyHaveAgency 'TheyHaveAgency
TheyHaveAgencyProof 'AsClient 'StBusy
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency ((forall (st' :: LeiosNotify point announcement vote).
  Message (LeiosNotify point announcement vote) 'StBusy st'
  -> Receiver
       (LeiosNotify point announcement vote) 'AsClient st' 'StIdle m C)
 -> Receiver
      (LeiosNotify point announcement vote)
      'AsClient
      'StBusy
      'StIdle
      m
      C)
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StBusy st'
    -> Receiver
         (LeiosNotify point announcement vote) 'AsClient st' 'StIdle m C)
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StBusy 'StIdle m C
forall a b. (a -> b) -> a -> b
$ \Message (LeiosNotify point announcement vote) 'StBusy st'
msg -> case Message (LeiosNotify point announcement vote) 'StBusy st'
msg of
      MsgLeiosBlockAnnouncement{} -> MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall msg.
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (msg -> m ())
-> msg
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
handler MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
   -> m ())
k0 Message (LeiosNotify point announcement vote) 'StBusy st'
Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg
      MsgLeiosBlockOffer{} -> MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall msg.
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (msg -> m ())
-> msg
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
handler MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
   -> m ())
k0 Message (LeiosNotify point announcement vote) 'StBusy st'
Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg
      MsgLeiosBlockTxsOffer{} -> MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall msg.
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (msg -> m ())
-> msg
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
handler MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
   -> m ())
k0 Message (LeiosNotify point announcement vote) 'StBusy st'
Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg
      MsgLeiosVotes{} -> MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall msg.
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (msg -> m ())
-> msg
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
handler MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
   -> m ())
k0 Message (LeiosNotify point announcement vote) 'StBusy st'
Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg
      MsgCanceled{} -> MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
      -> m ())
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall msg.
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (msg -> m ())
-> msg
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
handler MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived m (Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
   -> m ())
k0 Message (LeiosNotify point announcement vote) 'StBusy st'
Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
msg

  handler ::
    MutVar (PrimState m) WhetherDraining ->
    StrictTVar m Int ->
    m (msg -> m ()) ->
    msg ->
    Receiver (LeiosNotify point announcement vote) AsClient StIdle StIdle m C
  handler :: forall msg.
MutVar (PrimState m) WhetherDraining
-> StrictTVar m Int
-> m (msg -> m ())
-> msg
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
handler MutVar (PrimState m) WhetherDraining
stop StrictTVar m Int
arrived m (msg -> m ())
k msg
x = m (Receiver
     (LeiosNotify point announcement vote)
     'AsClient
     'StIdle
     'StIdle
     m
     C)
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (stdone :: ps)
       c.
m (Receiver ps pr st stdone m c) -> Receiver ps pr st stdone m c
ReceiverEffect (m (Receiver
      (LeiosNotify point announcement vote)
      'AsClient
      'StIdle
      'StIdle
      m
      C)
 -> Receiver
      (LeiosNotify point announcement vote)
      'AsClient
      'StIdle
      'StIdle
      m
      C)
-> m (Receiver
        (LeiosNotify point announcement vote)
        'AsClient
        'StIdle
        'StIdle
        m
        C)
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall a b. (a -> b) -> a -> b
$ do
    MutVar (PrimState m) WhetherDraining -> m WhetherDraining
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
Prim.readMutVar MutVar (PrimState m) WhetherDraining
stop m WhetherDraining -> (WhetherDraining -> 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
      WhetherDraining
AlreadyDraining -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      WhetherDraining
NotYetDraining -> m (msg -> m ())
k m (msg -> m ()) -> ((msg -> m ()) -> 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
>>= ((msg -> m ()) -> msg -> m ()
forall a b. (a -> b) -> a -> b
$ msg
x)
    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 Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
arrived (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    Receiver
  (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
-> m (Receiver
        (LeiosNotify point announcement vote)
        'AsClient
        'StIdle
        'StIdle
        m
        C)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Receiver
   (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
 -> m (Receiver
         (LeiosNotify point announcement vote)
         'AsClient
         'StIdle
         'StIdle
         m
         C))
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
-> m (Receiver
        (LeiosNotify point announcement vote)
        'AsClient
        'StIdle
        'StIdle
        m
        C)
forall a b. (a -> b) -> a -> b
$ C
-> Receiver
     (LeiosNotify point announcement vote) 'AsClient 'StIdle 'StIdle m C
forall c ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
c -> Receiver ps pr st st m c
ReceiverDone C
MkC

  drainThePipe :: a -> Nat n -> X point announcement vote StQuit m a n
  drainThePipe :: forall (n :: N).
a -> Nat n -> X point announcement vote 'StQuit m a n
drainThePipe a
x = \case
    Nat n
Zero ->
      TheyHaveAgencyProof 'AsClient 'StQuit
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StQuit st'
    -> Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         st'
         m
         a)
-> X point announcement vote 'StQuit m a n
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 'ServerAgency 'TheyHaveAgency 'TheyHaveAgency
TheyHaveAgencyProof 'AsClient 'StQuit
forall (r :: RelativeAgency). ReflRelativeAgency 'ServerAgency r r
ReflServerAgency ((forall (st' :: LeiosNotify point announcement vote).
  Message (LeiosNotify point announcement vote) 'StQuit st'
  -> Peer
       (LeiosNotify point announcement vote)
       'AsClient
       ('Pipelined n C)
       st'
       m
       a)
 -> X point announcement vote 'StQuit m a n)
-> (forall (st' :: LeiosNotify point announcement vote).
    Message (LeiosNotify point announcement vote) 'StQuit st'
    -> Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         st'
         m
         a)
-> X point announcement vote 'StQuit m a n
forall a b. (a -> b) -> a -> b
$ \Message (LeiosNotify point announcement vote) 'StQuit st'
R:MessageLeiosNotifyfromto point announcement vote 'StQuit st'
MsgDone ->
        NobodyHasAgencyProof 'AsClient st'
-> a
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     st'
     m
     a
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 'AsClient st'
forall (r :: RelativeAgency). ReflRelativeAgency 'NobodyAgency r r
ReflNobodyAgency a
x
    Succ Nat n
m ->
      Maybe
  (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StQuit
     m
     a)
-> (C
    -> Peer
         (LeiosNotify point announcement vote)
         'AsClient
         ('Pipelined n C)
         'StQuit
         m
         a)
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StQuit
     m
     a
forall ps (pr :: PeerRole) c (n :: N) (st :: ps) (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Peer ps pr ('Pipelined ('S n) c) st m a)
-> (c -> Peer ps pr ('Pipelined n c) st m a)
-> Peer ps pr ('Pipelined ('S n) c) st m a
Collect
        Maybe
  (Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined ('S n) C)
     'StQuit
     m
     a)
forall a. Maybe a
Nothing -- OK to block, since we're entirely passive now
        (\C
MkC -> a
-> Nat n
-> Peer
     (LeiosNotify point announcement vote)
     'AsClient
     ('Pipelined n C)
     'StQuit
     m
     a
forall (n :: N).
a -> Nat n -> X point announcement vote 'StQuit m a n
drainThePipe a
x Nat n
m)