Moduletyped-protocols-1.2.2.0

Network.TypedProtocol.Peer

8 types
2 values

Packagetyped-protocols-1.2.2.0
Exports14
LicenceApache-2.0

valuenatToInt :: Nat n -> Int

valueunsafeIntToNat :: Int -> Nat n

datadata N

Constructors

Z
S N

newtypenewtype Nat (n :: N)

Instances1Show

Show (Nat n)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core

patternpattern Succ :: () => m ~ 'S n => Nat n -> Nat m

patternpattern Zero :: () => 'Z ~ n => Nat n

familytype family Outstanding (pl :: IsPipelined ps) :: N where

Equations

familytype family OutstandingSenders (pl :: IsPipelined ps) :: N where

Equations

OutstandingSenders 'NonPipelined = 'Z
OutstandingSenders ('Pipelined _1 _2) = 'Z
OutstandingSenders ('Lookahead n _1) = n

datadata Peer ps (pr :: PeerRole) (pl :: IsPipelined ps) (st :: ps) (m :: Type -> Type) a where

Constructors

Effect :: m (Peer ps pr pl st m a) -> Peer ps pr pl st m a
Yield :: (StateTokenI st, StateTokenI st', ActiveState st, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => WeHaveAgencyProof pr st -> Message ps st st' -> Peer ps pr pl st' m a -> Peer ps pr pl st m a
Await :: (StateTokenI st, ActiveState st, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => TheyHaveAgencyProof pr st -> (forall (st' :: ps). Message ps st st' -> Peer ps pr pl st' m a) -> Peer ps pr pl st m a
Done :: (StateTokenI st, StateAgency st ~ 'NobodyAgency, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => NobodyHasAgencyProof pr st -> a -> Peer ps pr pl st m a
YieldPipelined :: (StateTokenI st, StateTokenI st', ActiveState st) => WeHaveAgencyProof pr st -> Message ps st st' -> Receiver ps pr st' st'' m c -> Peer ps pr ('Pipelined ('S n) c) st'' m a -> Peer ps pr ('Pipelined n c) st m a
Collect :: (StateTokenI st, ActiveState st) => Maybe (Peer ps pr ('Pipelined ('S n) c) st m a) -> (c -> Peer ps pr ('Pipelined n c) st m a) -> Peer ps pr ('Pipelined ('S n) c) st m a
AwaitLookahead :: (StateTokenI st, StateTokenI st', ActiveState st, ActiveState st') => TheyHaveAgencyProof pr st' -> Sender ps pr sv st st' m -> (forall (st'' :: ps). Message ps st' st'' -> Peer ps pr ('Lookahead ('S n) sv) st'' m a) -> Peer ps pr ('Lookahead n sv) st m a
FlushSender :: StateTokenI st => Maybe (Peer ps pr ('Lookahead ('S n) sv) st m a) -> Peer ps pr ('Lookahead n sv) st m a -> Peer ps pr ('Lookahead ('S n) sv) st m a

Instances1Functor

Functor m => Functor (Peer ps pr pl st m)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Peer

datadata PeerLookahead ps (pr :: PeerRole) (st :: ps) (m :: Type -> Type) a where

Constructors

PeerLookahead :: Peer ps pr ('Lookahead 'Z 'VariableSender) st m a -> PeerLookahead ps pr st m a
- runPeerLookahead :: Peer ps pr ('Lookahead 'Z 'VariableSender) st m a

Instances1Functor

Functor m => Functor (PeerLookahead ps pr st m)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Peer

datadata PeerLookaheadFixedSender ps (pr :: PeerRole) (st :: ps) (m :: Type -> Type) a where

Constructors

PeerLookaheadFixedSender :: Sender ps pr 'VariableSender apst apst' m -> Peer ps pr ('Lookahead 'Z ('FixedSender apst apst')) st m a -> PeerLookaheadFixedSender ps pr st m a

Instances1Functor

Functor m => Functor (PeerLookaheadFixedSender ps pr st m)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Peer

datadata PeerPipelined ps (pr :: PeerRole) (st :: ps) (m :: Type -> Type) a where

Constructors

PeerPipelined :: Peer ps pr ('Pipelined 'Z c) st m a -> PeerPipelined ps pr st m a
- runPeerPipelined :: Peer ps pr ('Pipelined 'Z c) st m a

Instances1Functor

Functor m => Functor (PeerPipelined ps pr st m)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Peer

datadata Receiver ps (pr :: PeerRole) (st :: ps) (stdone :: ps) (m :: Type -> Type) c where

Constructors

ReceiverEffect :: m (Receiver ps pr st stdone m c) -> Receiver ps pr st stdone m c
ReceiverDone :: c -> Receiver ps pr st st m c
ReceiverAwait :: (StateTokenI st, ActiveState st) => TheyHaveAgencyProof pr st -> (forall (st' :: ps). Message ps st st' -> Receiver ps pr st' stdone m c) -> Receiver ps pr st stdone m c

Instances1Functor

Functor m => Functor (Receiver ps pr st stdone m)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Peer

datadata Sender ps (pr :: PeerRole) (sv :: SenderVariability ps) (st :: ps) (stdone :: ps) (m :: Type -> Type) where

Constructors

TheSender :: Sender ps pr ('FixedSender st stdone) st stdone m
SenderEffect :: m (Sender ps pr 'VariableSender st stdone m) -> Sender ps pr 'VariableSender st stdone m
SenderDone :: Sender ps pr 'VariableSender st st m
SenderYield :: (StateTokenI st, StateTokenI st', ActiveState st) => !WeHaveAgencyProof pr st -> Message ps st st' -> Sender ps pr 'VariableSender st' stdone m -> Sender ps pr 'VariableSender st stdone m