%%% Compilation to Continuation-Passing Style
%%% Author: Frank Pfenning

cmp : exp -> (cval -> cexp) -> cexp -> type.

cmp_z : cmp z K (K z+).
cmp_s : cmp (s E) K E'
	 <- cmp E ([x:cval] K (s+ x)) E'.

% note duplication of K
cmp_case : cmp (case E1 E2 E3) K E'
	    <- cmp E2 K E2'
	    <- ({x:exp} {x':cval}
		  ({K'} cmp x K' (K' x'))
		  -> cmp (E3 x) K (E3' x'))
	    <- cmp E1 ([x1:cval] case+ x1 E2' E3') E'.

cmp_pair : cmp (pair E1 E2) K E'
	    <- ({x1':cval} cmp E2 ([x2':cval] K (pair+ x1' x2')) (E2' x1'))
	    <- cmp E1 E2' E'.

cmp_fst : cmp (fst E) K E'
	   <- cmp E ([x:cval] fst+ x K) E'.
cmp_snd : cmp (snd E) K E'
	   <- cmp E ([x:cval] snd+ x K) E'.

cmp_lam : cmp (lam E) K (K (lam+ E'))
	   <- ({x:exp} {x':cval}
		 ({K'} cmp x K' (K' x'))
		 -> {k:cval -> cexp}
		    cmp (E x) k (E' x' k)).

cmp_app : cmp (app E1 E2) K E'
	   <- ({x1:cval} cmp E2 ([x2:cval] app+ x1 x2 K) (E2' x1))
	   <- cmp E1 ([x1:cval] E2' x1) E'.

cmp_letv : cmp (letv E1 E2) K E'
	    <- ({x:exp} {x':cval}
		  ({K'} cmp x K' (K' x'))
		  -> cmp (E2 x) K (E2' x'))
	    <- cmp E1 ([x:cval] E2' x) E'.