{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Ouroboros.Network.Protocol.BlockFetch.Type where
import Data.Proxy (Proxy (..))
import Data.Void (Void)
import Network.TypedProtocol.Core (Protocol (..))
import Ouroboros.Network.Util.ShowProxy (ShowProxy (..))
data ChainRange point = ChainRange !point !point
deriving (Int -> ChainRange point -> ShowS
[ChainRange point] -> ShowS
ChainRange point -> String
(Int -> ChainRange point -> ShowS)
-> (ChainRange point -> String)
-> ([ChainRange point] -> ShowS)
-> Show (ChainRange point)
forall point. Show point => Int -> ChainRange point -> ShowS
forall point. Show point => [ChainRange point] -> ShowS
forall point. Show point => ChainRange point -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ChainRange point] -> ShowS
$cshowList :: forall point. Show point => [ChainRange point] -> ShowS
show :: ChainRange point -> String
$cshow :: forall point. Show point => ChainRange point -> String
showsPrec :: Int -> ChainRange point -> ShowS
$cshowsPrec :: forall point. Show point => Int -> ChainRange point -> ShowS
Show, ChainRange point -> ChainRange point -> Bool
(ChainRange point -> ChainRange point -> Bool)
-> (ChainRange point -> ChainRange point -> Bool)
-> Eq (ChainRange point)
forall point.
Eq point =>
ChainRange point -> ChainRange point -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ChainRange point -> ChainRange point -> Bool
$c/= :: forall point.
Eq point =>
ChainRange point -> ChainRange point -> Bool
== :: ChainRange point -> ChainRange point -> Bool
$c== :: forall point.
Eq point =>
ChainRange point -> ChainRange point -> Bool
Eq, Eq (ChainRange point)
Eq (ChainRange point)
-> (ChainRange point -> ChainRange point -> Ordering)
-> (ChainRange point -> ChainRange point -> Bool)
-> (ChainRange point -> ChainRange point -> Bool)
-> (ChainRange point -> ChainRange point -> Bool)
-> (ChainRange point -> ChainRange point -> Bool)
-> (ChainRange point -> ChainRange point -> ChainRange point)
-> (ChainRange point -> ChainRange point -> ChainRange point)
-> Ord (ChainRange point)
ChainRange point -> ChainRange point -> Bool
ChainRange point -> ChainRange point -> Ordering
ChainRange point -> ChainRange point -> ChainRange point
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall point. Ord point => Eq (ChainRange point)
forall point.
Ord point =>
ChainRange point -> ChainRange point -> Bool
forall point.
Ord point =>
ChainRange point -> ChainRange point -> Ordering
forall point.
Ord point =>
ChainRange point -> ChainRange point -> ChainRange point
min :: ChainRange point -> ChainRange point -> ChainRange point
$cmin :: forall point.
Ord point =>
ChainRange point -> ChainRange point -> ChainRange point
max :: ChainRange point -> ChainRange point -> ChainRange point
$cmax :: forall point.
Ord point =>
ChainRange point -> ChainRange point -> ChainRange point
>= :: ChainRange point -> ChainRange point -> Bool
$c>= :: forall point.
Ord point =>
ChainRange point -> ChainRange point -> Bool
> :: ChainRange point -> ChainRange point -> Bool
$c> :: forall point.
Ord point =>
ChainRange point -> ChainRange point -> Bool
<= :: ChainRange point -> ChainRange point -> Bool
$c<= :: forall point.
Ord point =>
ChainRange point -> ChainRange point -> Bool
< :: ChainRange point -> ChainRange point -> Bool
$c< :: forall point.
Ord point =>
ChainRange point -> ChainRange point -> Bool
compare :: ChainRange point -> ChainRange point -> Ordering
$ccompare :: forall point.
Ord point =>
ChainRange point -> ChainRange point -> Ordering
$cp1Ord :: forall point. Ord point => Eq (ChainRange point)
Ord)
data BlockFetch block point where
BFIdle :: BlockFetch block point
BFBusy :: BlockFetch block point
BFStreaming :: BlockFetch block point
BFDone :: BlockFetch block point
instance ShowProxy block => ShowProxy (BlockFetch block point) where
showProxy :: Proxy (BlockFetch block point) -> String
showProxy Proxy (BlockFetch block point)
_ = String
"BlockFetch" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy block -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy block
forall k (t :: k). Proxy t
Proxy :: Proxy block)
instance Protocol (BlockFetch block point) where
data Message (BlockFetch block point) from to where
MsgRequestRange
:: ChainRange point
-> Message (BlockFetch block point) BFIdle BFBusy
MsgStartBatch
:: Message (BlockFetch block point) BFBusy BFStreaming
MsgNoBlocks
:: Message (BlockFetch block point) BFBusy BFIdle
MsgBlock
:: block
-> Message (BlockFetch block point) BFStreaming BFStreaming
MsgBatchDone
:: Message (BlockFetch block point) BFStreaming BFIdle
MsgClientDone
:: Message (BlockFetch block point) BFIdle BFDone
data ClientHasAgency st where
TokIdle :: ClientHasAgency BFIdle
data ServerHasAgency st where
TokBusy :: ServerHasAgency BFBusy
TokStreaming :: ServerHasAgency BFStreaming
data NobodyHasAgency st where
TokDone :: NobodyHasAgency BFDone
exclusionLemma_ClientAndServerHaveAgency
:: forall (st :: BlockFetch block point).
ClientHasAgency st
-> ServerHasAgency st
-> Void
exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency = \ClientHasAgency st
TokIdle ServerHasAgency st
x -> case ServerHasAgency st
x of {}
exclusionLemma_NobodyAndClientHaveAgency
:: forall (st :: BlockFetch block point).
NobodyHasAgency st
-> ClientHasAgency st
-> Void
exclusionLemma_NobodyAndClientHaveAgency :: NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency = \NobodyHasAgency st
TokDone ClientHasAgency st
x -> case ClientHasAgency st
x of {}
exclusionLemma_NobodyAndServerHaveAgency
:: forall (st :: BlockFetch block point).
NobodyHasAgency st
-> ServerHasAgency st
-> Void
exclusionLemma_NobodyAndServerHaveAgency :: NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency = \NobodyHasAgency st
TokDone ServerHasAgency st
x -> case ServerHasAgency st
x of {}
instance (Show block, Show point)
=> Show (Message (BlockFetch block point) from to) where
show :: Message (BlockFetch block point) from to -> String
show (MsgRequestRange range) = String
"MsgRequestRange " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ChainRange point -> String
forall a. Show a => a -> String
show ChainRange point
range
show Message (BlockFetch block point) from to
MsgStartBatch = String
"MsgStartBatch"
show (MsgBlock block) = String
"MsgBlock " String -> ShowS
forall a. [a] -> [a] -> [a]
++ block -> String
forall a. Show a => a -> String
show block
block
show Message (BlockFetch block point) from to
MsgNoBlocks = String
"MsgNoBlocks"
show Message (BlockFetch block point) from to
MsgBatchDone = String
"MsgBatchDone"
show Message (BlockFetch block point) from to
MsgClientDone = String
"MsgClientDone"
instance Show (ClientHasAgency (st :: BlockFetch block point)) where
show :: ClientHasAgency st -> String
show ClientHasAgency st
TokIdle = String
"TokIdle"
instance Show (ServerHasAgency (st :: BlockFetch block point)) where
show :: ServerHasAgency st -> String
show ServerHasAgency st
TokBusy = String
"TokBusy"
show ServerHasAgency st
TokStreaming = String
"TokStreaming"