Changeset 2980
 Timestamp:
 Mar 27, 2013, 4:50:52 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r2970 r2980 456 456 Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d). 457 457 458 definition get_first_costlabel : ∀p,g.459 joint_closed_internal_function p g → costlabel ≝458 definition get_first_costlabel_next : ∀p,g. 459 joint_closed_internal_function p g → costlabel × (succ p) ≝ 460 460 λp,g,def. 461 461 match stmt_at … (joint_if_code … def) (joint_if_entry … def) … … 465 465 [ sequential s' nxt ⇒ 466 466 match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with 467 [ COST_LABEL c ⇒ λ_. c467 [ COST_LABEL c ⇒ λ_.〈c, nxt〉 468 468  _ ⇒ λabs.⊥ 469 469 ] … … 476 476 cases (entry_is_cost … good_def) #nxt' * #c #EQ >EQ #ABS destruct 477 477 qed. 478 479 definition get_first_costlabel ≝ λp,g,f.\fst (get_first_costlabel_next p g f). 478 480 479 481 definition partial_partition : ∀X.∀Y : DeqSet.(X → list Y) → Prop ≝ … … 578 580 (empty_map ? (joint_statement ??)) 579 581 entry in 580 let prologue ≝ added_prologue … data in581 let 〈init, entry'〉 ≝ adds_graph_pre ??? (λ_.λi.i) prologue entry init in582 let f_step ≝583 if not_emptyb … prologue then584 λlbl.if eq_identifier … lbl entry then λ_.bret … [ ] else f_step … data lbl585 else f_step … data in586 582 let f : label → joint_statement (src_g_pars : params) globals → 587 583 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ … … 589 585 match stmt with 590 586 [ sequential inst next ⇒ 591 b_adds_graph … (f_step lbl inst) lbl next def587 b_adds_graph … (f_step … data lbl inst) lbl next def 592 588  final inst ⇒ 593 589 b_fin_adds_graph … (f_fin … data lbl inst) lbl def … … 595 591 ] in 596 592 let def_out ≝ foldi ??? f (joint_if_code … def) init in 593 let prologue ≝ added_prologue … data in 597 594 let def_out ≝ 598 595 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'' 596 (* retrieve initial cost label and its next from src *) 597 let 〈init_c, nxt〉 ≝ 598 get_first_costlabel_next … def in 599 (* erase in dst the initial cost label *) 600 let def_out ≝ add_graph … entry 601 (sequential dst_g_pars … (NOOP …) nxt) def_out in 602 (* generate a new entry label *) 603 let 〈def_out, entry'〉 ≝ fresh_label … def_out in 604 (* add the initial cost label followed by the prologue *) 605 let def_out ≝ adds_graph … 〈[ ], λ_.COST_LABEL … init_c, prologue〉 606 entry' entry def_out in 607 (* redirect the entry *) 608 set_entry … def_out entry' 605 609 else def_out in 606 610 ««def_out, ?», ?».
Note: See TracChangeset
for help on using the changeset viewer.