(* protocol *)
sortdef protocol = type
(* binary role *)
sortdef role = {n:int|n==0||n==1}
(* atomics *)
stacst msg: (int, vt@ype) -> protocol
stacst nil: int -> protocol
stacst seq: (protocol, protocol) -> protocol
#define :: seq
(* connectives *)
stacst addi: (int, protocol, protocol) -> protocol // additives: oplus, amp
stacst mult: (int, protocol, protocol) -> protocol // multiplicatives: tensor, parr
(* type constructor *)
absvtype chan (int, protocol)
(* axiom *)
fun create {r:role} {p:protocol} (chan(1-r,p) -<lincloptr1> void): chan(r,p)
(* atomics *)
fun send {r:role} {p:protocol} {v:vt@ype} (!chan(r,msg(r,v)::p) >> chan(r,p), v): void
fun recv {r:role} {p:protocol} {v:vt@ype} (!chan(r,msg(1-r,v)::p) >> chan(r,p)): v
fun wait {r:role} (chan(r,nil(1-r))): void
fun close {r:role} (chan(r,nil r)): void
(* additive connectives *)
datavtype choice (protocol, p:protocol, q:protocol) =
| Left (p,p,q)
| Right (q,p,q)
fun amp {r:role} {p,q:protocol} (!chan(r,addi(1-r,p,q)) >> chan(r,s)): #[s:protocol] choice (s,p,q)
fun oplus {r:role} {p,q,s:protocol} (!chan(r,addi(r,p,q)) >> chan(r,s), choice (s,p,q)): void
(* multiplicative connectives *)
fun tensor {r:role} {p,q:protocol} (chan(r,mult(r,p,q)), chan(r,p) -<lincloptr1> void, chan(r,q) -<lincloptr1> void): void
fun parr {r:role} {p,q:protocol} (chan(r,mult(1-r,p,q))): @(chan(r,p), chan(r,q))
(* cut *)
fun cut {r:role} {p:protocol} (chan(r,p), chan(1-r,p)): void
staload "session.sats"
staload UN = "prelude/SATS/unsafe.sats"
(* these functions will be a mediator thread that also adds a tag/flag to distinguish the multiplexing of channel *)
extern fun cutmult {r:role} {p,q:protocol} (chan(r,mult(r,p,q)), chan(1-r,p), chan(1-r,q)): void
extern fun cutparr1 {r:role} {p,q:protocol} (chan(r,mult(1-r,p,q)), chan(1-r,p)): void
extern fun cutparr2 {r:role} {p,q:protocol} (chan(r,mult(1-r,p,q)), chan(1-r,q)): void
implement tensor {r} {p,q} (chan, fp, fq) = let
val pclient = create {1-r} (fp)
val qclient = create {1-r} (fq)
in
cutmult (chan, pclient, qclient)
end
implement parr {r} {p,q} (chan) = let
val copy = $UN.castvwtp1{chan(r,mult(1-r,p,q))} chan
val pclient = create {r} (llam pserver => cutparr1 {r}{p,q} (chan, pserver))
val qclient = create {r} (llam qserver => cutparr2 {r}{p,q} (copy, qserver))
in
@(pclient, qclient)
end
