% Call-by-push-value in CLF
%
% As written in 15-816, Nov 15, 2016
% Completed, Nov 15, 2016 -fp

neg : type.
pos : type.

arrow : pos -> neg -> neg.   % A -> B
with : neg -> neg -> neg.    % A & B
up : pos -> neg.             % up A

cross : pos -> pos -> pos.   % A * B
one : pos.                   % 1
plus : pos -> pos -> pos.    % A + B
down : neg -> pos.           % down A

% values and computations, indexed by their type
val : pos -> type.
comp : neg -> type.

% negative types
% A -> B
lam : (val A -> comp B) -> comp (arrow A B).
app : comp (arrow A B) -> val A -> comp B.

% A & B
cpair : comp A -> comp B -> comp (with A B).
pi1 : comp (with A B) -> comp A.
pi2 : comp (with A B) -> comp B.

% up A
return : val A -> comp (up A).
letval : comp (up A) -> (val A -> comp C) -> comp C.

% positive types
% A * B
vpair : val A -> val B -> val (cross A B).
mpair : val (cross A B) -> (val A -> val B -> comp C) -> comp C.

% 1
unit : val one.
munit : val one -> comp C -> comp C.

% A + B
inl : val A -> val (plus A B).
inr : val B -> val (plus A B).
mplus : val (plus A B) -> (val A -> comp C) -> (val B -> comp C) -> comp C.

% down A
thunk : comp A -> val (down A).
force : val (down A) -> comp A.

% runtime artefacts
dest : neg -> type.
frame : neg -> neg -> type.
app1 : val A -> frame (arrow A B) B.
pi1c : frame (with A B) A.
pi2c : frame (with A B) B.
letval1: (val A -> comp C) -> frame (up A) C.

% ssos predicates
eval : comp A -> dest A -> type.
retn : comp A -> dest A -> type.
cont : dest A -> frame A B -> dest B -> type.

% A -> B
eval/lam : eval (lam (\!x. M !x)) D -o {retn (lam (\!x. M !x)) D}.
eval/app : eval (app M V) D
            -o {Exists d'. eval M d' * cont d' (app1 V) D}.
eval/app1 : retn (lam (\!x. M !x)) D' * cont D' (app1 V) D
             -o {eval (M !V) D}.

% A & B
eval/cpair : eval (cpair M N) D -o {retn (cpair M N) D}.
eval/pi1 : eval (pi1 M) D -o {Exists d'. eval M d' * cont d' (pi1c) D}.
eval/pi1c : retn (cpair M N) D' * cont D' pi1c D -o {eval M D}.
eval/pi2 : eval (pi2 M) D -o {Exists d'. eval M d' * cont d' (pi2c) D}.
eval/pi2c : retn (cpair M N) D' * cont D' pi2c D -o {eval M D}.

% up A
eval/return : eval (return V) D -o {retn (return V) D}.
eval/letval : eval (letval M (\!x. N !x)) D
               -o {Exists d'. eval M d'
                   * cont d' (letval1 (\!x. N !x)) D}.
eval/letval1 : retn (return V) D' * cont D' (letval1 (\!x. N !x)) D
                -o {eval (N !V) D}.

% A * B
eval/mpair : eval (mpair (vpair V W) (\!x. \!y. N !x !y)) D
             -o {eval (N !V !W) D}.

% 1
eval/munit : eval (munit unit C) D -o {eval C D}.

% A + B
eval/mplus1 : eval (mplus (inl V) (\!x. M !x) (\!y. N !y)) D
              -o {eval (M !V) D}.
eval/mplus2 : eval (mplus (inr W) (\!x. M !x) (\!y. N !y)) D
              -o {eval (N !V) D}.

% down A
eval/force : eval (force (thunk M)) D
             -o {eval M D}.

#query * 1 * 1
Pi d0. eval (lam (\!x. return x)) d0 -o {retn M d0}.

#query * 1 * 1
Pi d0. eval (app (lam (\!x. return x)) (thunk (lam (\!y. return y)))) d0
 -o {retn M d0}.