%%% Closed Mini-ML Expressions
%%% Author: Frank Pfenning

closed : exp -> type.  %name closed U u.
%mode closed +E.

% Natural Numbers
clo_z     : closed z.
clo_s     : closed (s E)
	     <- closed E.


clo_case  : closed (case E1 E2 E3)
	     <- closed E1
	     <- closed E2
	     <- ({x:exp} closed x -> closed (E3 x)).

% Pairs
clo_pair : closed (pair E1 E2)
	      <- closed E1
	      <- closed E2.
clo_fst  : closed (fst E)
	      <- closed E.
clo_snd  : closed (snd E)
	      <- closed E.

% Functions
clo_lam : closed (lam E)
	     <- ({x:exp} closed x -> closed (E x)).
clo_app : closed (app E1 E2)
	     <- closed E1
	     <- closed E2.

% Definitions
clo_letv : closed (letv E1 E2)
	      <- closed E1
	      <- ({x:exp} closed x -> closed (E2 x)).
clo_letn : closed (letn E1 E2)
	      <- closed E1
	      <- ({x:exp} closed x -> closed (E2 x)).

% Recursion
clo_fix : closed (fix E)
	     <- ({x:exp} closed x -> closed (E x)).

%block lc : block {x:exp} {u:closed x}.
%worlds (lc) (closed E).
%terminates E (closed E).
%covers closed +E.
%total E (closed E).

%%% Open Mini-ML Expressions.
%%% Warning: one needs to assume that parameters are open!

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

% Natural Numbers
open_s     : open (s E) <- open E.
open_case1 : open (case E1 E2 E3) <- open E1.
open_case2 : open (case E1 E2 E3) <- open E2.
open_case3 : open (case E1 E2 E3) <- ({x:exp} open (E3 x)).

% Pairs
open_pair1 : open (pair E1 E2) <- open E1.
open_pair2 : open (pair E1 E2) <- open E2.
open_fst   : open (fst E) <- open E.
open_snd   : open (snd E) <- open E.

% Functions
open_lam  : open (lam E) <- ({x:exp} open (E x)).
open_app1 : open (app E1 E2) <- open E1.
open_app2 : open (app E1 E2) <- open E2.

% Definitions
open_letv1 : open (letv E1 E2) <- open E1.
open_letv2 : open (letv E1 E2) <- ({x:exp} open (E2 x)).
open_letn1 : open (letn E1 E2) <- open E1.
open_letn2 : open (letn E1 E2) <- ({x:exp} open (E2 x)).

% Recursion
open_fix : open (fix E) <- ({x:exp} open (E x)).

%block lo : block {x:exp}.
%worlds (lo) (open E).
%terminates E (open E).
% next reports z and #lo_x as missing
% %covers open +E.