%%% Simply Typed Lambda Calculus w/ small-step, allocation semantics
%%% Author: Matthew Fluet (June 2005)
%%% preservation.elf

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Preservation: If M1 ==> M2 and |- M1, then |- M2.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
pres           : step S1 E1 S2 E2 -> 
                 |-stwf S1 ST1 ->
                 |-exp ST1 E1 T
                  -> sttp_extend ST1 ST2 ->
                     |-stwf S2 ST2 ->
                     |-exp ST2 E2 T -> type.
%mode pres +DStep +DStTcWf1 +DExpTc1 -DStExtend -DStTcWf2 -DExpTc2.

-lam_alloc     : pres (lam_alloc_step DStAlloc)
                      DStTcWf
                      (|-exp_lam DExpTcF)
                      DSttpExtend
                      DStTcWf'
                      DExpTcL
		  <- pres_alloc DStTcWf 
		                (|-val_lam DExpTcF)
		                DStAlloc 
		                DSttpExtend
                                DStTcWf'
                                DExpTcL.
-app_ctxt1     : pres (app_ctxt1_step DStep)
                      DStTcWf
                      (|-exp_app DExpTcE2 DExpTcE1)
                      DSttpExtend
                      DStTcWf'
                      (|-exp_app DExpTcE2' DExpTcE1')
		  <- pres DStep
                          DStTcWf
                          DExpTcE1
                          DSttpExtend
		          DStTcWf'
                          DExpTcE1'
		  <- sttp_weak_|-exp DExpTcE2 DSttpExtend DExpTcE2'.
-app_ctxt2     : pres (app_ctxt2_step DStep)
                      DStTcWf
                      (|-exp_app DExpTcE2 DExpTcE1)
                      DSttpExtend
                      DStTcWf'
                      (|-exp_app DExpTcE2' DExpTcE1')
		  <- pres DStep
                          DStTcWf
                          DExpTcE2
                          DSttpExtend
		          DStTcWf'
                          DExpTcE2'
		  <- sttp_weak_|-exp DExpTcE1 DSttpExtend DExpTcE1'.
%% Church-style
-app_beta      : pres (app_beta_step DStLookupL1)
                      DStTcWf
                      (|-exp_app DExpTcL2
                                 (|-exp_loc (|-loc_ DSttpLookupL1)))
                      DSttpExtend
                      DStTcWf
                      DExpTcF1'L2
		  <- sttp!extend_refl _ DSttpExtend
		  <- pres_|-st_inversion DStTcWf 
                                         DSttpLookupL1
                                         DStLookupL1 
                                         DExpTcLam
		  <- pres_|-val_lam_inversion DExpTcLam DExpTcF1'*
		  <- pres_var DExpTcF1'* DExpTcL2 DExpTcF1'L2.
