%%% Mapping evaluations to evaluations in environments.
%%% Author: Frank Pfenning, based on [Hannan & Pfenning 92]
%%% Modified: Robert J. Simmons

map_eval : eval E V -> trans K F E
	      -> feval K F W -> vtrans W V -> type.

% Variables
mp_1  : map_eval D (tr_1 U1) (fev_1) U1
	   <- vtrans_val U1 P
	   <- val_eval P D.

mp_^  : map_eval D (tr_^ C1) (fev_^ D1') U1
	   <- map_eval D C1 D1' U1.

mp_1+ : map_eval D (tr_1+ C1) (fev_1+ D1') U1
	   <- map_eval D C1 D1' U1.

mp_^+ : map_eval D (tr_^+ C1) (fev_^+ D1') U1
	   <- map_eval D C1 D1' U1.

% Natural Numbers
mp_z       : map_eval (ev_z) (tr_z) (fev_z) (vtr_z).
mp_s       : map_eval (ev_s D1) (tr_s C1) (fev_s D1') (vtr_s U1)
	      <- map_eval D1 C1 D1' U1.
mp_case_z  : map_eval (ev_case_z D2 D1) (tr_case C3 C2 C1)
	      (fev_case_z D2' D1') U2
	      <- map_eval D1 C1 D1' (vtr_z)
	      <- map_eval D2 C2 D2' U2.
mp_case_s  : map_eval (ev_case_s D3 D1) (tr_case C3 C2 C1)
	      (fev_case_s D3' D1') U3
	      <- map_eval D1 C1 D1' (vtr_s U1')
	      <- map_eval D3 (C3 W1' V1' U1') D3' U3.

% Pairs
mp_pair : map_eval (ev_pair D2 D1) (tr_pair C2 C1)
		   (fev_pair D2' D1') (vtr_pair U2 U1)
	     <- map_eval D1 C1 D1' U1
	     <- map_eval D2 C2 D2' U2.

mp_fst  : map_eval (ev_fst D1) (tr_fst C1)
		   (fev_fst D1') U1
	     <- map_eval D1 C1 D1' (vtr_pair U2 U1).

mp_snd  : map_eval (ev_snd D1) (tr_snd C1)
		   (fev_snd D1') U2
	     <- map_eval D1 C1 D1' (vtr_pair U2 U1).

% Functions
mp_lam : map_eval (ev_lam) (tr_lam C)
		  (fev_lam) (vtr_lam (tr_lam C)).

mp_app : map_eval (ev_app D3 D2 D1) (tr_app C2 C1)
	  (fev_app D3' D2' D1') U3
	  <- map_eval D1 C1 D1' (vtr_lam (tr_lam C3))
	  <- map_eval D2 C2 D2' U2
	  <- map_eval D3 (C3 W2 V2 U2) D3' U3.

% Definitions
mp_letv : map_eval (ev_letv D2 D1) (tr_letv C2 C1)
	   (fev_letv D2' D1') U2
	   <- map_eval D1 C1 D1' U1
	   <- map_eval D2 (C2 W1 V1 U1) D2' U2.

mp_letn : map_eval (ev_letn D2) (tr_letn C2 C1)
	   (fev_letn D2') U2
	   <- map_eval D2 (C2 F1 E1 C1) D2' U2.

% Recursion
mp_fix : map_eval (ev_fix D1) (tr_fix C1)
		  (fev_fix D1') U1
	  <- map_eval D1 (C1 (fix' F1) (fix E1) (tr_fix C1)) D1' U1.

%mode map_eval +D +C -D' -U.
%worlds () (map_eval D C D' U).
% problem here---fixed in 2001 version
% %covers map_eval +D +C -D' -U.



% The copy of map_eval exists only to allow totality to be checked
% using a different mode.

map_eval' : eval E V -> trans K F E
	      -> feval K F W -> vtrans W V -> type.

% Variables
mp_1  : map_eval' D (tr_1 U1) (fev_1) U1
	   <- vtrans_val U1 P
	   <- val_eval P D.

mp_^  : map_eval' D (tr_^ C1) (fev_^ D1') U1
	   <- map_eval' D C1 D1' U1.

mp_1+ : map_eval' D (tr_1+ C1) (fev_1+ D1') U1
	   <- map_eval' D C1 D1' U1.

mp_^+ : map_eval' D (tr_^+ C1) (fev_^+ D1') U1
	   <- map_eval' D C1 D1' U1.

% Natural Numbers
mp_z       : map_eval' (ev_z) (tr_z) (fev_z) (vtr_z).
mp_s       : map_eval' (ev_s D1) (tr_s C1) (fev_s D1') (vtr_s U1)
	      <- map_eval' D1 C1 D1' U1.
mp_case_z  : map_eval' (ev_case_z D2 D1) (tr_case C3 C2 C1)
	      (fev_case_z D2' D1') U2
	      <- map_eval' D1 C1 D1' (vtr_z)
	      <- map_eval' D2 C2 D2' U2.
mp_case_s  : map_eval' (ev_case_s D3 D1) (tr_case C3 C2 C1)
	      (fev_case_s D3' D1') U3
	      <- map_eval' D1 C1 D1' (vtr_s U1')
	      <- map_eval' D3 (C3 W1' V1' U1') D3' U3.

% Pairs
mp_pair : map_eval' (ev_pair D2 D1) (tr_pair C2 C1)
		   (fev_pair D2' D1') (vtr_pair U2 U1)
	     <- map_eval' D1 C1 D1' U1
	     <- map_eval' D2 C2 D2' U2.

mp_fst  : map_eval' (ev_fst D1) (tr_fst C1)
		   (fev_fst D1') U1
	     <- map_eval' D1 C1 D1' (vtr_pair U2 U1).

mp_snd  : map_eval' (ev_snd D1) (tr_snd C1)
		   (fev_snd D1') U2
	     <- map_eval' D1 C1 D1' (vtr_pair U2 U1).

% Functions
mp_lam : map_eval' (ev_lam) (tr_lam C)
		  (fev_lam) (vtr_lam (tr_lam C)).

mp_app : map_eval' (ev_app D3 D2 D1) (tr_app C2 C1)
	  (fev_app D3' D2' D1') U3
	  <- map_eval' D1 C1 D1' (vtr_lam (tr_lam C3))
	  <- map_eval' D2 C2 D2' U2
	  <- map_eval' D3 (C3 W2 V2 U2) D3' U3.

% Definitions
mp_letv : map_eval' (ev_letv D2 D1) (tr_letv C2 C1)
	   (fev_letv D2' D1') U2
	   <- map_eval' D1 C1 D1' U1
	   <- map_eval' D2 (C2 W1 V1 U1) D2' U2.

mp_letn : map_eval' (ev_letn D2) (tr_letn C2 C1)
	   (fev_letn D2') U2
	   <- map_eval' D2 (C2 F1 E1 C1) D2' U2.

% Recursion
mp_fix : map_eval' (ev_fix D1) (tr_fix C1)
		  (fev_fix D1') U1
	  <- map_eval' D1 (C1 (fix' F1) (fix E1) (tr_fix C1)) D1' U1.


%mode map_eval' -D +C +D' -U.
%worlds () (map_eval' D C D' U).
%covers map_eval' -D +C +D' -U.