| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Network.TypedProtocol.Stateful.Proofs
Description
Proofs about the typed protocol framework.
It also provides helpful testing utilities.
Synopsis
- connect :: forall ps (pr :: PeerRole) (st :: ps) f m a b. (MonadSTM m, SingI pr) => f st -> Peer ps pr st f m a -> Peer ps (FlipAgency pr) st f m b -> m (a, b, TerminalStates ps)
- data TerminalStates ps where
- TerminalStates :: forall ps (st :: ps). StateAgency st ~ 'NobodyAgency => StateToken st -> StateToken st -> TerminalStates ps
- removeState :: forall (m :: Type -> Type) ps f (st :: ps) (pr :: PeerRole) a. Functor m => f st -> Peer ps pr st f m a -> Peer ps pr 'NonPipelined st m a
Documentation
connect :: forall ps (pr :: PeerRole) (st :: ps) f m a b. (MonadSTM m, SingI pr) => f st -> Peer ps pr st f m a -> Peer ps (FlipAgency pr) st f m b -> m (a, b, TerminalStates ps) Source #
data TerminalStates ps where #
The terminal states for the protocol. Used in connect and
connectPipelined to return the states in which the peers terminated.
Constructors
| TerminalStates | |
Fields
| |
removeState :: forall (m :: Type -> Type) ps f (st :: ps) (pr :: PeerRole) a. Functor m => f st -> Peer ps pr st f m a -> Peer ps pr 'NonPipelined st m a Source #
Remove state for non-pipelined peers.
TODO: There's a difficulty to write removeState for pipelined peers which
is type safe. The Peer doesn't track all pipelined transitions, just the
depth of pipelining, so we cannot push `f st` to a queue which type is
linked to Peer. For a similar reason there's no way to write
forgetPipelined function.
However, this is possible if Peer tracks all transitions.