Changeset 2675


Ignore:
Timestamp:
Feb 18, 2013, 6:26:22 PM (6 years ago)
Author:
tranquil
Message:
  • a generic graph program transformation
Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2674 r2675  
    3939definition translate_step:
    4040 ∀globals.
     41 unit →
    4142 label
    4243  →joint_step ERTL globals
    4344   →bind_step_block ERTLptr globals ≝
    44  λglobals.λl.λs.
     45 λglobals.λ_.λl.λs.
    4546match s return λ_.bind_step_block ERTLptr globals with
    4647[ CALL called args dest ⇒
     
    6869definition translate_fin_step:
    6970 ∀globals.
     71 unit →
    7072 label
    7173  →joint_fin_step ERTL
    7274   →bind_fin_block ERTLptr globals ≝
    73  λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
    74 
    75 definition translate_internal :  ∀globals: list ident.
    76   joint_closed_internal_function ERTL globals →
    77   joint_closed_internal_function ERTLptr globals ≝
    78   λglobals,int_fun.
    79   (* initialize internal function *)
    80   b_graph_translate ERTL ERTLptr globals
    81     (joint_if_result … int_fun)
    82     (joint_if_params … int_fun)
    83     (joint_if_stacksize … int_fun)
    84     (translate_step …)
    85     (translate_fin_step …)
    86     int_fun.
    87 cases daemon.
    88 qed.
     75 λglobals.λ_.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
    8976
    9077definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
    91   λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
     78  b_graph_transform_program ERTL ERTLptr (λ_.unit)
     79  (λglobals,int_fun.
     80    〈〈joint_if_result … int_fun,
     81      joint_if_params … int_fun,
     82      joint_if_stacksize … int_fun〉,
     83    it〉)
     84  translate_step
     85  translate_fin_step.
  • 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 :
  • src/joint/semanticsUtils.ma

    r2674 r2675  
    33include "utilities/hide.ma".
    44include "ASM/BitVectorTrie.ma".
    5 include "joint/TranslateUtils.ma".
    65
    76record hw_register_env : Type[0] ≝
     
    163162whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
    164163qed.
    165 
    166 (*lemma b_graph_translate_eval :
    167   ∀src : sem_graph_params.
    168   ∀dst : sem_graph_params.
    169   ∀globals: list ident.
    170   ∀init_ret,init_params,init_stack_size.
    171   ∀f_step,f_fin,def_in.
    172   let def_out ≝
    173     b_graph_translate src_g_pars dst_g_pars globals
    174       init_ret init_params init_stack_size f_step f_fin def_in in
    175   ∀st : state_pc src
    176 *)
Note: See TracChangeset for help on using the changeset viewer.