{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}

module Ouroboros.Network.Protocol.Handshake.Type
  ( -- * Handshake Protocol
    Handshake (..)
  , Message (..)
  , ClientHasAgency (..)
  , ServerHasAgency (..)
  , NobodyHasAgency (..)
    -- $simultanous-open
  , RefuseReason (..)
  , HandshakeProtocolError (..)
  ) where


import           Control.Exception
import           Data.Map (Map)
import           Data.Text (Text)
import           Data.Typeable (Typeable)

import           Network.TypedProtocol.Core
import           Ouroboros.Network.Util.ShowProxy (ShowProxy (..))

-- |
-- The handshake mini-protocol is used initially to agree the version and
-- associated parameters of the protocol to use for all subsequent
-- communication.
--
data Handshake vNumber vParams where
    StPropose :: Handshake vNumber vParams
    StConfirm :: Handshake vNumber vParams
    StDone    :: Handshake vNumber vParams

instance ShowProxy (Handshake vNumber vParams) where
    showProxy :: Proxy (Handshake vNumber vParams) -> String
showProxy Proxy (Handshake vNumber vParams)
_ = String
"Handshake"

-- |
-- Reasons by which a server can refuse proposed version.
--
data RefuseReason vNumber
  -- | All of the prosed versions where not known to the server.
  -- Since the server sends all versions that it can knows about, some of them
  -- we might not be able to decode, so we include raw tags @[Int]@.
  --
  = VersionMismatch [vNumber] [Int]

  -- | The server failed to decode version parameters.
  --
  | HandshakeDecodeError vNumber Text

  -- | The server refused to run the proposed version parameters
  --
  | Refused vNumber Text
  deriving (RefuseReason vNumber -> RefuseReason vNumber -> Bool
(RefuseReason vNumber -> RefuseReason vNumber -> Bool)
-> (RefuseReason vNumber -> RefuseReason vNumber -> Bool)
-> Eq (RefuseReason vNumber)
forall vNumber.
Eq vNumber =>
RefuseReason vNumber -> RefuseReason vNumber -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RefuseReason vNumber -> RefuseReason vNumber -> Bool
$c/= :: forall vNumber.
Eq vNumber =>
RefuseReason vNumber -> RefuseReason vNumber -> Bool
== :: RefuseReason vNumber -> RefuseReason vNumber -> Bool
$c== :: forall vNumber.
Eq vNumber =>
RefuseReason vNumber -> RefuseReason vNumber -> Bool
Eq, Int -> RefuseReason vNumber -> ShowS
[RefuseReason vNumber] -> ShowS
RefuseReason vNumber -> String
(Int -> RefuseReason vNumber -> ShowS)
-> (RefuseReason vNumber -> String)
-> ([RefuseReason vNumber] -> ShowS)
-> Show (RefuseReason vNumber)
forall vNumber.
Show vNumber =>
Int -> RefuseReason vNumber -> ShowS
forall vNumber. Show vNumber => [RefuseReason vNumber] -> ShowS
forall vNumber. Show vNumber => RefuseReason vNumber -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RefuseReason vNumber] -> ShowS
$cshowList :: forall vNumber. Show vNumber => [RefuseReason vNumber] -> ShowS
show :: RefuseReason vNumber -> String
$cshow :: forall vNumber. Show vNumber => RefuseReason vNumber -> String
showsPrec :: Int -> RefuseReason vNumber -> ShowS
$cshowsPrec :: forall vNumber.
Show vNumber =>
Int -> RefuseReason vNumber -> ShowS
Show)

instance (Typeable vNumber, Show vNumber) => Exception (RefuseReason vNumber)


