% Session-typed concurrency (SILL)
% Based on Carsten Schuermann's arbiter.clf
% Asynchronous 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.
msg : exp A -> ch A -> type.

c/fwd/+ : msg P D * proc (fwd_ D) C -o {msg P C}.
c/fwd/-/lolli : proc (fwd_ D) C * msg (send C W (\c'. fwd_ c')) C'
          -o msg (send D W (\c'. fwd_ c')) C'.
c/fwd/-/with1 : proc (fwd_ D) C * msg (select1 C (\c'. fwd_ c')) C'
          -o msg (select1 D (\c'. fwd_ c')) C'.
c/fwd/-/with2 : proc (fwd_ D) C * msg (select2 C (\c'. fwd_ c')) C'
          -o msg (select2 D (\c'. fwd_ c')) C'.

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

s/tensor : proc (send_ W P) C
        -o { Exists c'. proc P c' * msg (send_ W (fwd_ c')) C }.
r/tensor : msg (send_ W (fwd_ C')) C * proc (recv C (\x. \c'. Q x c')) D
        -o { proc (Q W C') D }.

s/lolli : proc (send C W (\c'. Q c')) D
          -o { Exists c'. msg (send C W (\c'. fwd_ c')) c' * proc (Q c') D }.
r/lolli : proc (recv_ (\x. P x)) C * msg (send C W (\c'. fwd_ c')) C'
          -o { proc (P W) C' }.

s/one : proc (close_) C 
        -o { msg (close_) C }.
r/one : msg (close_) C * proc (wait C Q) D
        -o { proc Q D }.

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

s/with1 : proc (select1 C (\c'. Q c')) D
        -o { Exists c'. msg (select1 C (\c'. fwd_ c')) c' * proc (Q c') D }.
r/with1 : proc (case_ < P1 , P2 >) C * msg (select1 C (\c'. fwd_ c')) C'
        -o { proc P1 C' }.
s/with2 : proc (select2 C (\c'. Q c')) D
        -o { Exists c'. msg (select2 C (\c'. fwd_ c')) c' * proc (Q c') D }.
r/with2 : proc (case_ < P1 , P2 >) C * msg (select2 C (\c'. fwd_ c')) C'
        -o { proc P2 C' }.

#query * 1 * 1
Pi c0:ch one. proc (spawn_ (close_) (\c1. wait c1 (close_))) c0 -o { msg 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 { msg 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 { Exists c1. msg P c1 * msg (Q c1) 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. msg P c1 * msg (Q c1) c0 }.