%%% Evaluation of CPS terms
%%% Author: Frank Pfenning

ceval : cexp -> cval -> type.

ceval_vl : ceval (vl+ V) V.

ceval_case_z : ceval (case+ z+ E2 E3) V
	       <- ceval E2 V.
ceval_case_s : ceval (case+ (s+ V1') E2 E3) V
		<- ceval (E3 V1') V.

ceval_fst : ceval (fst+ (pair+ V1 V2) K) V
	     <- ceval (K V1) V.
ceval_snd : ceval (snd+ (pair+ V1 V2) K) V
	     <- ceval (K V2) V.

ceval_app : ceval (app+ (lam+ E1') V2 K) V
	     <- ceval (E1' V2 K) V.