{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Ouroboros.Network.Protocol.KeepAlive.Type where
import Control.Monad.Class.MonadThrow (Exception)
import Data.Word (Word16)
import Network.TypedProtocol.Core
import Ouroboros.Network.Util.ShowProxy (ShowProxy (..))
newtype Cookie = Cookie {Cookie -> Word16
unCookie :: Word16 } deriving (Cookie -> Cookie -> Bool
(Cookie -> Cookie -> Bool)
-> (Cookie -> Cookie -> Bool) -> Eq Cookie
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cookie -> Cookie -> Bool
$c/= :: Cookie -> Cookie -> Bool
== :: Cookie -> Cookie -> Bool
$c== :: Cookie -> Cookie -> Bool
Eq, Int -> Cookie -> ShowS
[Cookie] -> ShowS
Cookie -> String
(Int -> Cookie -> ShowS)
-> (Cookie -> String) -> ([Cookie] -> ShowS) -> Show Cookie
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Cookie] -> ShowS
$cshowList :: [Cookie] -> ShowS
show :: Cookie -> String
$cshow :: Cookie -> String
showsPrec :: Int -> Cookie -> ShowS
$cshowsPrec :: Int -> Cookie -> ShowS
Show)
data KeepAliveProtocolFailure =
KeepAliveCookieMissmatch Cookie Cookie deriving (KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
(KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool)
-> (KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool)
-> Eq KeepAliveProtocolFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
$c/= :: KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
== :: KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
$c== :: KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
Eq, Int -> KeepAliveProtocolFailure -> ShowS
[KeepAliveProtocolFailure] -> ShowS
KeepAliveProtocolFailure -> String
(Int -> KeepAliveProtocolFailure -> ShowS)
-> (KeepAliveProtocolFailure -> String)
-> ([KeepAliveProtocolFailure] -> ShowS)
-> Show KeepAliveProtocolFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [KeepAliveProtocolFailure] -> ShowS
$cshowList :: [KeepAliveProtocolFailure] -> ShowS
show :: KeepAliveProtocolFailure -> String
$cshow :: KeepAliveProtocolFailure -> String
showsPrec :: Int -> KeepAliveProtocolFailure -> ShowS
$cshowsPrec :: Int -> KeepAliveProtocolFailure -> ShowS
Show)
instance Exception KeepAliveProtocolFailure
data KeepAlive where
StClient :: KeepAlive
StServer :: KeepAlive
StDone :: KeepAlive
instance ShowProxy KeepAlive where
showProxy :: Proxy KeepAlive -> String
showProxy Proxy KeepAlive
_ = String
"KeepAlive"
instance Protocol KeepAlive where
data Message KeepAlive from to where
MsgKeepAlive
:: Cookie
-> Message KeepAlive StClient StServer
MsgKeepAliveResponse
:: Cookie
-> Message KeepAlive StServer StClient
MsgDone
:: Message KeepAlive StClient StDone
data ClientHasAgency st where
TokClient :: ClientHasAgency StClient
data ServerHasAgency st where
TokServer :: ServerHasAgency StServer
data NobodyHasAgency st where
TokDone :: NobodyHasAgency StDone
exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
TokClient 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 {}
instance Show (Message KeepAlive from to) where
show :: Message KeepAlive from to -> String
show (MsgKeepAlive cookie) = String
"MsgKeepAlive " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Cookie -> String
forall a. Show a => a -> String
show Cookie
cookie
show (MsgKeepAliveResponse cookie) = String
"MsgKeepAliveResponse " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Cookie -> String
forall a. Show a => a -> String
show Cookie
cookie
show Message KeepAlive from to
MsgDone = String
"MsgDone"
instance Show (ClientHasAgency (st :: KeepAlive)) where
show :: ClientHasAgency st -> String
show ClientHasAgency st
TokClient = String
"TokClient"
instance Show (ServerHasAgency (st :: KeepAlive)) where
show :: ServerHasAgency st -> String
show ServerHasAgency st
TokServer = String
"TokServer"