Ignore:
Timestamp:
Feb 18, 2013, 6:26:22 PM (8 years ago)
Author:
tranquil
Message:
  • a generic graph program transformation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2674 r2675  
    255255    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
    256256                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
    257     src ~❨B,l❩~> dst in joint_if_code … def'.
     257    src ~❨B,src::l❩~> dst in joint_if_code … def'.
    258258 
    259259axiom fin_adds_graph_ok :
     
    269269    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
    270270                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
    271     src ~❨B,l❩~> it in joint_if_code … def'.
     271    src ~❨B,src::l❩~> it in joint_if_code … def'.
    272272
    273273(* preserves first statement if a cost label (should be an invariant) *)
     
    348348    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
    349349                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
    350     src ~❨B,l,r❩~> dst in joint_if_code … def'.
     350    src ~❨B,src::l,r❩~> dst in joint_if_code … def'.
    351351 
    352352definition b_fin_adds_graph :
     
    377377    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
    378378                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
    379     src ~❨B,l,r❩~> it in joint_if_code … def'.
     379    src ~❨B,src::l,r❩~> it in joint_if_code … def'.
    380380
    381381(* translation with inline fresh register allocation *)
     
    391391  (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
    392392  (* source function *)
    393   joint_internal_function src_g_pars globals →
     393  joint_closed_internal_function src_g_pars globals →
    394394  (* destination function *)
    395   joint_internal_function dst_g_pars globals ≝
     395  joint_closed_internal_function dst_g_pars globals ≝
    396396  λsrc_g_pars,dst_g_pars,globals,
    397397   init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def.
     
    414414    ] in
    415415  foldi … f (joint_if_code … def) init.
    416 @hide_prf >graph_code_has_point @mem_set_add_id qed.
     416@hide_prf [ cases daemon (* TODO *) | >graph_code_has_point @mem_set_add_id ] qed.
    417417
    418418definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
     
    453453  ∀init_ret,init_params,init_stack_size.
    454454  ∀f_step,f_fin,def_in.
    455   luniverse_ok ?? def_in →
    456   code_closed … (joint_if_code … def_in) →
    457455  let def_out ≝
    458456    b_graph_translate src_g_pars dst_g_pars globals
    459457      init_ret init_params init_stack_size f_step f_fin def_in in
     458  luniverse_ok ?? def_in →
    460459  luniverse_ok … def_out ∧
    461   code_closed … (joint_if_code … def_out) ∧
    462460  joint_if_result … def_out = init_ret ∧
    463461  joint_if_params … def_out = init_params ∧
     
    478476  match s with
    479477  [ sequential s' nxt ⇒
    480     l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out
     478    l ~❨f_step l s', l::lbls, regs❩~> nxt in joint_if_code … def_out
    481479  | final s' ⇒
    482     l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out
     480    l ~❨f_fin l s', l::lbls, regs❩~> it in joint_if_code … def_out
    483481  | FCOND abs _ _ _ ⇒ Ⓧabs
    484482  ].
     483
     484definition b_graph_transform_program :
     485  ∀src_g_pars,dst_g_pars : graph_params.
     486  ∀X : list ident → Type[0].
     487  (* initialization *)
     488  (∀globals.joint_closed_internal_function src_g_pars globals →
     489    (call_dest dst_g_pars) × (paramsT dst_g_pars) × ℕ × (X globals)) →
     490  (* functions dictating the translation *)
     491  (∀globals.X globals → label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
     492  (∀globals.X globals → label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
     493  joint_program src_g_pars → joint_program dst_g_pars ≝
     494  λsrc,dst,X,init,f_step,f_fin,p.
     495  transform_program ??? p
     496    (λvarnames.transf_fundef ?? (λdef_in.
     497      let 〈fields, init_data〉 ≝ init varnames def_in in
     498      let 〈init_ret, init_params, init_stack_size〉 ≝ fields in
     499      b_graph_translate … init_ret init_params init_stack_size
     500        (f_step ? init_data) (f_fin ? init_data) def_in)).
    485501
    486502definition added_registers :
Note: See TracChangeset for help on using the changeset viewer.