{-# 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 (..))


-- | Range of blocks, defined by a lower and upper point, inclusive.
--
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
    -- | request range of blocks
    MsgRequestRange
      :: ChainRange point
      -> Message (BlockFetch block point) BFIdle BFBusy
    -- | start block streaming
    MsgStartBatch
      :: Message (BlockFetch block point) BFBusy BFStreaming
    -- | respond that there are no blocks
    MsgNoBlocks
      :: Message (BlockFetch block point) BFBusy BFIdle
    -- | stream a single block
    MsgBlock
      :: block
      -> Message (BlockFetch block point) BFStreaming BFStreaming
    -- | end of block streaming
    MsgBatchDone
      :: Message (BlockFetch block point) BFStreaming BFIdle

    -- | client termination message
    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"