%
% mini-ml
% 
exp  : sort.  
val  : sort.  

z     : trm exp.
s     : trm exp -> trm exp.
case  : trm exp -> trm exp -> (trm val -> trm exp) -> trm exp.
pair  : trm exp -> trm exp -> trm exp.
fst   : trm exp -> trm exp.
snd   : trm exp -> trm exp.
lamm : (trm val -> trm exp) -> trm exp.
appm : trm exp -> trm exp -> trm exp.
letv  : trm exp -> (trm val -> trm exp) -> trm exp.
letn  : trm exp -> (trm exp -> trm exp) -> trm exp.
fix   :  (trm exp -> trm exp) -> trm exp.

vl    : trm val -> trm exp.

z*    : trm val.
s*    : trm val -> trm val.
pair* : trm val -> trm val -> trm val.
lamm*  : (trm val -> trm exp) -> trm val.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% continuation passing machine
%
% Machine Instructions

ev : trm exp -> atm.
return : trm val -> atm.

case1 : trm val -> trm exp -> (trm val -> trm exp) -> atm.
pair1 : trm val -> trm exp -> atm.
fst1 : trm val -> atm.
snd1 : trm val -> atm.
appm1 : trm val -> trm exp -> atm.
appm2 : trm val -> trm val -> atm.


%
% evaluation of machine
%
% queries should be: sqnt cpmG rnil rnil rnil rnil (^(return V) =>> ^(ev E)).
%	where E is some expression to evaluate.
% 
% Thus the ordered context is the stack of continuations left to execute.
%
% Note the use of left implications (>=>) in rules where a continuation expecting 
%  a new value s put onto the stack.
%

%% Natural Numbers
ev2 : prog(
^ ev z  
     <<= ^ return z*
).

ev3 : prog(
^ ev (s E)  
     <<= ((forall val [V]  ^ return V  <=< ^ return (s* V) ) 
	   =>>  ^ ev E )
). 

ev4 : prog(
^ ev (case E1 E2 E3)  
     <<= ((forall val [V] ^ return V  <=< ^ case1 V E2 E3 ) 
	  =>>  ^ ev E1 )
). 

ev5 : prog(
^ case1 z* E2 E3  
     <<= ^ ev E2 
). 

ev6 : prog(
^ case1 (s* V) E2 E3  
     <<= ^ ev (E3 V) 
).

%% Functions
ev7 : prog(
^ ev (lamm E)  
     <<= ^ return (lamm* E) 
).

ev8 : prog(
^ ev (appm E1 E2)  
     <<= ((forall val [V1] ^ return V1  <=< ^ appm1 V1 E2)
	  =>> ^ ev E1 )
). 

ev9 : prog(
^ appm1 V1 E2 
     <<= ((forall val [V2] ^ return V2 <=< ^ appm2 V1 V2) 
	  =>> ^ ev E2 )
).

ev10 : prog(
^ appm2 (lamm* E1') V2  
      <<= ^ ev (E1' V2) 
). 

%% Definitions 
ev11: prog(
^ ev (letv E1 E2)  
     <<= ((forall val [V1] ^ ev (E2 V1) >=> ^ return V1 ) 
	  =>> ^ ev E1 )
). 

ev12: prog(
^ ev (letn E1 E2)  
     <<= ^ ev (E2 E1)  
).

%%  Recursion 
ev13: prog(
^ ev (fix E) 
     <<= ^ ev (E (fix E)) 
). 

%% Values
ev14 : prog(
^ ev (vl V)  
     <<= ^ return V 
).