{-# 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 (..)
, Message (..)
, ClientHasAgency (..)
, ServerHasAgency (..)
, NobodyHasAgency (..)
, 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 (..))
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"
data RefuseReason vNumber
= VersionMismatch [vNumber] [Int]
| HandshakeDecodeError vNumber Text
| 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
MsgProposeVersions
:: Map vNumber vParams
-> Message (Handshake vNumber vParams) StPropose StConfirm
MsgReplyVersions
:: Map vNumber vParams
-> Message (Handshake vNumber vParams) StConfirm StDone
MsgAcceptVersion
:: vNumber
-> vParams
-> Message (Handshake vNumber vParams) StConfirm StDone
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 {}
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"
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)