% Intrinsically typed version of Mini-ML
% We eliminate "let name" from the language in favor of polymorphism
% Author: Frank Pfenning

%%% Expressions, including some types

term* :  type.  %name term* M x.

z*    : term*.
s*    : term* -> term*.
case* : term* -> term* -> (term* -> term*) -> term*.

pair* : term* -> term* -> term*.
fst*  : term* -> term*.
snd*  : term* -> term*.

lam*  : tp -> (term* -> term*) -> term*.
app*  : term* -> term* -> term*.

letv* : term* -> (term* -> term*) -> term*.
% no letn construct

fix*  : tp -> (term* -> term*) -> term*.

tlam* : (tp -> term*) -> term*.
tapp* : term* -> tp -> term*.

%%% Intrinsic Typing

of* : term* -> 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:term*} 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* T1 E) (arrow T1 T2)
	  <- ({x:term*} 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:term*} of* x T1 -> of* (E2 x) T2).

% no let name

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

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

tp_tapp* : of* (tapp* E T') (T T')
	    <- of* E (all [a] T a).

%covers of* +E *T.
%terminates E (of* E T).

%%% Types are unique

% Type equality
eq : tp -> tp -> type.			%name eq E e.
eq_nat : eq nat nat.
eq_cross : eq (cross T1 T2) (cross S1 S2)
	    <- eq T1 S1
	    <- eq T2 S2.
eq_arrow : eq (arrow T1 T2) (arrow S1 S2)
	    <- eq T1 S1
	    <- eq T2 S2.
eq_all : eq (all T) (all S)
	  <- ({a:tp} eq a a -> eq (T a) (S a)).

% Reflexivity
refl : {T:tp} eq T T -> type.
%mode refl +T -E.
refl_nat : refl nat eq_nat.
refl_cross : refl (cross T1 T2) (eq_cross E2 E1)
	      <- refl T1 E1
	      <- refl T2 E2.
refl_arrow : refl (arrow T1 T2) (eq_arrow E2 E1)
	      <- refl T1 E1
	      <- refl T2 E2.
refl_all : refl (all T) (eq_all E)
	    <- ({a:tp} {e:eq a a} refl a e -> refl (T a) (E a e)).
%covers refl +T -E.
%terminates T (refl T _).

% Uniqueness of types
tpu : of* E T -> of* E S -> eq T S -> type.
%mode tpu +P +Q -E.

tpu_z : tpu (tp_z*) (tp_z*) (eq_nat).
tpu_s : tpu (tp_s* P1) (tp_s* Q1) (eq_nat).
tpu_case : tpu (tp_case* P3 P2 P1) (tp_case* Q3 Q2 Q1) E
	    <- tpu P2 Q2 E.

tpu_pair : tpu (tp_pair* P2 P1) (tp_pair* Q2 Q1) (eq_cross E2 E1)
	    <- tpu P1 Q1 E1
	    <- tpu P2 Q2 E2.
tpu_fst : tpu (tp_fst* P') (tp_fst* Q') E1
	   <- tpu P' Q' (eq_cross E2 E1).
tpu_snd : tpu (tp_snd* P') (tp_snd* Q') E2
	   <- tpu P' Q' (eq_cross E2 E1).

tpu_lam : tpu (tp_lam* P2) (tp_lam* Q2) (eq_arrow E2 E1)
	   <- refl T1 E1
	   <- ({x:term*} {u:of* x T1}
		 tpu u u E1 -> tpu (P2 x u) (Q2 x u) E2).
tpu_app : tpu (tp_app* P2 P1) (tp_app* Q2 Q1) E1
	   <- tpu P1 Q1 (eq_arrow E1 E2). % note order!

tpu_letv : tpu (tp_letv* P2 P1) (tp_letv* Q2 Q1) E2
	    <- tpu P1 Q1 E1
	    <- ({x:term*} {u:of* x T1} {u':of* x T1'}
		  tpu u u' E1 -> tpu (P2 x u) (Q2 x u') E2).
tpu_fix : tpu (tp_fix* P1) (tp_fix* Q1) E
	   <- refl T E.

tpu_tlam : tpu (tp_tlam* P') (tp_tlam* Q') (eq_all E)
	    <- ({a:tp} {e:eq a a}
		  refl a e -> tpu (P' a) (Q' a) (E a e)).
