%%% Mini-ML types.
%%% Extended with intersection types
%%% Author: Frank Pfenning

tp : type.  %name tp T.

nat   : tp.				% Natural Numbers
pos   : tp.				% Positive Numbers
zero  : tp.				% Singleton Zero
cross : tp -> tp -> tp.			% Pairs
arrow : tp -> tp -> tp.			% Functions
and   : tp -> tp -> tp.			% Intersections
top   : tp.				% Top

* = cross.   %infix right 10 *.
=> = arrow.  %infix right 11 =>.
& = and.     %infix right 12 &.

%%% Subtyping
%%% Specification, not executable

sub : tp -> tp -> type.  %name sub C.

sub_refl : sub T T.
sub_trans : sub S T -> sub T R -> sub S R.
sub_pn : sub pos nat.
sub_zn : sub zero nat.
sub_* : sub T1 S1 
	 -> sub T2 S2
	 -> sub (T1 * T2) (S1 * S2).
sub_=> : sub S1 T1
	 -> sub T2 S2
	 -> sub (T1 => T2) (S1 => S2).
sub_&r : sub S T1
	 -> sub S T2
	 -> sub S (T1 & T2).
sub_&l1 : sub (T1 & T2) T1.
sub_&l2 : sub (T1 & T2) T2.
sub_topr : sub S top.
% no sub_topl rules

% no distributivity	  

%%% Typing rules
%%% Specification, not executable

of : exp -> tp -> type.  %name of P u.

% Subtyping
tp_sub : of E T
	  <- of E T'
	  <- sub T' T.

% Intersections
tp_&i : of E (T1 & T2)
	 <- of E T1
	 <- of E T2.

% Derived elimination rules
tp_&e1 : of E (T1 & T2) -> of E T1
       = [u:of E (T1 & T2)] tp_sub sub_&l1 u.
tp_&e2 : of E (T1 & T2) -> of E T2
       = [u:of E (T1 & T2)] tp_sub sub_&l2 u.

% Top
tp_topi : of E (top).
% no derived elimination rules

% Natural Numbers
% Standard rules
tp_z_nat : of z nat.
tp_s_nat : of (s E) nat
	    <- of E nat.
tp_case_nat : of (case E1 E2 E3) T
	       <- of E1 nat
	       <- of E2 T
	       <- ({x:exp} of x nat -> of (E3 x) T).

% New rules
tp_z_zero : of z zero.
tp_s_pos  : of (s E) pos
	     <- of E nat.
tp_case_zero : of (case E1 E2 E3) T
		<- of E1 zero
		<- of E2 T.
tp_case_pos : of (case E1 E2 E3) T
	       <- of E1 pos
	       <- ({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).
tp_letn : of (letn E1 E2) T2
	   <- of E1 T1
	   <- of (E2 E1) T2.

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