%%% Lambda-Calculus Fragment of Mini-ML.
%%% Author: Frank Pfenning

% Simple types
tp : type.				%name tp T.

arrow : tp -> tp -> tp.			% T1 => T2

% Expressions
exp : type.				%name exp E.

lam : (exp -> exp) -> exp.		% lam x. E
app : exp -> exp -> exp.		% (E1 E2)

% Type inference 
% |- E : T  (expression E has type T)

of : exp -> tp -> type.			%name of P.
%mode of +E *T.
% %mode of +E +T.  % incorrect at tp_app
% %mode of +E -T.  % incorrect at tp_lam

tp_lam : of (lam E) (arrow T1 T2)	% |- lam x. E : T1 => T2
	  <- ({x:exp}			% if  x:T1 |- E : T2.
		of x T1 -> of (E x) T2).

tp_app : of (app E1 E2) T1		% |- E1 E2 : T1
	  <- of E1 (arrow T2 T1)	% if  |- E1 : T2 => T1
	  <- of E2 T2.			% and |- E2 : T2.

% Evaluation (call-by-value) 
% E ==> V  (expression E evaluates to value V)

eval : exp -> exp -> type.		%name eval D.
%mode eval +E -V.

ev_lam  : eval (lam E) (lam E).		% lam x.E ==> lam x.E.

ev_app  : eval (app E1 E2) V		% E1 E2 ==> V
	    <- eval E1 (lam E1')	% if  E1 ==> lam x. E1'
	    <- eval E2 V2		% and E2 ==> V2
	    <- eval (E1' V2) V.		% and [V2/x]E1' ==> V.

% Regular world for type-checking
%block tp_var : some {T:tp} block {x:exp} {u:of x T}.
%worlds (tp_var) (of E T).

% Type inference terminates
%terminates E (of E T).

% There is at least one typing rule for every expression
%covers of +E *T.

% Next fails, because T is neither input nor output
% %total E (of E T).

% Closed worlds for evaluation
%worlds () (eval E V).

% There is a at least one evaluation rule for every closed expression
%covers eval +E -V.

% %terminates E (eval E V).   % fails for ev_app

% Type preservation as higher-level family
tps : eval E V -> of E T -> of V T -> type.

tps_lam : tps (ev_lam) (tp_lam P) (tp_lam P).
tps_app : tps (ev_app D3 D2 D1) (tp_app P2 P1) Q
	   <- tps D1 P1 (tp_lam Q1')
	   <- tps D2 P2 Q2
	   <- tps D3 (Q1' V2 Q2) Q.

%mode tps +D +P -Q.
%worlds () (tps D P _).
%total D (tps D P _).

% Type preservation proven automatically
%theorem
tpsa : forall* {E:exp} {V:exp} {T:tp}
       forall {D:eval E V} {P:of E T}
       exists {Q:of V T}
       true.

%prove 5 D (tpsa D P Q).

% Applying type preservation
e0 = (app (lam [x] x) (lam [y] y)).
%solve p0 : of e0 T.
%solve d0 : eval e0 V.
%solve tps0 : tps d0 p0 Q.      

% Example of regular worlds
% cp copies input to output.

cp : exp -> exp -> type.
cp_app : cp (app E1 E2) (app F1 F2)
	  <- cp E1 F1
	  <- cp E2 F2.

cp_lam : cp (lam [x] E x) (lam [x] F x)
	  <- ({x:exp} cp x x -> cp (E x) (F x)).

%mode cp +E -F.
%block cp_var : block {x:exp} {u:cp x x}.
%worlds (cp_var) (cp E _).
%total E (cp E _).

% Following version cannot be checked
% Input coverage on parameter y is violated
%{
cp : exp -> exp -> type.
cp_app : cp (app E1 E2) (app F1 F2)
	  <- cp E1 F1
	  <- cp E2 F2.

cp_lam : cp (lam [x] E x) (lam [x] F x)
	  <- ({x:exp} {y:exp} cp x y -> cp (E x) (F y)).

%mode cp +E -F.
%block cp_var : block {x:exp} {y:exp} {u:cp x y}.
%worlds (cp_var) (cp E _).
%total E (cp E _).
}%

% Following version cannot be checked
% Output coverage on (F y) is violated.
%{
cp : exp -> exp -> type.
cp_app : cp (app E1 E2) (app F1 F2)
	  <- cp E1 F1
	  <- cp E2 F2.

cp_lam : cp (lam [x] E x) (lam [x] F x)
	  <- ({x:exp} {y:exp} cp x y -> cp y y -> cp (E x) (F y)).

%mode cp +E -F.
%block cp_var : block {x:exp} {y:exp} {u:cp x y} {w:cp y y}.
%worlds (cp_var) (cp E _).
%total E (cp E _).
}%

%theorem cpt : forallG (pi {x:exp} {y:cp x x})
               forall {E:exp}
	       exists {F:exp} {C:cp E F}
               true.
%prove 5 E (cpt E _ _).