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

module Ouroboros.Network.Protocol.ChainSync.PipelineDecision
  ( PipelineDecision (..)
  , MkPipelineDecision (..)
  , runPipelineDecision
  , constantPipelineDecision
  , pipelineDecisionMax
  , pipelineDecisionMin
  , pipelineDecisionLowHighMark
  ) where

import           Control.Exception (assert)
import           Data.Word

import           Network.TypedProtocol.Pipelined

import           Ouroboros.Network.Block (BlockNo)
import           Ouroboros.Network.Point (WithOrigin (..))

-- | Pipeline decision: we can do either one of these:
--
-- * non-pipelined request
-- * pipeline a request
-- * collect or pipeline, but only when there are pipelined requests
-- * collect, as above, only when there are pipelined requests
--
-- There might be other useful pipelining scenarios: collect a given number of
-- requests (which also can be used to collect all outstanding requests).
--
data PipelineDecision n where
    Request           :: PipelineDecision Z
    Pipeline          :: PipelineDecision n
    CollectOrPipeline :: PipelineDecision (S n)
    Collect           :: PipelineDecision (S n)


-- | The callback gets the following arguments:
--
-- * how many requests are not yet collected (in flight or
--   already queued)
-- * block number of client's tip
-- * block number of server's tip
--
-- Client's tip block number and server's tip block number can only be equal
-- (from the client's perspective) when both the client's and the server's tip
-- headers agree. If they would not agree (server forked), then the server
-- sends 'MsgRollBackward', which rolls back one block and causes the client's
-- tip and the server's tip to differ.
--
-- In this module we implement three pipelining strategies:
--
-- * 'pipelineDecisionMax'
-- * 'pipelineDecisionMin'
-- * 'pipelineDecisionLowHighMark'
--
data MkPipelineDecision where
     MkPipelineDecision
       :: (forall n. Nat n
                  -> WithOrigin BlockNo
                  -> WithOrigin BlockNo
                  -> (PipelineDecision n, MkPipelineDecision))
       -> MkPipelineDecision

runPipelineDecision
    :: MkPipelineDecision
    -> Nat n -> WithOrigin BlockNo -> WithOrigin BlockNo
    -> (PipelineDecision n, MkPipelineDecision)
runPipelineDecision :: MkPipelineDecision
-> Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> (PipelineDecision n, MkPipelineDecision)
runPipelineDecision (MkPipelineDecision forall (n :: N).
Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> (PipelineDecision n, MkPipelineDecision)
f) Nat n
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo =
    Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> (PipelineDecision n, MkPipelineDecision)
forall (n :: N).
Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> (PipelineDecision n, MkPipelineDecision)
f Nat n
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo


constantPipelineDecision
   :: (forall n. Nat n -> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n)
   -> MkPipelineDecision
constantPipelineDecision :: (forall (n :: N).
 Nat n
 -> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n)
-> MkPipelineDecision
constantPipelineDecision forall (n :: N).
Nat n
-> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n
f = (forall (n :: N).
 Nat n
 -> WithOrigin BlockNo
 -> WithOrigin BlockNo
 -> (PipelineDecision n, MkPipelineDecision))
-> MkPipelineDecision
MkPipelineDecision
  ((forall (n :: N).
  Nat n
  -> WithOrigin BlockNo
  -> WithOrigin BlockNo
  -> (PipelineDecision n, MkPipelineDecision))
 -> MkPipelineDecision)
-> (forall (n :: N).
    Nat n
    -> WithOrigin BlockNo
    -> WithOrigin BlockNo
    -> (PipelineDecision n, MkPipelineDecision))
-> MkPipelineDecision
forall a b. (a -> b) -> a -> b
$ \Nat n
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo ->
    (Nat n
-> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n
forall (n :: N).
Nat n
-> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n
f Nat n
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo, (forall (n :: N).
 Nat n
 -> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n)
-> MkPipelineDecision
constantPipelineDecision forall (n :: N).
Nat n
-> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n
f)


-- | Present maximal pipelining of at most @omax@ requests.  Collect responses
-- either when we are at the same block number as the server or when we sent
-- more than @omax@ requests.
--
-- If @omax = 3@ this pipelining strategy will generate a sequence:
-- @
--    Pipeline
--    Pipeline
--    Pipeline
--    Collect
--    Pipeline
--    Collect
--    ....
--    Pipeline
--    Collect
--    Collect
--    Collect
-- @
--
pipelineDecisionMax :: Word32 -> Nat n -> WithOrigin BlockNo -> WithOrigin BlockNo
                    -> PipelineDecision n
pipelineDecisionMax :: Word32
-> Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> PipelineDecision n
pipelineDecisionMax Word32
omax Nat n
n WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo
srvTipBlockNo =
    case Nat n
n of
      Nat n
Zero   -- We are insync with the server's tip. We use
             -- equality so that this does not get triggered when we are ahead
             -- of the producer, and it will send us 'MsgRollBackward'.
             | WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo -> WithOrigin BlockNo -> Bool
forall a. Eq a => a -> a -> Bool
== WithOrigin BlockNo
srvTipBlockNo
             -> PipelineDecision n
PipelineDecision 'Z
Request

             | Bool
otherwise
             -> PipelineDecision n
forall (n :: N). PipelineDecision n
Pipeline

      Succ{} -- We pipelined some requests and we are now synchronised or we
             -- exceeded the pipelining limit, and thus we should await for a
             -- response.
             --
             -- Note: we add @omax'@ to avoid a deadlock in tests. This
             -- pipelining strategy collects at this stage a single result,
             -- this causes @n'@ to drop and we will pipeline the next
             -- message. This assures that when we approach the end of the
             -- chain we will collect all outstanding requests without
             -- pipelining a request.
             | WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo -> BlockNo -> WithOrigin BlockNo
`bnoPlus` BlockNo
n' WithOrigin BlockNo -> WithOrigin BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
>= WithOrigin BlockNo
srvTipBlockNo Bool -> Bool -> Bool
|| BlockNo
n' BlockNo -> BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
>= BlockNo
omax'
             -> PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
Collect

             | Bool
otherwise
             -> PipelineDecision n
forall (n :: N). PipelineDecision n
Pipeline
  where
    n' :: BlockNo
    n' :: BlockNo
n' = Int -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat n -> Int
forall (n :: N). Nat n -> Int
natToInt Nat n
n)

    omax' :: BlockNo
    omax' :: BlockNo
