%%% Mini-ML types.
%%% Extended with some atomic subtyping
%%% 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

* = cross.   %infix right 10 *.
=> = arrow.  %infix right 11 =>.

%%% Subtyping
%%% Specification, not executable

sub : tp -> tp -> type.  %name sub C.
%mode sub *T *T'.
%tabled sub.

sub_pn : sub pos nat. 
sub_zn : sub zero nat. 

sub_=> : sub (T1 => T2) (S1 => S2)
	  <- sub S1 T1
	 <-  sub T2 S2.


sub_refl : sub T T.
sub_trans :  sub S R
             <- sub S T
	     <- sub T R.

% sub_trans : sub S T -> sub T R -> sub S R.

%{
sub_* : sub T1 S1 
	 -> sub T2 S2
	 -> sub (T1 * T2) (S1 * S2).
}%



% worlds () (sub T S).

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

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

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


% 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).

% worlds (some {T:tp} pi {x:exp} {d:of x T}) (of E T).
% covers of +E *T.