{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Ouroboros.Network.Protocol.LocalStateQuery.Server
(
LocalStateQueryServer (..)
, ServerStIdle (..)
, ServerStAcquiring (..)
, ServerStAcquired (..)
, ServerStQuerying (..)
, localStateQueryServerPeer
) where
import Data.Kind (Type)
import Network.TypedProtocol.Core
import Ouroboros.Network.Protocol.LocalStateQuery.Type
newtype LocalStateQueryServer block point (query :: Type -> Type) m a = LocalStateQueryServer {
forall block point (query :: * -> *) (m :: * -> *) a.
LocalStateQueryServer block point query m a
-> m (ServerStIdle block point query m a)
runLocalStateQueryServer :: m (ServerStIdle block point query m a)
}
data ServerStIdle block point query m a = ServerStIdle {
forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: Target point
-> m (ServerStAcquiring block point query m a),
forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a -> m a
recvMsgDone :: m a
}
data ServerStAcquiring block point query m a where
SendMsgAcquired :: ServerStAcquired block point query m a
-> ServerStAcquiring block point query m a
SendMsgFailure :: AcquireFailure
-> ServerStIdle block point query m a
-> ServerStAcquiring block point query m a
data ServerStAcquired block point query m a = ServerStAcquired {
forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery :: forall result.
query result
-> m (ServerStQuerying block point query m a result),
forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: Target point
-> m (ServerStAcquiring block point query m a),
forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> m (ServerStIdle block point query m a)
recvMsgRelease :: m (ServerStIdle block point query m a)
}
data ServerStQuerying block point query m a result where
SendMsgResult :: result
-> ServerStAcquired block point query m a
-> ServerStQuerying block point query m a result
localStateQueryServerPeer
:: forall block point (query :: Type -> Type) m a.
Monad m
=> LocalStateQueryServer block point query m a
-> Peer (LocalStateQuery block point query) AsServer StIdle m a
localStateQueryServerPeer :: forall block point (query :: * -> *) (m :: * -> *) a.
Monad m =>
LocalStateQueryServer block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
localStateQueryServerPeer (LocalStateQueryServer m (ServerStIdle block point query m a)
handler) =
m (Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> m (Peer
(LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall a b. (a -> b) -> a -> b
$ ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle (ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> m (ServerStIdle block point query m a)
-> m (Peer
(LocalStateQuery block point query) 'AsServer 'StIdle m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ServerStIdle block point query m a)
handler
where
handleStIdle
:: ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) AsServer StIdle m a
handleStIdle :: ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle ServerStIdle{Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire :: Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire, m a
recvMsgDone :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStIdle block point query m a -> m a
recvMsgDone :: m a
recvMsgDone} =
TheyHaveAgency 'AsServer 'StIdle
-> (forall (st' :: LocalStateQuery block point query).
Message (LocalStateQuery block point query) 'StIdle st'
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall (pr :: PeerRole) ps (st :: ps) (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr st' m a)
-> Peer ps pr st m a
Await (ClientHasAgency 'StIdle -> PeerHasAgency 'AsClient 'StIdle
forall {ps} (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StIdle
forall {k} {k1} {block :: k} {point :: k1} {query :: * -> *}.
ClientHasAgency 'StIdle
TokIdle) ((forall (st' :: LocalStateQuery block point query).
Message (LocalStateQuery block point query) 'StIdle st'
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a)
-> (forall (st' :: LocalStateQuery block point query).
Message (LocalStateQuery block point query) 'StIdle st'
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
forall a b. (a -> b) -> a -> b
$ \Message (LocalStateQuery block point query) 'StIdle st'
req -> case Message (LocalStateQuery block point query) 'StIdle st'
req of
MsgAcquire Target point1
tgt -> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall a b. (a -> b) -> a -> b
$
ServerStAcquiring block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
ServerStAcquiring block point query m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquiring m a
handleStAcquiring (ServerStAcquiring block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (ServerStAcquiring block point query m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Target point -> m (ServerStAcquiring block point query m a)
recvMsgAcquire Target point
Target point1
tgt
Message (LocalStateQuery block point query) 'StIdle st'
R:MessageLocalStateQueryfromto
(*) (*) block point query 'StIdle st'
MsgDone -> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall a b. (a -> b) -> a -> b
$
NobodyHasAgency st'
-> a -> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall ps (st :: ps) a (pr :: PeerRole) (m :: * -> *).
NobodyHasAgency st -> a -> Peer ps pr st m a
Done NobodyHasAgency st'
NobodyHasAgency 'StDone
forall {k} {k1} {block :: k} {point :: k1} {query :: * -> *}.
NobodyHasAgency 'StDone
TokDone (a -> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m a
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
recvMsgDone
handleStAcquiring
:: ServerStAcquiring block point query m a
-> Peer (LocalStateQuery block point query) AsServer StAcquiring m a
handleStAcquiring :: ServerStAcquiring block point query m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquiring m a
handleStAcquiring ServerStAcquiring block point query m a
req = case ServerStAcquiring block point query m a
req of
SendMsgAcquired ServerStAcquired block point query m a
stAcquired ->
WeHaveAgency 'AsServer 'StAcquiring
-> Message
(LocalStateQuery block point query) 'StAcquiring 'StAcquired
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ServerHasAgency 'StAcquiring -> WeHaveAgency 'AsServer 'StAcquiring
forall {ps} (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StAcquiring
forall {k} {k1} {block :: k} {point :: k1} {query :: * -> *}.
ServerHasAgency 'StAcquiring
TokAcquiring)
Message
(LocalStateQuery block point query) 'StAcquiring 'StAcquired
forall {k} {k1} (block :: k) (point :: k1) (query :: * -> *).
Message
(LocalStateQuery block point query) 'StAcquiring 'StAcquired
MsgAcquired
(ServerStAcquired block point query m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a
handleStAcquired ServerStAcquired block point query m a
stAcquired)
SendMsgFailure AcquireFailure
failure ServerStIdle block point query m a
stIdle ->
WeHaveAgency 'AsServer 'StAcquiring
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquiring m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ServerHasAgency 'StAcquiring -> WeHaveAgency 'AsServer 'StAcquiring
forall {ps} (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency ServerHasAgency 'StAcquiring
forall {k} {k1} {block :: k} {point :: k1} {query :: * -> *}.
ServerHasAgency 'StAcquiring
TokAcquiring)
(AcquireFailure
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
forall {k} {k1} (block :: k) (point :: k1) (query :: * -> *).
AcquireFailure
-> Message (LocalStateQuery block point query) 'StAcquiring 'StIdle
MsgFailure AcquireFailure
failure)
(ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle ServerStIdle block point query m a
stIdle)
handleStAcquired
:: ServerStAcquired block point query m a
-> Peer (LocalStateQuery block point query) AsServer StAcquired m a
handleStAcquired :: ServerStAcquired block point query m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a
handleStAcquired ServerStAcquired{forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery :: forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery, Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire :: Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire, m (ServerStIdle block point query m a)
recvMsgRelease :: forall block point (query :: * -> *) (m :: * -> *) a.
ServerStAcquired block point query m a
-> m (ServerStIdle block point query m a)
recvMsgRelease :: m (ServerStIdle block point query m a)
recvMsgRelease} =
TheyHaveAgency 'AsServer 'StAcquired
-> (forall (st' :: LocalStateQuery block point query).
Message (LocalStateQuery block point query) 'StAcquired st'
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a
forall (pr :: PeerRole) ps (st :: ps) (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr st' m a)
-> Peer ps pr st m a
Await (ClientHasAgency 'StAcquired -> PeerHasAgency 'AsClient 'StAcquired
forall {ps} (st :: ps).
ClientHasAgency st -> PeerHasAgency 'AsClient st
ClientAgency ClientHasAgency 'StAcquired
forall {k} {k1} {block :: k} {point :: k1} {query :: * -> *}.
ClientHasAgency 'StAcquired
TokAcquired) ((forall (st' :: LocalStateQuery block point query).
Message (LocalStateQuery block point query) 'StAcquired st'
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a)
-> (forall (st' :: LocalStateQuery block point query).
Message (LocalStateQuery block point query) 'StAcquired st'
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a
forall a b. (a -> b) -> a -> b
$ \Message (LocalStateQuery block point query) 'StAcquired st'
req -> case Message (LocalStateQuery block point query) 'StAcquired st'
req of
MsgQuery query result
query -> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall a b. (a -> b) -> a -> b
$ query result
-> ServerStQuerying block point query m a result
-> Peer
(LocalStateQuery block point query)
'AsServer
('StQuerying result)
m
a
forall result.
query result
-> ServerStQuerying block point query m a result
-> Peer
(LocalStateQuery block point query)
'AsServer
('StQuerying result)
m
a
handleStQuerying query result
query (ServerStQuerying block point query m a result
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (ServerStQuerying block point query m a result)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> query result -> m (ServerStQuerying block point query m a result)
forall result.
query result -> m (ServerStQuerying block point query m a result)
recvMsgQuery query result
query
MsgReAcquire Target point1
tgt -> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall a b. (a -> b) -> a -> b
$ ServerStAcquiring block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
ServerStAcquiring block point query m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquiring m a
handleStAcquiring (ServerStAcquiring block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (ServerStAcquiring block point query m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Target point -> m (ServerStAcquiring block point query m a)
recvMsgReAcquire Target point
Target point1
tgt
Message (LocalStateQuery block point query) 'StAcquired st'
R:MessageLocalStateQueryfromto
(*) (*) block point query 'StAcquired st'
MsgRelease -> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
forall a b. (a -> b) -> a -> b
$ ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer st' m a
ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer 'StIdle m a
handleStIdle (ServerStIdle block point query m a
-> Peer (LocalStateQuery block point query) 'AsServer st' m a)
-> m (ServerStIdle block point query m a)
-> m (Peer (LocalStateQuery block point query) 'AsServer st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ServerStIdle block point query m a)
recvMsgRelease
handleStQuerying
:: query result
-> ServerStQuerying block point query m a result
-> Peer (LocalStateQuery block point query) AsServer (StQuerying result) m a
handleStQuerying :: forall result.
query result
-> ServerStQuerying block point query m a result
-> Peer
(LocalStateQuery block point query)
'AsServer
('StQuerying result)
m
a
handleStQuerying query result
query (SendMsgResult result
result ServerStAcquired block point query m a
stAcquired) =
WeHaveAgency 'AsServer ('StQuerying result)
-> Message
(LocalStateQuery block point query)
('StQuerying result)
'StAcquired
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a
-> Peer
(LocalStateQuery block point query)
'AsServer
('StQuerying result)
m
a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield (ServerHasAgency ('StQuerying result)
-> WeHaveAgency 'AsServer ('StQuerying result)
forall {ps} (st :: ps).
ServerHasAgency st -> PeerHasAgency 'AsServer st
ServerAgency (query result -> ServerHasAgency ('StQuerying result)
forall {k} {k1} (query :: * -> *) result (block :: k)
(point :: k1).
query result -> ServerHasAgency ('StQuerying result)
TokQuerying query result
query))
(query result
-> result
-> Message
(LocalStateQuery block point query)
('StQuerying result)
'StAcquired
forall {k} {k1} (query :: * -> *) result (block :: k)
(point :: k1).
query result
-> result
-> Message
(LocalStateQuery block point query)
('StQuerying result)
'StAcquired
MsgResult query result
query result
result)
(ServerStAcquired block point query m a
-> Peer
(LocalStateQuery block point query) 'AsServer 'StAcquired m a
handleStAcquired ServerStAcquired block point query m a
stAcquired)