omax' = Word32 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
omax


-- | Present minimum pipelining of at most @omax@ requests, collect responses
-- eagerly.
--
pipelineDecisionMin :: Word32 -> Nat n -> WithOrigin BlockNo -> WithOrigin BlockNo
                    -> PipelineDecision n
pipelineDecisionMin :: Word32
-> Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> PipelineDecision n
pipelineDecisionMin Word32
omax Nat n
n WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo
srvTipBlockNo =
    case Nat n
n of
      Nat n
Zero   -- We are insync with the server's tip. We use
             -- equality so that this does not get triggered when we are ahead
             -- of the producer, and it will send us 'MsgRollBackward'.
             | WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo -> WithOrigin BlockNo -> Bool
forall a. Eq a => a -> a -> Bool
== WithOrigin BlockNo
srvTipBlockNo
             -> PipelineDecision n
PipelineDecision 'Z
Request

             | Bool
otherwise
             -> PipelineDecision n
forall (n :: N). PipelineDecision n
Pipeline

      Succ{} -- We pipelined some requests and we are now synchronised or we
             -- exceeded the pipelining limit, and thus we should wait for a
             -- response.
             | WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo -> BlockNo -> WithOrigin BlockNo
`bnoPlus` BlockNo
n' WithOrigin BlockNo -> WithOrigin BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
>= WithOrigin BlockNo
srvTipBlockNo Bool -> Bool -> Bool
|| BlockNo
n' BlockNo -> BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
>= BlockNo
omax'
             -> PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
Collect

             | Bool
otherwise
             -> PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
CollectOrPipeline
  where
    n' :: BlockNo
    n' :: BlockNo
n' = Int -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat n -> Int
forall (n :: N). Nat n -> Int
natToInt Nat n
n)

    omax' :: BlockNo
    omax' :: BlockNo
omax' = Word32 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
omax


