Safe Haskell	Safe-Inferred
Language	Haskell2010

Trace.Forward.Protocol.DataPoint.Type

Description

The type of the DataPoint forwarding/accepting protocol.

Synopsis

type DataPointName = Text
type DataPointValue = ByteString
type DataPointValues = [(DataPointName, Maybe DataPointValue)]
data DataPointForward where
- StIdle :: DataPointForward
- StBusy :: DataPointForward
- StDone :: DataPointForward
data family Message ps (st :: ps) (st' :: ps)
data family ClientHasAgency (st :: ps)
data family ServerHasAgency (st :: ps)
data family NobodyHasAgency (st :: ps)

Documentation

type DataPointName = Text Source #

A kind to identify our protocol, and the types of the states in the state transition diagram of the protocol.

IMPORTANT NOTE: the following terminology is used:

From the protocol's point of view, two peers talk to each other: the forwarder and the acceptor.
The forwarder is an application that collects DataPoints and sends them to the acceptor by request (with MsgDataPointsReply).
The acceptor is an application that receives DataPoints from the forwarder.
You can think of the acceptor as a client, and the forwarder as a server. After the connection is established, the acceptor asks for DataPoints, the forwarder replies to it.

type DataPointValue = ByteString Source #

type DataPointValues = [(DataPointName, Maybe DataPointValue)] Source #

data DataPointForward where Source #

Constructors

StIdle :: DataPointForward	Both acceptor and forwarder are in idle state. The acceptor can send a request for a list of `DataPoint`s (`MsgDataPointsRequest`); the forwarder is waiting for a request, it will replay with `MsgDataPointsReply`.
StBusy :: DataPointForward	The acceptor has sent a next request for `DataPoint`s. The acceptor is now waiting for a reply, and the forwarder is busy getting ready to send a reply with new list of `DataPoint`s.
StDone :: DataPointForward	Both the acceptor and forwarder are in the terminal state. They're done.

Instances

Instances details

Protocol DataPointForward Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Associated Types data Message DataPointForward st st' Source # data ClientHasAgency st Source # data ServerHasAgency st Source # data NobodyHasAgency st Source # Methods exclusionLemma_ClientAndServerHaveAgency :: forall (st :: DataPointForward). ClientHasAgency st -> ServerHasAgency st -> Void Source # exclusionLemma_NobodyAndClientHaveAgency :: forall (st :: DataPointForward). NobodyHasAgency st -> ClientHasAgency st -> Void Source # exclusionLemma_NobodyAndServerHaveAgency :: forall (st :: DataPointForward). NobodyHasAgency st -> ServerHasAgency st -> Void Source #
ShowProxy DataPointForward Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Methods showProxy :: Proxy DataPointForward -> String Source #
Show (ClientHasAgency st) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Methods showsPrec :: Int -> ClientHasAgency st -> ShowS Source # show :: ClientHasAgency st -> String Source # showList :: [ClientHasAgency st] -> ShowS Source #
Show (ServerHasAgency st) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Methods showsPrec :: Int -> ServerHasAgency st -> ShowS Source # show :: ServerHasAgency st -> String Source # showList :: [ServerHasAgency st] -> ShowS Source #
Show (Message DataPointForward from to) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Methods showsPrec :: Int -> Message DataPointForward from to -> ShowS Source # show :: Message DataPointForward from to -> String Source # showList :: [Message DataPointForward from to] -> ShowS Source #
data ClientHasAgency (st :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data ClientHasAgency (st :: DataPointForward) where TokIdle :: ClientHasAgency 'StIdle
data Message DataPointForward (from :: DataPointForward) (to :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data Message DataPointForward (from :: DataPointForward) (to :: DataPointForward) where MsgDataPointsRequest :: [DataPointName] -> Message DataPointForward 'StIdle 'StBusy MsgDataPointsReply :: DataPointValues -> Message DataPointForward 'StBusy 'StIdle MsgDone :: Message DataPointForward 'StIdle 'StDone
data NobodyHasAgency (st :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data NobodyHasAgency (st :: DataPointForward) where TokDone :: NobodyHasAgency 'StDone
data ServerHasAgency (st :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data ServerHasAgency (st :: DataPointForward) where TokBusy :: ServerHasAgency 'StBusy

data family Message ps (st :: ps) (st' :: ps) Source #

The messages for this protocol. It is expected to be a GADT that is indexed by the from and to protocol states. That is the protocol state the message transitions from, and the protocol state it transitions into. These are the edges of the protocol state transition system.

Instances

Instances details

Show (Message DataPointForward from to) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Methods showsPrec :: Int -> Message DataPointForward from to -> ShowS Source # show :: Message DataPointForward from to -> String Source # showList :: [Message DataPointForward from to] -> ShowS Source #
Show lo => Show (Message (TraceObjectForward lo) from to) Source #
Instance details Defined in Trace.Forward.Protocol.TraceObject.Type Methods showsPrec :: Int -> Message (TraceObjectForward lo) from to -> ShowS Source # show :: Message (TraceObjectForward lo) from to -> String Source # showList :: [Message (TraceObjectForward lo) from to] -> ShowS Source #
data Message DataPointForward (from :: DataPointForward) (to :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data Message DataPointForward (from :: DataPointForward) (to :: DataPointForward) where MsgDataPointsRequest :: [DataPointName] -> Message DataPointForward 'StIdle 'StBusy MsgDataPointsReply :: DataPointValues -> Message DataPointForward 'StBusy 'StIdle MsgDone :: Message DataPointForward 'StIdle 'StDone
data Message (TraceObjectForward lo) (from :: TraceObjectForward lo) (to :: TraceObjectForward lo) Source #
Instance details Defined in Trace.Forward.Protocol.TraceObject.Type data Message (TraceObjectForward lo) (from :: TraceObjectForward lo) (to :: TraceObjectForward lo) where MsgTraceObjectsRequest :: forall {k} (blocking :: StBlockingStyle) (lo :: k). TokBlockingStyle blocking -> NumberOfTraceObjects -> Message (TraceObjectForward lo) ('StIdle :: TraceObjectForward lo) ('StBusy blocking :: TraceObjectForward lo) MsgTraceObjectsReply :: forall (blocking :: StBlockingStyle) lo1. BlockingReplyList blocking lo1 -> Message (TraceObjectForward lo1) ('StBusy blocking :: TraceObjectForward lo1) ('StIdle :: TraceObjectForward lo1) MsgDone :: forall {k} (lo :: k). Message (TraceObjectForward lo) ('StIdle :: TraceObjectForward lo) ('StDone :: TraceObjectForward lo)

data family ClientHasAgency (st :: ps) Source #

Tokens for those protocol states in which the client has agency.

Instances

Instances details

Show (ClientHasAgency st) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Methods showsPrec :: Int -> ClientHasAgency st -> ShowS Source # show :: ClientHasAgency st -> String Source # showList :: [ClientHasAgency st] -> ShowS Source #
Show (ClientHasAgency st) Source #
Instance details Defined in Trace.Forward.Protocol.TraceObject.Type Methods showsPrec :: Int -> ClientHasAgency st -> ShowS Source # show :: ClientHasAgency st -> String Source # showList :: [ClientHasAgency st] -> ShowS Source #
data ClientHasAgency (st :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data ClientHasAgency (st :: DataPointForward) where TokIdle :: ClientHasAgency 'StIdle
data ClientHasAgency (st :: TraceObjectForward lo) Source #
Instance details Defined in Trace.Forward.Protocol.TraceObject.Type data ClientHasAgency (st :: TraceObjectForward lo) where TokIdle :: forall {k} {lo :: k}. ClientHasAgency ('StIdle :: TraceObjectForward lo)

data family ServerHasAgency (st :: ps) Source #

Tokens for those protocol states in which the server has agency.

Instances

Instances details

Show (ServerHasAgency st) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type Methods showsPrec :: Int -> ServerHasAgency st -> ShowS Source # show :: ServerHasAgency st -> String Source # showList :: [ServerHasAgency st] -> ShowS Source #
Show (ServerHasAgency st) Source #
Instance details Defined in Trace.Forward.Protocol.TraceObject.Type Methods showsPrec :: Int -> ServerHasAgency st -> ShowS Source # show :: ServerHasAgency st -> String Source # showList :: [ServerHasAgency st] -> ShowS Source #
data ServerHasAgency (st :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data ServerHasAgency (st :: DataPointForward) where TokBusy :: ServerHasAgency 'StBusy
data ServerHasAgency (st :: TraceObjectForward lo) Source #
Instance details Defined in Trace.Forward.Protocol.TraceObject.Type data ServerHasAgency (st :: TraceObjectForward lo) where TokBusy :: forall {k} {lo :: k} (blocking :: StBlockingStyle). TokBlockingStyle blocking -> ServerHasAgency ('StBusy blocking :: TraceObjectForward lo)

data family NobodyHasAgency (st :: ps) Source #

Tokens for terminal protocol states in which neither the client nor server has agency.

Instances

Instances details

data NobodyHasAgency (st :: DataPointForward) Source #
Instance details Defined in Trace.Forward.Protocol.DataPoint.Type data NobodyHasAgency (st :: DataPointForward) where TokDone :: NobodyHasAgency 'StDone
data NobodyHasAgency (st :: TraceObjectForward lo) Source #
Instance details Defined in Trace.Forward.Protocol.TraceObject.Type data NobodyHasAgency (st :: TraceObjectForward lo) where TokDone :: forall {k} {lo :: k}. NobodyHasAgency ('StDone :: TraceObjectForward lo)