% Types of the simply-typed lambda calculus

tp : type.

base : tp.
arrow : tp -> tp -> tp.


% Terms of the simply-typed lambda calculus

tm : type.

const : tm.
app : tm -> tm -> tm.
lam : (tm -> tm) -> tm.


% Typing judgment

of : tm -> tp -> type.

of_const : of const base.

of_app : of (app E1 E2) T2
	  <- of E1 (arrow T1 T2)
	  <- of E2 T1.

of_lam : of (lam E) (arrow T1 T2)
	  <- ({X} of X T1
		-> of (E X) T2).


% Some test queries

%query 1 1 of const T.
%query 1 1 of (lam ([X] X)) T.
%query 1 1 of (app (lam ([X] X)) const) T.
%query 1 1 of (lam [X] lam [Y] app X Y) T.


% Evaluation

step : tm -> tm -> type.

beta : step (app (lam E1) E2) (E1 E2).

cong : step (app E1 E2) (app E1' E2)
	 <- step E1 E1'.


% Preservation theorem

preservation : of E1 T -> step E1 E2 -> of E2 T -> type.

- : preservation (of_app OF2 (of_lam OF1)) beta (OF1 _ OF2).

- : preservation (of_app OF2 OF1) (cong STEP) (of_app OF2 OF1')
     <- preservation OF1 STEP OF1'.

%mode preservation +OF1 +STEP -OF.
%worlds () (preservation OF1 STEP _).
%total STEP (preservation OF1 STEP _).


% Values

value : tm -> type.

value_const : value const.

value_lam : value (lam E).


% Progress

progress_result : tm -> type.

done : progress_result E
	<- value E.

stepped : progress_result E
	   <- step E E'.

progress : of E T -> progress_result E -> type.

- : progress of_const (done value_const).

- : progress (of_lam OF) (done value_lam).

- : progress (of_app OF2 (of_lam OF1)) (stepped beta).

- : progress (of_app OF3 (of_app OF2 OF1)) (stepped (cong STEP))
     <- progress (of_app OF2 OF1) (stepped STEP).

%mode progress +OF -RES.
%worlds () (progress OF _).
%total OF (progress OF _).



% Term well-formedness

wf : tm -> type.

wf_const : wf const.

wf_app : wf (app E1 E2)
	  <- wf E1
	  <- wf E2.

wf_lam : wf (lam E)
	  <- ({X} wf X
		-> wf (E X)).

%query 5 5 wf E.


% Well-typedness implies well-formedness

of_wf : of E T -> wf E -> type.

- : of_wf of_const wf_const.

- : of_wf (of_app OF2 OF1) (wf_app WF2 WF1)
     <- of_wf OF2 WF2
     <- of_wf OF1 WF1.

- : of_wf (of_lam OF) (wf_lam WF)
     <- ({X}
	   {OF' : of X T}
	   {WF' : wf X}
	   of_wf OF' WF'
	   -> of_wf (OF X OF') (WF X WF')).

%mode of_wf +OF -WF.
%block of_wf_hyp : some {T : tp}
		    block {x : tm} {of' : of x T} {wf' : wf x}
		    {of_wf' : of_wf of' wf'}.
%worlds (of_wf_hyp) (of_wf OF _).
%total OF (of_wf OF _).