{-# 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 (Word16)
import Network.TypedProtocol.Pipelined
import Ouroboros.Network.Block (BlockNo)
import Ouroboros.Network.Point (WithOrigin (..))
data PipelineDecision n where
Request :: PipelineDecision Z
Pipeline :: PipelineDecision n
CollectOrPipeline :: PipelineDecision (S n)
Collect :: PipelineDecision (S n)
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 :: forall (n :: N).
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 Nat n
-> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n
forall (n :: N).
Nat n
-> WithOrigin BlockNo -> WithOrigin BlockNo -> PipelineDecision n
f)
pipelineDecisionMax :: Word16 -> Nat n -> WithOrigin BlockNo -> WithOrigin BlockNo
-> PipelineDecision n
pipelineDecisionMax :: forall (n :: N).
Word16
-> Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> PipelineDecision n
pipelineDecisionMax Word16
omax Nat n
n WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo
srvTipBlockNo =
case Nat n
n of
Nat n
Zero
| 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{}
| 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
PipelineDecision ('S 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' = Word16 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
omax
pipelineDecisionMin :: Word16 -> Nat n -> WithOrigin BlockNo -> WithOrigin BlockNo
-> PipelineDecision n
pipelineDecisionMin :: forall (n :: N).
Word16
-> Nat n
-> WithOrigin BlockNo
-> WithOrigin BlockNo
-> PipelineDecision n
pipelineDecisionMin Word16
omax Nat n
n WithOrigin BlockNo
cliTipBlockNo WithOrigin BlockNo
srvTipBlockNo =
case Nat n
n of
Nat n
Zero
| 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{}
| 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
PipelineDecision ('S n)
forall (n :: N). PipelineDecision ('S n)
Collect
| Bool
otherwise
-> PipelineDecision n
PipelineDecision ('S 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' = Word16 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
omax
pipelineDecisionLowHighMark :: Word16 -> Word16-> MkPipelineDecision
pipelineDecisionLowHighMark :: Word16 -> Word16 -> MkPipelineDecision
pipelineDecisionLowHighMark Word16
lowMark Word16
highMark =
Bool -> MkPipelineDecision -> MkPipelineDecision
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Word16
lowMark Word16 -> Word16 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word16
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)
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
PipelineDecision ('S 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
PipelineDecision ('S n)
forall (n :: N). PipelineDecision ('S n)
Collect, MkPipelineDecision
goHigh)
| Bool
otherwise
-> (PipelineDecision n
PipelineDecision ('S 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
PipelineDecision ('S n)
forall (n :: N). PipelineDecision ('S n)
Collect, MkPipelineDecision
goHigh)
else (PipelineDecision n
PipelineDecision ('S 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' = Word16 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
lowMark
highMark' :: BlockNo
highMark' :: BlockNo
highMark' = Word16 -> BlockNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
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)