% Session-typed concurrency (SILL)
% Based on Carsten Schuermann's arbiter.clf
% Synchronous version
%
% 15-816 Substructural Logics, Fall 2016
% Completed the in-class version with the negative types

tp : type.
tensor : tp -> tp -> tp.
lolli : tp -> tp -> tp.
one : tp.
plus : tp -> tp -> tp.
with : 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.

send : ch (lolli A B) -o ch A -o (ch B -o exp C) -o exp C.
recv_ : (ch A -o exp B) -o exp (lolli A B).

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.

select1 : ch (with A B) -o (ch A -o exp C) -o exp C.
select2 : ch (with A B) -o (ch B -o exp C) -o exp C.
case_ : exp A & exp B -o exp (with A B).

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/lolli : proc (recv_ (\x. P x)) C * proc (send C W (\c'. Q c')) D
          -o { Exists c'. proc (P W) c' * proc (Q 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 }.
c/with1 : proc (case_ < P1 , P2 >) C * proc (select1 C (\c'. Q c')) D
        -o { Exists c'. proc P1 c' * proc (Q c') D }.
c/with2 : proc (case_ < P1 , P2 >) C * proc (select2 C (\c'. Q c')) D
        -o { Exists c'. proc P2 c' * proc (Q c') D }.

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

#query * 1 * 1
Pi A:tp. Pi B:tp. Pi c0:ch (lolli (tensor A B) (tensor B A)).
proc (recv_ (\x:ch (tensor A B). recv x (\y:ch A. \c1:ch B. send_ c1 (fwd_ y)))) c0
-o { Exists P. proc P c0 }.

#query * 1 * 1
Pi c0:ch one.
proc (spawn_ (spawn_ (close_) (\c1. send_ c1 (close_)))
     (\c2. recv c2 (\w. \c3. wait w (wait c3 (close_))))) c0
-o { proc P c0 }.

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


#query * 1 * 1
Pi c0:ch (plus one one).
proc (spawn_ (select1_ (close_)) (\c1. case c1 < (\c2. select2_ (fwd_ c2)) ,
                                                 (\c3. select1_ (fwd_ c3)) >)) c0
-o { Exists c1. proc P c1 * proc (Q c1) c0 }.