-- | Pipelining strategy which pipelines up to @highMark@ requests; if the
-- number of pipelined messages exceeds the high mark, it collects messages
-- until there are at most @lowMark@ outstanding requests.
--
pipelineDecisionLowHighMark :: Word32 -> Word32-> MkPipelineDecision
pipelineDecisionLowHighMark :: Word32 -> Word32 -> MkPipelineDecision
pipelineDecisionLowHighMark Word32
lowMark Word32
highMark =
    Bool -> MkPipelineDecision -> MkPipelineDecision
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Word32
lowMark Word32 -> Word32 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word32
highMark) MkPipelineDecision
goLow
  where
    goZero :: Nat Z -> WithOrigin BlockNo -> WithOrigin BlockNo
           -> (PipelineDecision Z, MkPipelineDecision)
    goZero :: Nat 'Z
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> (PipelineDecision 'Z, MkPipelineDecision)
goZero Nat 'Z
Zero WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo
      | WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo -> WithOrigin BlockNo -> Bool
forall a. Eq a => a -> a -> Bool
== WithOrigin BlockNo
serverTipBlockNo
      = (PipelineDecision 'Z
Request, MkPipelineDecision
goLow)

      | Bool
otherwise
      = (PipelineDecision 'Z
forall (n :: N). PipelineDecision n
Pipeline, MkPipelineDecision
goLow)

    -- Mutually recursive pipeline decision strategies; we start with 'goLow',
    -- when we go above the high mark, switch to 'goHigh', switch back to
    -- 'goLow' when we go below the low mark.
    goLow, goHigh  :: MkPipelineDecision

    goLow :: MkPipelineDecision
goLow = (forall (n :: N).
 Nat n
 -> WithOrigin BlockNo
 -> WithOrigin BlockNo
 -> (PipelineDecision n, MkPipelineDecision))
-> MkPipelineDecision
MkPipelineDecision ((forall (n :: N).
  Nat n
  -> WithOrigin BlockNo
  -> WithOrigin BlockNo
  -> (PipelineDecision n, MkPipelineDecision))
 -> MkPipelineDecision)
-> (forall (n :: N).
    Nat n
    -> WithOrigin BlockNo
    -> WithOrigin BlockNo
    -> (PipelineDecision n, MkPipelineDecision))
-> MkPipelineDecision
forall a b. (a -> b) -> a -> b
$
      \Nat n
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo ->
        case Nat n
n of
          Nat n
Zero   -> Nat 'Z
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> (PipelineDecision 'Z, MkPipelineDecision)
goZero Nat n
Nat 'Z
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo

          Succ{} | WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo -> BlockNo -> WithOrigin BlockNo
`bnoPlus` BlockNo
n' WithOrigin BlockNo -> WithOrigin BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
>= WithOrigin BlockNo
serverTipBlockNo
                 -> (PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
Collect, MkPipelineDecision
goLow)

                 | BlockNo
n' BlockNo -> BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
>= BlockNo
highMark'
                 -> (PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
Collect, MkPipelineDecision
goHigh)

                 | Bool
otherwise
                 -> (PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
CollectOrPipeline, MkPipelineDecision
goLow)
            where
              n' :: BlockNo
              n' :: BlockNo
n' = Int -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat n -> Int
forall (n :: N). Nat n -> Int
natToInt Nat n
n)

    goHigh :: MkPipelineDecision
goHigh = (forall (n :: N).
 Nat n
 -> WithOrigin BlockNo
 -> WithOrigin BlockNo
 -> (PipelineDecision n, MkPipelineDecision))
-> MkPipelineDecision
MkPipelineDecision ((forall (n :: N).
  Nat n
  -> WithOrigin BlockNo
  -> WithOrigin BlockNo
  -> (PipelineDecision n, MkPipelineDecision))
 -> MkPipelineDecision)
-> (forall (n :: N).
    Nat n
    -> WithOrigin BlockNo
    -> WithOrigin BlockNo
    -> (PipelineDecision n, MkPipelineDecision))
-> MkPipelineDecision
forall a b. (a -> b) -> a -> b
$
      \Nat n
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo ->
      case Nat n
n of
        Nat n
Zero   -> Nat 'Z
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> (PipelineDecision 'Z, MkPipelineDecision)
goZero Nat n
Nat 'Z
n WithOrigin BlockNo
clientTipBlockNo WithOrigin BlockNo
serverTipBlockNo

        Succ{} ->
            if BlockNo
n' BlockNo -> BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
> BlockNo
lowMark'
              then (PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
Collect,           MkPipelineDecision
goHigh)
              else (PipelineDecision n
forall (n :: N). PipelineDecision ('S n)
CollectOrPipeline, MkPipelineDecision
goLow)
          where
            n' :: BlockNo
            n' :: BlockNo
n' = Int -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat n -> Int
forall (n :: N). Nat n -> Int
natToInt Nat n
n)

    lowMark' :: BlockNo
    lowMark' :: BlockNo
lowMark' = Word32 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
lowMark

    highMark' :: BlockNo
    highMark' :: BlockNo
highMark' = Word32 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
highMark

bnoPlus :: WithOrigin BlockNo -> BlockNo -> WithOrigin BlockNo
bnoPlus :: WithOrigin BlockNo -> BlockNo -> WithOrigin BlockNo
bnoPlus (At BlockNo
x) BlockNo
y = BlockNo -> WithOrigin BlockNo
forall t. t -> WithOrigin t
At (BlockNo
x BlockNo -> BlockNo -> BlockNo
forall a. Num a => a -> a -> a
+ BlockNo
y)
bnoPlus WithOrigin BlockNo
Origin BlockNo
y = BlockNo -> WithOrigin BlockNo
forall t. t -> WithOrigin t
At (BlockNo
1 BlockNo -> BlockNo -> BlockNo
forall a. Num a => a -> a -> a
+ BlockNo
y)