Changeset 2452 for src/joint/lineariseProof.ma
 Timestamp:
 Nov 12, 2012, 12:50:21 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2447 r2452 302 302 whd in move_st1_st1'; 303 303 letin lin_prog ≝ (linearise ? graph_prog) 304 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … 304 305 cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun 306 307 cases (linearise_code_spec … p' graph_prog graph_fun 308 (joint_if_entry … graph_fun)) 309 * #lin_code_closed #sigma_entry_is_zero #sigma_spec 310 lapply (sigma_spec 311 (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1))) 312 sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) 2: skip ] 313 sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec; 314 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] 315 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved 316 #related_lin_stm_graph_stm 317 inversion (stmt_implicit_label ???) 318 [ whd in match (opt_All ???); #stmt_implicit_spec #_ 319 letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … 305 320 (ev_genv (lin_prog_params p p' lin_prog)) 306 321 (linearise_status_fun … sigma st1 wf_st1)) 307 whd in st2'; 308 whd in match (fetch_statement ?????) in st2'; 309 >fetch_function_sigma_commute in st2'; 310 whd in match (fetch_function ????) in st2'; 311 XXX 312 check fetch_statement 313 CSC 314 %{} 315 316 whd in classified_st1_cl; 317 whd in classified_st1_cl:(??%?); 318 inversion (fetch_statement ?????) in classified_st1_cl; 319 320 <classified_st1_cl cl 321 whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ] ?); 322 inversion (fetch_statement ?????) 323 324 inversion (fetch_statement ?????) 325 qed. 322 check st2_opt' 323 cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2') 324 [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' 325 normalize nodelta in st2_spec'; st2_opt' 326 %{st2'} %{(taaf_step … (taa_base …) …)} 327 [ cases daemon (* TODO, together with the previous one? *) 328  @st2_spec' ] 329 %[%] [%] 330 [ whd 331 whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec'; 332 whd in move_st1_st1':(??%?); 333 cut (fetch_statement (graph_prog_params p p' graph_prog) (graph_prog_params … graph_prog) … (ev_genv (graph_prog_params … graph_prog)) … (pc … st1) = OK ? 〈graph_fun,graph_stmt〉) 334 [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ] 335 #fetch_statement_ok >fetch_statement_ok in move_st1_st1'; 336 whd in ⊢ (??%? → ??%? → ?); normalize nodelta 337 inversion graph_stmt in stmt_implicit_spec; normalize nodelta 338 [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ] 339 XXXXXXXXXX siamo qua, caso GOTO e RETURN 340  cases daemon (* TODO, after the definition of label_rel, trivial *) ] 341 ] 342  .... 343 qed.
Note: See TracChangeset
for help on using the changeset viewer.