diff --git a/cabal.project b/cabal.project index 01337d6..124d763 100644 --- a/cabal.project +++ b/cabal.project @@ -31,3 +31,27 @@ if impl(ghc >= 9.6) , *:base , ekg-core:* , protolude:* + +source-repository-package + type: git + location: https://github.com/input-output-hk/typed-protocols + tag: fdfc6c580b964458e53776ea48417b67c7494d71 + --sha256: sha256-LoPuQIlMu1QNEzb/p2Gnb/SqMxJpBQLUQVGz0TlyIho= + subdir: + typed-protocols + typed-protocols-cborg + typed-protocols-examples + typed-protocols-stateful + typed-protocols-stateful-cborg + +source-repository-package + type: git + location: https://github.com/input-output-hk/ouroboros-network + tag: f1bb5e5fce3e704c9f252df9f36e687bd3d4f1cc + --sha256: sha256-TjXzP32jTJJEbyUseeUTLcPRX+UssMLYBf25aW+ZRbU= + subdir: network-mux + ouroboros-network + ouroboros-network-api + ouroboros-network-framework + ouroboros-network-protocols + ouroboros-network-testing diff --git a/ekg-forward.cabal b/ekg-forward.cabal index c1bca41..ca0d44a 100644 --- a/ekg-forward.cabal +++ b/ekg-forward.cabal @@ -66,11 +66,12 @@ library , network , ouroboros-network-api , ouroboros-network-framework >= 0.8 && < 0.10 + , singletons >= 3.0.0 , serialise , stm , text , time - , typed-protocols ^>= 0.1 + , typed-protocols ^>= 0.2 , typed-protocols-cborg , unordered-containers diff --git a/src/System/Metrics/Protocol/Acceptor.hs b/src/System/Metrics/Protocol/Acceptor.hs index efb5868..e931c39 100644 --- a/src/System/Metrics/Protocol/Acceptor.hs +++ b/src/System/Metrics/Protocol/Acceptor.hs @@ -12,8 +12,8 @@ module System.Metrics.Protocol.Acceptor ( , ekgAcceptorPeer ) where -import Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..), - PeerRole (..)) +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Client import System.Metrics.Protocol.Type @@ -36,14 +36,14 @@ data EKGAcceptor req resp m a where ekgAcceptorPeer :: Monad m => EKGAcceptor req resp m a - -> Peer (EKGForward req resp) 'AsClient 'StIdle m a + -> Client (EKGForward req resp) 'NonPipelined 'Empty 'StIdle m stm a ekgAcceptorPeer = \case SendMsgReq req next -> -- Send our message (request for the new metrics from the forwarder). - Yield (ClientAgency TokIdle) (MsgReq req) $ + Yield (MsgReq req) $ -- We're now into the 'StBusy' state, and now we'll wait for a reply -- from the forwarder. - Await (ServerAgency TokBusy) $ \(MsgResp resp) -> + Await $ \(MsgResp resp) -> Effect $ ekgAcceptorPeer <$> next resp @@ -53,4 +53,4 @@ ekgAcceptorPeer = \case -- 'done', with a return value. Effect $ do r <- getResult - return $ Yield (ClientAgency TokIdle) MsgDone (Done TokDone r) + return $ Yield MsgDone (Done r) diff --git a/src/System/Metrics/Protocol/Codec.hs b/src/System/Metrics/Protocol/Codec.hs index d22dd42..43af878 100644 --- a/src/System/Metrics/Protocol/Codec.hs +++ b/src/System/Metrics/Protocol/Codec.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} @@ -14,9 +15,9 @@ import Codec.CBOR.Read (DeserialiseFailure) import Control.Monad.Class.MonadST (MonadST) import qualified Data.ByteString.Lazy as LBS import Text.Printf (printf) -import Network.TypedProtocol.Codec.CBOR (Codec, PeerHasAgency (..), - PeerRole (..), SomeMessage (..), - mkCodecCborLazyBS) +import Network.TypedProtocol.Core +import Network.TypedProtocol.Codec (Codec, SomeMessage (..)) +import Network.TypedProtocol.Codec.CBOR (mkCodecCborLazyBS) import System.Metrics.Protocol.Type @@ -34,47 +35,46 @@ codecEKGForward encodeReq decodeReq mkCodecCborLazyBS encode decode where -- Encode messages. - encode :: forall (pr :: PeerRole) - (st :: EKGForward req resp) + encode :: forall (st :: EKGForward req resp) (st' :: EKGForward req resp). - PeerHasAgency pr st - -> Message (EKGForward req resp) st st' + Message (EKGForward req resp) st st' -> CBOR.Encoding - encode (ClientAgency TokIdle) (MsgReq req) = + encode (MsgReq req) = CBOR.encodeListLen 2 <> CBOR.encodeWord 0 <> encodeReq req - encode (ClientAgency TokIdle) MsgDone = + encode MsgDone = CBOR.encodeListLen 1 <> CBOR.encodeWord 1 - encode (ServerAgency TokBusy) (MsgResp resp) = + encode (MsgResp resp) = CBOR.encodeListLen 2 <> CBOR.encodeWord 1 <> encodeResp resp -- Decode messages - decode :: forall (pr :: PeerRole) - (st :: EKGForward req resp) s. - PeerHasAgency pr st + decode :: forall (st :: EKGForward req resp) s. + ActiveState st + => StateToken st -> CBOR.Decoder s (SomeMessage st) decode stok = do len <- CBOR.decodeListLen key <- CBOR.decodeWord case (key, len, stok) of - (0, 2, ClientAgency TokIdle) -> + (0, 2, SingIdle) -> SomeMessage . MsgReq <$> decodeReq - (1, 1, ClientAgency TokIdle) -> + (1, 1, SingIdle) -> return $ SomeMessage MsgDone - (1, 2, ServerAgency TokBusy) -> + (1, 2, SingBusy) -> SomeMessage . MsgResp <$> decodeResp -- Failures per protocol state - (_, _, ClientAgency TokIdle) -> + (_, _, SingIdle) -> fail (printf "codecEKGForward (%s) unexpected key (%d, %d)" (show stok) key len) - (_, _, ServerAgency TokBusy) -> + (_, _, SingBusy) -> fail (printf "codecEKGForward (%s) unexpected key (%d, %d)" (show stok) key len) + (_, _, SingDone) -> notActiveState stok diff --git a/src/System/Metrics/Protocol/Forwarder.hs b/src/System/Metrics/Protocol/Forwarder.hs index 38572c3..d94bd53 100644 --- a/src/System/Metrics/Protocol/Forwarder.hs +++ b/src/System/Metrics/Protocol/Forwarder.hs @@ -8,8 +8,8 @@ module System.Metrics.Protocol.Forwarder ( , ekgForwarderPeer ) where -import Network.TypedProtocol.Core (Peer (..), PeerHasAgency (..), - PeerRole (..)) +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Server import System.Metrics.Protocol.Type @@ -34,18 +34,18 @@ data EKGForwarder req resp m a = EKGForwarder { ekgForwarderPeer :: Monad m => EKGForwarder req resp m a - -> Peer (EKGForward req resp) 'AsServer 'StIdle m a + -> Server (EKGForward req resp) 'NonPipelined 'Empty 'StIdle m stm a ekgForwarderPeer EKGForwarder{..} = -- In the 'StIdle' state the forwarder is awaiting a request message -- from the acceptor. - Await (ClientAgency TokIdle) $ \case + Await $ \case -- The acceptor sent us a request for new metrics, so now we're -- in the 'StBusy' state which means it's the forwarder's turn to send -- a reply. MsgReq req -> Effect $ do (resp, next) <- recvMsgReq req - return $ Yield (ServerAgency TokBusy) (MsgResp resp) (ekgForwarderPeer next) + return $ Yield (MsgResp resp) (ekgForwarderPeer next) -- The acceptor sent the done transition, so we're in the 'StDone' state -- so all we can do is stop using 'done', with a return value. - MsgDone -> Effect $ Done TokDone <$> recvMsgDone + MsgDone -> Effect $ Done <$> recvMsgDone diff --git a/src/System/Metrics/Protocol/Type.hs b/src/System/Metrics/Protocol/Type.hs index 5cc26b0..869bb69 100644 --- a/src/System/Metrics/Protocol/Type.hs +++ b/src/System/Metrics/Protocol/Type.hs @@ -4,6 +4,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} -- | The type of the EKG forwarding/accepting protocol. @@ -13,14 +14,12 @@ module System.Metrics.Protocol.Type ( EKGForward (..) + , SingEKGForward (..) , Message (..) - , ClientHasAgency (..) - , ServerHasAgency (..) - , NobodyHasAgency (..) ) where -import Data.Proxy (Proxy(..)) -import Network.TypedProtocol.Core (Protocol (..)) +import Data.Singletons +import Network.TypedProtocol.Core import Ouroboros.Network.Util.ShowProxy (ShowProxy(..)) -- | A kind to identify our protocol, and the types of the states in the state @@ -69,6 +68,16 @@ instance (ShowProxy req, ShowProxy resp) , ")" ] +data SingEKGForward (st :: EKGForward req resp) where + SingIdle :: SingEKGForward 'StIdle + SingBusy :: SingEKGForward 'StBusy + SingDone :: SingEKGForward 'StDone + +deriving instance Show (SingEKGForward st) +instance StateTokenI 'StIdle where stateToken = SingIdle +instance StateTokenI 'StBusy where stateToken = SingBusy +instance StateTokenI 'StDone where stateToken = SingDone + instance Protocol (EKGForward req resp) where -- | The messages in the EKG forwarding/accepting protocol. @@ -91,32 +100,12 @@ instance Protocol (EKGForward req resp) where -- 2. When both peers are in Busy state, the forwarder is expected to send -- a reply to the acceptor (list of new metrics). -- - -- So we assume that, from __interaction__ point of view: - -- 1. ClientHasAgency (from 'Network.TypedProtocol.Core') corresponds to acceptor's agency. - -- 3. ServerHasAgency (from 'Network.TypedProtocol.Core') corresponds to forwarder's agency. - -- - data ClientHasAgency st where - TokIdle :: ClientHasAgency 'StIdle - - data ServerHasAgency st where - TokBusy :: ServerHasAgency 'StBusy - - data NobodyHasAgency st where - TokDone :: NobodyHasAgency 'StDone - - -- | Impossible cases. - exclusionLemma_ClientAndServerHaveAgency TokIdle tok = case tok of {} - exclusionLemma_NobodyAndClientHaveAgency TokDone tok = case tok of {} - exclusionLemma_NobodyAndServerHaveAgency TokDone tok = case tok of {} + type StateAgency 'StIdle = 'ClientAgency + type StateAgency 'StBusy = 'ServerAgency + type StateAgency 'StDone = 'NobodyAgency -instance (Show req, Show resp) - => Show (Message (EKGForward req resp) from to) where - show MsgReq{} = "MsgReq" - show MsgResp{} = "MsgResp" - show MsgDone{} = "MsgDone" + type StateToken = SingEKGForward -instance Show (ClientHasAgency (st :: EKGForward req resp)) where - show TokIdle = "TokIdle" -instance Show (ServerHasAgency (st :: EKGForward req resp)) where - show TokBusy = "TokBusy" +deriving instance (Show req, Show resp) + => Show (Message (EKGForward req resp) from to)