Changeset 2970


Ignore:
Timestamp:
Mar 26, 2013, 7:13:07 PM (4 years ago)
Author:
tranquil
Message:

now joint_if_entry can change when a preamble is added, so code points are always preserved

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2946 r2970  
    270270*)
    271271
    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 
    278272(*
    279273definition insert_epilogue ≝
     
    463457
    464458definition get_first_costlabel : ∀p,g.
    465   joint_closed_internal_function p g → costlabel × (succ p)
     459  joint_closed_internal_function p g → costlabel
    466460  λp,g,def.
    467461  match stmt_at … (joint_if_code … def) (joint_if_entry … def)
     
    471465    [ sequential s' nxt ⇒
    472466      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
    473       [ COST_LABEL c ⇒ λ_.〈c, nxt〉
     467      [ COST_LABEL c ⇒ λ_.c
    474468      | _ ⇒ λabs.⊥
    475469      ]
     
    487481(∀x.bool_to_Prop (uniqueb … (f x))) ∧
    488482(∀x1,x2,y.y ∈ f x1 → y ∈ f x2 → x1 = x2).
     483
     484definition not_emptyb : ∀X.list X → bool ≝
     485λX,l.match l with [ nil ⇒ false | cons _ _ ⇒ true].
    489486
    490487record b_graph_translate_props
     
    502499; ss_def_out_eq :
    503500           joint_if_stacksize … def_out = init_stack_size … data
    504 ; entry_eq : joint_if_entry … def_out = joint_if_entry … def_in
    505501; partition_lbls : partial_partition … f_lbls
    506502; partition_regs : partial_partition … f_regs
     
    523519  [ sequential s' nxt ⇒
    524520    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 … [ ]
    527524      else
    528525        f_step … data l s' in
     
    532529  | FCOND abs _ _ _ ⇒ Ⓧabs
    533530  ]
     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)
    534538}.
    535539
    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 -b
    541 [ ** #a #b #c normalize >append_nil %
    542 | #f #IH @bnew_proper #r @IH
    543 ]
    544 qed.
    545 
    546540definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉.
     541definition 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*).
    547552
    548553(* translation with inline fresh register allocation *)
     
    564569  let runiv ≝ \fst runiv_data in
    565570  let data ≝ \snd runiv_data in
    566   let entry ≝ joint_if_entry … def in
     571  let entry ≝ joint_if_entry … def in 
    567572  let init ≝
    568573    mk_joint_internal_function dst_g_pars globals
     
    571576    (init_ret … data) (init_params … data) (init_stack_size … data)
    572577    (joint_if_local_stacksize … def)
    573     (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
     578    (empty_map ? (joint_statement ??))
    574579    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
    575586  let f : label → joint_statement (src_g_pars : params) globals →
    576587    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     
    578589    match stmt with
    579590    [ sequential inst next ⇒
    580       b_adds_graph … (f_step … data lbl inst) lbl next def
     591      b_adds_graph … (f_step lbl inst) lbl next def
    581592    | final inst ⇒
    582593      b_fin_adds_graph … (f_fin … data lbl inst) lbl def
     
    584595    ] in
    585596  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, ?», ?».
    589607@hide_prf
    590608[ cases daemon
Note: See TracChangeset for help on using the changeset viewer.