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

module Ouroboros.Network.Protocol.ChainSync.ClientPipelined
  ( ChainSyncClientPipelined (..)
  , ClientPipelinedStIdle (..)
  , ClientStNext (..)
  , ClientPipelinedStIntersect (..)
  , ChainSyncInstruction (..)
  , chainSyncClientPeerPipelined
  , chainSyncClientPeerSender
  , mapChainSyncClientPipelined
  ) where

import           Data.Kind (Type)

import           Network.TypedProtocol.Core
import           Network.TypedProtocol.Pipelined

import           Ouroboros.Network.Protocol.ChainSync.Type


-- | Pipelined chain sync client.  It can only pipeline 'MsgRequestNext'
-- messages, while the 'MsgFindIntersect' are non pipelined.  This has a penalty
-- cost of an RTT, but they are send relatively seldom and their response might
-- impact how many messages one would like to pipeline.  It also simplifies the
-- receiver callback.
--
newtype ChainSyncClientPipelined header point tip m a =
  ChainSyncClientPipelined {
    ChainSyncClientPipelined header point tip m a
-> m (ClientPipelinedStIdle 'Z header point tip m a)
runChainSyncClientPipelined :: m (ClientPipelinedStIdle Z header point tip m a)
  }


-- | Pipelined sender which starts in 'StIdle' state.  It can either
--
-- * Send 'MsgRequestNext' (no pipelining), which might be useful when we are at
--   the tip of the chain.  It can only be send when there is no pipelined
--   message in flight (all responses were collected);
--
-- * Pipeline 'MsgRequestNext';
--
-- * Send 'MsgFindIntersect' (no pipelining); It can only be send when there is
--   no pipelined message in flight (all responses were collected);
--
-- * Collect responses of pipelined message;
--
-- * Terminate the protocol with by sending 'MsgDone'.
--
data ClientPipelinedStIdle n header point tip  m a where

    SendMsgRequestNext
      ::    ClientStNext       Z header point tip m a
      -> m (ClientStNext       Z header point tip m a)
      -> ClientPipelinedStIdle Z header point tip m a

    SendMsgRequestNextPipelined
      :: ClientPipelinedStIdle (S n) header point tip m a
      -> ClientPipelinedStIdle    n  header point tip m a

    SendMsgFindIntersect
      :: [point]
      -> ClientPipelinedStIntersect   header point tip m a
      -> ClientPipelinedStIdle      Z header point tip m a

    CollectResponse
      :: Maybe (m (ClientPipelinedStIdle (S n) header point tip m a))
      -> ClientStNext                       n  header point tip m a
      -> ClientPipelinedStIdle           (S n) header point tip m a

    SendMsgDone
      :: a
      -> ClientPipelinedStIdle Z header point tip m a

-- | Callback for responses received after sending 'MsgRequestNext'.
--
-- We could receive 'MsgAwaitReply'. In this case we will wait for the next
-- message which must be 'MsgRollForward' or 'MsgRollBackward'; thus we need
-- only the two callbacks.
--
data ClientStNext n header point tip m a =
     ClientStNext {
       -- | Callback for 'MsgRollForward' message.
       --
       ClientStNext n header point tip m a
-> header
-> tip
-> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward
         :: header
         -> tip
         -> m (ClientPipelinedStIdle n header point tip m a),

       -- | Callback for 'MsgRollBackward' message.
       --
       ClientStNext n header point tip m a
-> point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward
         :: point
         -> tip
         -> m (ClientPipelinedStIdle n header point tip m a)
     }

-- | Callbacks for messages received after sending 'MsgFindIntersect'.
--
-- We might receive either 'MsgIntersectFound' or 'MsgIntersectNotFound'.
--
data ClientPipelinedStIntersect header point tip m a =
     ClientPipelinedStIntersect {

       ClientPipelinedStIntersect header point tip m a
-> point
-> tip
-> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound
         :: point
         -> tip
          -> m (ClientPipelinedStIdle Z header point tip m a),

       ClientPipelinedStIntersect header point tip m a
-> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound
         :: tip
         -> m (ClientPipelinedStIdle Z header point tip m a)
     }

-- | Transform a 'ChainSyncClientPipelined' by mapping over the tx header and
-- the chain tip values.
--
-- Note the direction of the individual mapping functions corresponds to
-- whether the types are used as protocol inputs or outputs (or both, as is
-- the case for points).
--
mapChainSyncClientPipelined :: forall header header' point point' tip tip' (m :: Type -> Type) a.
  Functor m
  => (point -> point')
  -> (point' -> point)
  -> (header' -> header)
  -> (tip' -> tip)
  -> ChainSyncClientPipelined header point tip m a
  -> ChainSyncClientPipelined header' point' tip' m a
mapChainSyncClientPipelined :: (point -> point')
-> (point' -> point)
-> (header' -> header)
-> (tip' -> tip)
-> ChainSyncClientPipelined header point tip m a
-> ChainSyncClientPipelined header' point' tip' m a
mapChainSyncClientPipelined point -> point'
toPoint' point' -> point
toPoint header' -> header
toHeader tip' -> tip
toTip (ChainSyncClientPipelined m (ClientPipelinedStIdle 'Z header point tip m a)
mInitialIdleClient)
  = m (ClientPipelinedStIdle 'Z header' point' tip' m a)
-> ChainSyncClientPipelined header' point' tip' m a
forall header point tip (m :: * -> *) a.
m (ClientPipelinedStIdle 'Z header point tip m a)
-> ChainSyncClientPipelined header point tip m a
ChainSyncClientPipelined (ClientPipelinedStIdle 'Z header point tip m a
-> ClientPipelinedStIdle 'Z header' point' tip' m a
forall (n :: N).
ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle (ClientPipelinedStIdle 'Z header point tip m a
 -> ClientPipelinedStIdle 'Z header' point' tip' m a)
-> m (ClientPipelinedStIdle 'Z header point tip m a)
-> m (ClientPipelinedStIdle 'Z header' point' tip' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ClientPipelinedStIdle 'Z header point tip m a)
mInitialIdleClient)
  where
    goIdle :: ClientPipelinedStIdle n header point tip  m a
           -> ClientPipelinedStIdle n header' point' tip'  m a
    goIdle :: ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle ClientPipelinedStIdle n header point tip m a
client = case ClientPipelinedStIdle n header point tip m a
client of
      SendMsgRequestNext ClientStNext 'Z header point tip m a
next m (ClientStNext 'Z header point tip m a)
mNext -> ClientStNext 'Z header' point' tip' m a
-> m (ClientStNext 'Z header' point' tip' m a)
-> ClientPipelinedStIdle 'Z header' point' tip' m a
forall header point tip (m :: * -> *) a.
ClientStNext 'Z header point tip m a
-> m (ClientStNext 'Z header point tip m a)
-> ClientPipelinedStIdle 'Z header point tip m a
SendMsgRequestNext (ClientStNext 'Z header point tip m a
-> ClientStNext 'Z header' point' tip' m a
forall (n :: N).
ClientStNext n header point tip m a
-> ClientStNext n header' point' tip' m a
goNext ClientStNext 'Z header point tip m a
next) (ClientStNext 'Z header point tip m a
-> ClientStNext 'Z header' point' tip' m a
forall (n :: N).
ClientStNext n header point tip m a
-> ClientStNext n header' point' tip' m a
goNext (ClientStNext 'Z header point tip m a
 -> ClientStNext 'Z header' point' tip' m a)
-> m (ClientStNext 'Z header point tip m a)
-> m (ClientStNext 'Z header' point' tip' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ClientStNext 'Z header point tip m a)
mNext)
      SendMsgRequestNextPipelined ClientPipelinedStIdle ('S n) header point tip m a
idle -> ClientPipelinedStIdle ('S n) header' point' tip' m a
-> ClientPipelinedStIdle n header' point' tip' m a
forall (n :: N) header point tip (m :: * -> *) a.
ClientPipelinedStIdle ('S n) header point tip m a
-> ClientPipelinedStIdle n header point tip m a
SendMsgRequestNextPipelined (ClientPipelinedStIdle ('S n) header point tip m a
-> ClientPipelinedStIdle ('S n) header' point' tip' m a
forall (n :: N).
ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle ClientPipelinedStIdle ('S n) header point tip m a
idle)
      SendMsgFindIntersect [point]
points ClientPipelinedStIntersect header point tip m a
inter -> [point']
-> ClientPipelinedStIntersect header' point' tip' m a
-> ClientPipelinedStIdle 'Z header' point' tip' m a
forall point header tip (m :: * -> *) a.
[point]
-> ClientPipelinedStIntersect header point tip m a
-> ClientPipelinedStIdle 'Z header point tip m a
SendMsgFindIntersect (point -> point'
toPoint' (point -> point') -> [point] -> [point']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [point]
points) (ClientPipelinedStIntersect header point tip m a
-> ClientPipelinedStIntersect header' point' tip' m a
goIntersect ClientPipelinedStIntersect header point tip m a
inter)
      CollectResponse Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
idleMay ClientStNext n header point tip m a
next -> Maybe (m (ClientPipelinedStIdle ('S n) header' point' tip' m a))
-> ClientStNext n header' point' tip' m a
-> ClientPipelinedStIdle ('S n) header' point' tip' m a
forall (m :: * -> *) (n :: N) header point tip a.
Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
-> ClientStNext n header point tip m a
-> ClientPipelinedStIdle ('S n) header point tip m a
CollectResponse ((ClientPipelinedStIdle ('S n) header point tip m a
 -> ClientPipelinedStIdle ('S n) header' point' tip' m a)
-> m (ClientPipelinedStIdle ('S n) header point tip m a)
-> m (ClientPipelinedStIdle ('S n) header' point' tip' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClientPipelinedStIdle ('S n) header point tip m a
-> ClientPipelinedStIdle ('S n) header' point' tip' m a
forall (n :: N).
ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle (m (ClientPipelinedStIdle ('S n) header point tip m a)
 -> m (ClientPipelinedStIdle ('S n) header' point' tip' m a))
-> Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
-> Maybe (m (ClientPipelinedStIdle ('S n) header' point' tip' m a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
idleMay) (ClientStNext n header point tip m a
-> ClientStNext n header' point' tip' m a
forall (n :: N).
ClientStNext n header point tip m a
-> ClientStNext n header' point' tip' m a
goNext ClientStNext n header point tip m a
next)
      SendMsgDone a
a -> a -> ClientPipelinedStIdle 'Z header' point' tip' m a
forall a header point tip (m :: * -> *).
a -> ClientPipelinedStIdle 'Z header point tip m a
SendMsgDone a
a

    goNext :: ClientStNext n header point tip  m a
           -> ClientStNext n header' point' tip'  m a
    goNext :: ClientStNext n header point tip m a
-> ClientStNext n header' point' tip' m a
goNext ClientStNext{ header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward :: header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> header
-> tip
-> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward, point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward :: point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward } = ClientStNext :: forall (n :: N) header point tip (m :: * -> *) a.
(header -> tip -> m (ClientPipelinedStIdle n header point tip m a))
-> (point
    -> tip -> m (ClientPipelinedStIdle n header point tip m a))
-> ClientStNext n header point tip m a
ClientStNext
      { recvMsgRollForward :: header'
-> tip' -> m (ClientPipelinedStIdle n header' point' tip' m a)
recvMsgRollForward = \header'
header' tip'
tip' -> ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
forall (n :: N).
ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle (ClientPipelinedStIdle n header point tip m a
 -> ClientPipelinedStIdle n header' point' tip' m a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (ClientPipelinedStIdle n header' point' tip' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward (header' -> header
toHeader header'
header') (tip' -> tip
toTip tip'
tip')
      , recvMsgRollBackward :: point'
-> tip' -> m (ClientPipelinedStIdle n header' point' tip' m a)
recvMsgRollBackward = \point'
point' tip'
tip' -> ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
forall (n :: N).
ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle (ClientPipelinedStIdle n header point tip m a
 -> ClientPipelinedStIdle n header' point' tip' m a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (ClientPipelinedStIdle n header' point' tip' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward (point' -> point
toPoint point'
point') (tip' -> tip
toTip tip'
tip')
      }

    goIntersect :: ClientPipelinedStIntersect header point tip m a
                -> ClientPipelinedStIntersect header' point' tip' m a
    goIntersect :: ClientPipelinedStIntersect header point tip m a
-> ClientPipelinedStIntersect header' point' tip' m a
goIntersect ClientPipelinedStIntersect{ point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound :: point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound :: forall header point tip (m :: * -> *) a.
ClientPipelinedStIntersect header point tip m a
-> point
-> tip
-> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound, tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound :: tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound :: forall header point tip (m :: * -> *) a.
ClientPipelinedStIntersect header point tip m a
-> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound } = ClientPipelinedStIntersect :: forall header point tip (m :: * -> *) a.
(point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a))
-> (tip -> m (ClientPipelinedStIdle 'Z header point tip m a))
-> ClientPipelinedStIntersect header point tip m a
ClientPipelinedStIntersect
      { recvMsgIntersectFound :: point'
-> tip' -> m (ClientPipelinedStIdle 'Z header' point' tip' m a)
recvMsgIntersectFound = \point'
point' tip'
tip' -> ClientPipelinedStIdle 'Z header point tip m a
-> ClientPipelinedStIdle 'Z header' point' tip' m a
forall (n :: N).
ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle (ClientPipelinedStIdle 'Z header point tip m a
 -> ClientPipelinedStIdle 'Z header' point' tip' m a)
-> m (ClientPipelinedStIdle 'Z header point tip m a)
-> m (ClientPipelinedStIdle 'Z header' point' tip' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound (point' -> point
toPoint point'
point') (tip' -> tip
toTip tip'
tip')
      , recvMsgIntersectNotFound :: tip' -> m (ClientPipelinedStIdle 'Z header' point' tip' m a)
recvMsgIntersectNotFound = \tip'
tip' -> ClientPipelinedStIdle 'Z header point tip m a
-> ClientPipelinedStIdle 'Z header' point' tip' m a
forall (n :: N).
ClientPipelinedStIdle n header point tip m a
-> ClientPipelinedStIdle n header' point' tip' m a
goIdle (ClientPipelinedStIdle 'Z header point tip m a
 -> ClientPipelinedStIdle 'Z header' point' tip' m a)
-> m (ClientPipelinedStIdle 'Z header point tip m a)
-> m (ClientPipelinedStIdle 'Z header' point' tip' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound (tip' -> tip
toTip tip'
tip')
      }


--
-- Pipelined Peer
--

-- | Data received through pipelining: either roll forward or roll backward
-- instruction. If the server replied with 'MsgAwaitReply' the pipelined
-- receiver will await for the next message which must come with an instruction
-- how to update our chain.
--
-- Note: internal API, not exposed by this module.
--
data ChainSyncInstruction header point tip
    = RollForward  !header !tip
    | RollBackward !point  !tip


chainSyncClientPeerPipelined
    :: forall header point tip m a.
       Monad m
    => ChainSyncClientPipelined header point tip m a
    -> PeerPipelined (ChainSync header point tip) AsClient StIdle m a

chainSyncClientPeerPipelined :: ChainSyncClientPipelined header point tip m a
-> PeerPipelined (ChainSync header point tip) 'AsClient 'StIdle m a
chainSyncClientPeerPipelined (ChainSyncClientPipelined m (ClientPipelinedStIdle 'Z header point tip m a)
mclient) =
    PeerSender
  (ChainSync header point tip)
  'AsClient
  'StIdle
  'Z
  (ChainSyncInstruction header point tip)
  m
  a
-> PeerPipelined (ChainSync header point tip) 'AsClient 'StIdle m a
forall ps (pr :: PeerRole) (st :: ps) c (m :: * -> *) a.
PeerSender ps pr st 'Z c m a -> PeerPipelined ps pr st m a
PeerPipelined (PeerSender
   (ChainSync header point tip)
   'AsClient
   'StIdle
   'Z
   (ChainSyncInstruction header point tip)
   m
   a
 -> PeerPipelined
      (ChainSync header point tip) 'AsClient 'StIdle m a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
-> PeerPipelined (ChainSync header point tip) 'AsClient 'StIdle m a
forall a b. (a -> b) -> a -> b
$ m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      'Z
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      'Z
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        'Z
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$ Nat 'Z
-> ClientPipelinedStIdle 'Z header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat 'Z
forall (n :: N). ('Z ~ n) => Nat n
Zero (ClientPipelinedStIdle 'Z header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      'Z
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle 'Z header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        'Z
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ClientPipelinedStIdle 'Z header point tip m a)
mclient


chainSyncClientPeerSender
    :: forall n header point tip m a.
       Monad m
    => Nat n
    -> ClientPipelinedStIdle n header point tip m a
    -> PeerSender (ChainSync header point tip)
                  AsClient StIdle n
                  (ChainSyncInstruction header point tip)
                  m a

chainSyncClientPeerSender :: Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender n :: Nat n
n@Nat n
Zero (SendMsgRequestNext ClientStNext 'Z header point tip m a
stNext m (ClientStNext 'Z header point tip m a)
stAwait) =

    WeHaveAgency 'AsClient 'StIdle
-> Message
     (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StCanAwait)
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) c (m :: * -> *)
       a.
WeHaveAgency pr st
-> Message ps st st'
-> PeerSender ps pr st' 'Z c m a
-> PeerSender ps pr st 'Z c m a
SenderYield
      (ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
forall k k k (header :: k) (point :: k) (tip :: k).
ClientHasAgency 'StIdle
TokIdle)
      Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
forall k k k (header :: k) (point :: k) (tip :: k).
Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
MsgRequestNext
      (TheyHaveAgency 'AsClient ('StNext 'StCanAwait)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
    -> PeerSender
         (ChainSync header point tip)
         'AsClient
         st'
         'Z
         (ChainSyncInstruction header point tip)
         m
         a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StCanAwait)
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) c (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps).
    Message ps st st' -> PeerSender ps pr st' 'Z c m a)
-> PeerSender ps pr st 'Z c m a
SenderAwait
        (ServerHasAgency ('StNext 'StCanAwait)
-> PeerHasAgency 'AsServer ('StNext 'StCanAwait)
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency (TokNextKind 'StCanAwait -> ServerHasAgency ('StNext 'StCanAwait)
forall k k k (header :: k) (point :: k) (tip :: k)
       (k :: StNextKind).
TokNextKind k -> ServerHasAgency ('StNext k)
TokNext TokNextKind 'StCanAwait
TokCanAwait))
          ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
  -> PeerSender
       (ChainSync header point tip)
       'AsClient
       st'
       'Z
       (ChainSyncInstruction header point tip)
       m
       a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      ('StNext 'StCanAwait)
      'Z
      (ChainSyncInstruction header point tip)
      m
      a)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
    -> PeerSender
         (ChainSync header point tip)
         'AsClient
         st'
         'Z
         (ChainSyncInstruction header point tip)
         m
         a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StCanAwait)
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$ \case
            MsgRollForward header tip ->
              m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$
                  Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n
                    (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward header
header
header tip
tip
tip
                where
                  ClientStNext {header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward :: header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> header
-> tip
-> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward} = ClientStNext 'Z header point tip m a
stNext

            MsgRollBackward pRollback tip ->
              m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$
                  Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n
                    (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward point
point
pRollback tip
tip
tip
                where
                  ClientStNext {point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward :: point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward} = ClientStNext 'Z header point tip m a
stNext

            Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
MsgAwaitReply ->
              TheyHaveAgency 'AsClient ('StNext 'StMustReply)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StMustReply) st'
    -> PeerSender
         (ChainSync header point tip)
         'AsClient
         st'
         'Z
         (ChainSyncInstruction header point tip)
         m
         a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StMustReply)
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) c (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps).
    Message ps st st' -> PeerSender ps pr st' 'Z c m a)
-> PeerSender ps pr st 'Z c m a
SenderAwait
                (ServerHasAgency ('StNext 'StMustReply)
-> PeerHasAgency 'AsServer ('StNext 'StMustReply)
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency (TokNextKind 'StMustReply -> ServerHasAgency ('StNext 'StMustReply)
forall k k k (header :: k) (point :: k) (tip :: k)
       (k :: StNextKind).
TokNextKind k -> ServerHasAgency ('StNext k)
TokNext TokNextKind 'StMustReply
TokMustReply))
                ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) ('StNext 'StMustReply) st'
  -> PeerSender
       (ChainSync header point tip)
       'AsClient
       st'
       'Z
       (ChainSyncInstruction header point tip)
       m
       a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      ('StNext 'StMustReply)
      'Z
      (ChainSyncInstruction header point tip)
      m
      a)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StMustReply) st'
    -> PeerSender
         (ChainSync header point tip)
         'AsClient
         st'
         'Z
         (ChainSyncInstruction header point tip)
         m
         a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StMustReply)
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$ \case
                  MsgRollForward header tip ->
                    m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$ do
                      ClientStNext {header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward :: header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> header
-> tip
-> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward} <- m (ClientStNext 'Z header point tip m a)
stAwait
                      Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n
                        (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward header
header
header tip
tip
tip

                  MsgRollBackward pRollback tip ->
                    m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$ do
                      ClientStNext {point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward :: point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward} <- m (ClientStNext 'Z header point tip m a)
stAwait
                      Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n
                        (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward point
point
pRollback tip
tip
tip)


chainSyncClientPeerSender Nat n
n (SendMsgRequestNextPipelined ClientPipelinedStIdle ('S n) header point tip m a
next) =

    -- pipeline 'MsgRequestNext', the receiver will await for an instruction.
    WeHaveAgency 'AsClient 'StIdle
-> Message
     (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StCanAwait)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     ('S n)
     (ChainSyncInstruction header point tip)
     m
     a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (st'' :: ps)
       (m :: * -> *) c (n :: N) a.
WeHaveAgency pr st
-> Message ps st st'
-> PeerReceiver ps pr st' st'' m c
-> PeerSender ps pr st'' ('S n) c m a
-> PeerSender ps pr st n c m a
SenderPipeline
      (ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
forall k k k (header :: k) (point :: k) (tip :: k).
ClientHasAgency 'StIdle
TokIdle)
      Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
forall k k k (header :: k) (point :: k) (tip :: k).
Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
MsgRequestNext

      (TheyHaveAgency 'AsClient ('StNext 'StCanAwait)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
    -> PeerReceiver
         (ChainSync header point tip)
         'AsClient
         st'
         'StIdle
         m
         (ChainSyncInstruction header point tip))
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StCanAwait)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall (pr :: PeerRole) ps (st :: ps) (stdone :: ps) (m :: * -> *)
       c.
TheyHaveAgency pr st
-> (forall (st' :: ps).
    Message ps st st' -> PeerReceiver ps pr st' stdone m c)
-> PeerReceiver ps pr st stdone m c
ReceiverAwait (ServerHasAgency ('StNext 'StCanAwait)
-> PeerHasAgency 'AsServer ('StNext 'StCanAwait)
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency (TokNextKind 'StCanAwait -> ServerHasAgency ('StNext 'StCanAwait)
forall k k k (header :: k) (point :: k) (tip :: k)
       (k :: StNextKind).
TokNextKind k -> ServerHasAgency ('StNext k)
TokNext TokNextKind 'StCanAwait
TokCanAwait))
        -- await for the reply
        ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
  -> PeerReceiver
       (ChainSync header point tip)
       'AsClient
       st'
       'StIdle
       m
       (ChainSyncInstruction header point tip))
 -> PeerReceiver
      (ChainSync header point tip)
      'AsClient
      ('StNext 'StCanAwait)
      'StIdle
      m
      (ChainSyncInstruction header point tip))
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
    -> PeerReceiver
         (ChainSync header point tip)
         'AsClient
         st'
         'StIdle
         m
         (ChainSyncInstruction header point tip))
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StCanAwait)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall a b. (a -> b) -> a -> b
$ \case
          MsgRollForward  header    tip -> ChainSyncInstruction header point tip
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall c ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
c -> PeerReceiver ps pr st st m c
ReceiverDone (header -> tip -> ChainSyncInstruction header point tip
forall header point tip.
header -> tip -> ChainSyncInstruction header point tip
RollForward header
header tip
tip)
          MsgRollBackward pRollback tip -> ChainSyncInstruction header point tip
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall c ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
c -> PeerReceiver ps pr st st m c
ReceiverDone (point -> tip -> ChainSyncInstruction header point tip
forall header point tip.
point -> tip -> ChainSyncInstruction header point tip
RollBackward point
pRollback tip
tip)

          -- we need to wait for the next message; this time it must come with
          -- an instruction
          Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
MsgAwaitReply -> TheyHaveAgency 'AsClient ('StNext 'StMustReply)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StMustReply) st'
    -> PeerReceiver
         (ChainSync header point tip)
         'AsClient
         st'
         'StIdle
         m
         (ChainSyncInstruction header point tip))
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StMustReply)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall (pr :: PeerRole) ps (st :: ps) (stdone :: ps) (m :: * -> *)
       c.
TheyHaveAgency pr st
-> (forall (st' :: ps).
    Message ps st st' -> PeerReceiver ps pr st' stdone m c)
-> PeerReceiver ps pr st stdone m c
ReceiverAwait (ServerHasAgency ('StNext 'StMustReply)
-> PeerHasAgency 'AsServer ('StNext 'StMustReply)
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency (TokNextKind 'StMustReply -> ServerHasAgency ('StNext 'StMustReply)
forall k k k (header :: k) (point :: k) (tip :: k)
       (k :: StNextKind).
TokNextKind k -> ServerHasAgency ('StNext k)
TokNext TokNextKind 'StMustReply
TokMustReply))
            ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) ('StNext 'StMustReply) st'
  -> PeerReceiver
       (ChainSync header point tip)
       'AsClient
       st'
       'StIdle
       m
       (ChainSyncInstruction header point tip))
 -> PeerReceiver
      (ChainSync header point tip)
      'AsClient
      ('StNext 'StMustReply)
      'StIdle
      m
      (ChainSyncInstruction header point tip))
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StMustReply) st'
    -> PeerReceiver
         (ChainSync header point tip)
         'AsClient
         st'
         'StIdle
         m
         (ChainSyncInstruction header point tip))
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     ('StNext 'StMustReply)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall a b. (a -> b) -> a -> b
$ \case
              MsgRollForward  header    tip -> ChainSyncInstruction header point tip
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall c ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
c -> PeerReceiver ps pr st st m c
ReceiverDone (header -> tip -> ChainSyncInstruction header point tip
forall header point tip.
header -> tip -> ChainSyncInstruction header point tip
RollForward header
header tip
tip)
              MsgRollBackward pRollback tip -> ChainSyncInstruction header point tip
-> PeerReceiver
     (ChainSync header point tip)
     'AsClient
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall c ps (pr :: PeerRole) (st :: ps) (m :: * -> *).
c -> PeerReceiver ps pr st st m c
ReceiverDone (point -> tip -> ChainSyncInstruction header point tip
forall header point tip.
point -> tip -> ChainSyncInstruction header point tip
RollBackward point
pRollback tip
tip))

      (Nat ('S n)
-> ClientPipelinedStIdle ('S n) header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     ('S n)
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
n) ClientPipelinedStIdle ('S n) header point tip m a
next)

chainSyncClientPeerSender Nat n
n (SendMsgFindIntersect [point]
points
                              ClientPipelinedStIntersect
                                { point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound :: point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound :: forall header point tip (m :: * -> *) a.
ClientPipelinedStIntersect header point tip m a
-> point
-> tip
-> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound
                                , tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound :: tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound :: forall header point tip (m :: * -> *) a.
ClientPipelinedStIntersect header point tip m a
-> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound
                                }) =

    -- non pipelined 'MsgFindIntersect'
    WeHaveAgency 'AsClient 'StIdle
-> Message (ChainSync header point tip) 'StIdle 'StIntersect
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIntersect
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) c (m :: * -> *)
       a.
WeHaveAgency pr st
-> Message ps st st'
-> PeerSender ps pr st' 'Z c m a
-> PeerSender ps pr st 'Z c m a
SenderYield
      (ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
forall k k k (header :: k) (point :: k) (tip :: k).
ClientHasAgency 'StIdle
TokIdle)
      ([point]
-> Message (ChainSync header point tip) 'StIdle 'StIntersect
forall k k point (header :: k) (tip :: k).
[point]
-> Message (ChainSync header point tip) 'StIdle 'StIntersect
MsgFindIntersect [point]
points)
      (TheyHaveAgency 'AsClient 'StIntersect
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) 'StIntersect st'
    -> PeerSender
         (ChainSync header point tip)
         'AsClient
         st'
         'Z
         (ChainSyncInstruction header point tip)
         m
         a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIntersect
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) c (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps).
    Message ps st st' -> PeerSender ps pr st' 'Z c m a)
-> PeerSender ps pr st 'Z c m a
SenderAwait (ServerHasAgency 'StIntersect
-> PeerHasAgency 'AsServer 'StIntersect
forall ps (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StIntersect
forall k k k (header :: k) (point :: k) (tip :: k).
ServerHasAgency 'StIntersect
TokIntersect)
        -- await for the response and recurse
        ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) 'StIntersect st'
  -> PeerSender
       (ChainSync header point tip)
       'AsClient
       st'
       'Z
       (ChainSyncInstruction header point tip)
       m
       a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIntersect
      'Z
      (ChainSyncInstruction header point tip)
      m
      a)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) 'StIntersect st'
    -> PeerSender
         (ChainSync header point tip)
         'AsClient
         st'
         'Z
         (ChainSyncInstruction header point tip)
         m
         a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIntersect
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$ \case
          MsgIntersectFound pIntersect tip ->
            m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$
              Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectFound point
point
pIntersect tip
tip
tip
          MsgIntersectNotFound tip ->
            m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$
              Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound tip
tip
tip
          )

chainSyncClientPeerSender n :: Nat n
n@(Succ Nat n
n')
                          (CollectResponse Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
mStIdle
                            ClientStNext
                              { header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward :: header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> header
-> tip
-> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward
                              , point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward :: point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward :: forall (n :: N) header point tip (m :: * -> *) a.
ClientStNext n header point tip m a
-> point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward
                              }) =

    Maybe
  (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     ('S n)
     (ChainSyncInstruction header point tip)
     m
     a)
-> (ChainSyncInstruction header point tip
    -> PeerSender
         (ChainSync header point tip)
         'AsClient
         'StIdle
         n
         (ChainSyncInstruction header point tip)
         m
         a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     ('S n)
     (ChainSyncInstruction header point tip)
     m
     a
forall ps (pr :: PeerRole) (st :: ps) (n1 :: N) c (m :: * -> *) a.
Maybe (PeerSender ps pr st ('S n1) c m a)
-> (c -> PeerSender ps pr st n1 c m a)
-> PeerSender ps pr st ('S n1) c m a
SenderCollect
      (m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> (m (ClientPipelinedStIdle n header point tip m a)
    -> m (PeerSender
            (ChainSync header point tip)
            'AsClient
            'StIdle
            n
            (ChainSyncInstruction header point tip)
            m
            a))
-> m (ClientPipelinedStIdle n header point tip m a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n) (m (ClientPipelinedStIdle n header point tip m a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> Maybe (m (ClientPipelinedStIdle n header point tip m a))
-> Maybe
     (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (m (ClientPipelinedStIdle n header point tip m a))
Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
mStIdle)
      (\ChainSyncInstruction header point tip
instr -> m (PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) (n :: N) c a.
m (PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
SenderEffect (m (PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall a b. (a -> b) -> a -> b
$ Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     n
     (ChainSyncInstruction header point tip)
     m
     a
chainSyncClientPeerSender Nat n
n' (ClientPipelinedStIdle n header point tip m a
 -> PeerSender
      (ChainSync header point tip)
      'AsClient
      'StIdle
      n
      (ChainSyncInstruction header point tip)
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (PeerSender
        (ChainSync header point tip)
        'AsClient
        'StIdle
        n
        (ChainSyncInstruction header point tip)
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ChainSyncInstruction header point tip
-> m (ClientPipelinedStIdle n header point tip m a)
collect ChainSyncInstruction header point tip
instr)
    where
      collect :: ChainSyncInstruction header point tip
-> m (ClientPipelinedStIdle n header point tip m a)
collect (RollForward header
header tip
point) =
        header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward header
header tip
point
      collect (RollBackward point
pRollback tip
tip) =
        point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward point
pRollback tip
tip

chainSyncClientPeerSender Nat n
Zero (SendMsgDone a
a) =
    WeHaveAgency 'AsClient 'StIdle
-> Message (ChainSync header point tip) 'StIdle 'StDone
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StDone
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StIdle
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) c (m :: * -> *)
       a.
WeHaveAgency pr st
-> Message ps st st'
-> PeerSender ps pr st' 'Z c m a
-> PeerSender ps pr st 'Z c m a
SenderYield
      (ClientHasAgency 'StIdle -> WeHaveAgency 'AsClient 'StIdle
forall ps (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
forall k k k (header :: k) (point :: k) (tip :: k).
ClientHasAgency 'StIdle
TokIdle)
      Message (ChainSync header point tip) 'StIdle 'StDone
forall k k k (header :: k) (point :: k) (tip :: k).
Message (ChainSync header point tip) 'StIdle 'StDone
MsgDone
      (NobodyHasAgency 'StDone
-> a
-> PeerSender
     (ChainSync header point tip)
     'AsClient
     'StDone
     'Z
     (ChainSyncInstruction header point tip)
     m
     a
forall ps (st :: ps) a (pr :: PeerRole) c (m :: * -> *).
NobodyHasAgency st -> a -> PeerSender ps pr st 'Z c m a
SenderDone NobodyHasAgency 'StDone
forall k k k (header :: k) (point :: k) (tip :: k).
NobodyHasAgency 'StDone
TokDone a
a)