{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Ouroboros.Network.Protocol.KeepAlive.Type where
import Control.DeepSeq
import Control.Monad.Class.MonadThrow (Exception)
import Data.Word (Word16)
import GHC.Generics
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
$c== :: Cookie -> Cookie -> Bool
== :: Cookie -> Cookie -> Bool
$c/= :: Cookie -> Cookie -> Bool
/= :: 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
$cshowsPrec :: Int -> Cookie -> ShowS
showsPrec :: Int -> Cookie -> ShowS
$cshow :: Cookie -> String
show :: Cookie -> String
$cshowList :: [Cookie] -> ShowS
showList :: [Cookie] -> ShowS
Show, (forall x. Cookie -> Rep Cookie x)
-> (forall x. Rep Cookie x -> Cookie) -> Generic Cookie
forall x. Rep Cookie x -> Cookie
forall x. Cookie -> Rep Cookie x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Cookie -> Rep Cookie x
from :: forall x. Cookie -> Rep Cookie x
$cto :: forall x. Rep Cookie x -> Cookie
to :: forall x. Rep Cookie x -> Cookie
Generic, Cookie -> ()
(Cookie -> ()) -> NFData Cookie
forall a. (a -> ()) -> NFData a
$crnf :: Cookie -> ()
rnf :: Cookie -> ()
NFData)
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
$c== :: KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
== :: KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
$c/= :: KeepAliveProtocolFailure -> KeepAliveProtocolFailure -> Bool
/= :: 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
$cshowsPrec :: Int -> KeepAliveProtocolFailure -> ShowS
showsPrec :: Int -> KeepAliveProtocolFailure -> ShowS
$cshow :: KeepAliveProtocolFailure -> String
show :: KeepAliveProtocolFailure -> String
$cshowList :: [KeepAliveProtocolFailure] -> ShowS
showList :: [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 :: forall (st :: KeepAlive).
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
R:ClientHasAgencyKeepAlivest st
TokClient ServerHasAgency st
tok = case ServerHasAgency st
tok of {}
exclusionLemma_NobodyAndClientHaveAgency :: forall (st :: KeepAlive).
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st
R:NobodyHasAgencyKeepAlivest st
TokDone ClientHasAgency st
tok = case ClientHasAgency st
tok of {}
exclusionLemma_NobodyAndServerHaveAgency :: forall (st :: KeepAlive).
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st
R:NobodyHasAgencyKeepAlivest st
TokDone ServerHasAgency st
tok = case ServerHasAgency st
tok of {}
instance forall (st :: KeepAlive). NFData (ClientHasAgency st) where
rnf :: ClientHasAgency st -> ()
rnf ClientHasAgency st
R:ClientHasAgencyKeepAlivest st
TokClient = ()
instance forall (st :: KeepAlive). NFData (ServerHasAgency st) where
rnf :: ServerHasAgency st -> ()
rnf ServerHasAgency st
R:ServerHasAgencyKeepAlivest st
TokServer = ()
instance forall (st :: KeepAlive). NFData (NobodyHasAgency st) where
rnf :: NobodyHasAgency st -> ()
rnf NobodyHasAgency st
R:NobodyHasAgencyKeepAlivest st
TokDone = ()
instance NFData (Message KeepAlive from to) where
rnf :: Message KeepAlive from to -> ()
rnf (MsgKeepAlive Cookie
c) = Cookie -> ()
forall a. NFData a => a -> ()
rnf Cookie
c
rnf (MsgKeepAliveResponse Cookie
c) = Cookie -> ()
forall a. NFData a => a -> ()
rnf Cookie
c
rnf Message KeepAlive from to
R:MessageKeepAlivefromto from to
MsgDone = ()
instance forall (st :: KeepAlive) pr. NFData (PeerHasAgency pr st) where
rnf :: PeerHasAgency pr st -> ()
rnf (ClientAgency ClientHasAgency st
x) = ClientHasAgency st -> ()
forall a. NFData a => a -> ()
rnf ClientHasAgency st
x
rnf (ServerAgency ServerHasAgency st
x) = ServerHasAgency st -> ()
forall a. NFData a => a -> ()
rnf ServerHasAgency st
x
instance Show (Message KeepAlive from to) where
show :: Message KeepAlive from to -> String
show (MsgKeepAlive Cookie
cookie) = String
"MsgKeepAlive " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Cookie -> String
forall a. Show a => a -> String
show Cookie
cookie
show (MsgKeepAliveResponse Cookie
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
R:MessageKeepAlivefromto from to
MsgDone = String
"MsgDone"
instance Show (ClientHasAgency (st :: KeepAlive)) where
show :: ClientHasAgency st -> String
show ClientHasAgency st
R:ClientHasAgencyKeepAlivest st
TokClient = String
"TokClient"
instance Show (ServerHasAgency (st :: KeepAlive)) where
show :: ServerHasAgency st -> String
show ServerHasAgency st
R:ServerHasAgencyKeepAlivest st
TokServer = String
"TokServer"