{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE EmptyCase         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE PolyKinds         #-}
{-# LANGUAGE TypeFamilies      #-}

-- | The type of the keep alive protocol.
--
-- The keep alive protocol is used for
--
-- * sending keep alive messages
-- * making round trip measuremnets
--
-- Each side will run its own version of the keep alive protocol.  It should be
-- configured so that any intermediate state (such as in customer premise
-- equipment or in a carrier grade NAT) is kept alive. This has to be a per-node
-- configuration element as this is about the properties of that nodes network
-- connectivity.
--
-- For making round trip measurements its in the interest of the other side to
-- reply promptly.
--
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 (..))

-- | A 16bit value used to match responses to requests.
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

-- | A kind to identify our protocol, and the types of the states in the state
-- transition diagram of the protocol.
--
data KeepAlive where

    -- | The client can send a request and the server is waiting for a request.
    --
    StClient :: KeepAlive

    -- | The server is responsible for sending response back.
    --
    StServer :: KeepAlive

    -- | Both the client and server are in the terminal state. They're done.
    --
    StDone   :: KeepAlive

instance ShowProxy KeepAlive where
    showProxy :: Proxy KeepAlive -> String
showProxy Proxy KeepAlive
_ = String
"KeepAlive"

instance Protocol KeepAlive where
    -- | The messages in the keep alive protocol.
    --
    -- In this protocol the consumer initiates and the producer replies.
    --
    data Message KeepAlive from to where

      -- | Send a keep alive message.
      --
      MsgKeepAlive
        :: Cookie
        -> Message KeepAlive StClient StServer

      -- | Keep alive response.
      --
      MsgKeepAliveResponse
        :: Cookie
        -> Message KeepAlive StServer StClient

      -- | The client side terminating message of the protocol.
      --
      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"