{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE EmptyCase                  #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# 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.DeepSeq
import Control.Monad.Class.MonadThrow (Exception)
import Data.Word (Word16)
import GHC.Generics
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
$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

-- | 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 :: 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"