% Call-by-push-value in CLF
% !!! Incomplete !!!
%
% As written in 15-816, Nov 15, 2016


neg : type.
pos : type.

arrow : pos -> neg -> neg.
with : neg -> neg -> neg.
up : pos -> neg.

cross : pos -> pos -> pos.
one : pos.
plus : pos -> pos -> pos.
down : neg -> pos.

val : pos -> type.
comp : neg -> type.

lam : (val A -> comp B) -> comp (arrow A B).
app : comp (arrow A B) -> val A -> comp B.
return : val A -> comp (up A).
letval : comp (up A) -> (val A -> comp C) -> comp C.

pair : val A -> val B -> val (cross A B).
mpair : val (cross A B) -> (val A -> val B -> comp C) -> comp C.
thunk : comp A -> val (down A).
force : val (down A) -> comp A.

dest : neg -> type.
frame : neg -> neg -> type.
app1 : val A -> frame (arrow A B) B.
letval1: (val A -> comp C) -> frame (up A) C.

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

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}.
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}.

#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}.