staload "./session.sats"
#define S 0
#define C 1
// for all session type x, given an unlimited function for session x,
// return a service using that function x
// comes from behavior polymorphims from Frank Pfenning's group
stadef cloud = pquan2(C, lam (x:stype):stype => pmsg(C, chan(S,x)->void) :: prep(C,x))
extern fun cloudserver (chan (S, cloud)): void
implement cloudserver (ch) = let
prval [x:stype] ch = exify2 ch
val f = recv {S,C} {prep(C,x)} {chan(S,x)->void} ch
prval _ = service ch
fun loop {x:stype} (ch:chan(S,pfix(lam s=>pbrch(C,pmsg(1-1,chan(C,x))::s,pend(C)))), f:chan(S,x)->void): void = let
prval _ = recurse ch
val choice = offer ch
in
case+ choice of
| ~Right() => wait ch
| ~Left() =>
let
val ep = create {C,S} {x} (llam ch => f ch)
val _ = send (ch, ep)
in
loop {x} (ch, f)
end
end
in
loop {x} (ch, f)
end
stadef sub = pmsg(C,string)::pend(C)
extern fun client (chan(C, cloud)): void
implement client (ch) = let
fun echo (c:chan(S,sub)): void = (println!(recv c); wait c)
prval _ = unify2 ch
val _ = send (ch, echo)
prval _ = service ch
fun loop (ch:chan(C,pfix(lam s=>pbrch(C,pmsg(1-1,chan(C,sub))::s,pend(C)))), n:int): void = let
prval _ = recurse ch
in
if n <= 0
then (choose(ch,Right()); close ch)
else
let
val _ = choose(ch,Left())
val ep = recv ch
val _ = send (ep, "hello")
val _ = close ep
in
loop (ch, n-1)
end
end
in
loop (ch, 10)
end
extern fun test (): void
implement test () = let
val ch = create {C,S} {cloud} (llam ch => cloudserver ch)
in
client ch
end
#define ATS_EXTERN_PREFIX "libsession__"
sortdef role = {a:int|a==0||a==1}
datasort stype =
| pmsg of (int, vt@ype) (* used with pseq for syntax brevity *)
| pseq of (stype, stype)
| pbrch of (int, stype, stype)
| pend of (int)
| pquan of (int, int -> stype)
| pquan2 of (int, stype -> stype)
| pfix of (stype -> stype)
| pite of (bool, stype, stype)
| pfix2 of ((int -> stype) -> (int -> stype), int)
| prep of (int, stype)
(* used for syntax brevity *)
#define :: pseq
(* channel *)
absvtype chan (int, stype) = ptr
fun create {r1,r2:role} {p:stype} {r1 != r2} (chan(r2,p) -<lincloptr1> void): chan(r1,p) = "mac#%"
fun send {r,r0:role} {p:stype} {a:vt@ype} {r0 == r} (!chan(r, pmsg(r0,a)::p) >> chan(r,p), a): void = "mac#%"
fun recv {r,r0:role} {p:stype} {a:vt@ype} {r0 != r} (!chan(r, pmsg(r0,a)::p) >> chan(r,p)): a = "mac#%"
fun close {r,r0:role} {p:stype} {r0 == r} (chan(r, pend r0)): void = "mac#%"
fun wait {r,r0:role} {p:stype} {r0 != r} (chan(r, pend r0)): void = "mac#%"
fun cut {r1,r2:role} {p:stype} {r1 != r2} (chan(r1,p), chan(r2,p)): void = "mac#%"
prfun service {r,r0:role} {p:stype} (!chan(r,prep(r0,p)) >> chan(r,pfix(lam s=>pbrch(r0,pmsg(1-r0,chan(r0,p))::s,pend(r0))))): void
//prfun request {r,r0:role} {p:stype} {r == r0} (!chan(r,prep(r0,p)) >> chan(r,pfix(lam s=>pbrch(r0,pmsg(1-r,chan(r0,p))::s,pend(r0))))): void
//prfun accept {r,r0:role} {p:stype} {r != r0} (!chan(r,prep(r0,p)) >> chan(r,pfix(lam s=>pbrch(r0,pmsg(r,chan(r0,p))::s,pend(r0))))): void
datavtype choice (stype, p:stype, q:stype) =
| Left (p, p, q) of ()
| Right (q, p, q) of ()
fun offer {r,r0:role} {p1,p2:stype} {r0 != r} (!chan(r, pbrch(r0,p1,p2)) >> chan(r,p)): #[p:stype] choice(p,p1,p2) = "mac#%"
fun choose {r,r0:role} {p,p1,p2:stype} {r0 == r} (!chan(r, pbrch(r0,p1,p2)) >> chan(r,p), choice(p,p1,p2)): void = "mac#%"
prfun itet {r:role} {pt,pf:stype} (!chan(r, pite(true,pt,pf)) >> chan(r,pt)): void
prfun itef {r:role} {pt,pf:stype} (!chan(r, pite(false,pt,pf)) >> chan(r,pf)): void
prfun exify {r,r0:role} {fp:int->stype} {r0 != r} (!chan(r, pquan(r0,fp)) >> [n:int] chan (r,fp(n))): void
prfun unify {r,r0:role} {fp:int->stype} {r0 == r} (!chan(r, pquan(r0,fp)) >> {n:int} chan (r,fp(n))): void
prfun exify2 {r,r0:role} {fp:stype->stype} {r0 != r} (chan(r, pquan2(r0,fp))): [s:stype] chan (r,fp(s))
prfun unify2 {r,r0:role} {fp:stype->stype} {r0 == r} (!chan(r, pquan2(r0,fp)) >> {s:stype} chan (r,fp(s))): void
prfun recurse {r:role} {p:stype} {fp:stype->stype} (!chan (r, pfix(fp)) >> chan (r, fp(pfix(fp)))): void
prfun recurse2 {r:role} {fp:(int->stype)->(int->stype)} {n:int} (!chan (r, pfix2(fp,n)) >> chan(r, fp(lam n=>pfix2(fp,n))(n))): void
