Type Preservation for MLref

%%% Mini-ML with References
%%% Type Preservation
%%% Author: Frank Pfenning

%%% Four type preservation theorems
%%% Mode declarations below indicate quantifiers
%%% Lex declarations below indicate structural induction variables

tpex : exec K I W -> ofk K T S -> ofi I T -> off W S -> type.
tpcl : close W W' -> off W T -> off W' T -> type.
tpct : contains C V -> ofc C T -> ofv V T -> type.
tprd : read C V -> ofc C T -> ofv V T -> type.

tpev : ceval E W -> ofe E T -> off W T -> type.

%mode -tpex +Ex +Ok +Oi -Of
%lex Ex

%mode -tpcl +Ec +Of -Of'
%lex Ec

%mode -tpct +Et -Oc -Ov
%lex Et

%mode -tprd +Ed -Oc -Ov
%lex Ed

%mode -tpev +Ev +Oe -Of
%lex Ev

%%% Reading the state without affecting it

tprd_rd : tprd (rd ^ () ^ Et) Oc Ov
            o- tpct Et Oc Ov
            o- .

%%% Execution

% Natural Numbers
tpex_z : tpex (ex_z ^ Ex1) Ok (ofi_ev (ofe_z)) Of
	  o- tpex Ex1 Ok (ofi_return (ofv_z)) Of.

tpex_s : tpex (ex_s ^ Ex1) Ok (ofi_ev (ofe_s Oe1)) Of
	  o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 nat]
				   ofi_return (ofv_s ov1)))
	          (ofi_ev Oe1) Of.
			 
tpex_case : tpex (ex_case ^ Ex1) Ok (ofi_ev (ofe_case Oe3 Oe2 Oe1)) Of
	     o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 nat]
				      ofi_case1 Oe3 Oe2 ov1))
		     (ofi_ev Oe1) Of.

tpex_case1_z : tpex (ex_case1_z ^ Ex1) Ok (ofi_case1 Oe3 Oe2 (ofv_z)) Of
		o- tpex Ex1 Ok (ofi_ev Oe2) Of.

tpex_case1_s : tpex (ex_case1_s ^ Ex1) Ok (ofi_case1 Oe3 Oe2 (ofv_s Ov1)) Of
		o- tpex Ex1 Ok (ofi_ev (Oe3 V1 Ov1)) Of.

% Unit
tpex_unit : tpex (ex_unit ^ Ex1) Ok (ofi_ev (ofe_unit)) Of
	     o- tpex Ex1 Ok (ofi_return (ofv_unit)) Of.

% Pairs
tpex_pair : tpex (ex_pair ^ Ex1) Ok (ofi_ev (ofe_pair Oe2 Oe1)) Of
	     o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 T1]
				      ofi_pair1 Oe2 ov1))
		     (ofi_ev Oe1) Of.

tpex_pair1 : tpex (ex_pair1 ^ Ex1) Ok (ofi_pair1 Oe2 Ov1) Of
	      o- tpex Ex1 (ofk_; Ok ([x2:val] [ov2:ofv x2 T2]
				       ofi_return (ofv_pair ov2 Ov1)))
		      (ofi_ev Oe2) Of.

tpex_fst : tpex (ex_fst ^ Ex1) Ok (ofi_ev (ofe_fst Oe1)) Of
	    o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 (T1 * T2)]
				     ofi_fst1 ov1))
	            (ofi_ev Oe1) Of.

tpex_fst1 : tpex (ex_fst1 ^ Ex1) Ok (ofi_fst1 (ofv_pair Ov2 Ov1)) Of
	     o- tpex Ex1 Ok (ofi_return Ov1) Of.

tpex_snd : tpex (ex_snd ^ Ex1) Ok (ofi_ev (ofe_snd Oe1)) Of
	    o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 (T1 * T2)]
				     ofi_snd1 ov1))
	            (ofi_ev Oe1) Of.

tpex_snd1 : tpex (ex_snd1 ^ Ex1) Ok (ofi_snd1 (ofv_pair Ov2 Ov1)) Of
	     o- tpex Ex1 Ok (ofi_return Ov2) Of.

% Functions
tpex_lam : tpex (ex_lam ^ Ex1) Ok (ofi_ev (ofe_lam Oe1)) Of
	    o- tpex Ex1 Ok (ofi_return (ofv_lam Oe1)) Of.

tpex_app : tpex (ex_app ^ Ex1) Ok (ofi_ev (ofe_app Oe2 Oe1)) Of
	    o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 (T2 => T1)]
				     ofi_app1 Oe2 ov1))
	            (ofi_ev Oe1) Of.

tpex_app1 : tpex (ex_app1 ^ Ex1) Ok (ofi_app1 Oe2 Ov1) Of
	     o- tpex Ex1 (ofk_; Ok ([x2:val] [ov2:ofv x2 T2]
				      ofi_app2 ov2 Ov1))
		     (ofi_ev Oe2) Of.

tpex_app2 : tpex (ex_app2 ^ Ex1) Ok (ofi_app2 Ov2 (ofv_lam Oe1)) Of
	     o- tpex Ex1 Ok (ofi_ev (Oe1 V2 Ov2)) Of.

