%%% Translation to representation using de Bruijn indices
%%% Version restricted to pure lambda-calculus
%%% Author: Frank Pfenning, based on [Hannan & Pfenning 92]

trans  : env -> exp' -> exp -> type.  %name trans C.
vtrans : val -> exp -> type.          %name vtrans U.
% Direction for compilation
%mode trans +N -F +E.
%mode vtrans +W +V.

% Direction for de-compilation
% %mode trans +N +F -E.
% %mode vtrans +W -V.

% Functions
tr_lam : trans N (lam' F) (lam E)
	    <- ({w:val} {x:exp}
		  vtrans w x -> trans (N , w) F (E x)).
tr_app : trans N (app' F1 F2) (app E1 E2)
	    <- trans N F1 E1
	    <- trans N F2 E2.

% Variables
tr_1  : trans (N , W) 1 E
	 <- vtrans W E.
tr_^  : trans (N , W) (F ^) E
	 <- trans N F E.

% Values
vtr_lam : vtrans (clo N (lam' F)) (lam E)
	   <- trans N (lam' F) (lam E).

%terminates {(E V) (N W)} (trans N _ E) (vtrans W V).

% termination in other direction cannot be checked.