Changeset 2473 for src/joint/linearise.ma
 Timestamp:
 Nov 16, 2012, 6:59:24 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/linearise.ma
r2440 r2473 1 1 include "joint/TranslateUtils.ma". 2 include "common/extraGlobalenvs.ma". 2 3 include "utilities/hide.ma". 3 4 … … 553 554 qed. 554 555 556 557 definition good_local_sigma : 558 ∀p:unserialized_params. 559 ∀globals. 560 ∀g:codeT (mk_graph_params p) globals. 561 (Σl.bool_to_Prop (code_has_label … g l)) → 562 codeT (mk_lin_params p) globals → 563 (label → option ℕ) → Prop ≝ 564 λp,globals,g,entry,c,sigma. 565 sigma entry = Some ? 0 ∧ 566 ∀l,n.sigma l = Some ? n → 567 ∃s. lookup … g l = Some ? s ∧ 568 opt_Exists ? 569 (λls.let 〈lopt, ts〉 ≝ ls in 570 opt_All ? (eq ? l) lopt ∧ 571 ts = graph_to_lin_statement … s ∧ 572 opt_All ? 573 (λnext.Or (sigma next = Some ? (S n)) 574 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 575 (stmt_implicit_label … s)) (nth_opt … n c). 576 555 577 definition linearise_code: 556 578 ∀p : unserialized_params.∀globals. 557 579 ∀g : codeT (mk_graph_params p) globals.code_closed … g → 558 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). 559 (Σc : codeT (mk_lin_params p) globals. 560 code_closed … c ∧ 580 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)) 581 .Σ〈c, sigma〉. 582 good_local_sigma … g entry c sigma ∧ 583 code_closed … c 584 (* ∧ 561 585 ∃ sigma : identifier_map LabelTag ℕ. 562 586 lookup … sigma entry = Some ? 0 ∧ … … 570 594 (λnext.Or (lookup … sigma next = Some ? (S n)) 571 595 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 572 (stmt_implicit_label … s)) (nth_opt … n c) )596 (stmt_implicit_label … s)) (nth_opt … n c)*) 573 597 ≝ 574 598 λp,globals,g,g_prf,entry_sig. … … 583 607 let crev ≝ \snd triple in 584 608 let lbld_code ≝ rev ? crev in 585 mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ]. 586 [ (* done later *) 609 〈filter_labels … (λl.l∈required) lbld_code, lookup … sigma〉 ]. 610 [ cases (graph_visit ????????????????????) 611 (* done later *) 587 612  #i >mem_set_empty * 588 613 3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS) … … 594 619  >commutative_plus change with (? ≤ g) % 595 620 ] 596 lapply (refl … triple) 597 generalize in match triple in ⊢ (???%→%); ** 598 #visited #required #generated #EQtriple 599 >EQtriple in H ⊢ %; normalize nodelta **** 621 ** 622 #visited #required #generated normalize nodelta **** 600 623 #entry_O #req_vis #last_fin #labels_in_req #sigma_prop 601 % >EQtriple 602 [ #i #s 624 % 625 [ % [assumption] 626 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) 627 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 628 % [2: % [ assumption ] ] 629 >nth_opt_filter_labels in ⊢ (???%); 630 >nth_opt_is_stmt >m_return_bind whd >m_return_bind 631 % [ % ] 632 [ elim (lbl ∈ required) % 633  % 634  lapply succ_is_in 635 lapply (refl … (stmt_implicit_label … stmt)) 636 cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %] 637 #next #EQ_next * 638 [ #H %1{H} ] 639 #H %2 640 >nth_opt_filter_labels >H % 641 ] 642  #i #s 603 643 >stmt_at_filter_labels #EQ 604 644 % … … 628 668 ] 629 669 ] 630 %{visited} % [assumption] 631 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) 632 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 633 % [2: % [ assumption ] ] 634 >nth_opt_filter_labels in ⊢ (???%); 635 >nth_opt_is_stmt >m_return_bind whd >m_return_bind 636 % [ % ] 637 [ elim (lbl ∈ required) % 638  % 639  lapply succ_is_in 640 lapply (refl … (stmt_implicit_label … stmt)) 641 cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %] 642 #next #EQ_next * 643 [ #H %1{H} ] 644 #H %2 645 >nth_opt_filter_labels >H % 646 ] 647 qed. 648 649 (* Paolo: for now I'm leaving the closed graph stuff out, waiting for it to 650 be done on all passes *) 670 qed. 671 651 672 definition linearise_int_fun : 652 673 ∀p : unserialized_params. 653 674 ∀globals. 654 joint_closed_internal_function (mk_graph_params p) globals → 655 joint_closed_internal_function (mk_lin_params p) globals 675 ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals 676 .Σ〈fn_out : joint_closed_internal_function (mk_lin_params p) globals, 677 sigma : ?〉. 678 good_local_sigma … (joint_if_code … fn_in) (joint_if_entry … fn_in) 679 (joint_if_code … fn_out) sigma 656 680 (* ∃sigma : identifier_map LabelTag ℕ. 657 681 let g ≝ joint_if_code ?? (pi1 … fin) in … … 669 693 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 670 694 (stmt_implicit_label … s)) (nth_opt … n c)*) ≝ 671 λp,globals,f_sig.let f_in ≝ pi1 … f_sig in 672 «mk_joint_internal_function (mk_lin_params p) globals 673 (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in) 674 (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in) 675 (joint_if_stacksize ?? f_in) 676 (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in)) 677 0 0 (* exit is dummy! *), ?». [2,4:// ] 678 elim (linearise_code ?????) #c * #code_closed 679 [3: #_ assumption ] 680 @hide_prf 681 * #sigma * #O_in #sigma_prop 682 >lin_code_has_point 683 elim (sigma_prop … O_in) #s * #_ 684 cases c 685 [1,3: * 686 *: #hd #tl #_ % 695 λp,globals,f_sig. 696 let code_sigma ≝ linearise_code … 697 (joint_if_code … f_sig) 698 (pi2 … f_sig) 699 (joint_if_entry … f_sig) in 700 let code ≝ \fst code_sigma in 701 let sigma ≝ \snd code_sigma in 702 let entry : Σpt.bool_to_Prop (code_has_point … code pt) ≝ «0, hide_prf ??» in 703 〈«mk_joint_internal_function (mk_lin_params p) globals 704 (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) 705 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig) 706 (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?», 707 sigma〉. 708 normalize nodelta 709 cases (linearise_code ?????) * #code #sigma normalize nodelta * #H1 #H2 710 [ @H2 711  @H1 712  cases H1 #H3 #H4 elim (H4 … H3) 713 #s * #_ >lin_code_has_point cases code 714 [ *  #hd #tl #_ % ] 687 715 ] 688 716 qed. … … 690 718 definition linearise : ∀p : unserialized_params. 691 719 program (joint_function (mk_graph_params p)) ℕ → 692 program (joint_function (mk_lin_params p)) ℕ ≝ 720 program (joint_function (mk_lin_params p)) ℕ 721 ≝ 693 722 λp,pr.transform_program ??? pr 694 (λglobals.transf_fundef ?? (linearise_int_fun p globals)). 723 (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))). 724 725 726 definition good_sigma : 727 ∀p:unserialized_params. 728 ∀prog_in : joint_program (mk_graph_params p). 729 ((Σi.is_internal_function_of_program … prog_in i) → label → option ℕ) → Prop ≝ 730 λp,prog_in,sigma. 731 let prog_out ≝ linearise … prog_in in 732 ∀i. 733 let fn_in ≝ prog_if_of_function ?? prog_in i in 734 let fn_out ≝ prog_if_of_function ?? prog_out «i, hide_prf ??» in 735 let sigma_local ≝ sigma i in 736 good_local_sigma ?? (joint_if_code ?? fn_in) (joint_if_entry … fn_in) 737 (joint_if_code ?? fn_out) sigma_local. 738 @if_propagate @(pi2 … i) 739 qed. 740 741 lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma. 742 #p #prog 743 letin sigma ≝ 744 (λi. 745 let fn_in ≝ prog_if_of_function ?? prog i in 746 \snd (linearise_int_fun … fn_in)) 747 %{sigma} 748 * #i #i_prf >(prog_if_of_function_transform … i_prf) 749 normalize nodelta 750 cases (linearise_int_fun ???) * #fn_out #sigma_loc 751 normalize nodelta #prf @prf 752 qed.
Note: See TracChangeset
for help on using the changeset viewer.