Changeset 3046
- Timestamp:
- Mar 30, 2013, 1:11:01 AM (8 years ago)
- Location:
- src/Clight
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/SwitchAndLabel.ma
r3044 r3046 89 89 ] qed. 90 90 91 lemma interactive_switch_step : ∀ge,ge'. 92 switch_removal_globals ? fundef_switch_removal ge ge' → 93 ∀s1,s1',o,k. 94 exec_step ge s1 = Interact … o k → 95 switch_state_sim ge s1 s1' → 96 ∃k'. 97 exec_step ge' s1' = Interact … o k' ∧ 98 ∀i. ∃tr,s2. 99 k i = Value … 〈tr,s2〉 ∧ 100 ∃s2'. 101 k' i = Value … 〈tr,s2'〉 ∧ 102 switch_state_sim ge s2 s2'. 103 #ge #ge' #RG #s1 #s1' #o #k #EX 104 cases (exec_step_interaction … EX) 105 #vf * #fn * #argtys * #retty * #vargs * #k' * #m #E 106 destruct 107 #S inversion S 108 [1,3,4: #H1 #H2 #H3 #H4 destruct 109 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 110 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 destruct 111 ] 112 #s_vf #s_fd #s_args #s_k #s_k_ext #s_m #s_m_ext #s_writeable #s_me #s_H 113 #E1 #E2 #E3 destruct 114 whd in EX:(??%?); 115 @(bindIO_res_interact ?????????? EX) -EX 116 #vs #CHECK #EX whd in EX:(??%?); destruct 117 % [2: % 118 [ whd in ⊢ (??%?); 119 >CHECK in ⊢ (??%?); 120 whd in ⊢ (??%?); 121 @refl 122 | #i 123 % [2: % [2: % 124 [ @refl 125 | % [2: % 126 [ @refl 127 | @(sws_returnstate … s_me) // ] 128 | skip ] ] | skip ] 129 ] ]| skip 130 ] qed. 131 132 lemma Value_eq_l : ∀tr,s,tr',s'. 133 Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 → 134 tr = tr'. 135 #tr #s #tr' #s' #E destruct % 136 qed. 137 138 lemma Value_eq_r : ∀tr,s,tr',s'. 139 Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 → 140 s = s'. 141 #tr #s #tr' #s' #E destruct % 142 qed. 91 143 92 144 let corec build_exec … … 121 173 cases (switch_removal_correction … SRG … S1 EX1) 122 174 #n1 #A1 123 cases (after_n_result … A1) #tr1' * #s2' * * #E destruct (E) #S1' #A1'175 cases (after_n_result … A1) #tr1' * #s2' * * #E @(match E with [refl ⇒ ?]) #S1' #A1' 124 176 cases (steps_with_labels … RG … S2 A1') 125 177 #n #AF cases (after_inv clight_fullexec ????? AF) #tr' * #s' * * #TWL #S' … … 130 182 @(build_exec … SRG RG … S1' S') >E1' in NW1; // 131 183 | #r <(final_related … S') <(switch_final_related … S1') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?); 132 >(exec_e_step_not_final ?? clight_fullexec … E1) #E destruct184 >(exec_e_step_not_final ?? clight_fullexec … E1) #E' destruct 133 185 ] 134 186 | #E1 135 187 cases (extract_interact ?? clight_fullexec … E1) 136 188 #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk 137 cases (interactive_step_with_labels … RG … EX1 S) 138 #k2' * #EX2 #H2 @(match sym_eq … EX2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%); 189 cases (interactive_switch_step … SRG … EX1 S1) #k2' * #EX2 #H2 190 cases (interactive_step_with_labels … RG … EX2 S2) 191 #k3' * #EX3 #H3 @(match sym_eq … EX3 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%); 139 192 @swl_interact 140 #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S' 193 #i cases (H3 i) #tr2 * #s2' * #K2 * #tr3 * #s3' * * #K3 #TR2 #S2' 194 cases (H2 i) #tr1 * #s1' * #K1 * #s2x' * @(match sym_eq … K2 with [refl ⇒ ?]) #Ex 195 @(match (Value_eq_r … Ex) with [refl ⇒ ?]) #S1' 141 196 lapply (NWk i) 142 @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?]) 143 @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????); 144 cases (is_final s2') 145 [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec // 146 inversion NW' 147 [ #H1 #H2 #H3 #H4 #H5 destruct 148 | #H7 #H8 #H9 #H10 #H11 #H12 destruct // 149 | #H14 #H15 #H16 #H17 #H18 destruct 197 @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); 198 @(match sym_eq … (switch_final_related … S1') with [refl ⇒ ?]) @(match sym_eq … (final_related … S2') with [refl ⇒ ?]) 199 @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge3 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); 200 @(match sym_eq … K3 with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????); 201 cases (is_final s3') 202 [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) 203 [ destruct // 204 | @build_exec // 205 inversion NW' 206 [ #H1 #H2 #H3 #H4 #H5 destruct 207 | #H7 #H8 #H9 #H10 #H11 #H12 destruct // 208 | #H14 #H15 #H16 #H17 #H18 destruct 209 ] 150 210 ] 151 | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //211 | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) destruct // 152 212 ] 153 213 ] qed. -
src/Clight/switchRemoval.ma
r3044 r3046 2000 2000 ∀ssc_writeable. 2001 2001 ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable. 2002 (match ssc_fd with2002 switch_cont_sim (match ssc_fd with 2003 2003 [ CL_Internal ssc_f ⇒ 2004 switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext2005 | _ ⇒ True ])→2004 (\snd (function_switch_removal ssc_f)) 2005 | _ ⇒ [ ] ]) ssc_k ssc_k_ext → 2006 2006 switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m) 2007 2007 (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext) … … 2921 2921 [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl 2922 2922 %2{sss_writeable … sss_mem_hyp} 2923 cases called_fundef 2924 [ 2: #id #tl #ty @I 2925 | 1: #called_function whd 2926 cut (sss_func_tr = \fst (function_switch_removal sss_func)) 2927 [ 1: <sss_func_hyp @refl ] #H >H -H 2928 cut (sss_new_vars = \snd (function_switch_removal sss_func)) 2929 [ 1: <sss_func_hyp @refl ] #H >H -H 2930 @(swc_call … sss_k_hyp) try assumption 2931 <sss_func_hyp @refl ] 2923 cut (sss_func_tr = \fst (function_switch_removal sss_func)) 2924 [ 1: <sss_func_hyp @refl ] #H >H -H 2925 cut (sss_new_vars = \snd (function_switch_removal sss_func)) 2926 [ 1: <sss_func_hyp @refl ] #H >H -H 2927 @(swc_call … sss_k_hyp) try assumption 2928 <sss_func_hyp @refl 2932 2929 | 2: #ret_expr #Hexec_ret_expr 2933 2930 cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret … … 2938 2935 [ 1: <sss_func_hyp @refl ] #H >H -H 2939 2936 @(sws_callstate … sss_writeable … sss_mem_hyp) 2940 cases called_fundef 2941 [ 2: #id #tl #ty @I 2942 | 1: #called_function whd 2943 cut (sss_func_tr = \fst (function_switch_removal sss_func)) 2944 [ 1: <sss_func_hyp @refl ] #H >H -H 2945 cut (sss_new_vars = \snd (function_switch_removal sss_func)) 2946 [ 1: <sss_func_hyp @refl ] #H >H -H 2947 @(swc_call … sss_k_hyp) try assumption 2948 <sss_func_hyp @refl ] ] 2937 cut (sss_func_tr = \fst (function_switch_removal sss_func)) 2938 [ 1: <sss_func_hyp @refl ] #H >H -H 2939 cut (sss_new_vars = \snd (function_switch_removal sss_func)) 2940 [ 1: <sss_func_hyp @refl ] #H >H -H 2941 @(swc_call … sss_k_hyp) try assumption 2942 <sss_func_hyp @refl ] 2949 2943 | 4: (* Sequence statement *) 2950 2944 #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec)
Note: See TracChangeset
for help on using the changeset viewer.