lambda-uc-0.1.0.0
Safe HaskellSafe
LanguageGHC2021

LambdaUC.UC.Core

Synopsis

Documentation

type HListPort x y = HListPair '[] '[x] :> HListPair '[] '[y] #

type OnlySendPort a = HListPort a Void #

type OnlyRecvPort a = HListPort Void a #

type PingSendPort = OnlySendPort () #

type PingRecvPort = OnlyRecvPort () #

type Pid = String #

knownHPPortsAppendPid :: KnownHPPortsD down -> KnownHPPortsD (MapConcat2 '[] '[Pid] down) #

mapConcatCompL :: forall l r ports. KnownHPPortsD ports -> MapConcat2 l '[] (MapConcat2 '[] r ports) :~: MapConcat2 l r ports #

mapConcatId :: KnownHPPortsD ports -> MapConcat2 '[] '[] ports :~: ports #

type NoInitExec ports = ExecBuilder ExecIndexInit (ExecIndexSome ports InitAbsent) () #

type NoInitProc ports = AsyncT ports NextRecv NextRecv Void #

type UcExec l r adv up down = NoInitExec (UcProcessPorts l r adv up down) #

An interactive algorithm with that we use for defining ideal functionalities and protocols.

Has the following interfaces.

  • up interface to its callers,
  • down interfaces to its subroutines,
  • a single PingSendPort interface to yield control to the environment.

type UcProc l r adv up down = NoInitProc (UcProcessPorts l r adv up down) #

type UcProcessPorts l r adv up down = Concat2 l r PingSendPort : (PortDual adv : MapConcat2 l r (PortDual up : down)) #

type MultSidIdeal rest sid adv up down = UcExec (sid : rest) '[Pid] (Concat2 (sid : rest) '[] adv) up down #

A UcExec where up and down interfaces are appropriately marked with ESID and PID values to handle multiple sessions in one process.

This is used by multiSidIdealShell to implement multiple sessions of SingleSidIdeal inside.

type MultSidReal rest sid adv up down = HListPair '[] '[Pid] -> UcExec (sid : rest) '[] (Concat2 (sid : rest) '[] adv) up down #

A UcExec that implements a single process in a real (multi-session) protocol.

type SingleSidIdeal sid adv up down = HListPair '[sid] '[] -> UcExec '[] '[Pid] (Concat2 '[] '[] adv) up down #

A UcExec that implements a single session. The interface it provides to its caller is maked only with PID values.

Use this with multiSidIdealShell to get a multi-session extension.

type SingleSidReal sid adv up down = HListPair '[sid] '[Pid] -> UcExec '[] '[] (Concat2 '[] '[] adv) up down #

A UcExec that implements a single process in a real (single-session) protocol.