%%% type rules for explicitly typed language with units of measure.
%%% by Ralph Melton (based on Kennedy97)

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


% Numbers
of_num     : of E (num u1)
	      <- number E.

of_+     : of (E1 + E2) (num U1)
	    <- of E1 (num U1)
	    <- of E2 (num U1).
of_-     : of (E1 - E2) (num U1)
	    <- of E1 (num U1)
	    <- of E2 (num U1).

of_*     : of (E1 * E2) (num (U1 u* U2))
	    <- of E1 (num U1)
	    <- of E2 (num U2).
of_/     : of (E1 / E2) (num (U1 u* U2 u-1))
	    <- of E1 (num U1)
	    <- of E2 (num U2).

of_<     : of (E1 < E2) bool
	    <- of E1 (num U)
	    <- of E2 (num U).

%% unit cast
of_un    : of (un U) (num U).

%% functions
of_lam   : of (lam T1 E) (T1 => T2)
	    <- ({x:exp} of x T1 -> of (E x) T2).
of_app   : of (app E1 E2) T1
	    <- of E1 (T2 => T1)
	    <- of E2 T2.


%% conditionals
of_false : of false bool.
of_true  : of true bool.
of_if    : of (if E1 E2 E3) T2
	    <- of E1 bool
	    <- of E2 T2
	    <- of E3 T2.


%% recursion
of_rec   : of (rec T E) T
	    <- ({x: exp} of x T -> of (E x) T).


%% units abstraction and application
of_LAM   : of (LAM E) (forall T)
	    <- ({u: unit} of (E u) (T u)).
of_APP   : {u: unit} of (APP E u) (T u)
	    <- of E (forall T).

%% lets
of_letv  : of (letv E1 E2) T2
	    <- of E1 T1
	    <- ({x:exp} of x T1 -> of (E2 x) T2).
of_letn  : of (letn E1 E2) T2
	    <- of E1 T1
	    <- of (E2 E1) T2.


%% equality
of_eq    : of E T2
	    <- of E T1
	    <- eqtypes T1 T2.