Changeset 3263 for src/joint/TranslateUtils.ma
 Timestamp:
 May 10, 2013, 1:40:31 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r3037 r3263 412 412 { init_ret : call_dest dst 413 413 ; init_params : paramsT dst 414 ; init_stack_size : ℕ 414 ; added_local_stacksize : ℕ 415 ; added_params_stacksize : ℕ 416 ; added_spilled_stacksize : ℕ 415 417 ; added_prologue : list (joint_seq dst globals) 416 418 ; new_regs : list register (* new registers added globally *) … … 499 501 ; pars_def_out_eq : 500 502 joint_if_params … def_out = init_params … data 501 ; ss_def_out_eq : 502 joint_if_stacksize … def_out = init_stack_size … data 503 ; local_ss_def_out_eq : 504 joint_if_local_stacksize … def_out = 505 joint_if_local_stacksize … def_in + added_local_stacksize … data 506 ; params_ss_def_out_eq : 507 joint_if_params_stacksize … def_out = 508 joint_if_params_stacksize … def_in + added_params_stacksize … data 509 ; spilled_ss_def_out_eq : 510 joint_if_spilled_stacksize … def_out = 511 joint_if_spilled_stacksize … def_in + added_spilled_stacksize … data 503 512 ; partition_lbls : partial_partition … f_lbls 504 513 ; partition_regs : partial_partition … f_regs … … 541 550 542 551 definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉. 552 543 553 definition set_entry ≝ 544 554 λglobals: list ident. … … 551 561 (joint_if_params … int_fun) (joint_if_stacksize … int_fun) 552 562 (joint_if_local_stacksize … int_fun) 563 (joint_if_params_stacksize … int_fun) 553 564 (joint_if_code … int_fun) entry (*exit*). 554 565 … … 576 587 (joint_if_luniverse … def) 577 588 runiv 578 (init_ret … data) (init_params … data) (init_stack_size … data) 579 (joint_if_local_stacksize … def) 589 (init_ret … data) (init_params … data) 590 (joint_if_local_stacksize … def + added_local_stacksize … data) 591 (joint_if_params_stacksize … def + added_params_stacksize … data) 592 (joint_if_spilled_stacksize … def + added_spilled_stacksize … data) 580 593 (empty_map ? (joint_statement ??)) 581 594 entry in … … 677 690 add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). 678 691 *) 692 693 include "joint/joint_stacksizes.ma". 694 695 lemma bind_new_P_mp' : ∀R,X,P,Q,m. 696 (∀l,x.P l x → Q l x) → 697 bind_new_P' R X P m → bind_new_P' R X Q m. 698 #R #X #P #Q #m lapply Q Q lapply P P elim m m 699 [ #x #P #Q #H #G @H @G 700  #f #IH #P #Q #H #G #r 701 @IH [3: @(G r) *:] #l @H 702 ] 703 qed. 704 705 lemma joint_transform_monotone_stacksizes : 706 ∀src_g_pars,dst_g_pars : graph_params. 707 (* initialization *) 708 ∀data. 709 ∀p_in. 710 let p_out ≝ b_graph_transform_program src_g_pars dst_g_pars data p_in in 711 stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out). 712 #src #dst #data #p_in 713 whd 714 @list_map_opt_All2 715 [ @(λid_def1,id_def2. 716 match \snd id_def1 with 717 [ Internal f1 ⇒ 718 match \snd id_def2 with 719 [ Internal f2 ⇒ 720 \fst id_def1 = \fst id_def2 ∧ 721 le (joint_if_stacksize … f1) (joint_if_stacksize … f2) 722  _ ⇒ False 723 ] 724  External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False  External _ ⇒ True ] 725 ]) 726  * #id * #f1 * #id' * #f2 normalize nodelta [*: * %] 727 ** #H %{H} % ] 728 @All2_of_map * #id * #f normalize nodelta [2: %] 729 % [%] 730 cases (b_graph_translate ?????) 731 whd in match (jp_functions dst ?); 732 lapply f f 733 generalize in match (?@jp_functions ??); #globals 734 #f_in #f_out * #data' * #regs * #f_lbls * #f_regs * #inst #props 735 whd in match joint_if_stacksize; normalize nodelta 736 @le_plus [ @le_plus ] 737 [ >(spilled_ss_def_out_eq … props) 738  >(params_ss_def_out_eq … props) 739  >(local_ss_def_out_eq … props) 740 ] // 741 qed.
Note: See TracChangeset
for help on using the changeset viewer.