staload "sessions.sats"
staload UN = "prelude/SATS/unsafe.sats"
#define C 1
#define S 0
stadef fp (a:t@ype) = lam (p:int->protocol):int->protocol => lam n => pite (n>0, pbrch(C, pmsg(C,a)::p(n+1), pmsg(S,a)::p(n-1)), pmsg(C,a)::p(n+1))
stadef queue (a:t@ype) = pfix2 (fp a)
extern fun empty {a:t@ype} (): chan(C, (queue a) 0)
extern fun elem {a:t@ype} {n:nat} (chan(C, (queue a) n), a): chan(C, (queue a) (n+1))
implement empty {a} () = let
fun server (out: chan(S, (queue a) 0)): void = let
val _ = recurse2 {S} {lam (p:int->protocol):int->protocol => lam n => pite (n>0, pbrch(C, pmsg(C,a)::p(n+1), pmsg(S,a)::p(n-1)), pmsg(C,a)::p(n+1))} {0} out
val _ = ite_false out
val x = recv out
val tail = empty {a} ()
val q = elem {a} {0} (tail, x)
in
cut (q, out)
end
in
create (llam out => server out)
end
implement main0 () = () where {
val queue = empty {int} ()
val _ = recurse2 {C} {fp int} {0} queue
val _ = ite_false queue
val _ = send (queue, 1)
// This line works
val _ = recurse2 {C} {fp int} {0+1} queue
// But this equivalent line doesn't
// val _ = recurse2 {C} {fp int} {1} queue
// The constraint is as follows,
// eqeq:
// app(app(pfix2; lam(p; lam(n; app(pite; app(>; var(n), 0), app(pbrch; 1, app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))), app(pseq; app(pmsg; 0, int), app(var(p); app(-; var(n), 1)))), app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))))))); app(+; 0, 1));
// app(app(pfix2; lam(p; lam(n; app(pite; app(>; var(n), 0), app(pbrch; 1, app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))), app(pseq; app(pmsg; 0, int), app(var(p); app(-; var(n), 1)))), app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))))))); 1)))
//
// it is saying "0+1 == 1" can not be verified. However, it is obviously true.
val _ = $UN.cast2void queue
}
////
implement elem {a} (inp, x) = let
fun server (out: chan(S,queue(a)), inp: chan(C,queue(a))): void = let
val _ = recurse out
val c = offer out
in
case+ c of
| ~Left() =>
let
val y = recv out
val _ = recurse inp
val _ = choose (inp, Left())
val _ = send (inp, y)
in
server (out, inp)
end
| ~Right() =>
let
val _ = choose (out, Right())
val _ = send (out, x)
in
cut (out, inp)
end
end
in
create (llam out => server (out, inp))
end
#define ATS_EXTERN_PREFIX "libsession_"
sortdef role = {a:int|a==0||a==1}
datasort protocol =
| pmsg of (int, vt@ype)
| prpt of (int, protocol)
| pbrch of (int, protocol, protocol)
| pend of (int)
| pseq of (protocol, protocol)
| pquan of (int, int -> protocol)
| pquan2 of (int, int -> protocol, int -> bool)
| pfix of (protocol -> protocol)
| pite of (bool, protocol, protocol)
stacst pfix2: ((int -> protocol) -> (int -> protocol)) -> (int -> protocol)
stacst pfix3: (((int,int)->protocol) -> ((int,int)->protocol)) -> ((int,int) -> protocol)
#define :: pseq
absvtype chan (int, protocol)
fun create {r:role} {p:protocol} (chan (1-r, p) -<lincloptr1> void): chan (r, p)
fun send {r:role} {p:protocol} {a:vt@ype} (!chan (r, pmsg(r,a) :: p) >> chan (r, p), a): void
fun recv {r:role} {p:protocol} {a:vt@ype} (!chan (r, pmsg(1-r,a) :: p) >> chan (r, p)): a
fun close {r:role} {p:protocol} (chan (r, pend r)): void
fun wait {r:role} {p:protocol} (chan (r, pend (1-r))): void
fun ite_true {r:role} {pt,pf:protocol} (!chan(r, pite (true, pt, pf)) >> chan(r, pt)): void
fun ite_false {r:role} {pt,pf:protocol} (!chan(r, pite (false, pt, pf)) >> chan (r, pf)): void
datavtype choice (protocol, p:protocol, q:protocol) =
| Left (p, p, q) of ()
| Right (q, p, q) of ()
fun offer {r:role} {p1,p2:protocol} (!chan (r, pbrch(1-r,p1,p2)) >> chan (r, p)): #[p:protocol] choice (p, p1, p2)
fun choose {r:role} {p,p1,p2:protocol} (!chan (r, pbrch(r,p1,p2)) >> chan (r, p), choice (p, p1, p2)): void
fun unroll1 {r:role} {p1,p2:protocol} {n:int|n>0} (!chan (r, prpt(n,p1) :: p2) >> chan (r, p1 :: prpt(n-1,p1) :: p2)): void
fun unroll0 {r:role} {p1,p2:protocol} (!chan (r, prpt(0,p1) :: p2) >> chan (r, p2)): void
fun unify {r:role} {fp:int->protocol} (!chan (r, pquan (r, fp)) >> {n:int} chan (r, fp(n))): void
fun exify {r:role} {fp:int->protocol} (!chan (r, pquan (1-r, fp)) >> [n:int] chan (r, fp(n))): void
fun unify2 {r:role} {fp:int->protocol} {guard:int->bool} (!chan (r, pquan2 (r, fp, guard)) >> {n:int|guard(n)} chan (r, fp(n))): void
fun exify2 {r:role} {fp:int->protocol} {guard:int->bool} (!chan (r, pquan2 (1-r, fp, guard)) >> [n:int|guard(n)] chan (r, fp(n))): void
fun recurse {r:role} {p:protocol} {fp:protocol->protocol} (!chan (r, pfix (fp)) >> chan (r, fp (pfix (fp)))): void
fun recurse2 {r:role} {fp:(int->protocol)->(int->protocol)} {n:int} (!chan (r, (pfix2 fp) n) >> chan(r, (fp (pfix2 fp)) n)): void
fun recurse3 {r:role} {fp:((int,int)->protocol)->((int,int)->protocol)} {m,n:int} (!chan(r, (pfix3 fp)(n,m)) >> chan(r, (fp(pfix3 fp))(n,m))): void
fun cut {r:role} {p:protocol} (chan (r,p), chan (1-r,p)): void
