%%% Continuation Machine for Mini-ML
%%% Author: Frank Pfenning

% Machine Instructions
inst : type.  %name inst I.

ev : exp -> inst.
return : val -> inst.

case1 : val -> exp -> (val -> exp) -> inst.
pair1 : val -> exp -> inst.
fst1 : val -> inst.
snd1 : val -> inst.
app1 : val -> exp -> inst.
app2 : val -> val -> inst.

% Continuations
cont : type.  %name cont K.

init : cont.
;    : cont -> (val -> inst) -> cont.
%infix left 8 ;.

% Continuation Machine States
state : type.  %name state S.

# : cont -> inst -> state.
answer : val -> state.
%infix none 7 #.