staload "sessions.sats"
stadef proto = pquan2(0, lam (s:stype):stype => pmsg(1, chan(1,s)) :: s)
stadef subproto = pmsg(0, string) :: pend(0)
extern fun server (!chan(0,proto) >> chan(0,s)): #[s:stype] chan(1,s)
extern fun client (chan(1,proto)): void
implement server (ch) = let
prval _ = exify2 ch
val ch2 = recv ch
in
ch2
end
implement client (ch1) = let
val ch2 = create {1,0} {subproto} (llam ch2 => (send (ch2, "hello"); close ch2))
prval _ = unify2 ch1
val _ = send {1,1} (ch1, ch2)
val str = recv ch1
val _ = println! str
in
wait ch1
end
extern fun test (): void
implement test () = let
val ch = create {1,0} {proto} (llam ch1 => let val ch2 = server ch1 in cut (ch1, ch2) end)
in
client (ch)
end
//#define ATS_PACKNAME "libsession"
#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)
(* 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#%"
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 ite_true {r:role} {pt,pf:stype} (!chan(r, pite(true,pt,pf)) >> chan(r,pt)): void
prfun ite_false {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))): void
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
fun cut {r1,r2:role} {p:stype} {r1 != r2} (chan(r1,p), chan(r2,p)): void = "mac#%"
//fun wait {r,r0:role} {p:stype} {r0 != r} (chan(r, pend r0)): void
//stacst pfix3: (((int,int)->stype) -> ((int,int)->stype)) -> ((int,int) -> stype)
//fun recurse3 {r:role} {fp:((int,int)->stype)->((int,int)->stype)} {m,n:int} (!chan(r, (pfix3 fp)(n,m)) >> chan(r, (fp(pfix3 fp))(n,m))): void
//fun unify2 {r:role} {fp:int->stype} {guard:int->bool} (!chan (r, pquan2 (r, fp, guard)) >> {n:int|guard(n)} chan (r, fp(n))): void
//fun exify2 {r:role} {fp:int->stype} {guard:int->bool} (!chan (r, pquan2 (1-r, fp, guard)) >> [n:int|guard(n)] chan (r, fp(n))): void
