Changeset 1643 for src/joint/TranslateUtils_paolo.ma
 Timestamp:
 Jan 13, 2012, 12:23:30 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils_paolo.ma
r1640 r1643 97 97 bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals) 98 98 (* 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)) → 99 103 (* initialized function definition with empty graph *) 100 104 joint_internal_function globals dst_g_pars → … … 103 107 (* destination function *) 104 108 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. 106 110 let f : label → joint_statement (src_g_pars : params) globals → 107 111 joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ … … 111 115  GOTO next ⇒ add_graph … lbl (GOTO … next) def 112 116  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) 113 120 ] in 114 121 foldi … f (joint_if_code … def) empty. 122 123 definition 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. 115 145 116 146 (* translation without register allocation *) … … 121 151 (label → joint_instruction src_g_pars globals → 122 152 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)) → 123 157 (* initialized function definition with empty graph *) 124 158 joint_internal_function … dst_g_pars → … … 127 161 (* destination function *) 128 162 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. 130 164 let f : label → joint_statement (src_g_pars : params) globals → 131 165 joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ … … 136 170  GOTO next ⇒ add_graph … lbl (GOTO … next) def 137 171  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) 138 175 ] in 139 176 foldi ??? f (joint_if_code ?? def) empty. 177 178 definition 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 140 199 141 200 (*
Note: See TracChangeset
for help on using the changeset viewer.