tpu_tapp : tpu (tp_tapp* (P' : of* M (all T)))
	       (tp_tapp* (Q' : of* M (all S)))
	    (E T' E')
	    <- refl T' E'
	    <- tpu P' Q' (eq_all E).

%covers tpu +P +Q -E.
%terminates [P Q] (tpu P Q _).

%%% Evaluation, rules basically unchanged

eval* : term* -> term* -> type.
%mode eval* +M -V.

% Natural Numbers
ev_z*      : eval* z* z*.
ev_s*      : eval* (s* M) (s* V)
	     <- eval* M V.
ev_case_z* : eval* (case* M1 M2 M3) V
	     <- eval* M1 z*
	     <- eval* M2 V.
ev_case_s* : eval* (case* M1 M2 M3) V
	     <- eval* M1 (s* V1')
	     <- eval* (M3 V1') V.

% Pairs
ev_pair* : eval* (pair* M1 M2) (pair* V1 V2)
	   <- eval* M1 V1
	   <- eval* M2 V2.
ev_fst*  : eval* (fst* M) V1
	   <- eval* M (pair* V1 V2).
ev_snd*  : eval* (snd* M) V2
	   <- eval* M (pair* V1 V2).

% Functions
ev_lam* : eval* (lam* T M) (lam* T M).
ev_app* : eval* (app* M1 M2) V
	  <- eval* M1 (lam* T2 M1*)
	  <- eval* M2 V2
	  <- eval* (M1* V2) V.

% Definitions
ev_letv* : eval* (letv* M1 M2) V
	   <- eval* M1 V1
	   <- eval* (M2 V1) V.
% no letn

% Recursion
ev_fix*  : eval* (fix* T M) V
	   <- eval* (M (fix* T M)) V.

% Polymorphism
% Could evaluate underneath abstractions
ev_tlam* : eval* (tlam* M) (tlam* M).
ev_tapp* : eval* (tapp* M T) V
	    <- eval* M (tlam* M*)
	    <- eval* (M* T) V.

%worlds () (eval* M V).
%covers eval* +M *V.

%%% Relating extrinsic and intrinsic formulations

erase : exp -> term* -> type.
%mode erase -E +M.

er_z : erase z z*.
er_s : erase (s E) (s* M)
	<- erase E M.
er_case : erase (case E1 E2 E3) (case* M1 M2 M3)
	   <- erase E1 M1
	   <- erase E2 M2
	   <- ({x:exp} {y:term*} erase x y -> erase (E3 x) (M3 y)).
er_pair : erase (pair E1 E2) (pair* M1 M2)
	   <- erase E1 M1
	   <- erase E2 M2.
er_fst : erase (fst E) (fst* M)
	  <- erase E M.
er_snd : erase (snd E) (snd* M)
	  <- erase E M.
er_lam : erase (lam E) (lam* T1 M)
	  <- ({x:exp} {y:term*} erase x y -> erase (E x) (M y)).
er_app : erase (app E1 E2) (app* M1 M2)
	  <- erase E1 M1
	  <- erase E2 M2.
er_letv : erase (letv E1 E2) (letv* M1 M2)
	   <- erase E1 M1
	   <- ({x:exp} {y:term*} erase x y -> erase (E2 x) (M2 y)).
er_fix : erase (fix E) (fix* T M)
	  <- ({x:exp} {y:term*} erase x y -> erase (E x) (M y)).
er_tlam : erase E (tlam* M)
	   <- ({a:tp} erase E (M a)).
er_tapp : erase E (tapp* M T)
	   <- erase E M.

%covers erase -E +M.
%terminates M (erase _ M).

rel : of E T -> erase E M -> of* M T -> type.

rel_z : rel (tp_z) (er_z) (tp_z*).
rel_s : rel (tp_s P1) (er_s R1) (tp_s* Q1)
	 <- rel P1 R1 Q1.
rel_case : rel (tp_case P3 P2 P1) (er_case R3 R2 R1) (tp_case* Q3 Q2 Q1)
	    <- rel P1 R1 Q1
	    <- rel P2 R2 Q2
	    <- ({x:exp} {y:term*} 
		  {u:of x nat} {r:erase x y} {w:of* y nat}
		  rel u r w -> rel (P3 x u) (R3 x y r) (Q3 y w)).
rel_pair : rel (tp_pair P2 P1) (er_pair R2 R1) (tp_pair* Q2 Q1)
	    <- rel P1 R1 Q1
	    <- rel P2 R2 Q2.
rel_fst : rel (tp_fst P') (er_fst R') (tp_fst* Q')
	   <- rel P' R' Q'.
rel_snd : rel (tp_snd P') (er_snd R') (tp_snd* Q')
	   <- rel P' R' Q'.
rel_lam : rel (tp_lam P2) (er_lam R2) (tp_lam* Q2)
	   <- ({x:exp} {y:term*}
		 {u:of x T1} {r:erase x y} {w:of* y T1}
		 rel u r w -> rel (P2 x u) (R2 x y r) (Q2 y w)).
rel_app : rel (tp_app P2 P1) (er_app R2 R1) (tp_app* Q2 Q1)
	   <- rel P1 R1 Q1
	   <- rel P2 R2 Q2.
rel_letv : rel (tp_letv P2 P1) (er_letv R2 R1) (tp_letv* Q2 Q1)
	    <- rel P1 R1 Q1
	    <- ({x:exp} {y:term*}
		  {u:of x T1} {r:erase x y} {w:of* y T1}
		  rel u r w -> rel (P2 x u) (R2 x y r) (Q2 y w)).
rel_fix : rel (tp_fix P1) (er_fix R1) (tp_fix* Q1)
	    <- ({x:exp} {y:term*}
		  {u:of x T} {r:erase x y} {w:of* y T}
		  rel u r w -> rel (P1 x u) (R1 x y r) (Q1 y w)).
rel_tlam : rel (tp_alli P) (er_tlam R1) (tp_tlam* Q1)
	    <- ({a:tp} rel (P a) (R1 a) (Q1 a)).
rel_tapp : rel (tp_alle T' P1) (er_tapp R1) (tp_tapp* (Q1:of* M (all T)))
	    <- rel P1 R1 Q1.

%mode rel +P -R -Q.
%covers rel +P *R *Q.
%terminates P (rel P _ _).

%mode rel -P +R +Q.
%covers rel -P +R +Q.
%terminates R (rel _ R Q).