{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
module Ouroboros.Network.Protocol.LocalTxSubmission.Type where
import Network.TypedProtocol.Core
import Ouroboros.Network.Util.ShowProxy
data LocalTxSubmission tx reject where
StIdle :: LocalTxSubmission tx reject
StBusy :: LocalTxSubmission tx reject
StDone :: LocalTxSubmission tx reject
instance ( ShowProxy tx
, ShowProxy reject
) => ShowProxy (LocalTxSubmission tx reject) where
showProxy :: Proxy (LocalTxSubmission tx reject) -> String
showProxy Proxy (LocalTxSubmission tx reject)
_ = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
"LocalTxSubmission ("
, Proxy tx -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy tx
forall k (t :: k). Proxy t
Proxy :: Proxy tx)
, String
") ("
, Proxy reject -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy reject
forall k (t :: k). Proxy t
Proxy :: Proxy reject)
, String
")"
]
data SubmitResult reason
= SubmitSuccess
| SubmitFail reason
deriving (SubmitResult reason -> SubmitResult reason -> Bool
(SubmitResult reason -> SubmitResult reason -> Bool)
-> (SubmitResult reason -> SubmitResult reason -> Bool)
-> Eq (SubmitResult reason)
forall reason.
Eq reason =>
SubmitResult reason -> SubmitResult reason -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SubmitResult reason -> SubmitResult reason -> Bool
$c/= :: forall reason.
Eq reason =>
SubmitResult reason -> SubmitResult reason -> Bool
== :: SubmitResult reason -> SubmitResult reason -> Bool
$c== :: forall reason.
Eq reason =>
SubmitResult reason -> SubmitResult reason -> Bool
Eq, a -> SubmitResult b -> SubmitResult a
(a -> b) -> SubmitResult a -> SubmitResult b
(forall a b. (a -> b) -> SubmitResult a -> SubmitResult b)
-> (forall a b. a -> SubmitResult b -> SubmitResult a)
-> Functor SubmitResult
forall a b. a -> SubmitResult b -> SubmitResult a
forall a b. (a -> b) -> SubmitResult a -> SubmitResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SubmitResult b -> SubmitResult a
$c<$ :: forall a b. a -> SubmitResult b -> SubmitResult a
fmap :: (a -> b) -> SubmitResult a -> SubmitResult b
$cfmap :: forall a b. (a -> b) -> SubmitResult a -> SubmitResult b
Functor)
instance Protocol (LocalTxSubmission tx reject) where
data Message (LocalTxSubmission tx reject) from to where
MsgSubmitTx
:: tx
-> Message (LocalTxSubmission tx reject) StIdle StBusy
MsgAcceptTx
:: Message (LocalTxSubmission tx reject) StBusy StIdle
MsgRejectTx
:: reject
-> Message (LocalTxSubmission tx reject) StBusy StIdle
MsgDone
:: Message (LocalTxSubmission tx reject) StIdle StDone
data ClientHasAgency st where
TokIdle :: ClientHasAgency StIdle
data ServerHasAgency st where
TokBusy :: ServerHasAgency StBusy
data NobodyHasAgency st where
TokDone :: NobodyHasAgency StDone
exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
TokIdle 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 (Eq tx, Eq reject) =>
Eq (Message (LocalTxSubmission tx reject) from to)
deriving instance (Show tx, Show reject) =>
Show (Message (LocalTxSubmission tx reject) from to)
instance Show (ClientHasAgency (st :: LocalTxSubmission tx reject)) where
show :: ClientHasAgency st -> String
show ClientHasAgency st
TokIdle = String
"TokIdle"
instance Show (ServerHasAgency (st :: LocalTxSubmission tx reject)) where
show :: ServerHasAgency st -> String
show ServerHasAgency st
TokBusy = String
"TokBusy"