% References
tpex_ref : tpex (ex_ref ^ Ex1) Ok (ofi_ev (ofe_ref Oe1)) Of
	    o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 T1] ofi_ref1 ov1))
	            (ofi_ev Oe1) Of.

tpex_ref1 : tpex (ex_ref1 ^ Ex1) Ok (ofi_ref1 Ov1) (off_new Of)
	     o- ({c:cell} {et:contains c V1} {oc:ofc c T1}
		   tpct et oc Ov1
		   -o tpex (Ex1 c ^ et) Ok (ofi_return (ofv_ref oc))
		           (Of c oc)).

tpex_deref : tpex (ex_deref ^ Ex1) Ok (ofi_ev (ofe_deref Oe1)) Of
	      o- tpex Ex1 (ofk_; Ok ([x1:val] [Ov1:ofv x1 (rf T1)]
				       ofi_deref1 Ov1))
		      (ofi_ev Oe1) Of.

tpex_deref1 : tpex (ex_deref1 ^ (Rd1 , Ex1)) Ok (ofi_deref1 (ofv_ref Oc)) Of
                o- tprd Rd1 Oc Ov1 & tpex Ex1 Ok (ofi_return Ov1) Of.

%{ or, multiplicatively:
tpex_deref1 : tpex (ex_deref1 ^ Ex2 ^ Et1) Ok (ofi_deref1 (ofv_ref Oc)) Of
	       o- tpct Et1 Oc Ov1  % Oc is unique!
	       o- ({et1:contains C1 V1}
		      tpct et1 Oc Ov1
		      -o tpex (Ex2 ^ et1) Ok (ofi_return Ov1) Of).
}%

tpex_assign : tpex (ex_assign ^ Ex1) Ok (ofi_ev (ofe_assign Oe2 Oe1)) Of
	       o- tpex Ex1 (ofk_; Ok ([x1:val] [Ov1:ofv x1 (rf T)]
					ofi_assign1 Oe2 Ov1))
		  (ofi_ev Oe1) Of.

tpex_assign1 : tpex (ex_assign1 ^ Ex1) Ok (ofi_assign1 Oe2 Ov1) Of
		o- tpex Ex1 (ofk_; Ok ([x2:val] [Ov2:ofv x2 T]
					 ofi_assign2 Ov2 Ov1))
		        (ofi_ev Oe2) Of.

tpex_assign2 : tpex (ex_assign2 ^ Ex2 ^ Et1) Ok
                    (ofi_assign2 Ov2 (ofv_ref Oc)) Of
		o- tpct Et1 Oc Ov1  % Oc is unique!
		o- ({et2:contains C1 V2} 
		      tpct et2 Oc Ov2
		      -o tpex (Ex2 ^ et2) Ok (ofi_return (ofv_unit)) Of).

tpex_seq : tpex (ex_seq ^ Ex1) Ok (ofi_ev (ofe_seq Oe2 Oe1)) Of
	    o- tpex Ex1 (ofk_; Ok ([x1:val] [Ov1:ofv x1 T1]
				     ofi_ev Oe2))
	            (ofi_ev Oe1) Of.

% Let
tpex_let : tpex (ex_let ^ Ex1) Ok (ofi_ev (ofe_let Oe2 Oe1)) Of
	    o- tpex Ex1 (ofk_; Ok ([x1:val] [ov1:ofv x1 T1]
				     ofi_let1 Oe2 ov1))
	            (ofi_ev Oe1) Of.

tpex_let1 : tpex (ex_let1 ^ Ex2) Ok (ofi_let1 Oe2 Ov1) Of
	     o- tpex Ex2 Ok (ofi_ev (Oe2 V1 Ov1)) Of.

tpex_letv : tpex (ex_letv ^ Ex2) Ok (ofi_ev (ofe_letv Oe2)) Of
	     o- tpex Ex2 Ok (ofi_ev Oe2) Of.

% Recursion
tpex_fix  : % {Oe: {u:exp} ofe u T -> ofe (E u) T}
	     tpex (ex_fix ^ Ex1) Ok (ofi_ev (ofe_fix Oe)) Of
	     o- tpex Ex1 Ok (ofi_ev (Oe (fix E) (ofe_fix Oe))) Of.

% Values
tpex_vl   : tpex (ex_vl ^ Ex1) Ok (ofi_ev (ofe_vl Ov)) Of
	     o- tpex Ex1 Ok (ofi_return Ov) Of.

tpex_return : tpex (ex_return ^ Ex1) (ofk_; Ok Oc) (ofi_return Ov) Of
	       o- tpex Ex1 Ok (Oc V Ov) Of.

tpex_init : tpex (ex_init ^ Ec1) (ofk_init) (ofi_return Ov) Of
	     o- tpcl Ec1 (off_val Ov) Of.

%%% Collecting the final state

tpcl_done : tpcl (close_done) Of Of.

tpcl_loc  : tpcl (close_loc ^ Ec2 ^ Et1) Of Of'
	     o- tpct Et1 Oc1 Ov1
	     o- tpcl Ec2 (off_loc Of Ov1 Oc1) Of'.

%%% Evaluation

tpev_cev : tpev (cev ^ Ex) Oe Of
	    o- tpex Ex (ofk_init) (ofi_ev Oe) Of.

Frank Pfenning