{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} module Ouroboros.Network.Protocol.ObjectDiffusion.Direct (directPipelined) where import Network.TypedProtocol.Core import Network.TypedProtocol.Proofs (Queue (..), enqueue) import Ouroboros.Network.Protocol.ObjectDiffusion.Inbound import Ouroboros.Network.Protocol.ObjectDiffusion.Outbound import Ouroboros.Network.Protocol.ObjectDiffusion.Type (BlockingReplyList (..), SingBlockingStyle (..)) directPipelined :: forall objectId object m a b. Monad m => ObjectDiffusionOutbound objectId object m a -> ObjectDiffusionInboundPipelined objectId object m b -> m b directPipelined :: forall objectId object (m :: * -> *) a b. Monad m => ObjectDiffusionOutbound objectId object m a -> ObjectDiffusionInboundPipelined objectId object m b -> m b directPipelined (ObjectDiffusionOutbound m (OutboundStIdle objectId object m a) mOutbound) (ObjectDiffusionInboundPipelined InboundStIdle 'Z objectId object m b inbound) = do outbound <- m (OutboundStIdle objectId object m a) mOutbound directSender EmptyQ inbound outbound where directSender :: forall (n :: N). Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b directSender :: forall (n :: N). Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b directSender Queue n (Collect objectId object) q (SendMsgRequestObjectIdsBlocking NumObjectIdsAck ackNo NumObjectIdsReq reqNo NonEmpty objectId -> InboundStIdle 'Z objectId object m b inboundNext) OutboundStIdle{forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds :: forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds :: forall objectId object (m :: * -> *) a. OutboundStIdle objectId object m a -> forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds} = do reply <- SingBlockingStyle 'StBlocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds 'StBlocking objectId object m a) forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds SingBlockingStyle 'StBlocking SingBlocking NumObjectIdsAck ackNo NumObjectIdsReq reqNo case reply of SendMsgReplyObjectIds (BlockingReply NonEmpty objectId objectIds) OutboundStIdle objectId object m a outbound' -> do let inbound' :: InboundStIdle 'Z objectId object m b inbound' = NonEmpty objectId -> InboundStIdle 'Z objectId object m b inboundNext NonEmpty objectId objectIds Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b forall (n :: N). Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b directSender Queue n (Collect objectId object) q InboundStIdle n objectId object m b InboundStIdle 'Z objectId object m b inbound' OutboundStIdle objectId object m a outbound' directSender Queue n (Collect objectId object) q (SendMsgRequestObjectIdsPipelined NumObjectIdsAck ackNo NumObjectIdsReq reqNo InboundStIdle ('S n) objectId object m b inbound') OutboundStIdle{forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds :: forall objectId object (m :: * -> *) a. OutboundStIdle objectId object m a -> forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds :: forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds} = do reply <- SingBlockingStyle 'StNonBlocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds 'StNonBlocking objectId object m a) forall (blocking :: StBlockingStyle). SingBlockingStyle blocking -> NumObjectIdsAck -> NumObjectIdsReq -> m (OutboundStObjectIds blocking objectId object m a) recvMsgRequestObjectIds SingBlockingStyle 'StNonBlocking SingNonBlocking NumObjectIdsAck ackNo NumObjectIdsReq reqNo case reply of SendMsgReplyObjectIds (NonBlockingReply [objectId] objectIds) OutboundStIdle objectId object m a outbound' -> do Queue ('S n) (Collect objectId object) -> InboundStIdle ('S n) objectId object m b -> OutboundStIdle objectId object m a -> m b forall (n :: N). Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b directSender (Collect objectId object -> Queue n (Collect objectId object) -> Queue ('S n) (Collect objectId object) forall a (n :: N). a -> Queue n a -> Queue ('S n) a enqueue (NumObjectIdsReq -> [objectId] -> Collect objectId object forall objectId object. NumObjectIdsReq -> [objectId] -> Collect objectId object CollectObjectIds NumObjectIdsReq reqNo [objectId] objectIds) Queue n (Collect objectId object) q) InboundStIdle ('S n) objectId object m b inbound' OutboundStIdle objectId object m a outbound' directSender Queue n (Collect objectId object) q (SendMsgRequestObjectsPipelined [objectId] objectIds InboundStIdle ('S n) objectId object m b inbound') OutboundStIdle{[objectId] -> m (OutboundStObjects objectId object m a) recvMsgRequestObjects :: [objectId] -> m (OutboundStObjects objectId object m a) recvMsgRequestObjects :: forall objectId object (m :: * -> *) a. OutboundStIdle objectId object m a -> [objectId] -> m (OutboundStObjects objectId object m a) recvMsgRequestObjects} = do SendMsgReplyObjects objects outbound' <- [objectId] -> m (OutboundStObjects objectId object m a) recvMsgRequestObjects [objectId] objectIds directSender (enqueue (CollectObjects objectIds objects) q) inbound' outbound' directSender Queue n (Collect objectId object) q (CollectPipelined (Just InboundStIdle ('S n1) objectId object m b noWaitInbound') Collect objectId object -> InboundStIdle n1 objectId object m b _inboundNext) OutboundStIdle objectId object m a outbound = do Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b forall (n :: N). Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b directSender Queue n (Collect objectId object) q InboundStIdle n objectId object m b InboundStIdle ('S n1) objectId object m b noWaitInbound' OutboundStIdle objectId object m a outbound directSender (ConsQ Collect objectId object c Queue n1 (Collect objectId object) q) (CollectPipelined Maybe (InboundStIdle ('S n1) objectId object m b) _maybeNoWaitInbound' Collect objectId object -> InboundStIdle n1 objectId object m b inboundNext) OutboundStIdle objectId object m a outbound = do let inbound' :: InboundStIdle n1 objectId object m b inbound' = Collect objectId object -> InboundStIdle n1 objectId object m b inboundNext Collect objectId object c Queue n1 (Collect objectId object) -> InboundStIdle n1 objectId object m b -> OutboundStIdle objectId object m a -> m b forall (n :: N). Queue n (Collect objectId object) -> InboundStIdle n objectId object m b -> OutboundStIdle objectId object m a -> m b directSender Queue n1 (Collect objectId object) q InboundStIdle n1 objectId object m b InboundStIdle n1 objectId object m b inbound' OutboundStIdle objectId object m a outbound directSender Queue n (Collect objectId object) q (WithEffect m (InboundStIdle n objectId object m b) mInbound) OutboundStIdle objectId object m a outbound = do inbound' <- m (InboundStIdle n objectId object m b) mInbound directSender q inbound' outbound directSender Queue n (Collect objectId object) EmptyQ (SendMsgDone b v) OutboundStIdle objectId object m a _outbound = b -> m b forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure b v