 Timestamp:
 Mar 26, 2013, 7:13:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r2946 r2970 270 270 *) 271 271 272 definition append_seq_list :273 ∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) →274 bind_step_block p g ≝275 λp,g,bbl,bl.276 ! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉.277 278 272 (* 279 273 definition insert_epilogue ≝ … … 463 457 464 458 definition get_first_costlabel : ∀p,g. 465 joint_closed_internal_function p g → costlabel × (succ p)≝459 joint_closed_internal_function p g → costlabel ≝ 466 460 λp,g,def. 467 461 match stmt_at … (joint_if_code … def) (joint_if_entry … def) … … 471 465 [ sequential s' nxt ⇒ 472 466 match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with 473 [ COST_LABEL c ⇒ λ_. 〈c, nxt〉467 [ COST_LABEL c ⇒ λ_.c 474 468  _ ⇒ λabs.⊥ 475 469 ] … … 487 481 (∀x.bool_to_Prop (uniqueb … (f x))) ∧ 488 482 (∀x1,x2,y.y ∈ f x1 → y ∈ f x2 → x1 = x2). 483 484 definition not_emptyb : ∀X.list X → bool ≝ 485 λX,l.match l with [ nil ⇒ false  cons _ _ ⇒ true]. 489 486 490 487 record b_graph_translate_props … … 502 499 ; ss_def_out_eq : 503 500 joint_if_stacksize … def_out = init_stack_size … data 504 ; entry_eq : joint_if_entry … def_out = joint_if_entry … def_in505 501 ; partition_lbls : partial_partition … f_lbls 506 502 ; partition_regs : partial_partition … f_regs … … 523 519 [ sequential s' nxt ⇒ 524 520 let block ≝ 525 if eq_identifier … (joint_if_entry … def_in) l then 526 append_seq_list … (f_step … data l s') (added_prologue … data) 521 if not_emptyb … (added_prologue … data) ∧ 522 eq_identifier … (joint_if_entry … def_in) l then 523 bret … [ ] 527 524 else 528 525 f_step … data l s' in … … 532 529  FCOND abs _ _ _ ⇒ Ⓧabs 533 530 ] 531 ; prologue_ok : 532 if not_emptyb … (added_prologue … data) then 533 ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 534 joint_if_entry … def_out 535 ~❨〈[ ],λ_.COST_LABEL … (get_first_costlabel … def_in), added_prologue … data〉, 536 f_lbls … lbl❩~> joint_if_entry … def_in in joint_if_code … def_out 537 else (joint_if_entry … def_out = joint_if_entry … def_in) 534 538 }. 535 539 536 lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y.537 #A * #x #y #EQ >EQ % qed.538 539 lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b.540 #p #g #b elim b b541 [ ** #a #b #c normalize >append_nil %542  #f #IH @bnew_proper #r @IH543 ]544 qed.545 546 540 definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉. 541 definition set_entry ≝ 542 λglobals: list ident. 543 λpars: params. 544 λint_fun: joint_internal_function pars globals. 545 λentry. 546 (*λexit.*) 547 mk_joint_internal_function pars globals 548 (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) 549 (joint_if_params … int_fun) (joint_if_stacksize … int_fun) 550 (joint_if_local_stacksize … int_fun) 551 (joint_if_code … int_fun) entry (*exit*). 547 552 548 553 (* translation with inline fresh register allocation *) … … 564 569 let runiv ≝ \fst runiv_data in 565 570 let data ≝ \snd runiv_data in 566 let entry ≝ joint_if_entry … def in 571 let entry ≝ joint_if_entry … def in 567 572 let init ≝ 568 573 mk_joint_internal_function dst_g_pars globals … … 571 576 (init_ret … data) (init_params … data) (init_stack_size … data) 572 577 (joint_if_local_stacksize … def) 573 ( add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))578 (empty_map ? (joint_statement ??)) 574 579 entry in 580 let prologue ≝ added_prologue … data in 581 let 〈init, entry'〉 ≝ adds_graph_pre ??? (λ_.λi.i) prologue entry init in 582 let f_step ≝ 583 if not_emptyb … prologue then 584 λlbl.if eq_identifier … lbl entry then λ_.bret … [ ] else f_step … data lbl 585 else f_step … data in 575 586 let f : label → joint_statement (src_g_pars : params) globals → 576 587 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ … … 578 589 match stmt with 579 590 [ sequential inst next ⇒ 580 b_adds_graph … (f_step … datalbl inst) lbl next def591 b_adds_graph … (f_step lbl inst) lbl next def 581 592  final inst ⇒ 582 593 b_fin_adds_graph … (f_fin … data lbl inst) lbl def … … 584 595 ] in 585 596 let def_out ≝ foldi ??? f (joint_if_code … def) init in 586 let init_c_nxt ≝ get_first_costlabel … def in 587 let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in 588 ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?». 597 let def_out ≝ 598 if not_emptyb … prologue then 599 let init_c ≝ get_first_costlabel … def in 600 let 〈def_out, entry''〉 ≝ fresh_label … def_out in 601 let def_out ≝ 602 add_graph … entry'' (sequential … (COST_LABEL … init_c) entry') def_out 603 in 604 set_entry … def_out entry'' 605 else def_out in 606 ««def_out, ?», ?». 589 607 @hide_prf 590 608 [ cases daemon
Note: See TracChangeset
for help on using the changeset viewer.