{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Ouroboros.Network.Protocol.LocalStateQuery.Type where
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import Network.TypedProtocol.Core
import Ouroboros.Network.Util.ShowProxy (ShowProxy (..))
data LocalStateQuery block point (query :: Type -> Type) where
StIdle :: LocalStateQuery block point query
StAcquiring :: LocalStateQuery block point query
StAcquired :: LocalStateQuery block point query
StQuerying :: result -> LocalStateQuery block point query
StDone :: LocalStateQuery block point query
instance ( ShowProxy block
, ShowProxy query
) => ShowProxy (LocalStateQuery block point query) where
showProxy :: Proxy (LocalStateQuery block point query) -> String
showProxy Proxy (LocalStateQuery block point query)
_ = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
"LocalStateQuery "
, Proxy block -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy block
forall k (t :: k). Proxy t
Proxy :: Proxy block)
, String
" "
, Proxy query -> String
forall k (p :: k). ShowProxy p => Proxy p -> String
showProxy (Proxy query
forall k (t :: k). Proxy t
Proxy :: Proxy query)
]
instance Protocol (LocalStateQuery block point query) where
data Message (LocalStateQuery block point query) from to where
MsgAcquire
:: Maybe point
-> Message (LocalStateQuery block point query) StIdle StAcquiring
MsgAcquired
:: Message (LocalStateQuery block point query) StAcquiring StAcquired
MsgFailure
:: AcquireFailure
-> Message (LocalStateQuery block point query) StAcquiring StIdle
MsgQuery
:: query result
-> Message (LocalStateQuery block point query) StAcquired (StQuerying result)
MsgResult
:: query result
-> result
-> Message (LocalStateQuery block point query) (StQuerying result) StAcquired
MsgRelease
:: Message (LocalStateQuery block point query) StAcquired StIdle
MsgReAcquire
:: Maybe point
-> Message (LocalStateQuery block point query) StAcquired StAcquiring
MsgDone
:: Message (LocalStateQuery block point query) StIdle StDone
data ClientHasAgency st where
TokIdle :: ClientHasAgency StIdle
TokAcquired :: ClientHasAgency StAcquired
data ServerHasAgency st where
TokAcquiring :: ServerHasAgency StAcquiring
TokQuerying :: query result
-> ServerHasAgency (StQuerying result :: LocalStateQuery block point query)
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_ClientAndServerHaveAgency ClientHasAgency st
TokAcquired 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 AcquireFailure = AcquireFailurePointTooOld
| AcquireFailurePointNotOnChain
deriving (AcquireFailure -> AcquireFailure -> Bool
(AcquireFailure -> AcquireFailure -> Bool)
-> (AcquireFailure -> AcquireFailure -> Bool) -> Eq AcquireFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AcquireFailure -> AcquireFailure -> Bool
$c/= :: AcquireFailure -> AcquireFailure -> Bool
== :: AcquireFailure -> AcquireFailure -> Bool
$c== :: AcquireFailure -> AcquireFailure -> Bool
Eq, Int -> AcquireFailure
AcquireFailure -> Int
AcquireFailure -> [AcquireFailure]
AcquireFailure -> AcquireFailure
AcquireFailure -> AcquireFailure -> [AcquireFailure]
AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure]
(AcquireFailure -> AcquireFailure)
-> (AcquireFailure -> AcquireFailure)
-> (Int -> AcquireFailure)
-> (AcquireFailure -> Int)
-> (AcquireFailure -> [AcquireFailure])
-> (AcquireFailure -> AcquireFailure -> [AcquireFailure])
-> (AcquireFailure -> AcquireFailure -> [AcquireFailure])
-> (AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure])
-> Enum AcquireFailure
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromThenTo :: AcquireFailure
-> AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFromTo :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromTo :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFromThen :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
$cenumFromThen :: AcquireFailure -> AcquireFailure -> [AcquireFailure]
enumFrom :: AcquireFailure -> [AcquireFailure]
$cenumFrom :: AcquireFailure -> [AcquireFailure]
fromEnum :: AcquireFailure -> Int
$cfromEnum :: AcquireFailure -> Int
toEnum :: Int -> AcquireFailure
$ctoEnum :: Int -> AcquireFailure
pred :: AcquireFailure -> AcquireFailure
$cpred :: AcquireFailure -> AcquireFailure
succ :: AcquireFailure -> AcquireFailure
$csucc :: AcquireFailure -> AcquireFailure
Enum, Int -> AcquireFailure -> ShowS
[AcquireFailure] -> ShowS
AcquireFailure -> String
(Int -> AcquireFailure -> ShowS)
-> (AcquireFailure -> String)
-> ([AcquireFailure] -> ShowS)
-> Show AcquireFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AcquireFailure] -> ShowS
$cshowList :: [AcquireFailure] -> ShowS
show :: AcquireFailure -> String
$cshow :: AcquireFailure -> String
showsPrec :: Int -> AcquireFailure -> ShowS
$cshowsPrec :: Int -> AcquireFailure -> ShowS
Show)
instance Show (ClientHasAgency (st :: LocalStateQuery block point query)) where
show :: ClientHasAgency st -> String
show ClientHasAgency st
TokIdle = String
"TokIdle"
show ClientHasAgency st
TokAcquired = String
"TokAcquired"
instance (forall result. Show (query result))
=> Show (ServerHasAgency (st :: LocalStateQuery block point query)) where
show :: ServerHasAgency st -> String
show ServerHasAgency st
TokAcquiring = String
"TokAcquiring"
show (TokQuerying query) = String
"TokQuerying " String -> ShowS
forall a. [a] -> [a] -> [a]
++ query result -> String
forall a. Show a => a -> String
show query result
query
class (forall result. Show (query result)) => ShowQuery query where
showResult :: forall result. query result -> result -> String
instance (ShowQuery query, Show point)
=> Show (Message (LocalStateQuery block point query) st st') where
showsPrec :: Int -> Message (LocalStateQuery block point query) st st' -> ShowS
showsPrec Int
p Message (LocalStateQuery block point query) st st'
msg = case Message (LocalStateQuery block point query) st st'
msg of
MsgAcquire pt -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"MsgAcquire " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> Maybe point -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Maybe point
pt
Message (LocalStateQuery block point query) st st'
MsgAcquired ->
String -> ShowS
showString String
"MsgAcquired"
MsgFailure failure -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"MsgFailure " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> AcquireFailure -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 AcquireFailure
failure
MsgQuery query -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"MsgQuery " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> query result -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 query result
query
MsgResult query result -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"MsgResult " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Bool -> ShowS -> ShowS
showParen Bool
True (String -> ShowS
showString (query result -> result -> String
forall (query :: * -> *) result.
ShowQuery query =>
query result -> result -> String
showResult query result
query result
result))
Message (LocalStateQuery block point query) st st'
MsgRelease ->
String -> ShowS
showString String
"MsgRelease"
MsgReAcquire pt -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"MsgReAcquire " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> Maybe point -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Maybe point
pt
Message (LocalStateQuery block point query) st st'
MsgDone ->
String -> ShowS
showString String
"MsgDone"