{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
module Ouroboros.Network.Protocol.LocalTxMonitor.Type where
import Data.Word
import GHC.Generics (Generic)
import Network.TypedProtocol.Core
import Ouroboros.Network.Util.ShowProxy
data LocalTxMonitor txid tx slot where
StIdle :: LocalTxMonitor txid tx slot
StAcquiring :: LocalTxMonitor txid tx slot
StAcquired :: LocalTxMonitor txid tx slot
StBusy :: StBusyKind -> LocalTxMonitor txid tx slot
StDone :: LocalTxMonitor txid tx slot
instance
( ShowProxy txid
, ShowProxy tx
, ShowProxy slot
) =>
ShowProxy (LocalTxMonitor txid tx slot)
where
showProxy :: Proxy (LocalTxMonitor txid tx slot) -> String
showProxy Proxy (LocalTxMonitor txid tx slot)
_ = [String] -> String
unwords
[ String
"LocalTxMonitor"
, Proxy txid -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy txid
forall k (t :: k). Proxy t
Proxy :: Proxy txid)
, Proxy tx -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy tx
forall k (t :: k). Proxy t
Proxy :: Proxy tx)
, Proxy slot -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy slot
forall k (t :: k). Proxy t
Proxy :: Proxy slot)
]
data StBusyKind where
NextTx :: StBusyKind
HasTx :: StBusyKind
GetSizes :: StBusyKind
data MempoolSizeAndCapacity = MempoolSizeAndCapacity
{ MempoolSizeAndCapacity -> Word32
capacityInBytes :: !Word32
, MempoolSizeAndCapacity -> Word32
sizeInBytes :: !Word32
, MempoolSizeAndCapacity -> Word32
numberOfTxs :: !Word32
} deriving ((forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x)
-> (forall x.
Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity)
-> Generic MempoolSizeAndCapacity
forall x. Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity
forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MempoolSizeAndCapacity x -> MempoolSizeAndCapacity
$cfrom :: forall x. MempoolSizeAndCapacity -> Rep MempoolSizeAndCapacity x
Generic, MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
(MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool)
-> (MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool)
-> Eq MempoolSizeAndCapacity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
$c/= :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
== :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
$c== :: MempoolSizeAndCapacity -> MempoolSizeAndCapacity -> Bool
Eq, Int -> MempoolSizeAndCapacity -> ShowS
[MempoolSizeAndCapacity] -> ShowS
MempoolSizeAndCapacity -> String
(Int -> MempoolSizeAndCapacity -> ShowS)
-> (MempoolSizeAndCapacity -> String)
-> ([MempoolSizeAndCapacity] -> ShowS)
-> Show MempoolSizeAndCapacity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MempoolSizeAndCapacity] -> ShowS
$cshowList :: [MempoolSizeAndCapacity] -> ShowS
show :: MempoolSizeAndCapacity -> String
$cshow :: MempoolSizeAndCapacity -> String
showsPrec :: Int -> MempoolSizeAndCapacity -> ShowS
$cshowsPrec :: Int -> MempoolSizeAndCapacity -> ShowS
Show)
instance Protocol (LocalTxMonitor txid tx slot) where
data Message (LocalTxMonitor txid tx slot) from to where
MsgAcquire
:: Message (LocalTxMonitor txid tx slot) StIdle StAcquiring
MsgAcquired
:: slot
-> Message (LocalTxMonitor txid tx slot) StAcquiring StAcquired
MsgAwaitAcquire
:: Message (LocalTxMonitor txid tx slot) StAcquired StAcquiring
MsgNextTx
:: Message (LocalTxMonitor txid tx slot) StAcquired (StBusy NextTx)
MsgReplyNextTx
:: Maybe tx
-> Message (LocalTxMonitor txid tx slot) (StBusy NextTx) StAcquired
MsgHasTx
:: txid
-> Message (LocalTxMonitor txid tx slot) StAcquired (StBusy HasTx)
MsgReplyHasTx
:: Bool
-> Message (LocalTxMonitor txid tx slot) (StBusy HasTx) StAcquired
MsgGetSizes
:: Message (LocalTxMonitor txid tx slot) StAcquired (StBusy GetSizes)
MsgReplyGetSizes
:: MempoolSizeAndCapacity
-> Message (LocalTxMonitor txid tx slot) (StBusy GetSizes) StAcquired
MsgRelease
:: Message (LocalTxMonitor txid tx slot) StAcquired StIdle
MsgDone
:: Message (LocalTxMonitor txid tx slot) StIdle StDone
data ClientHasAgency st where
TokIdle :: ClientHasAgency StIdle
TokAcquired :: ClientHasAgency StAcquired
data ServerHasAgency st where
TokAcquiring :: ServerHasAgency StAcquiring
TokBusy :: TokBusyKind k -> ServerHasAgency (StBusy k)
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 {}
data TokBusyKind (k :: StBusyKind) where
TokNextTx :: TokBusyKind NextTx
TokHasTx :: TokBusyKind HasTx
TokGetSizes :: TokBusyKind GetSizes
deriving instance (Show txid, Show tx, Show slot)
=> Show (Message (LocalTxMonitor txid tx slot) from to)
instance Show (ClientHasAgency (st :: LocalTxMonitor txid tx slot)) where
show :: ClientHasAgency st -> String
show = \case
ClientHasAgency st
TokIdle -> String
"TokIdle"
ClientHasAgency st
TokAcquired -> String
"TokAcquired"
instance Show (ServerHasAgency (st :: LocalTxMonitor txid tx slot)) where
show :: ServerHasAgency st -> String
show = \case
ServerHasAgency st
TokAcquiring -> String
"TokAcquiring"
TokBusy TokNextTx -> String
"TokBusy TokNextTx"
TokBusy TokHasTx -> String
"TokBusy TokHasTx"
TokBusy TokGetSizes -> String
"TokBusy TokGetSizes"