Changeset 2980


Ignore:
Timestamp:
Mar 27, 2013, 4:50:52 PM (4 years ago)
Author:
tranquil
Message:

fixed b_graph_translate

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2970 r2980  
    456456Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d).
    457457
    458 definition get_first_costlabel : ∀p,g.
    459   joint_closed_internal_function p g → costlabel
     458definition get_first_costlabel_next : ∀p,g.
     459  joint_closed_internal_function p g → costlabel × (succ p)
    460460  λp,g,def.
    461461  match stmt_at … (joint_if_code … def) (joint_if_entry … def)
     
    465465    [ sequential s' nxt ⇒
    466466      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
    467       [ COST_LABEL c ⇒ λ_.c
     467      [ COST_LABEL c ⇒ λ_.〈c, nxt〉
    468468      | _ ⇒ λabs.⊥
    469469      ]
     
    476476cases (entry_is_cost … good_def) #nxt' * #c #EQ >EQ #ABS destruct
    477477qed.
     478
     479definition get_first_costlabel ≝ λp,g,f.\fst (get_first_costlabel_next p g f).
    478480
    479481definition partial_partition : ∀X.∀Y : DeqSet.(X → list Y) → Prop ≝
     
    578580    (empty_map ? (joint_statement ??))
    579581    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
    586582  let f : label → joint_statement (src_g_pars : params) globals →
    587583    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     
    589585    match stmt with
    590586    [ sequential inst next ⇒
    591       b_adds_graph … (f_step lbl inst) lbl next def
     587      b_adds_graph … (f_step … data lbl inst) lbl next def
    592588    | final inst ⇒
    593589      b_fin_adds_graph … (f_fin … data lbl inst) lbl def
     
    595591    ] in
    596592  let def_out ≝ foldi ??? f (joint_if_code … def) init in
     593  let prologue ≝ added_prologue … data in
    597594  let def_out ≝
    598595    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'
    605609    else def_out in
    606610  ««def_out, ?», ?».
Note: See TracChangeset for help on using the changeset viewer.