Changeset 2529 for src/joint/linearise.ma
 Timestamp:
 Dec 4, 2012, 6:16:25 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/linearise.ma
r2481 r2529 173 173 ] n_prf 174 174 ] (chop_ok ? (λx.x∈visited) visiting). 175 (* cases daemon qed. *)175 (* cases daemon qed. *) 176 176 whd 177 177 [ (* base case, visiting is all visited *) … … 555 555 qed. 556 556 557 558 557 definition good_local_sigma : 559 558 ∀p:unserialized_params. … … 565 564 λp,globals,g,entry,c,sigma. 566 565 sigma entry = Some ? 0 ∧ 566 (∀l,n.point_of_label … c l = Some ? n → sigma l = Some ? n) ∧ 567 567 ∀l,n.sigma l = Some ? n → 568 ∃s. lookup … g l = Some ? s ∧ 569 opt_Exists ? 570 (λls.let 〈lopt, ts〉 ≝ ls in 571 opt_All ? (eq ? l) lopt ∧ 572 ts = graph_to_lin_statement … s ∧ 573 opt_All ? 574 (λnext.Or (sigma next = Some ? (S n)) 575 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 576 (stmt_implicit_label … s)) (nth_opt … n c). 568 ∃s. stmt_at … g l = Some ? s ∧ 569 All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧ 570 opt_All ? 571 (λnext.Or (sigma next = Some ? (S n)) 572 (stmt_at … c (S n) = Some ? (GOTO … next))) 573 (stmt_implicit_label … s) ∧ 574 stmt_at … c n = Some ? (graph_to_lin_statement … s). 577 575 578 576 definition linearise_code: … … 624 622 #entry_O #req_vis #last_fin #labels_in_req #sigma_prop 625 623 % 626 [ % [assumption] 627 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) 628 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 629 % [2: % [ assumption ] ] 630 >nth_opt_filter_labels in ⊢ (???%); 631 >nth_opt_is_stmt >m_return_bind whd >m_return_bind 632 % [ % ] 633 [ elim (lbl ∈ required) % 634  % 635  lapply succ_is_in 636 lapply (refl … (stmt_implicit_label … stmt)) 637 cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %] 638 #next #EQ_next * 639 [ #H %1{H} ] 640 #H %2 641 >nth_opt_filter_labels >H % 624 [ % [ % [assumption]] 625 #lbl #n 626 [ change with (If ? then with prf do ? else ? = ? → ?) 627 @If_elim [2: #_ #ABS destruct(ABS) ] 628 #H lapply H 629 >occurs_exactly_once_filter_labels 630 elim (true_or_false_Prop … (occurs_exactly_once ?? lbl ?)) 631 [1,2: #H1 >H1 *:] [2: * ] 632 elim (true_or_false_Prop … (lbl ∈ required)) #H2 >H2 * 633 lapply (in_map_domain … visited lbl) >(req_vis … H2) 634 * #n_lbl #EQsigma 635 elim (sigma_prop … EQsigma) #_ * #stmt ** #_ #EQnth_opt #_ 636 >(nth_opt_index_of_label ???? n_lbl (graph_to_lin_statement … stmt) H) 637 [ normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption 638  >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind 639 >H2 % 640 ] 641  #eq_lookup elim (sigma_prop ?? eq_lookup) 642 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 643 % [2: % [ % [ % [ assumption ]]] ] 644 [ @All_append 645 [ lapply succ_is_in elim (stmt_implicit_label ???) [ * % ] 646 #nxt #nxt_spec % [2: %] cases nxt_spec nxt_spec 647 [ #EQ >EQ % #ABS destruct(ABS) 648  #goto_in lapply (in_map_domain … visited nxt) 649 >req_vis [ * #n #EQ >EQ % #ABS destruct(ABS) ] 650 @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 651 whd in ⊢ (??%?); >goto_in % 652 ] 653  <graph_to_lin_labels @(All_mp … (labels_in_req …)) 654 [ #lbl #H 655 lapply (in_map_domain … visited lbl) >(req_vis … H) * #n #EQ >EQ % #ABS destruct(ABS) 656  whd in ⊢ (??%?); >nth_opt_is_stmt %  657 ] 658 ] 659  lapply succ_is_in 660 cases (stmt_implicit_label … stmt) [#_ %] 661 #next * 662 [ #H %1{H} ] 663 #H %2 664 >stmt_at_filter_labels whd in ⊢ (??%?); >H % 665  >stmt_at_filter_labels whd in ⊢ (??%?); >nth_opt_is_stmt % 666 ] 642 667 ] 643 668  #i #s … … 711 736 [ @H2 712 737  @H1 713  cases H1 #H3 #H4 elim (H4… H3)714 #s * #_ >lin_code_has_point cases code715 [ * #hd #tl #_ % ]738  cases H1 * #H3 #H4 #H5 elim (H5 … H3) 739 #s *** #_ #_ #_ >lin_code_has_point cases code 740 [ #ABS normalize in ABS; destruct(ABS)  #hd #tl #_ % ] 716 741 ] 717 742 qed. … … 724 749 (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))). 725 750 726 751 (* 727 752 definition good_sigma : 728 753 ∀p:unserialized_params. … … 742 767 #p #prog 743 768 letin sigma ≝ 744 (λi : Σi.is_internal_function_of_program … prog i. 745 let fn_in ≝ if_of_function … i in 769 (λi : Σi.is_internal_function_of_program … prog i. let fn_in ≝ if_of_function … i in 746 770 \snd (linearise_int_fun … fn_in)) 747 771 %{sigma} … … 751 775 normalize nodelta #prf @prf 752 776 qed. 777 *)
Note: See TracChangeset
for help on using the changeset viewer.