Changeset 2466
 Timestamp:
 Nov 14, 2012, 7:17:16 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2460 r2466 178 178  whd >(opt_eq_from_res ???? L) % #E destruct 179 179 ] qed. 180 181 182 (* Show how the global environments match up. *) 183 184 lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'. 185 map_partial_All A B P f l H = OK ? l' → 186 All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'. 187 #A #B #P #f #l 188 elim l 189 [ #H #l' #MAP normalize in MAP; destruct // 190  #h #t #IH * #p #H #l' 191 whd in ⊢ (??%? → ?); 192 lapply (refl ? (f h p)) whd in match (proj1 ???); 193 cases (f h p) in ⊢ (???% → %); 194 [ #b #E #MAP cases (bind_inversion ????? MAP) 195 #tl' * #MAP' #E' normalize in E'; destruct 196 % [ %{p} @E  @IH [ @H  @MAP' ] ] 197  #m #_ #X normalize in X; destruct 198 ] 199 ] qed. 200 201 202 definition clight_cminor_matching : clight_program → matching ≝ 203 λp. 204 let tmpuniverse ≝ universe_for_program p in 205 let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in 206 let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in 207 let globals ≝ fun_globals @ var_globals in 208 mk_matching 209 ?? (list init_data × type) (list init_data) 210 (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor) 211 (λv,w. \fst v = w). 212 213 lemma clight_to_cminor_varnames : ∀p,p'. 214 clight_to_cminor p = OK ? p' → 215 prog_var_names … p = prog_var_names … p'. 216 * #vars #fns #main * #vars' #fns' #main' 217 #TO cases (bind_inversion ????? TO) #fns'' * #MAP #E 218 whd in E:(??%%); destruct 219 MAP normalize 220 elim vars 221 [ // 222  * * #id #r * #d #t #tl #IH normalize >IH // 223 ] qed. 224 225 226 lemma clight_to_cminor_matches : ∀p,p'. 227 clight_to_cminor p = OK ? p' → 228 match_program (clight_cminor_matching p) p p'. 229 * #vars #fns #main * #vars' #fns' #main' 230 #TO cases (bind_inversion ????? TO) #fns'' * #MAP #E 231 whd in E:(??%%); destruct 232 % 233 [ MAP whd in match (m_V ?); whd in match (m_W ?); 234 elim vars 235 [ // 236  * * #id #r * #init #ty #tl #IH % 237 [ % // 238  @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/ 239 ] 240 ] 241  @(All2_mp … (map_partial_All_to_All2 … MAP)) MAP 242 * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E 243 normalize in E; destruct 244 <(clight_to_cminor_varnames … TO) 245 % whd 246 % [2: % [2: @TRANSF  skip ]  skip ] 247  % 248 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.