{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Ouroboros.Network.Protocol.ObjectDiffusion.Inbound
(
ObjectDiffusionInboundPipelined (..)
, InboundStIdle (..)
, Collect (..)
, objectDiffusionInboundPeerPipelined
) where
import Data.List.NonEmpty (NonEmpty)
import Network.TypedProtocol.Core
import Network.TypedProtocol.Peer (Peer, PeerPipelined (..))
import Network.TypedProtocol.Peer.Client
import Ouroboros.Network.Protocol.ObjectDiffusion.Type
data ObjectDiffusionInboundPipelined objectId object m a where
ObjectDiffusionInboundPipelined
:: InboundStIdle Z objectId object m a
-> ObjectDiffusionInboundPipelined objectId object m a
data Collect objectId object
=
CollectObjectIds NumObjectIdsReq [objectId]
|
CollectObjects [objectId] [object]
data InboundStIdle (n :: N) objectId object m a where
SendMsgRequestObjectIdsBlocking
:: NumObjectIdsAck
-> NumObjectIdsReq
-> (NonEmpty objectId -> InboundStIdle Z objectId object m a)
-> InboundStIdle Z objectId object m a
SendMsgRequestObjectIdsPipelined
:: NumObjectIdsAck
-> NumObjectIdsReq
-> InboundStIdle (S n) objectId object m a
-> InboundStIdle n objectId object m a
SendMsgRequestObjectsPipelined
:: [objectId]
-> InboundStIdle (S n) objectId object m a
-> InboundStIdle n objectId object m a
CollectPipelined
:: Maybe (InboundStIdle (S n) objectId object m a)
-> (Collect objectId object -> InboundStIdle n objectId object m a)
-> InboundStIdle (S n) objectId object m a
SendMsgDone
:: a
-> InboundStIdle Z objectId object m a
WithEffect :: m (InboundStIdle n objectId object m a)
-> InboundStIdle n objectId object m a
objectDiffusionInboundPeerPipelined
:: forall objectId object m a.
(Functor m)
=> ObjectDiffusionInboundPipelined objectId object m a
-> PeerPipelined (ObjectDiffusion objectId object) AsClient StInit m a
objectDiffusionInboundPeerPipelined :: forall objectId object (m :: * -> *) a.
Functor m =>
ObjectDiffusionInboundPipelined objectId object m a
-> PeerPipelined
(ObjectDiffusion objectId object) 'AsClient 'StInit m a
objectDiffusionInboundPeerPipelined (ObjectDiffusionInboundPipelined InboundStIdle 'Z objectId object m a
inboundSt) =
Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined 'Z (Collect objectId object))
'StInit
m
a
-> PeerPipelined
(ObjectDiffusion objectId object) 'AsClient 'StInit m a
forall ps (pr :: PeerRole) c (st :: ps) (m :: * -> *) a.
Peer ps pr ('Pipelined 'Z c) st m a -> PeerPipelined ps pr st m a
PeerPipelined (Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined 'Z (Collect objectId object))
'StInit
m
a
-> PeerPipelined
(ObjectDiffusion objectId object) 'AsClient 'StInit m a)
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined 'Z (Collect objectId object))
'StInit
m
a
-> PeerPipelined
(ObjectDiffusion objectId object) 'AsClient 'StInit m a
forall a b. (a -> b) -> a -> b
$ Message (ObjectDiffusion objectId object) 'StInit 'StIdle
-> Client
(ObjectDiffusion objectId object)
('Pipelined 'Z (Collect objectId object))
'StIdle
m
a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined 'Z (Collect objectId object))
'StInit
m
a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
(st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield Message (ObjectDiffusion objectId object) 'StInit 'StIdle
forall objectId object.
Message (ObjectDiffusion objectId object) 'StInit 'StIdle
MsgInit (Client
(ObjectDiffusion objectId object)
('Pipelined 'Z (Collect objectId object))
'StIdle
m
a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined 'Z (Collect objectId object))
'StInit
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined 'Z (Collect objectId object))
'StIdle
m
a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined 'Z (Collect objectId object))
'StInit
m
a
forall a b. (a -> b) -> a -> b
$ InboundStIdle 'Z objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined 'Z (Collect objectId object))
'StIdle
m
a
forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run InboundStIdle 'Z objectId object m a
inboundSt
where
run
:: InboundStIdle n objectId object m a
-> Peer (ObjectDiffusion objectId object) AsClient (Pipelined n (Collect objectId object)) StIdle m a
run :: forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run (SendMsgRequestObjectIdsBlocking NumObjectIdsAck
ackNo NumObjectIdsReq
reqNo NonEmpty objectId -> InboundStIdle 'Z objectId object m a
k) =
Message
(ObjectDiffusion objectId object)
'StIdle
('StObjectIds 'StBlocking)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
('StObjectIds 'StBlocking)
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
(st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield (SingBlockingStyle 'StBlocking
-> NumObjectIdsAck
-> NumObjectIdsReq
-> Message
(ObjectDiffusion objectId object)
'StIdle
('StObjectIds 'StBlocking)
forall (blocking :: StBlockingStyle) objectId object.
SingBlockingStyle blocking
-> NumObjectIdsAck
-> NumObjectIdsReq
-> Message
(ObjectDiffusion objectId object) 'StIdle ('StObjectIds blocking)
MsgRequestObjectIds SingBlockingStyle 'StBlocking
SingBlocking NumObjectIdsAck
ackNo NumObjectIdsReq
reqNo)
(Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
('StObjectIds 'StBlocking)
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
('StObjectIds 'StBlocking)
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall a b. (a -> b) -> a -> b
$ (forall (st' :: ObjectDiffusion objectId object).
Message
(ObjectDiffusion objectId object) ('StObjectIds 'StBlocking) st'
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
st'
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
('StObjectIds 'StBlocking)
m
a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency,
Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Client ps pl st' m a)
-> Client ps pl st m a
Await
((forall (st' :: ObjectDiffusion objectId object).
Message
(ObjectDiffusion objectId object) ('StObjectIds 'StBlocking) st'
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
st'
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
('StObjectIds 'StBlocking)
m
a)
-> (forall (st' :: ObjectDiffusion objectId object).
Message
(ObjectDiffusion objectId object) ('StObjectIds 'StBlocking) st'
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
st'
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
('StObjectIds 'StBlocking)
m
a
forall a b. (a -> b) -> a -> b
$ \case
MsgReplyObjectIds (BlockingReply NonEmpty objectId
objectIds) ->
InboundStIdle n objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run (NonEmpty objectId -> InboundStIdle 'Z objectId object m a
k NonEmpty objectId
objectIds)
run (SendMsgRequestObjectIdsPipelined NumObjectIdsAck
ackNo NumObjectIdsReq
reqNo InboundStIdle ('S n) objectId object m a
k) =
Message
(ObjectDiffusion objectId object)
'StIdle
('StObjectIds 'StNonBlocking)
-> Receiver
(ObjectDiffusion objectId object)
('StObjectIds 'StNonBlocking)
'StIdle
m
(Collect objectId object)
-> Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
(st'' :: ps).
(StateTokenI st, StateTokenI st',
StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
YieldPipelined
(SingBlockingStyle 'StNonBlocking
-> NumObjectIdsAck
-> NumObjectIdsReq
-> Message
(ObjectDiffusion objectId object)
'StIdle
('StObjectIds 'StNonBlocking)
forall (blocking :: StBlockingStyle) objectId object.
SingBlockingStyle blocking
-> NumObjectIdsAck
-> NumObjectIdsReq
-> Message
(ObjectDiffusion objectId object) 'StIdle ('StObjectIds blocking)
MsgRequestObjectIds SingBlockingStyle 'StNonBlocking
SingNonBlocking NumObjectIdsAck
ackNo NumObjectIdsReq
reqNo)
((forall (st' :: ObjectDiffusion objectId object).
Message
(ObjectDiffusion objectId object) ('StObjectIds 'StNonBlocking) st'
-> Receiver
(ObjectDiffusion objectId object)
st'
'StIdle
m
(Collect objectId object))
-> Receiver
(ObjectDiffusion objectId object)
('StObjectIds 'StNonBlocking)
'StIdle
m
(Collect objectId object)
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
(StateTokenI st, ActiveState st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
Message ps st st' -> Receiver ps st' stdone m c)
-> Receiver ps st stdone m c
ReceiverAwait
((forall (st' :: ObjectDiffusion objectId object).
Message
(ObjectDiffusion objectId object) ('StObjectIds 'StNonBlocking) st'
-> Receiver
(ObjectDiffusion objectId object)
st'
'StIdle
m
(Collect objectId object))
-> Receiver
(ObjectDiffusion objectId object)
('StObjectIds 'StNonBlocking)
'StIdle
m
(Collect objectId object))
-> (forall (st' :: ObjectDiffusion objectId object).
Message
(ObjectDiffusion objectId object) ('StObjectIds 'StNonBlocking) st'
-> Receiver
(ObjectDiffusion objectId object)
st'
'StIdle
m
(Collect objectId object))
-> Receiver
(ObjectDiffusion objectId object)
('StObjectIds 'StNonBlocking)
'StIdle
m
(Collect objectId object)
forall a b. (a -> b) -> a -> b
$ \(MsgReplyObjectIds (NonBlockingReply [objectId]
objectIds)) ->
Collect objectId object
-> Receiver
(ObjectDiffusion objectId object)
st'
st'
m
(Collect objectId object)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (NumObjectIdsReq -> [objectId] -> Collect objectId object
forall objectId object.
NumObjectIdsReq -> [objectId] -> Collect objectId object
CollectObjectIds NumObjectIdsReq
reqNo [objectId]
objectIds)
)
(InboundStIdle ('S n) objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a
forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run InboundStIdle ('S n) objectId object m a
k)
run (SendMsgRequestObjectsPipelined [objectId]
objectIds InboundStIdle ('S n) objectId object m a
k) =
Message (ObjectDiffusion objectId object) 'StIdle 'StObjects
-> Receiver
(ObjectDiffusion objectId object)
'StObjects
'StIdle
m
(Collect objectId object)
-> Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
(st'' :: ps).
(StateTokenI st, StateTokenI st',
StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
YieldPipelined
([objectId]
-> Message (ObjectDiffusion objectId object) 'StIdle 'StObjects
forall objectId object.
[objectId]
-> Message (ObjectDiffusion objectId object) 'StIdle 'StObjects
MsgRequestObjects [objectId]
objectIds)
((forall (st' :: ObjectDiffusion objectId object).
Message (ObjectDiffusion objectId object) 'StObjects st'
-> Receiver
(ObjectDiffusion objectId object)
st'
'StIdle
m
(Collect objectId object))
-> Receiver
(ObjectDiffusion objectId object)
'StObjects
'StIdle
m
(Collect objectId object)
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
(StateTokenI st, ActiveState st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
Message ps st st' -> Receiver ps st' stdone m c)
-> Receiver ps st stdone m c
ReceiverAwait
((forall (st' :: ObjectDiffusion objectId object).
Message (ObjectDiffusion objectId object) 'StObjects st'
-> Receiver
(ObjectDiffusion objectId object)
st'
'StIdle
m
(Collect objectId object))
-> Receiver
(ObjectDiffusion objectId object)
'StObjects
'StIdle
m
(Collect objectId object))
-> (forall (st' :: ObjectDiffusion objectId object).
Message (ObjectDiffusion objectId object) 'StObjects st'
-> Receiver
(ObjectDiffusion objectId object)
st'
'StIdle
m
(Collect objectId object))
-> Receiver
(ObjectDiffusion objectId object)
'StObjects
'StIdle
m
(Collect objectId object)
forall a b. (a -> b) -> a -> b
$ \(MsgReplyObjects [object]
objects) ->
Collect objectId object
-> Receiver
(ObjectDiffusion objectId object)
st'
st'
m
(Collect objectId object)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone ([objectId] -> [object] -> Collect objectId object
forall objectId object.
[objectId] -> [object] -> Collect objectId object
CollectObjects [objectId]
objectIds [object]
objects)
)
(InboundStIdle ('S n) objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a
forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run InboundStIdle ('S n) objectId object m a
k)
run (CollectPipelined Maybe (InboundStIdle ('S n) objectId object m a)
none Collect objectId object -> InboundStIdle n objectId object m a
collect) =
Maybe
(Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a)
-> (Collect objectId object
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a
forall ps (st :: ps) (n :: N) c (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Client ps ('Pipelined ('S n) c) st m a)
-> (c -> Client ps ('Pipelined n c) st m a)
-> Client ps ('Pipelined ('S n) c) st m a
Collect
(InboundStIdle ('S n) objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a
forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run (InboundStIdle ('S n) objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a)
-> Maybe (InboundStIdle ('S n) objectId object m a)
-> Maybe
(Client
(ObjectDiffusion objectId object)
('Pipelined ('S n) (Collect objectId object))
'StIdle
m
a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (InboundStIdle ('S n) objectId object m a)
none)
(InboundStIdle n objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run (InboundStIdle n objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> (Collect objectId object -> InboundStIdle n objectId object m a)
-> Collect objectId object
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Collect objectId object -> InboundStIdle n objectId object m a
collect)
run (SendMsgDone a
done) =
Message (ObjectDiffusion objectId object) 'StIdle 'StDone
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StDone
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
(st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Yield Message (ObjectDiffusion objectId object) 'StIdle 'StDone
forall objectId object.
Message (ObjectDiffusion objectId object) 'StIdle 'StDone
MsgDone (Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StDone
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StDone
m
a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall a b. (a -> b) -> a -> b
$ a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StDone
m
a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
Outstanding pl ~ 'Z) =>
a -> Client ps pl st m a
Done a
done
run (WithEffect m (InboundStIdle n objectId object m a)
mNext) =
m (Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
m (Client ps pl st m a) -> Client ps pl st m a
Effect (m (Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> m (Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall a b. (a -> b) -> a -> b
$ InboundStIdle n objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a
forall (n :: N).
InboundStIdle n objectId object m a
-> Peer
(ObjectDiffusion objectId object)
'AsClient
('Pipelined n (Collect objectId object))
'StIdle
m
a
run (InboundStIdle n objectId object m a
-> Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
-> m (InboundStIdle n objectId object m a)
-> m (Client
(ObjectDiffusion objectId object)
('Pipelined n (Collect objectId object))
'StIdle
m
a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (InboundStIdle n objectId object m a)
mNext