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

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


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

eqlemma : {C : cell} ofv V T1 -> ofc C T1 -> ofc C T2 -> ofv V T2 -> type.

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


%%% Reading the state without affecting it


tprd_rd :  tprd (rd ^ ^ CONT) OFC Ov
 	   <- tpct CONT OFC Ov.


%%% Execution

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

tpex_s : tpex ^ (ex_s ^ Ex1) Ok (ofi_ev (ofe_s Oe1)) Of
	  <- 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
	     <- 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
		<- tpex ^ Ex1 Ok (ofi_ev Oe2) Of.

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

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

% Pairs
tpex_pair : tpex ^ (ex_pair ^ Ex1) Ok (ofi_ev (ofe_pair Oe2 Oe1)) Of
	     <- 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
	      <- 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
	    <- 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
	     <- tpex ^ Ex1 Ok (ofi_return Ov1) Of.

tpex_snd : tpex ^ (ex_snd ^ Ex1) Ok (ofi_ev (ofe_snd Oe1)) Of
	    <- 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
	     <- tpex ^ Ex1 Ok (ofi_return Ov2) Of.

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

tpex_app : tpex ^ (ex_app ^ Ex1) Ok (ofi_ev (ofe_app Oe2 Oe1)) Of
 	    <- 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
 	     <- 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
 	     <- tpex ^ Ex1 Ok (ofi_ev (Oe1 V2 Ov2)) Of.

% References

tpex_ref : tpex ^ (ex_ref ^ Ex1) Ok (ofi_ev (ofe_ref Oe1)) Of
 	    <- 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 : ofv V1 T1)) (off_new Of)
 	     <- ({c:cell} {dc:ofc c T1} {a:w} {et : contains c V1 @ a} 
 		   tpct et dc Ov1 -> 
		     ({V : val} {Ov : ofv V T1} eqlemma c Ov dc dc Ov) -> 
		      tpex ^ (Ex1 c ^ et) Ok (ofi_return (ofv_ref dc)) (Of c dc)).

tpex_deref : tpex ^ (ex_deref ^ Ex1) Ok (ofi_ev (ofe_deref Oe1)) Of
  	      <- 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
	       <- tprd Rd1 Oc Ov
	       <- eqlemma C Ov Oc Oc' Ov'
	       <- tpex ^ Ex1 Ok (ofi_return Ov') Of.

tpex_assign : tpex ^ (ex_assign ^ Ex1) Ok (ofi_ev (ofe_assign Oe2 Oe1)) Of
 	       <- 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
 		<- 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 Ovnew (ofv_ref OFC)) Of
		<- tpct Et1 OFC' Ovold
		<- eqlemma _ Ovnew OFC OFC' Ovnew'
 		<- ({a:w} {et2:contains C Vnew @ a} 
 		      tpct et2 OFC' Ovnew'
 		      -> tpex ^ (Ex2 ^ et2) Ok (ofi_return (ofv_unit)) Of).

tpex_seq : tpex ^ (ex_seq ^ Ex1) Ok (ofi_ev (ofe_seq Oe2 Oe1)) Of
	    <- 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
	    <- 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
	     <- tpex ^ Ex2 Ok (ofi_ev (Oe2 V1 Ov1)) Of.

tpex_letv : tpex ^ (ex_letv ^ Ex2) Ok (ofi_ev (ofe_letv Oe2)) Of
	     <- 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
	     <- 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
	     <- tpex ^ Ex1 Ok (ofi_return Ov) Of.

tpex_return : {Ov:ofv _ T1} 
	       tpex ^ (ex_return ^ Ex1) (ofk_; Ok Oc) (ofi_return Ov) Of
	       <- tpex ^ Ex1 Ok (Oc V Ov) Of.

tpex_init : tpex ^ (ex_init ^ Ec1) (ofk_init) (ofi_return Ov) Of
	     <- 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'
	     <- tpct Et1 Oc Ov1
	     <- tpcl Ec2 (off_loc Of Ov1 Oc) Of'.

%%% Evaluation

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

cc : cell.
oc : ofc cc 1.
- : eqlemma cc Ov oc oc Ov .

%block b : 
some {V1 : val} {T1 : tp} {Ov1 : ofv V1 T1}
block {c:cell} {dc : ofc c T1} {a:w} 
	    {et : contains c V1 a} 
	    {d : tpct et dc Ov1}
	    {d' : {V : val} {Ov : ofv V T1} eqlemma c Ov dc dc Ov}.

%block b' :
some  {T2 : tp} {C : cell} {V2 : val} {Oc : ofc C T2} {Ov2 : ofv V2 T2}
block {a:w} 
	     {et2 : contains C V2 a} 
	     {d : tpct et2 Oc Ov2}.

%mode (tpex +P +Ex +Ok +Oi -Of)
 (tpcl +Ec +Of -Of')
 (tpct +Et -Oc -Ov)
 (tprd +Ed -Oc -Ov)
 (tpev +Ev +Oe -Of)
 (eqlemma +C +Ov1 +Oc1 +Oc2 -Ov2).

%worlds (b | b' ) 
 (tpct _ _ _)
 (tpcl _ _ _)
 (tpex _ _ _ _ _)
 (tprd _ _ _)
 (tpev _ _ _)
 (eqlemma _ _ _ _ _).

%total C (eqlemma C _ _ _ _).

%total (Et Ec Ex Ed Ev) 
 (tpct Et _ _)
 (tpcl Ec _ _)
 (tpex _ Ex _ _ _)
 (tprd Ed _ _)
 (tpev Ev _ _).