Ignore:
Timestamp:
Jan 13, 2012, 12:23:30 PM (8 years ago)
Author:
tranquil
Message:
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils_paolo.ma

    r1640 r1643  
    9797    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
    9898    (* this can be added to allow redirections: × label *)) →
     99  (label → ext_fin_instruction src_g_pars →
     100    (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals))
     101    ×
     102    (joint_statement dst_g_pars globals)) →
    99103  (* initialized function definition with empty graph *)
    100104  joint_internal_function globals dst_g_pars →
     
    103107  (* destination function *)
    104108  joint_internal_function globals dst_g_pars ≝
    105   λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def.
     109  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def.
    106110  let f : label → joint_statement (src_g_pars : params) globals →
    107111    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     
    111115    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    112116    | RETURN ⇒ add_graph … lbl (RETURN …) def
     117    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
     118      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     119      b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    113120    ] in
    114121  foldi … f (joint_if_code … def) empty.
     122
     123definition b_graph_translate_no_fin :
     124  ∀src_g_pars : graph_params.
     125  ext_fin_instruction src_g_pars = void →
     126  ∀dst_g_pars : graph_params.
     127  ∀globals: list ident.
     128  (* type of allocatable registers (unit if not in RTLabs) *)
     129  ∀T : Type[0].
     130  (* fresh register creation *)
     131  freshT globals dst_g_pars (localsT dst_g_pars) T →
     132  (* function dictating the translation *)
     133  (label → joint_instruction src_g_pars globals →
     134    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
     135    (* this can be added to allow redirections: × label *)) →
     136  (* initialized function definition with empty graph *)
     137  joint_internal_function globals dst_g_pars →
     138  (* source function *)
     139  joint_internal_function globals src_g_pars →
     140  (* destination function *)
     141  joint_internal_function globals dst_g_pars ≝
     142  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.
     143    b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg
     144      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
    115145 
    116146(* translation without register allocation *)
     
    121151  (label → joint_instruction src_g_pars globals →
    122152    list (joint_instruction dst_g_pars globals)) →
     153  (label → ext_fin_instruction src_g_pars →
     154    (list (joint_instruction dst_g_pars globals))
     155    ×
     156    (joint_statement dst_g_pars globals)) →
    123157  (* initialized function definition with empty graph *)
    124158  joint_internal_function … dst_g_pars →
     
    127161  (* destination function *)
    128162  joint_internal_function … dst_g_pars ≝
    129   λsrc_g_pars,dst_g_pars,globals,trans,empty,def.
     163  λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def.
    130164  let f : label → joint_statement (src_g_pars : params) globals →
    131165    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
     
    136170    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    137171    | RETURN ⇒ add_graph … lbl (RETURN …) def
     172    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
     173      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     174      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    138175    ] in
    139176  foldi ??? f (joint_if_code ?? def) empty.
     177 
     178definition graph_translate_no_fin :
     179  ∀src_g_pars : graph_params.
     180  ext_fin_instruction src_g_pars = void →
     181  ∀dst_g_pars : graph_params.
     182  ∀globals: list ident.
     183  (* type of allocatable registers (unit if not in RTLabs) *)
     184  (* function dictating the translation *)
     185  (label → joint_instruction src_g_pars globals →
     186    list (joint_instruction dst_g_pars globals)
     187    (* this can be added to allow redirections: × label *)) →
     188  (* initialized function definition with empty graph *)
     189  joint_internal_function globals dst_g_pars →
     190  (* source function *)
     191  joint_internal_function globals src_g_pars →
     192  (* destination function *)
     193  joint_internal_function globals dst_g_pars ≝
     194  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans.
     195    graph_translate src_g_pars dst_g_pars globals
     196      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
     197 
     198
    140199     
    141200(*
Note: See TracChangeset for help on using the changeset viewer.