Skip to content

Commit

Permalink
WIP: Use typed-protocols-0.2.0.0
Browse files Browse the repository at this point in the history
  • Loading branch information
coot committed Sep 26, 2023
1 parent 9257480 commit e40e684
Show file tree
Hide file tree
Showing 6 changed files with 76 additions and 62 deletions.
24 changes: 24 additions & 0 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 2 additions & 1 deletion ekg-forward.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
12 changes: 6 additions & 6 deletions src/System/Metrics/Protocol/Acceptor.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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

Expand All @@ -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)
36 changes: 18 additions & 18 deletions src/System/Metrics/Protocol/Codec.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
Expand All @@ -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

Expand All @@ -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
12 changes: 6 additions & 6 deletions src/System/Metrics/Protocol/Forwarder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
51 changes: 20 additions & 31 deletions src/System/Metrics/Protocol/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}

-- | The type of the EKG forwarding/accepting protocol.
Expand All @@ -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
Expand Down Expand Up @@ -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.
Expand All @@ -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)

0 comments on commit e40e684

Please sign in to comment.