%% Curry-style
% -app_beta      : pres (app_beta_step DStLookupL1)
%                       DStTcWf
%                       (|-exp_app DExpTcL2
%                                  (|-exp_loc (|-loc_ DSttpLookupL1)))
%                       DSttpExtend
%                       DStTcWf
%                       DExpTcF1'L2
%                   <- sttp!extend_refl _ DSttpExtend
%                   <- pres_|-st_inversion DStTcWf 
%                                          DSttpLookupL1
%                                          DStLookupL1 
%                                          (|-val_lam DExpTcF1'*)
%                   <- pres_var DExpTcF1'* DExpTcL2 DExpTcF1'L2.
-unit_alloc    : pres (unit_alloc_step DStAlloc)
                      DStTcWf
                      (|-exp_unit)
                      DSttpExtend
                      DStTcWf'
                      DExpTcL
		  <- pres_alloc DStTcWf 
		                (|-val_unit)
		                DStAlloc 
		                DSttpExtend
                                DStTcWf'
                                DExpTcL.
-letunit_ctxt  : pres (letunit_ctxt_step DStep)
                      DStTcWf
                      (|-exp_letunit DExpTcE2 DExpTcE1)
                      DSttpExtend
                      DStTcWf'
                      (|-exp_letunit DExpTcE2' DExpTcE1')
		  <- pres DStep
                          DStTcWf
                          DExpTcE1
                          DSttpExtend
		          DStTcWf'
                          DExpTcE1'
		  <- sttp_weak_|-exp DExpTcE2 DSttpExtend DExpTcE2'.
-letunit_beta  : pres (letunit_beta_step _)
                      DStTcWf
                      (|-exp_letunit DExpTcE2 DExpTcE1)
                      DSttpExtend
                      DStTcWf
                      DExpTcE2
		  <- sttp!extend_refl _ DSttpExtend.
-pair_ctxt1    : pres (pair_ctxt1_step DStep)
                      DStTcWf
                      (|-exp_pair DExpTcE2 DExpTcE1)
                      DSttpExtend
                      DStTcWf'
                      (|-exp_pair DExpTcE2' DExpTcE1')
		  <- pres DStep
                          DStTcWf
                          DExpTcE1
                          DSttpExtend
		          DStTcWf'
                          DExpTcE1'
		  <- sttp_weak_|-exp DExpTcE2 DSttpExtend DExpTcE2'.
-pair_ctxt2    : pres (pair_ctxt2_step DStep)
                      DStTcWf
                      (|-exp_pair DExpTcE2 DExpTcE1)
                      DSttpExtend
                      DStTcWf'
                      (|-exp_pair DExpTcE2' DExpTcE1')
		  <- pres DStep
                          DStTcWf
                          DExpTcE2
                          DSttpExtend
		          DStTcWf'
                          DExpTcE2'
		  <- sttp_weak_|-exp DExpTcE1 DSttpExtend DExpTcE1'.
-pair_alloc    : pres (pair_alloc_step DStAlloc)
                      DStTcWf
                      (|-exp_pair (|-exp_loc DLocTcL2) (|-exp_loc DLocTcL1))
		      DSttpExtend
                      DStTcWf'
                      DExpTcL
		  <- pres_alloc DStTcWf
		                (|-val_pair DLocTcL2 DLocTcL1)
                                DStAlloc
                                DSttpExtend
                                DStTcWf'
                                DExpTcL.
-letpair_ctxt  : pres (letpair_ctxt_step DStep)
                      DStTcWf
                      (|-exp_letpair DExpTcF2 DExpTcE1)
                      DSttpExtend
                      DStTcWf'
                      (|-exp_letpair DExpTcF2' DExpTcE1')
		  <- pres DStep
                          DStTcWf
                          DExpTcE1
                          DSttpExtend
		          DStTcWf'
                          DExpTcE1'
		  <- ({x}{DVarTcX: |-var x Tx}
                      {y}{DVarTcY: |-var y Ty}
			sttp_weak_|-exp (DExpTcF2 x DVarTcX y DVarTcY)
                                        DSttpExtend 
			                (DExpTcF2' x DVarTcX y DVarTcY)).
-letpair_beta  : pres (letpair_beta_step DStLookup)
                      DStTcWf
                      (|-exp_letpair DExpTcF2**
                                     (|-exp_loc (|-loc_ DSttpLookup)))
                      DSttpExtend
                      DStTcWf
                      DExpTcF2LxLy
		  <- sttp!extend_refl _ DSttpExtend
		  <- pres_|-st_inversion DStTcWf
                                         DSttpLookup
                                         DStLookup
                                         (|-val_pair DLocTcLy DLocTcLx)
		  <- ({x}{DVarTcX: |-var x Tx}
			pres_var (DExpTcF2** x DVarTcX) 
                                 (|-exp_loc DLocTcLy)
                                 (DExpTcF2*Ly x DVarTcX))
		  <- pres_var DExpTcF2*Ly (|-exp_loc DLocTcLx) DExpTcF2LxLy.
%terminates DStep (pres DStep _ _ _ _ _).
%worlds () (pres _ _ _ _ _ _).
%covers pres +DStep +DSt1TcWf +DE1Tc -DStEx -DSt2TcWf -DE2Tc.
%total DStep (pres DStep _ _ _ _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Preservation: If M1 ==>* M2 and |- M1, then |- M2.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
pres*          : step* S1 E1 S2 E2 -> 
                 |-stwf S1 ST1 ->
                 |-exp ST1 E1 T
                  -> sttp_extend ST1 ST2 ->
                     |-stwf S2 ST2 ->
                     |-exp ST2 E2 T -> type.
%mode pres* +DSteps +DStTcWf1 +DExpTc1 -DStExtend -DStTcWf2 -DExpTc2.

-refl          : pres* (refl_step*)
                       DStTcWf
                       DExpTc
                       DSttpExtend
                       DStTcWf
                       DExpTc
		  <- sttp!extend_refl _ DSttpExtend.
-trans         : pres* (trans_step* DSteps23 DSteps12)
                       DStTcWf1
		       DExpTc1
                       DSttpExtend13
                       DStTcWf3
                       DExpTc3
		  <- pres* DSteps12 DStTcWf1 DExpTc1 DSttpExtend12 DStTcWf2 DExpTc2
		  <- pres* DSteps23 DStTcWf2 DExpTc2 DSttpExtend23 DStTcWf3 DExpTc3
		  <- sttp!extend_trans DSttpExtend12 DSttpExtend23 DSttpExtend13.
-step          : pres* (step_step* DStep)
                       DStTcWf
                       DExpTc
                       DSttpExtend'
                       DStTcWf'
                       DExpTc'
		  <- pres DStep DStTcWf DExpTc DSttpExtend' DStTcWf' DExpTc'.

%terminates DSteps (pres* DSteps _ _ _ _ _).
%worlds () (pres* _ _ _ _ _ _).
%covers pres* +DSteps +DSt1TcWf +DE1Tc -DStEx -DSt2TcWf -DE2Tc.
%total DSteps (pres* DSteps _ _ _ _ _).