%%% The Mini-ML typing rules
%%% extended for parametric polymorphism
%%% These cannot be used for type inference because
%%% of the polymorphic type assignment rules
%%% Author: Frank Pfenning, based on [Michaylov & Pfenning 92]

of : exp -> tp -> type.  %name of P u.
%mode of +E *T.

% Natural Numbers
tp_z     : of z nat.
tp_s     : of (s E) nat
	    <- of E nat.
tp_case  : of (case E1 E2 E3) T
	    <- of E1 nat
	    <- of E2 T
	    <- ({x:exp} of x nat -> of (E3 x) T).

% Pairs
tp_pair : of (pair E1 E2) (cross T1 T2)
	   <- of E1 T1
	   <- of E2 T2.
tp_fst  : of (fst E) T1
	   <- of E (cross T1 T2).
tp_snd  : of (snd E) T2
	   <- of E (cross T1 T2).

% Functions
tp_lam : of (lam E) (arrow T1 T2)
	  <- ({x:exp} of x T1 -> of (E x) T2).
tp_app : of (app E1 E2) T1
	  <- of E1 (arrow T2 T1)
	  <- of E2 T2.

% Definitions
tp_letv : of (letv E1 E2) T2
	   <- of E1 T1
	   <- ({x:exp} of x T1 -> of (E2 x) T2).

% no let name

% Recursion
tp_fix : of (fix E) T
	  <- ({x:exp} of x T -> of (E x) T).

% Polymorphism
tp_alli : of E (all [a] T a)
	   <- ({a:tp} of E (T a)).

tp_alle : {T':tp} of E (T T')
	   <- of E (all [a] T a).


%worlds (some {T:tp} pi {x:exp} {d:of x T}
        | pi {a:tp})
(of E T).

%covers of +E *T.