%%% Parametric Polymorphism
%%% Translation between intrinisic and extrinsic formulations
%%% Author: Frank Pfenning

trans : term T -> of E T -> type.
%mode trans +M -P.

% Natural Numbers
tr_z : trans z' tp_z.
tr_s : trans (s' M) (tp_s P)
	<- trans M P.
tr_case : trans (case' M1 M2 M3) (tp_case P3 P2 P1)
	   <- trans M1 P1
	   <- trans M2 P2
	   <- ({x':term nat} {x:exp} {u:of x nat}
		 trans x' u -> trans (M3 x') (P3 x u)).

% Pairs
tr_pair : trans (pair' M1 M2) (tp_pair P2 P1)
	   <- trans M1 P1
	   <- trans M2 P2.
tr_fst : trans (fst' M) (tp_fst P)
	  <- trans M P.
tr_snd : trans (snd' M) (tp_snd P)
	  <- trans M P.

% Functions
tr_lam : trans (lam' M) (tp_lam P)
	  <- ({x':term T1} {x:exp} {u:of x T1}
		trans x' u -> trans (M x') (P x u)).
tr_app : trans (app' M1 M2) (tp_app P2 P1)
	  <- trans M1 P1
	  <- trans M2 P2.

% Definitions
tr_letv : trans (letv' M1 M2) (tp_letv P2 P1)
	   <- trans M1 P1
	   <- ({x':term T1} {x:exp} {u:of x T1}
		 trans x' u -> trans (M2 x') (P2 x u)).

% Recursion
tr_fix : trans (fix' M) (tp_fix P)
	  <- ({x':term T} {x:exp} {u:of x T}
		trans x' u -> trans (M x') (P x u)).

% Polymorphism
tr_tlam : trans (tlam' M) (tp_alli P)
	   <- ({a:tp} trans (M a) (P a)).
tr_tapp : trans (tapp' M T) (tp_alle T P)
	   <- trans M P.

%worlds (some {T:tp} pi {x':term T} {x:exp} {u:of x T} {q:trans x' u}
	| pi {a:tp})
(trans M P).

%covers trans +M -P.
%covers trans -M +P.