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

#if __GLASGOW_HASKELL__ > 810 && __GLASGOW_HASKELL__ < 904
{-# OPTIONS -fno-full-laziness #-}
#endif

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.Peer.Client

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 sent 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 {
    forall header point tip (m :: * -> *) a.
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
      :: m ()   -- ^ promptly invoked when 'MsgAwaitReply' is received
      -> ClientStNext          Z header point tip m a
      -> ClientPipelinedStIdle Z header point tip m a

    SendMsgRequestNextPipelined
      :: m ()   -- ^ promptly invoked when 'MsgAwaitReply' is received
      -> 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.
       --
       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
         :: header
         -> tip
         -> m (ClientPipelinedStIdle n header point tip m a),

       -- | Callback for 'MsgRollBackward' message.
       --
       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
         :: 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 {

       forall header point tip (m :: * -> *) a.
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),

       forall 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 :: forall header header' point point' tip tip' (m :: * -> *) 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'
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 :: 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
client = case ClientPipelinedStIdle n header point tip m a
client of
      SendMsgRequestNext m ()
stAwait ClientStNext 'Z header point tip m a
stNext -> m ()
-> ClientStNext 'Z header' point' tip' m a
-> ClientPipelinedStIdle 'Z header' point' tip' m a
forall (m :: * -> *) header point tip a.
m ()
-> ClientStNext 'Z header point tip m a
-> ClientPipelinedStIdle 'Z header point tip m a
SendMsgRequestNext m ()
stAwait (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
stNext)
      SendMsgRequestNextPipelined m ()
await ClientPipelinedStIdle ('S n) header point tip m a
idle -> m ()
-> ClientPipelinedStIdle ('S n) header' point' tip' m a
-> ClientPipelinedStIdle n header' point' tip' m a
forall (m :: * -> *) (n :: N) header point tip a.
m ()
-> ClientPipelinedStIdle ('S n) header point tip m a
-> ClientPipelinedStIdle n header point tip m a
SendMsgRequestNextPipelined m ()
await (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 a b. (a -> b) -> m a -> m b
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 :: forall (n :: N).
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 :: 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 :: header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward, 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 :: point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward } = 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 :: forall header point tip (m :: * -> *) a.
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)
recvMsgIntersectFound, 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 :: tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound } = 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
    -> ClientPipelined (ChainSync header point tip) StIdle m a

chainSyncClientPeerPipelined :: forall header point tip (m :: * -> *) a.
Monad m =>
ChainSyncClientPipelined header point tip m a
-> ClientPipelined (ChainSync header point tip) 'StIdle m a
chainSyncClientPeerPipelined (ChainSyncClientPipelined m (ClientPipelinedStIdle 'Z header point tip m a)
mclient) =
    Client
  (ChainSync header point tip)
  ('Pipelined 'Z (ChainSyncInstruction header point tip))
  'StIdle
  m
  a
-> ClientPipelined (ChainSync header point tip) 'StIdle m a
forall ps (st :: ps) (m :: * -> *) a c.
Client ps ('Pipelined 'Z c) st m a -> ClientPipelined ps st m a
ClientPipelined (Client
   (ChainSync header point tip)
   ('Pipelined 'Z (ChainSyncInstruction header point tip))
   'StIdle
   m
   a
 -> ClientPipelined (ChainSync header point tip) 'StIdle m a)
-> Client
     (ChainSync header point tip)
     ('Pipelined 'Z (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
-> ClientPipelined (ChainSync header point tip) 'StIdle m a
forall a b. (a -> b) -> a -> b
$ m (Client
     (ChainSync header point tip)
     ('Pipelined 'Z (ChainSyncInstruction header point tip))
     'StIdle
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined 'Z (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined 'Z (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined 'Z (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined 'Z (ChainSyncInstruction header point tip))
        'StIdle
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined 'Z (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall a b. (a -> b) -> a -> b
$ Nat 'Z
-> ClientPipelinedStIdle 'Z header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined 'Z (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat 'Z
forall (n :: N). ('Z ~ n) => Nat n
Zero (ClientPipelinedStIdle 'Z header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined 'Z (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
-> m (ClientPipelinedStIdle 'Z header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined 'Z (ChainSyncInstruction header point tip))
        'StIdle
        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
    -> Client (ChainSync header point tip)
              (Pipelined n (ChainSyncInstruction header point tip)) StIdle
              m a

chainSyncClientPeerSender :: forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender n :: Nat n
n@Nat n
Zero (SendMsgRequestNext m ()
stAwait ClientStNext 'Z header point tip m a
stNext) =

    Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     ('StNext 'StCanAwait)
     m
     a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield
      Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
forall {k} {k1} {k2} (header :: k) (point :: k1) (tip :: k2).
Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
MsgRequestNext
      ((forall (st' :: ChainSync header point tip).
 Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     ('StNext 'StCanAwait)
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Client ps pl st' m a)
-> Client ps pl st m a
Await ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
  -> Client
       (ChainSync header point tip)
       ('Pipelined n (ChainSyncInstruction header point tip))
       st'
       m
       a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      ('StNext 'StCanAwait)
      m
      a)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
    -> Client
         (ChainSync header point tip)
         ('Pipelined n (ChainSyncInstruction header point tip))
         st'
         m
         a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     ('StNext 'StCanAwait)
     m
     a
forall a b. (a -> b) -> a -> b
$ \case
        MsgRollForward header1
header tip1
tip -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$
            Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
n
              (ClientPipelinedStIdle n header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        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
header1
header tip
tip1
tip
          where
            ClientStNext {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 :: header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward} = ClientStNext 'Z header point tip m a
stNext

        MsgRollBackward point1
pRollback tip1
tip -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$
            Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
n
              (ClientPipelinedStIdle n header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        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
point1
pRollback tip
tip1
tip
          where
            ClientStNext {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 :: point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward} = ClientStNext 'Z header point tip m a
stNext

        Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
R:MessageChainSyncfromto
  (*) (*) (*) header point tip ('StNext 'StCanAwait) st'
MsgAwaitReply -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$ do
          m ()
stAwait
          Client
  (ChainSync header point tip)
  ('Pipelined n (ChainSyncInstruction header point tip))
  st'
  m
  a
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Client
   (ChainSync header point tip)
   ('Pipelined n (ChainSyncInstruction header point tip))
   st'
   m
   a
 -> m (Client
         (ChainSync header point tip)
         ('Pipelined n (ChainSyncInstruction header point tip))
         st'
         m
         a))
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
forall a b. (a -> b) -> a -> b
$ (forall (st' :: ChainSync header point tip).
 Message (ChainSync header point tip) st' st'
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Client ps pl st' m a)
-> Client ps pl st m a
Await ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) st' st'
  -> Client
       (ChainSync header point tip)
       ('Pipelined n (ChainSyncInstruction header point tip))
       st'
       m
       a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) st' st'
    -> Client
         (ChainSync header point tip)
         ('Pipelined n (ChainSyncInstruction header point tip))
         st'
         m
         a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$ \case
            MsgRollForward header1
header tip1
tip -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$
                Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
n
                  (ClientPipelinedStIdle n header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        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
header1
header tip
tip1
tip
              where
                ClientStNext {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 :: header -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollForward} = ClientStNext 'Z header point tip m a
stNext

            MsgRollBackward point1
pRollback tip1
tip -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$
                Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
n
                  (ClientPipelinedStIdle n header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        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
point1
pRollback tip
tip1
tip
              where
                ClientStNext {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 :: point -> tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgRollBackward} = ClientStNext 'Z header point tip m a
stNext)


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

    -- pipeline 'MsgRequestNext', the receiver will await for an instruction.
    Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
-> Receiver
     (ChainSync header point tip)
     ('StNext 'StCanAwait)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
-> Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
       (st'' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
YieldPipelined
      Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
forall {k} {k1} {k2} (header :: k) (point :: k1) (tip :: k2).
Message (ChainSync header point tip) 'StIdle ('StNext 'StCanAwait)
MsgRequestNext
      ((forall (st' :: ChainSync header point tip).
 Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
 -> Receiver
      (ChainSync header point tip)
      st'
      'StIdle
      m
      (ChainSyncInstruction header point tip))
-> Receiver
     (ChainSync header point tip)
     ('StNext 'StCanAwait)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
(StateTokenI st, ActiveState st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 Message ps st st' -> Receiver ps st' stdone m c)
-> Receiver ps st stdone m c
ReceiverAwait
        -- await for the reply
        ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
  -> Receiver
       (ChainSync header point tip)
       st'
       'StIdle
       m
       (ChainSyncInstruction header point tip))
 -> Receiver
      (ChainSync header point tip)
      ('StNext 'StCanAwait)
      'StIdle
      m
      (ChainSyncInstruction header point tip))
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) ('StNext 'StCanAwait) st'
    -> Receiver
         (ChainSync header point tip)
         st'
         'StIdle
         m
         (ChainSyncInstruction header point tip))
-> Receiver
     (ChainSync header point tip)
     ('StNext 'StCanAwait)
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall a b. (a -> b) -> a -> b
$ \case
          MsgRollForward  header1
header    tip1
tip -> ChainSyncInstruction header point tip
-> Receiver
     (ChainSync header point tip)
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (header -> tip -> ChainSyncInstruction header point tip
forall header point tip.
header -> tip -> ChainSyncInstruction header point tip
RollForward header
header1
header tip
tip1
tip)
          MsgRollBackward point1
pRollback tip1
tip -> ChainSyncInstruction header point tip
-> Receiver
     (ChainSync header point tip)
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (point -> tip -> ChainSyncInstruction header point tip
forall header point tip.
point -> tip -> ChainSyncInstruction header point tip
RollBackward point
point1
pRollback tip
tip1
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'
R:MessageChainSyncfromto
  (*) (*) (*) header point tip ('StNext 'StCanAwait) st'
MsgAwaitReply -> m (Receiver
     (ChainSync header point tip)
     st'
     'StIdle
     m
     (ChainSyncInstruction header point tip))
-> Receiver
     (ChainSync header point tip)
     st'
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
m (Receiver ps st stdone m c) -> Receiver ps st stdone m c
ReceiverEffect (m (Receiver
      (ChainSync header point tip)
      st'
      'StIdle
      m
      (ChainSyncInstruction header point tip))
 -> Receiver
      (ChainSync header point tip)
      st'
      'StIdle
      m
      (ChainSyncInstruction header point tip))
-> m (Receiver
        (ChainSync header point tip)
        st'
        'StIdle
        m
        (ChainSyncInstruction header point tip))
-> Receiver
     (ChainSync header point tip)
     st'
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall a b. (a -> b) -> a -> b
$ do
            m ()
await
            Receiver
  (ChainSync header point tip)
  st'
  'StIdle
  m
  (ChainSyncInstruction header point tip)
-> m (Receiver
        (ChainSync header point tip)
        st'
        'StIdle
        m
        (ChainSyncInstruction header point tip))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Receiver
   (ChainSync header point tip)
   st'
   'StIdle
   m
   (ChainSyncInstruction header point tip)
 -> m (Receiver
         (ChainSync header point tip)
         st'
         'StIdle
         m
         (ChainSyncInstruction header point tip)))
-> Receiver
     (ChainSync header point tip)
     st'
     'StIdle
     m
     (ChainSyncInstruction header point tip)
-> m (Receiver
        (ChainSync header point tip)
        st'
        'StIdle
        m
        (ChainSyncInstruction header point tip))
forall a b. (a -> b) -> a -> b
$ (forall (st' :: ChainSync header point tip).
 Message (ChainSync header point tip) st' st'
 -> Receiver
      (ChainSync header point tip)
      st'
      'StIdle
      m
      (ChainSyncInstruction header point tip))
-> Receiver
     (ChainSync header point tip)
     st'
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
(StateTokenI st, ActiveState st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 Message ps st st' -> Receiver ps st' stdone m c)
-> Receiver ps st stdone m c
ReceiverAwait ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) st' st'
  -> Receiver
       (ChainSync header point tip)
       st'
       'StIdle
       m
       (ChainSyncInstruction header point tip))
 -> Receiver
      (ChainSync header point tip)
      st'
      'StIdle
      m
      (ChainSyncInstruction header point tip))
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) st' st'
    -> Receiver
         (ChainSync header point tip)
         st'
         'StIdle
         m
         (ChainSyncInstruction header point tip))
-> Receiver
     (ChainSync header point tip)
     st'
     'StIdle
     m
     (ChainSyncInstruction header point tip)
forall a b. (a -> b) -> a -> b
$ \case
              MsgRollForward  header1
header    tip1
tip -> ChainSyncInstruction header point tip
-> Receiver
     (ChainSync header point tip)
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (header -> tip -> ChainSyncInstruction header point tip
forall header point tip.
header -> tip -> ChainSyncInstruction header point tip
RollForward header
header1
header tip
tip1
tip)
              MsgRollBackward point1
pRollback tip1
tip -> ChainSyncInstruction header point tip
-> Receiver
     (ChainSync header point tip)
     st'
     st'
     m
     (ChainSyncInstruction header point tip)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (point -> tip -> ChainSyncInstruction header point tip
forall header point tip.
point -> tip -> ChainSyncInstruction header point tip
RollBackward point
point1
pRollback tip
tip1
tip))

      (Nat ('S n)
-> ClientPipelinedStIdle ('S n) header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     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 :: forall header point tip (m :: * -> *) a.
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)
recvMsgIntersectFound
                                , 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 :: tip -> m (ClientPipelinedStIdle 'Z header point tip m a)
recvMsgIntersectNotFound
                                }) =

    -- non pipelined 'MsgFindIntersect'
    Message (ChainSync header point tip) 'StIdle 'StIntersect
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIntersect
     m
     a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield
      ([point]
-> Message (ChainSync header point tip) 'StIdle 'StIntersect
forall {k} {k2} point1 (header :: k) (tip :: k2).
[point1]
-> Message (ChainSync header point1 tip) 'StIdle 'StIntersect
MsgFindIntersect [point]
points)
      ((forall (st' :: ChainSync header point tip).
 Message (ChainSync header point tip) 'StIntersect st'
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIntersect
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Client ps pl st' m a)
-> Client ps pl st m a
Await
        -- await for the response and recurse
        ((forall (st' :: ChainSync header point tip).
  Message (ChainSync header point tip) 'StIntersect st'
  -> Client
       (ChainSync header point tip)
       ('Pipelined n (ChainSyncInstruction header point tip))
       st'
       m
       a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      'StIntersect
      m
      a)
-> (forall (st' :: ChainSync header point tip).
    Message (ChainSync header point tip) 'StIntersect st'
    -> Client
         (ChainSync header point tip)
         ('Pipelined n (ChainSyncInstruction header point tip))
         st'
         m
         a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIntersect
     m
     a
forall a b. (a -> b) -> a -> b
$ \case
          MsgIntersectFound point1
pIntersect tip1
tip -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$
              Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
n (ClientPipelinedStIdle n header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        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
point1
pIntersect tip
tip1
tip
          MsgIntersectNotFound tip1
tip -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     st'
     m
     a
forall a b. (a -> b) -> a -> b
$
              Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
n (ClientPipelinedStIdle n header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      st'
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        st'
        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
tip1
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 :: 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 :: header -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollForward
                              , 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 :: point -> tip -> m (ClientPipelinedStIdle n header point tip m a)
recvMsgRollBackward
                              }) =

    Maybe
  (Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a)
-> (ChainSyncInstruction header point tip
    -> Client
         (ChainSync header point tip)
         ('Pipelined n (ChainSyncInstruction header point tip))
         'StIdle
         m
         a)
-> Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (st :: ps) (n :: N) c (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Client ps ('Pipelined ('S n) c) st m a)
-> (c -> Client ps ('Pipelined n c) st m a)
-> Client ps ('Pipelined ('S n) c) st m a
Collect
      (m (Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined ('S n) (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined ('S n) (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
-> (m (ClientPipelinedStIdle ('S n) header point tip m a)
    -> m (Client
            (ChainSync header point tip)
            ('Pipelined ('S n) (ChainSyncInstruction header point tip))
            'StIdle
            m
            a))
-> m (ClientPipelinedStIdle ('S n) header point tip m a)
-> Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ClientPipelinedStIdle ('S n) header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined ('S n) (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
-> m (ClientPipelinedStIdle ('S n) header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined ('S n) (ChainSyncInstruction header point tip))
        'StIdle
        m
        a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Nat ('S n)
-> ClientPipelinedStIdle ('S n) header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined ('S n) (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
Nat ('S n)
n) (m (ClientPipelinedStIdle ('S n) header point tip m a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined ('S n) (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
-> Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
-> Maybe
     (Client
        (ChainSync header point tip)
        ('Pipelined ('S n) (ChainSyncInstruction header point tip))
        'StIdle
        m
        a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (m (ClientPipelinedStIdle ('S n) header point tip m a))
mStIdle)
      (\ChainSyncInstruction header point tip
instr -> m (Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        'StIdle
        m
        a)
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall a b. (a -> b) -> a -> b
$ Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall (n :: N) header point tip (m :: * -> *) a.
Monad m =>
Nat n
-> ClientPipelinedStIdle n header point tip m a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
chainSyncClientPeerSender Nat n
Nat n
n' (ClientPipelinedStIdle n header point tip m a
 -> Client
      (ChainSync header point tip)
      ('Pipelined n (ChainSyncInstruction header point tip))
      'StIdle
      m
      a)
-> m (ClientPipelinedStIdle n header point tip m a)
-> m (Client
        (ChainSync header point tip)
        ('Pipelined n (ChainSyncInstruction header point tip))
        'StIdle
        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) =
    Message (ChainSync header point tip) 'StIdle 'StDone
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StDone
     m
     a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StIdle
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield Message (ChainSync header point tip) 'StIdle 'StDone
forall {k} {k1} {k2} (header :: k) (point :: k1) (tip :: k2).
Message (ChainSync header point tip) 'StIdle 'StDone
MsgDone (a
-> Client
     (ChainSync header point tip)
     ('Pipelined n (ChainSyncInstruction header point tip))
     'StDone
     m
     a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
a -> Client ps pl st m a
Done a
a)