1 | include "RTL/RTLTailcall.ma". |
---|
2 | include "utilities/RegisterSet.ma". |
---|
3 | include "common/Identifiers.ma". |
---|
4 | include "ERTL/ERTL.ma". |
---|
5 | include "joint/TranslateUtils.ma". |
---|
6 | |
---|
7 | definition save_hdws ≝ |
---|
8 | λglobals,l. |
---|
9 | let save_hdws_internal ≝ |
---|
10 | λdestr_srcr.λstart_lbl. |
---|
11 | let 〈destr, srcr〉 ≝ destr_srcr in |
---|
12 | adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl |
---|
13 | in |
---|
14 | map ? ? save_hdws_internal l. |
---|
15 | |
---|
16 | definition restore_hdws ≝ |
---|
17 | λglobals,l. |
---|
18 | let restore_hdws_internal ≝ |
---|
19 | λsrcr_destr: register × Register. |
---|
20 | λstart_lbl: label. |
---|
21 | let 〈srcr, destr〉 ≝ srcr_destr in |
---|
22 | adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl |
---|
23 | in |
---|
24 | map ? ? restore_hdws_internal l. |
---|
25 | |
---|
26 | definition get_params_hdw ≝ |
---|
27 | λglobals. |
---|
28 | λparams: list register. |
---|
29 | match params with |
---|
30 | [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ joint_st_goto … start_lbl ] start_lbl] |
---|
31 | | _ ⇒ |
---|
32 | let l ≝ zip_pottier ? ? params RegisterParams in |
---|
33 | save_hdws globals l ]. |
---|
34 | |
---|
35 | definition get_param_stack ≝ |
---|
36 | λglobals. |
---|
37 | λoff: nat. |
---|
38 | λdestr. |
---|
39 | λstart_lbl, dest_lbl: label. |
---|
40 | λdef. |
---|
41 | let 〈def, addr1〉 ≝ fresh_reg … def in |
---|
42 | let 〈def, addr2〉 ≝ fresh_reg … def in |
---|
43 | let 〈def, tmpr〉 ≝ fresh_reg … def in |
---|
44 | let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in |
---|
45 | adds_graph ertl_params1 globals [ |
---|
46 | joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl; |
---|
47 | joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl; |
---|
48 | joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl; |
---|
49 | joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl; |
---|
50 | joint_st_sequential … (joint_instr_op2 … Add addr1 addr1 tmpr) start_lbl; |
---|
51 | joint_st_sequential … (joint_instr_int … addr2 (bitvector_of_nat 8 0)) start_lbl; |
---|
52 | joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl; |
---|
53 | joint_st_sequential … (joint_instr_op2 … Addc addr2 addr2 tmpr) start_lbl; |
---|
54 | joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl |
---|
55 | ] start_lbl dest_lbl def. |
---|
56 | |
---|
57 | definition get_params_stack ≝ |
---|
58 | λglobals,params. |
---|
59 | match params with |
---|
60 | [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl ] |
---|
61 | | _ ⇒ mapi ? ? (get_param_stack globals) params ]. |
---|
62 | |
---|
63 | definition get_params ≝ |
---|
64 | λglobals,params. |
---|
65 | let n ≝ min (length … params) (length … RegisterParams) in |
---|
66 | let 〈hdw_params, stack_params〉 ≝ list_split … n params in |
---|
67 | let hdw_params ≝ get_params_hdw globals hdw_params in |
---|
68 | hdw_params @ (get_params_stack … stack_params). |
---|
69 | |
---|
70 | definition add_prologue ≝ |
---|
71 | λglobals. |
---|
72 | λparams: list register. |
---|
73 | λsral. |
---|
74 | λsrah. |
---|
75 | λsregs. |
---|
76 | λdef. |
---|
77 | let start_lbl ≝ joint_if_entry … (ertl_params globals) def in |
---|
78 | let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in |
---|
79 | match lookup … (joint_if_code … def) start_lbl |
---|
80 | return λx. x ≠ None ? → ertl_internal_function globals with |
---|
81 | [ None ⇒ λnone_absrd. ⊥ |
---|
82 | | Some last_stmt ⇒ λsome_prf. |
---|
83 | let def ≝ |
---|
84 | add_translates … |
---|
85 | ((adds_graph ertl_params1 … [ |
---|
86 | joint_st_sequential ertl_params_ … (joint_instr_extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl |
---|
87 | ]) :: |
---|
88 | (adds_graph … [ |
---|
89 | joint_st_sequential … (joint_instr_pop … sral) start_lbl; |
---|
90 | joint_st_sequential … (joint_instr_pop … srah) start_lbl |
---|
91 | ]) :: |
---|
92 | (save_hdws … sregs) @ |
---|
93 | (get_params … params)) |
---|
94 | start_lbl tmp_lbl def |
---|
95 | in |
---|
96 | add_graph … tmp_lbl last_stmt def |
---|
97 | ] ?. |
---|
98 | [ cases start_lbl #x #H @H |
---|
99 | | cases (none_absrd) /2/ ] |
---|
100 | qed. |
---|
101 | |
---|
102 | definition save_return ≝ |
---|
103 | λglobals. |
---|
104 | λret_regs. |
---|
105 | λstart_lbl: label. |
---|
106 | λdest_lbl: label. |
---|
107 | λdef: ertl_internal_function globals. |
---|
108 | let 〈def, tmpr〉 ≝ fresh_reg … def in |
---|
109 | match reduce_strong ? ? RegisterSTS ret_regs with |
---|
110 | [ dp crl crl_proof ⇒ |
---|
111 | let commonl ≝ \fst (\fst crl) in |
---|
112 | let commonr ≝ \fst (\snd crl) in |
---|
113 | let restl ≝ \snd (\fst crl) in |
---|
114 | let restr ≝ \snd (\snd crl) in |
---|
115 | let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero …)) start_lbl in |
---|
116 | let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in |
---|
117 | let saves ≝ map2 … f_save commonl commonr crl_proof in |
---|
118 | let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in |
---|
119 | let defaults ≝ map … f_default restl in |
---|
120 | adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def |
---|
121 | ]. |
---|
122 | |
---|
123 | definition assign_result ≝ |
---|
124 | λglobals.λstart_lbl: label. |
---|
125 | match reduce_strong ? ? RegisterRets RegisterSTS with |
---|
126 | [ dp crl crl_proof ⇒ |
---|
127 | let commonl ≝ \fst (\fst crl) in |
---|
128 | let commonr ≝ \fst (\snd crl) in |
---|
129 | let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in |
---|
130 | let insts ≝ map2 ? ? ? f commonl commonr crl_proof in |
---|
131 | adds_graph ertl_params1 … insts start_lbl |
---|
132 | ]. |
---|
133 | |
---|
134 | definition add_epilogue ≝ |
---|
135 | λglobals. |
---|
136 | λret_regs. |
---|
137 | λsral. |
---|
138 | λsrah. |
---|
139 | λsregs. |
---|
140 | λdef. |
---|
141 | let start_lbl ≝ joint_if_exit … (ertl_params globals) def in |
---|
142 | let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in |
---|
143 | match lookup … (joint_if_code … def) start_lbl |
---|
144 | return λx. x ≠ None ? → ertl_internal_function globals with |
---|
145 | [ None ⇒ λnone_absrd. ⊥ |
---|
146 | | Some last_stmt ⇒ λsome_prf. |
---|
147 | let def ≝ |
---|
148 | add_translates ertl_params1 … ( |
---|
149 | [save_return globals ret_regs] @ |
---|
150 | restore_hdws … sregs @ |
---|
151 | [adds_graph … [ |
---|
152 | joint_st_sequential … (joint_instr_push … srah) start_lbl; |
---|
153 | joint_st_sequential … (joint_instr_push … sral) start_lbl |
---|
154 | ]] @ |
---|
155 | [adds_graph ertl_params1 … [ |
---|
156 | joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl |
---|
157 | ]] @ |
---|
158 | [assign_result globals] |
---|
159 | ) start_lbl tmp_lbl def |
---|
160 | in |
---|
161 | let def' ≝ add_graph … tmp_lbl last_stmt def in |
---|
162 | set_joint_if_exit … tmp_lbl def' ? |
---|
163 | ] ?. |
---|
164 | [ cases start_lbl #x #H @H |
---|
165 | | cases (none_absrd) /2/ |
---|
166 | | cases daemon (* CSC: XXXXX *) |
---|
167 | ] |
---|
168 | qed. |
---|
169 | |
---|
170 | |
---|
171 | definition allocate_regs ≝ |
---|
172 | λglobals. |
---|
173 | λrs. |
---|
174 | λsaved: rs_set rs. |
---|
175 | λdef. |
---|
176 | let allocate_regs_internal ≝ |
---|
177 | λr: Register. |
---|
178 | λdef_sregs. |
---|
179 | let 〈def, sregs〉 ≝ def_sregs in |
---|
180 | let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in |
---|
181 | 〈def, 〈r', r〉 :: sregs〉 |
---|
182 | in |
---|
183 | rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. |
---|
184 | |
---|
185 | definition add_pro_and_epilogue ≝ |
---|
186 | λglobals. |
---|
187 | λparams. |
---|
188 | λret_regs. |
---|
189 | λdef. |
---|
190 | match fresh_regs_strong … globals def 2 with |
---|
191 | [ dp def_sra def_sra_proof ⇒ |
---|
192 | let def ≝ \fst def_sra in |
---|
193 | let sra ≝ \snd def_sra in |
---|
194 | let sral ≝ nth_safe ? 0 sra ? in |
---|
195 | let srah ≝ nth_safe ? 1 sra ? in |
---|
196 | let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in |
---|
197 | let def ≝ add_prologue … params sral srah sregs def in |
---|
198 | let def ≝ add_epilogue … ret_regs sral srah sregs def in |
---|
199 | def |
---|
200 | ]. |
---|
201 | >def_sra_proof // |
---|
202 | qed. |
---|
203 | |
---|
204 | definition set_params_hdw ≝ |
---|
205 | λglobals,params. |
---|
206 | match params with |
---|
207 | [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl] |
---|
208 | | _ ⇒ |
---|
209 | let l ≝ zip_pottier ? ? params RegisterParams in |
---|
210 | restore_hdws globals l |
---|
211 | ]. |
---|
212 | |
---|
213 | definition set_param_stack ≝ |
---|
214 | λglobals. |
---|
215 | λoff. |
---|
216 | λsrcr. |
---|
217 | λstart_lbl: label. |
---|
218 | λdest_lbl: label. |
---|
219 | λdef: ertl_internal_function globals. |
---|
220 | let 〈def, addr1〉 ≝ fresh_reg … def in |
---|
221 | let 〈def, addr2〉 ≝ fresh_reg … def in |
---|
222 | let 〈def, tmpr〉 ≝ fresh_reg … def in |
---|
223 | let 〈ignore, int_off〉 ≝ half_add ? off int_size in |
---|
224 | adds_graph ertl_params1 … [ |
---|
225 | joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl; |
---|
226 | joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl; |
---|
227 | joint_st_sequential … (joint_instr_clear_carry …) start_lbl; |
---|
228 | joint_st_sequential … (joint_instr_op2 … Sub addr1 tmpr addr1) start_lbl; |
---|
229 | joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl; |
---|
230 | joint_st_sequential … (joint_instr_int … addr2 (zero ?)) start_lbl; |
---|
231 | joint_st_sequential … (joint_instr_op2 … Sub addr2 tmpr addr2) start_lbl; |
---|
232 | joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) start_lbl |
---|
233 | ] start_lbl dest_lbl def. |
---|
234 | |
---|
235 | definition set_params_stack ≝ |
---|
236 | λglobals,params. |
---|
237 | match params with |
---|
238 | [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [joint_st_goto … start_lbl] start_lbl] |
---|
239 | | _ ⇒ |
---|
240 | let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in |
---|
241 | mapi ? ? f params]. |
---|
242 | |
---|
243 | definition set_params ≝ |
---|
244 | λglobals,params. |
---|
245 | let n ≝ min (|params|) (|RegisterParams|) in |
---|
246 | let hdw_stack_params ≝ split ? params n ? in |
---|
247 | let hdw_params ≝ \fst hdw_stack_params in |
---|
248 | let stack_params ≝ \snd hdw_stack_params in |
---|
249 | set_params_hdw globals hdw_params @ set_params_stack globals stack_params. |
---|
250 | /2/ |
---|
251 | qed. |
---|
252 | |
---|
253 | definition fetch_result ≝ |
---|
254 | λglobals. |
---|
255 | λret_regs. |
---|
256 | λstart_lbl: label. |
---|
257 | match reduce_strong ? ? RegisterSTS RegisterRets with |
---|
258 | [ dp crl first_crl_proof ⇒ |
---|
259 | let commonl ≝ \fst (\fst crl) in |
---|
260 | let commonr ≝ \fst (\snd crl) in |
---|
261 | let f_save ≝ λst. λret. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware st, hardware ret〉) start_lbl in |
---|
262 | let saves ≝ map2 ? ? ? f_save commonl commonr ? in |
---|
263 | match reduce_strong ? ? ret_regs RegisterSTS with |
---|
264 | [ dp crl second_crl_proof ⇒ |
---|
265 | let commonl ≝ \fst (\fst crl) in |
---|
266 | let commonr ≝ \fst (\snd crl) in |
---|
267 | let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in |
---|
268 | let restores ≝ map2 ? ? ? f_restore commonl commonr ? in |
---|
269 | adds_graph ertl_params1 … (saves @ restores) start_lbl]]. |
---|
270 | [@second_crl_proof | @first_crl_proof] |
---|
271 | qed. |
---|
272 | |
---|
273 | definition translate_call_id ≝ |
---|
274 | λglobals,f. |
---|
275 | λargs. |
---|
276 | λret_regs. |
---|
277 | λstart_lbl. |
---|
278 | λdest_lbl. |
---|
279 | λdef. |
---|
280 | let nb_args ≝ |args| in |
---|
281 | add_translates ertl_params1 globals ( |
---|
282 | set_params … args @ [ |
---|
283 | adds_graph ertl_params1 … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ]; |
---|
284 | fetch_result … ret_regs |
---|
285 | ] |
---|
286 | ) start_lbl dest_lbl def. |
---|
287 | |
---|
288 | definition translate_stmt : |
---|
289 | ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals |
---|
290 | ≝ |
---|
291 | λglobals. |
---|
292 | λlbl. |
---|
293 | λstmt. |
---|
294 | λdef. |
---|
295 | match stmt with |
---|
296 | [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def |
---|
297 | | joint_st_return ⇒ add_graph … lbl (joint_st_return …) def |
---|
298 | | joint_st_sequential seq lbl' ⇒ |
---|
299 | match seq with |
---|
300 | [ joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) |
---|
301 | | joint_instr_pop _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) |
---|
302 | | joint_instr_call_id f args ret_regs ⇒ |
---|
303 | translate_call_id … f args ret_regs lbl lbl' def |
---|
304 | | joint_instr_move rs ⇒ |
---|
305 | let 〈r1,r2〉 ≝ rs in |
---|
306 | let rs ≝ 〈pseudo r1, pseudo r2〉 in |
---|
307 | add_graph ertl_params1 ? lbl (joint_st_sequential … (joint_instr_move … rs) lbl') def |
---|
308 | | joint_instr_extension ext ⇒ |
---|
309 | match ext with |
---|
310 | [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *) |
---|
311 | | rtlntc_st_ext_address r1 r2 ⇒ |
---|
312 | adds_graph ertl_params1 … [ |
---|
313 | joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl; |
---|
314 | joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl |
---|
315 | ] lbl lbl' def] |
---|
316 | (*CSC: everything is just copied to re-type it from now on; |
---|
317 | the problem is call_id that takes different parameters, but that is pattern-matched |
---|
318 | above. It could be made nicer at the cost of making all the rest of the code uglier *) |
---|
319 | | joint_instr_cost_label cost_lbl ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cost_label … cost_lbl) lbl') def |
---|
320 | | joint_instr_address x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_address … x prf r1 r2) lbl') def |
---|
321 | | joint_instr_int r i ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_int … r i) lbl') def |
---|
322 | | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒ |
---|
323 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def |
---|
324 | | joint_instr_op1 op1 destr srcr ⇒ |
---|
325 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op1 … op1 destr srcr) lbl') def |
---|
326 | | joint_instr_op2 op2 destr srcr1 srcr2 ⇒ |
---|
327 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def |
---|
328 | | joint_instr_clear_carry ⇒ |
---|
329 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_clear_carry …) lbl') def |
---|
330 | | joint_instr_set_carry ⇒ |
---|
331 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_set_carry …) lbl') def |
---|
332 | | joint_instr_load destr addr1 addr2 ⇒ |
---|
333 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_load … destr addr1 addr2) lbl') def |
---|
334 | | joint_instr_store addr1 addr2 srcr ⇒ |
---|
335 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) lbl') def |
---|
336 | | joint_instr_cond srcr lbl_true ⇒ |
---|
337 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cond … srcr lbl_true) lbl') def |
---|
338 | | joint_instr_comment msg ⇒ |
---|
339 | add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_comment … msg) lbl') def |
---|
340 | ]]. |
---|
341 | @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *) |
---|
342 | qed. |
---|
343 | |
---|
344 | (* hack with empty graphs used here *) |
---|
345 | definition translate_funct_internal ≝ |
---|
346 | λglobals.λdef:rtlntc_internal_function globals. |
---|
347 | let nb_params ≝ |joint_if_params ?? def| in |
---|
348 | let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in |
---|
349 | let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in |
---|
350 | let entry' ≝ joint_if_entry … def in |
---|
351 | let exit' ≝ joint_if_exit … def in |
---|
352 | let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in |
---|
353 | let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in |
---|
354 | let def' ≝ |
---|
355 | mk_joint_internal_function globals (ertl_params globals) |
---|
356 | (joint_if_luniverse … def) (joint_if_runiverse … def) it |
---|
357 | nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) |
---|
358 | graph' ? ? in |
---|
359 | let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in |
---|
360 | add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'. |
---|
361 | whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction |
---|
362 | makes the next application fail. Why? *) |
---|
363 | % |
---|
364 | [ @entry' | @graph_add_lookup @graph_add |
---|
365 | | @exit' | @graph_add ] |
---|
366 | qed. |
---|
367 | |
---|
368 | definition generate ≝ |
---|
369 | λglobals. |
---|
370 | λstmt. |
---|
371 | λdef: joint_internal_function … (ertl_params globals). |
---|
372 | let 〈entry, nuniv〉 ≝ fresh_label … def in |
---|
373 | let graph ≝ add ? ? (joint_if_code … def) entry stmt in |
---|
374 | mk_joint_internal_function ? (ertl_params globals) |
---|
375 | nuniv (joint_if_runiverse … def) it (joint_if_params … def) |
---|
376 | (joint_if_locals … def) (joint_if_stacksize … def) graph |
---|
377 | ? ?. |
---|
378 | [ % [ @entry | @graph_add ] |
---|
379 | | cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF ] |
---|
380 | qed. |
---|
381 | |
---|
382 | let rec find_and_remove_first_cost_label_internal (globals: list ident) |
---|
383 | (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat) |
---|
384 | on num_nodes ≝ |
---|
385 | match num_nodes with |
---|
386 | [ O ⇒ 〈None ?, def〉 |
---|
387 | | S num_nodes' ⇒ |
---|
388 | match lookup … (joint_if_code … def) lbl with |
---|
389 | [ None ⇒ 〈None ?, def〉 |
---|
390 | | Some stmt ⇒ |
---|
391 | match stmt with |
---|
392 | [ joint_st_sequential inst lbl ⇒ |
---|
393 | match inst with |
---|
394 | [ joint_instr_cost_label cost_lbl ⇒ |
---|
395 | 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (joint_st_goto … lbl) def〉 |
---|
396 | | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] |
---|
397 | | joint_st_return ⇒ 〈None …, def〉 |
---|
398 | | joint_st_goto lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' |
---|
399 | ]]]. |
---|
400 | |
---|
401 | definition find_and_remove_first_cost_label ≝ |
---|
402 | λglobals,def. |
---|
403 | find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)). |
---|
404 | |
---|
405 | definition move_first_cost_label_up_internal ≝ |
---|
406 | λglobals,def. |
---|
407 | let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in |
---|
408 | match cost_label with |
---|
409 | [ None ⇒ def |
---|
410 | | Some cost_label ⇒ generate … (joint_st_sequential ertl_params_ globals (joint_instr_cost_label … cost_label) (joint_if_entry … def)) def |
---|
411 | ]. |
---|
412 | |
---|
413 | definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). |
---|
414 | |
---|
415 | definition translate : rtl_program → ertl_program ≝ |
---|
416 | λp. |
---|
417 | let p ≝ tailcall_simplify p in (* tailcall simplification here *) |
---|
418 | transform_program ??? p (transf_fundef ?? (translate_funct …)). |
---|