instance Protocol (Handshake vNumber vParams) where

    data Message (Handshake vNumber vParams) from to where

      -- |
      -- Propose versions together with version parameters.  It must be
      -- encoded to a sorted list.
      --
      MsgProposeVersions
        :: Map vNumber vParams
        -> Message (Handshake vNumber vParams) StPropose StConfirm

      -- |
      -- `MsgReplyVersions` received as a response to 'MsgProposeVersions'.  It
      -- is not supported to explicitly send this message. It can only be
      -- received as a copy of 'MsgProposeVersions' in a simultaneous open
      -- scenario.
      --
      MsgReplyVersions
        :: Map vNumber vParams
        -> Message (Handshake vNumber vParams) StConfirm StDone

      -- |
      -- The remote end decides which version to use and sends chosen version.
      -- The server is allowed to modify version parameters.
      --
      MsgAcceptVersion
        :: vNumber
        -> vParams
        -> Message (Handshake vNumber vParams) StConfirm StDone

      -- |
      -- or it refuses to run any version,
      --
      MsgRefuse
        :: RefuseReason vNumber
        -> Message (Handshake vNumber vParams) StConfirm StDone

    data ClientHasAgency st where
      TokPropose :: ClientHasAgency StPropose

    data ServerHasAgency st where
      TokConfirm :: ServerHasAgency StConfirm

    data NobodyHasAgency st where
      TokDone    :: NobodyHasAgency StDone

    exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
TokPropose 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 {}

-- $simultanous-open
--
-- On simultaneous open both sides will send `MsgProposeVersions`, which will be
-- decoded as `MsgReplyVersions`.  It is a terminal message of the protocol.  It
-- is important to stress that in this case both sides will make the choice
-- which version and parameters to pick.  Our algorithm for picking version is
-- symmetric, which ensures that both sides will end up with the same choice.
-- If one side decides to refuse the version it will close the connection,
-- without sending the reason to the other side.

deriving instance (Show vNumber, Show vParams)
    => Show (Message (Handshake vNumber vParams) from to)

instance Show (ClientHasAgency (st :: Handshake vNumber vParams)) where
    show :: ClientHasAgency st -> String
show ClientHasAgency st
TokPropose       = String
"TokPropose"

instance Show (ServerHasAgency (st :: Handshake vNumber vParams)) where
    show :: ServerHasAgency st -> String
show ServerHasAgency st
TokConfirm = String
"TokConfirm"

-- | Extends handshake error @'RefuseReason'@ type, by client specific errors.
--
data HandshakeProtocolError vNumber
  = HandshakeError (RefuseReason vNumber)
  | NotRecognisedVersion vNumber
  | InvalidServerSelection vNumber Text
  deriving (HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
(HandshakeProtocolError vNumber
 -> HandshakeProtocolError vNumber -> Bool)
-> (HandshakeProtocolError vNumber
    -> HandshakeProtocolError vNumber -> Bool)
-> Eq (HandshakeProtocolError vNumber)
forall vNumber.
Eq vNumber =>
HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
$c/= :: forall vNumber.
Eq vNumber =>
HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
== :: HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
$c== :: forall vNumber.
Eq vNumber =>
HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
Eq, Int -> HandshakeProtocolError vNumber -> ShowS
[HandshakeProtocolError vNumber] -> ShowS
HandshakeProtocolError vNumber -> String
(Int -> HandshakeProtocolError vNumber -> ShowS)
-> (HandshakeProtocolError vNumber -> String)
-> ([HandshakeProtocolError vNumber] -> ShowS)
-> Show (HandshakeProtocolError vNumber)
forall vNumber.
Show vNumber =>
Int -> HandshakeProtocolError vNumber -> ShowS
forall vNumber.
Show vNumber =>
[HandshakeProtocolError vNumber] -> ShowS
forall vNumber.
Show vNumber =>
HandshakeProtocolError vNumber -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HandshakeProtocolError vNumber] -> ShowS
$cshowList :: forall vNumber.
Show vNumber =>
[HandshakeProtocolError vNumber] -> ShowS
show :: HandshakeProtocolError vNumber -> String
$cshow :: forall vNumber.
Show vNumber =>
HandshakeProtocolError vNumber -> String
showsPrec :: Int -> HandshakeProtocolError vNumber -> ShowS
$cshowsPrec :: forall vNumber.
Show vNumber =>
Int -> HandshakeProtocolError vNumber -> ShowS
Show)

instance (Typeable vNumber, Show vNumber)
    => Exception (HandshakeProtocolError vNumber)