% An interpreter for the *, 1, + fragment of SILL
%
% 15-816 Substructural Logics, Fall 2016
% Written jointly in lecture, following ideas by Schuermann
%
% This is a synchronous semantics
% For the asynchronous semantics, see session-async.sill

tp : type.
tensor : tp -> tp -> tp.
one : tp.
plus : tp -> tp -> tp.

ch : tp -> type.
exp : tp -> type.

fwd_ : ch A -o exp A.
spawn_ : exp A -o (ch A -o exp C) -o exp C.

send_ : ch A -o exp B -o exp (tensor A B).
recv : ch (tensor A B) -o (ch A -o ch B -o exp C) -o exp C.

close_ : exp one.
wait : ch one -o exp C -o exp C.

select1_ : exp A -o exp (plus A B).
select2_ : exp B -o exp (plus A B).
case : ch (plus A B) -o (ch A -o exp C) & (ch B -o exp C) -o exp C.

proc : exp A -> ch A -> type.

c/fwd : proc P D * proc (fwd_ D) C
        -o { proc P C }.
c/spawn : proc (spawn_ P (\x. Q x)) C
        -o { Exists a. proc P a * proc (Q a) C }.

c/tensor : proc (send_ W P) C * proc (recv C (\x. \c'. Q x c')) D
        -o { Exists c'. proc P c' * proc (Q W c') D }.
c/one : proc (close_) C * proc (wait C Q) D
        -o { proc Q D }.

c/plus1 : proc (select1_ P) C * proc (case C <(\c'. Q1 c'),(\c'. Q2 c')>) D
         -o { Exists c'. proc P c' * proc (Q1 c') D }.
c/plus2 : proc (select2_ P) C * proc (case C <(\c'. Q1 c'),(\c'. Q2 c')>) D
         -o { Exists c'. proc P c' * proc (Q2 c') D }.

#query * 1 * 1
Pi c0. proc (spawn_ (close_) (\c1. wait c1 (close_))) c0 -o {proc P c0}.

#query * 1 * 1
Pi c0. proc (spawn_ (select2_ close_)
            (\c1. case c1 <(\c2. wait c2 (select2_ close_)) ,
                           (\c3. wait c3 (select1_ close_))>)) c0
-o { proc P c0 }.