staload "./libsession.sats"
stadef proto_eq = pmsg(1,int)::pmsg(1,int)::pmsg(0,bool)::pend(1)
stadef proto_eq_dep = pquan(1,lam (n:int) => pquan(1,lam (m:int) => pmsg(1,int n)::pmsg(1, int m)::pmsg(0, bool (m==n))::pend(1)))
extern fun eq_cli (session(1,proto_eq)): void
extern fun eq_srv (session(0,proto_eq)): void
implement eq_cli (session) = let
val _ = session_send (session, 1)
val _ = session_send (session, 2)
val result = session_recv (session)
val _ = println! result
in
session_close (session)
end
implement eq_srv (session) = let
val a = session_recv (session)
val b = session_recv (session)
val _ = session_send (session, a = b)
in
session_wait (session)
end
extern fun eq_dep_cli (session(1,proto_eq_dep)): void
extern fun eq_dep_srv (session(0,proto_eq_dep)): void
implement eq_dep_cli (session) = let
val session = session_unify (session)
val session = session_unify (session)
val a = 1
val b = 2
val _ = session_send (session, a)
val _ = session_send (session, b)
val result = session_recv (session)
in
session_close (session)
end
implement eq_dep_srv (session) = let
val session = session_exify (session)
val session = session_exify (session)
val a = session_recv (session)
val b = session_recv (session)
val _ = session_send (session, ~(a != b))
in
session_wait (session)
end
sortdef role = int
(* session types *)
datasort stype =
| pend of (role)
| pmsg of (role, vt@ype)
| pseq of (stype, stype)
| pmult of (role, stype, stype)
| paddi of (role, stype, stype)
| pquan of (role, int -> stype)
stadef :: = pseq
absvtype session (role, stype) = ptr
(* session api *)
fun {} session_create
{r1,r2:role|r1 != r2} {s:stype}
(int r1, session(r2,s) -<lincloptr1> void): session (r1,s)
fun {} session_send
{self,from:role|self == from} {s:stype} {a:vt@ype}
(!session(self,pmsg(from,a)::s) >> session(self,s), a): void
fun {} session_recv
{self,from:role|self != from} {s:stype} {a:vt@ype}
(!session(self,pmsg(from,a)::s) >> session(self,s)): a
fun {} session_close
{self,r:role|self == r}
(session(self,pend(r))): void
fun {} session_wait
{self,r:role|self != r}
(session(self,pend(r))): void
castfn session_exify
{self,r:role|self != r} {fp:int->stype}
(session(self,pquan(r,fp))): [n:int] session(self,fp(n))
castfn session_unify
{self,r:role|self == r} {fp:int->stype}
(session(self,pquan(r,fp))): {n:int} session(self,fp(n))
(* session combinators *)
fun {} session_mconj
{self,r:role|self == r} {s1,s2:stype}
(session(self,pmult(r,s1,s2))): @(session(self,s1), session(self,s2))
fun {} session_mdisj
{self,r:role|self != r} {s1,s2:stype}
(session(self,pmult(r,s1,s2)), session(self,s1) -<lincloptr1> void, session(self,s2) -<lincloptr1> void): void
datavtype choice (stype, p:stype, q:stype) =
| Left (p, p, q) of ()
| Right (q, p, q) of ()
fun {} session_aconj
{self,r:role|self == r} {s,s1,s2:stype}
(!session(self,paddi(r,s1,s2)) >> session(self,s), choice(s,s1,s2)): void
fun {} session_adisj
{self,r:role|self != r} {s1,s2:stype}
(!session(self,paddi(r,s1,s2)) >> session(self,s)): #[s:stype] choice (s,s1,s2)
fun {} session_cut
{r1,r2:role|r1 != r2} {s:stype}
(session(r1,s), session(r2,s)): void
all: main.tc
%.tc: %.dats
patsopt -tc -d $<
