 Timestamp:
 Feb 22, 2013, 8:04:38 PM (7 years ago)
 Location:
 src/joint
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r2688 r2712 446 446 (p : params) (globals : list ident) (def : joint_internal_function p globals) 447 447 : Prop ≝ 448 { unique_cost_labels : 449 ∀l1,l2,c,nxt1,nxt2. 450 stmt_at … (joint_if_code … def) l1 = 451 Some … (sequential … (COST_LABEL … c) nxt1) → 452 stmt_at … (joint_if_code … def) l2 = 453 Some … (sequential … (COST_LABEL … c) nxt2) → 454 l1 = l2 455 ; entry_costed : 448 { entry_costed : 456 449 ∃l,nxt. 457 450 stmt_at … (joint_if_code … def) (joint_if_entry … def) = 458 451 Some … (sequential … (COST_LABEL … l) nxt) 452 ; entry_unused : 453 let entry ≝ pi1 … (joint_if_entry … def) in 454 let code ≝ joint_if_code … def in 455 forall_statements_i … 456 (λpt,stmt.stmt_forall_labels … (λlbl.point_of_label … code lbl ≠ Some ? entry) stmt ∧ 457 stmt_forall_succ … (λnxt.point_of_succ … pt nxt ≠ entry) stmt) code 459 458 ; code_is_closed : code_closed … (joint_if_code … def) 460 459 ; code_is_in_universe : 
src/joint/linearise.ma
r2708 r2712 661 661 ∀g : codeT (mk_graph_params p) globals.code_closed … g → 662 662 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)) 663 .Σ〈c, sigma〉. 663 .Σc_sigma. 664 let c ≝ \fst c_sigma in 665 let sigma ≝ \snd c_sigma in 664 666 good_local_sigma … g entry c sigma ∧ 665 667 code_closed … c … … 809 811 ] 810 812 qed. 811 *)812 813 813 814 definition linearise_int_fun : … … 815 816 ∀globals. 816 817 ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals 817 .Σ 〈fn_out : joint_closed_internal_function (mk_lin_params p) globals,818 sigma : ?〉.818 .Σfn_out_sigma : 819 (joint_closed_internal_function (mk_lin_params p) globals × ?). 819 820 good_local_sigma … (joint_if_code … fn_in) (joint_if_entry … fn_in) 820 (joint_if_code … fn_out) sigma821 (joint_if_code … (\fst fn_out_sigma)) (\snd fn_out_sigma) 821 822 (* ∃sigma : identifier_map LabelTag ℕ. 822 823 let g ≝ joint_if_code ?? (pi1 … fin) in … … 837 838 let code_sigma ≝ linearise_code … 838 839 (joint_if_code … f_sig) 839 ( pi2 … f_sig)840 (code_is_closed … (pi2 … f_sig)) 840 841 (joint_if_entry … f_sig) in 841 842 let code ≝ \fst code_sigma in 842 843 let sigma ≝ \snd code_sigma in 843 844 let entry : Σpt.bool_to_Prop (code_has_point … code pt) ≝ «0, hide_prf ??» in 844 〈«mk_joint_internal_function (mk_lin_params p) globals845 «〈«mk_joint_internal_function (mk_lin_params p) globals 845 846 (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) 846 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig) 847 (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?», 848 sigma〉. 849 normalize nodelta 850 cases (linearise_code ?????) * #code #sigma normalize nodelta * #H1 #H2 851 [ @H2 852  @H1 853  cases H1 * #H3 #H4 #H5 elim (H5 … H3) 847 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) 848 (joint_if_stacksize ?? f_sig) code entry (* exit is dummy! *), hide_prf ??», 849 sigma〉, proj1 ?? (pi2 ?? code_sigma)». 850 [2: whd in match code; cases code_sigma code_sigma * #code #sigma 851 normalize nodelta *** #H3 #H4 #H5 852 elim (H5 … H3) 854 853 #s ** #_ #_ >lin_code_has_point cases code 855 [ cases s [ * [ #s'  #a #ltrue ] #nxt  #s'  * ] 856 [ * #ABS #_  * [ * #ABS #_  #ABS ]  #ABS ] normalize in ABS; destruct(ABS) 857  #hd #tl #_ % 854 [ cases s [ * [ #cost  #f #args #dest  #a #ltrue  #s' ] #nxt  #s'  * ] 855 [1,2,4: * #EQnth_opt #_ 3: * [ * ] #EQnth_opt [ #_ ] 5: #EQnth_opt ] 856 normalize in EQnth_opt; destruct(EQnth_opt) 857  #hd #tl #_ #_ % 858 ] 859  @hide_prf % 860 (* TODO *) 861 [ cases daemon 862  cases daemon 863  @(proj2 ?? (pi2 ?? code_sigma)) 864  cases daemon 858 865 ] 859 866 ]
Note: See TracChangeset
for help on using the changeset viewer.