{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Ouroboros.Network.Protocol.ChainSync.Type where
import Data.Proxy (Proxy (..))
import Network.TypedProtocol.Core (Protocol (..))
import Ouroboros.Network.Util.ShowProxy (ShowProxy (..))
data ChainSync header point tip where
StIdle :: ChainSync header point tip
StNext :: StNextKind -> ChainSync header point tip
StIntersect :: ChainSync header point tip
StDone :: ChainSync header point tip
instance (ShowProxy header, ShowProxy tip)
=> ShowProxy (ChainSync header point tip) where
showProxy :: Proxy (ChainSync header point tip) -> String
showProxy Proxy (ChainSync header point tip)
_ = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
"ChainSync ("
, Proxy header -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy header
forall k (t :: k). Proxy t
Proxy :: Proxy header)
, String
") ("
, Proxy tip -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy tip
forall k (t :: k). Proxy t
Proxy :: Proxy tip)
, String
")"
]
data StNextKind where
StCanAwait :: StNextKind
StMustReply :: StNextKind
instance Protocol (ChainSync header point tip) where
data Message (ChainSync header point tip) from to where
MsgRequestNext :: Message (ChainSync header point tip)
StIdle (StNext StCanAwait)
MsgAwaitReply :: Message (ChainSync header point tip)
(StNext StCanAwait) (StNext StMustReply)
MsgRollForward :: header -> tip
-> Message (ChainSync header point tip)
(StNext any) StIdle
MsgRollBackward :: point -> tip
-> Message (ChainSync header point tip)
(StNext any) StIdle
MsgFindIntersect :: [point]
-> Message (ChainSync header point tip)
StIdle StIntersect
MsgIntersectFound :: point -> tip
-> Message (ChainSync header point tip)
StIntersect StIdle
MsgIntersectNotFound :: tip
-> Message (ChainSync header point tip)
StIntersect StIdle
MsgDone :: Message (ChainSync header point tip)
StIdle StDone
data ClientHasAgency st where
TokIdle :: ClientHasAgency StIdle
data ServerHasAgency st where
TokNext :: TokNextKind k -> ServerHasAgency (StNext k)
TokIntersect :: ServerHasAgency StIntersect
data NobodyHasAgency st where
TokDone :: NobodyHasAgency StDone
exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
TokIdle ServerHasAgency st
tok = case ServerHasAgency st
tok of {}
exclusionLemma_NobodyAndClientHaveAgency :: NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st
TokDone ClientHasAgency st
tok = case ClientHasAgency st
tok of {}
exclusionLemma_NobodyAndServerHaveAgency :: NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st
TokDone ServerHasAgency st
tok = case ServerHasAgency st
tok of {}
data TokNextKind (k :: StNextKind) where
TokCanAwait :: TokNextKind StCanAwait
TokMustReply :: TokNextKind StMustReply
instance (Show header, Show point, Show tip)
=> Show (Message (ChainSync header point tip) from to) where
show :: Message (ChainSync header point tip) from to -> String
show Message (ChainSync header point tip) from to
MsgRequestNext = String
"MsgRequestNext"
show Message (ChainSync header point tip) from to
MsgAwaitReply = String
"MsgAwaitReply"
show (MsgRollForward h tip) = String
"MsgRollForward "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ header -> String
forall a. Show a => a -> String
show header
h
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
show (MsgRollBackward p tip) = String
"MsgRollBackward "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ point -> String
forall a. Show a => a -> String
show point
p
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
show (MsgFindIntersect ps) = String
"MsgFindIntersect " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [point] -> String
forall a. Show a => a -> String
show [point]
ps
show (MsgIntersectFound p tip) = String
"MsgIntersectFound "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ point -> String
forall a. Show a => a -> String
show point
p
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
show (MsgIntersectNotFound tip) = String
"MsgIntersectNotFound "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ tip -> String
forall a. Show a => a -> String
show tip
tip
show MsgDone{} = String
"MsgDone"
instance Show (ClientHasAgency (st :: ChainSync header point tip)) where
show :: ClientHasAgency st -> String
show ClientHasAgency st
TokIdle = String
"TokIdle"
instance Show (ServerHasAgency (st :: ChainSync header point tip)) where
show :: ServerHasAgency st -> String
show (TokNext TokCanAwait) = String
"TokNext TokCanAwait"
show (TokNext TokMustReply) = String
"TokNext TokMustReply"
show ServerHasAgency st
TokIntersect = String
"TokIntersect"