Network.TypedProtocol.Peer.Server · typed-protocols-1.2.2.0

pattern

pattern Await :: () => (StateTokenI st, StateAgency st ~ 'ClientAgency, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => (forall (st' :: ps). Message ps st st' -> Server ps pl st' m a) -> Server ps pl st m a

#

pattern

pattern AwaitLookahead :: () => (StateTokenI st, StateTokenI st', ActiveState st, StateAgency st' ~ 'ClientAgency) => Sender ps sv st st' m -> (forall (st'' :: ps). Message ps st' st'' -> Server ps ('Lookahead ('S n) sv) st'' m a) -> Server ps ('Lookahead n sv) st m a

#

pattern

pattern Collect :: () => (StateTokenI st, ActiveState st) => Maybe (Server ps ('Pipelined ('S n) c) st m a) -> (c -> Server ps ('Pipelined n c) st m a) -> Server ps ('Pipelined ('S n) c) st m a

#

pattern

pattern Done :: () => (StateTokenI st, StateAgency st ~ 'NobodyAgency, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => a -> Server ps pl st m a

#

patternpattern Effect :: m (Server ps pl st m a) -> Server ps pl st m a

#

pattern

pattern FlushSender :: () => StateTokenI st => Maybe (Server ps ('Lookahead ('S n) sv) st m a) -> Server ps ('Lookahead n sv) st m a -> Server ps ('Lookahead ('S n) sv) st m a

#

pattern

pattern ReceiverAwait :: () => (StateTokenI st, ActiveState st, StateAgency st ~ 'ClientAgency) => (forall (st' :: ps). Message ps st st' -> Receiver ps st' stdone m c) -> Receiver ps st stdone m c

#

patternpattern ReceiverDone :: c -> Receiver ps stdone stdone m c

#

patternpattern ReceiverEffect :: m (Receiver ps st stdone m c) -> Receiver ps st stdone m c

#

patternpattern SenderDone :: Sender ps 'VariableSender stdone stdone m

#

patternpattern SenderEffect :: m (Sender ps 'VariableSender st stdone m) -> Sender ps 'VariableSender st stdone m

#

pattern

pattern SenderYield :: () => (StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency) => Message ps st st' -> Sender ps 'VariableSender st' stdone m -> Sender ps 'VariableSender st stdone m

#

pattern

pattern ServerLookaheadFixedSender :: Sender ps 'VariableSender apst apst' m -> Server ps ('Lookahead 'Z ('FixedSender apst apst')) st m a -> ServerLookaheadFixedSender ps st m a

#

patternpattern TheSender :: () => sv ~ 'FixedSender st stdone => Sender ps sv st stdone m

#

pattern

pattern Yield :: () => (StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => Message ps st st' -> Server ps pl st' m a -> Server ps pl st m a

#

pattern

pattern YieldPipelined :: () => (StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency) => Message ps st st' -> Receiver ps st' st'' m c -> Server ps ('Pipelined ('S n) c) st'' m a -> Server ps ('Pipelined n c) st m a

#

datadata IsPipelined ps where

#

Constructors

Pipelined :: N -> Type -> IsPipelined ps
NonPipelined :: IsPipelined ps
Lookahead :: N -> SenderVariability ps -> IsPipelined ps

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 SenderVariability ps where

#

Constructors

VariableSender :: SenderVariability ps
FixedSender :: ps -> ps -> SenderVariability ps

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

#

Instances1Functor

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

patternpattern ServerLookahead :: Server ps ('Lookahead 'Z 'VariableSender) st m a -> ServerLookahead ps st m a

#

valuerunServerLookahead

:: ServerLookahead ps st m a
-> Server ps ('Lookahead 'Z 'VariableSender) st m a

#

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

#

Instances1Functor

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

patternpattern ServerPipelined :: Server ps ('Pipelined 'Z c) st m a -> ServerPipelined ps st m a

#

valuerunServerPipelined :: ()

#

typetype Receiver ps (st :: ps) (stdone :: ps) (m :: Type -> Type) c = Receiver ps 'AsServer st stdone m c

#

type

type Sender ps (sv :: SenderVariability ps) (st :: ps) (stdone :: ps) (m :: Type -> Type) = Sender ps 'AsServer sv st stdone m

#

typetype Server ps (pl :: IsPipelined ps) (st :: ps) (m :: Type -> Type) a = Peer ps 'AsServer pl st m a

#

typetype ServerLookahead ps (st :: ps) (m :: Type -> Type) a = PeerLookahead ps 'AsServer st m a

#

typetype ServerLookaheadFixedSender ps (st :: ps) (m :: Type -> Type) a = PeerLookaheadFixedSender ps 'AsServer st m a

#

typetype ServerPipelined ps (st :: ps) (m :: Type -> Type) a = PeerPipelined ps 'AsServer st m a

#