source: src/RTL/RTLtoERTL.ma @ 1245

Last change on this file since 1245 was 1245, checked in by sacerdot, 9 years ago

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

File size: 20.6 KB
Line 
1include "RTL/RTLTailcall.ma".
2include "utilities/RegisterSet.ma".
3include "common/Identifiers.ma".
4include "ERTL/ERTL.ma".
5                     
6definition add_graph ≝
7  λl: label.
8  λstmt.
9  λp.
10  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
11  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
12  let ertl_if_params' ≝ ertl_if_params p in
13  let ertl_if_locals' ≝ ertl_if_locals p in
14  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
15  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
16  let ertl_if_entry' ≝ ertl_if_entry p in
17  let ertl_if_exit' ≝ ertl_if_exit p in
18    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
19                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
20                              ertl_if_graph' ? ?.
21  normalize nodelta;
22  [1: generalize in match ertl_if_entry';
23      #HYP
24      cases HYP
25      #LBL #LBL_PRF
26      %
27      [1: @LBL
28      |2: @graph_add_lookup
29          @LBL_PRF
30      ]
31  |2: generalize in match ertl_if_exit';
32      #HYP
33      cases HYP
34      #LBL #LBL_PRF
35      %
36      [1: @LBL
37      |2: @graph_add_lookup
38          @LBL_PRF
39      ]
40  ]
41qed.
42                           
43definition fresh_label ≝
44  λdef.
45    fresh LabelTag (ertl_if_luniverse def).
46   
47definition change_label ≝
48  λl.
49  λe: ertl_statement.
50  match e with
51  [ ertl_st_skip _ ⇒ ertl_st_skip l
52  | ertl_st_comment s _ ⇒ ertl_st_comment s l
53  | ertl_st_cost c _ ⇒ ertl_st_cost c l
54  | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
55  | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
56  | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
57  | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
58  | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
59  | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
60  | ertl_st_pop r _ ⇒ ertl_st_pop r l
61  | ertl_st_push r _ ⇒ ertl_st_push r l
62  | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
63  | ertl_st_int r i _ ⇒ ertl_st_int r i l
64  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
65  | ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l
66  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
67  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
68  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
69  | ertl_st_set_carry _ ⇒ ertl_st_set_carry l
70  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
71  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
72  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
73  | ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2
74  | ertl_st_return ⇒ ertl_st_return
75  ].
76 
77let rec adds_graph
78  (stmt_list: list ertl_statement) (start_lbl: label)
79  (dest_lbl: label) (def: ertl_internal_function)
80    on stmt_list ≝
81  match stmt_list with
82  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
83  | cons stmt stmt_list ⇒
84    match stmt_list with
85    [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def
86    | _ ⇒
87      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
88      let stmt ≝ change_label tmp_lbl stmt in
89      let def ≝ add_graph start_lbl stmt def in
90        adds_graph stmt_list tmp_lbl dest_lbl def
91    ]
92  ].
93
94let rec add_translates
95  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
96  (def: ertl_internal_function)
97    on translate_list ≝
98  match translate_list with
99  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
100  | cons trans translate_list ⇒
101    match translate_list with
102    [ nil ⇒ trans start_lbl dest_lbl def
103    | _ ⇒
104      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
105      let def ≝ trans start_lbl tmp_lbl def in
106        add_translates translate_list tmp_lbl dest_lbl def
107    ]
108  ].
109
110axiom register_fresh: universe RegisterTag → register.
111
112definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝
113  λdef.
114    let r ≝ register_fresh (ertl_if_runiverse def) in
115    let locals ≝ r :: ertl_if_locals def in
116    let ertl_if_luniverse' ≝ ertl_if_luniverse def in
117    let ertl_if_runiverse' ≝ ertl_if_runiverse def in
118    let ertl_if_params' ≝ ertl_if_params def in
119    let ertl_if_locals' ≝ locals in
120    let ertl_if_stacksize' ≝ ertl_if_stacksize def in
121    let ertl_if_graph' ≝ ertl_if_graph def in
122    let ertl_if_entry' ≝ ertl_if_entry def in
123    let ertl_if_exit' ≝ ertl_if_exit def in
124      〈mk_ertl_internal_function
125        ertl_if_luniverse' ertl_if_runiverse' ertl_if_params'
126        ertl_if_locals' ertl_if_stacksize' ertl_if_graph'
127        ertl_if_entry' ertl_if_exit', r〉.
128
129let rec fresh_regs
130  (def: ertl_internal_function) (n: nat)
131    on n ≝
132  match n with
133  [ O ⇒ 〈def, [ ]〉
134  | S n' ⇒
135    let 〈def', regs'〉 ≝ fresh_regs def n' in
136    let 〈def', reg〉 ≝ fresh_reg def' in
137      〈def', reg :: regs'〉
138  ].
139 
140axiom fresh_regs_length:
141  ∀def: ertl_internal_function.
142  ∀n: nat.
143    |(\snd (fresh_regs def n))| = n.
144
145definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). |\snd regs| = n ≝
146  λdef: ertl_internal_function.
147  λn: nat.
148    fresh_regs def n.
149  @fresh_regs_length
150qed.
151 
152definition save_hdws_internal ≝
153  λdestr_srcr: register × Register.
154  λstart_lbl: label.
155    let 〈destr, srcr〉 ≝ destr_srcr in
156      adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
157 
158definition save_hdws ≝
159  λl.
160    map ? ? save_hdws_internal l.
161   
162definition restore_hdws_internal ≝
163  λdestr_srcr: Register × register.
164  λstart_lbl: label.
165    let 〈destr, srcr〉 ≝ destr_srcr in
166    adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
167   
168definition swap_components ≝
169  λA, B: Type[0].
170  λp: A × B.
171  let 〈l, r〉 ≝ p in
172  〈r, l〉.
173   
174definition restore_hdws ≝
175  λl.
176    map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
177
178definition get_params_hdw_internal ≝
179  λstart_lbl: label.
180    adds_graph [ ertl_st_skip start_lbl ] start_lbl.
181
182definition get_params_hdw ≝
183  λparams: list register.
184  match params with
185  [ nil ⇒ [get_params_hdw_internal]
186  | _ ⇒
187    let l ≝ zip_pottier ? ? params RegisterParams in
188      save_hdws l
189  ].
190
191definition get_param_stack ≝
192  λoff: nat.
193  λdestr.
194  λstart_lbl, dest_lbl: label.
195  λdef.
196  let 〈def, addr1〉 ≝ fresh_reg def in
197  let 〈def, addr2〉 ≝ fresh_reg def in
198  let 〈def, tmpr〉 ≝ fresh_reg def in
199  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
200  adds_graph [
201    ertl_st_frame_size addr1 start_lbl;
202    ertl_st_int tmpr int_offset start_lbl;
203    ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
204    ertl_st_get_hdw tmpr RegisterSPL start_lbl;
205    ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
206    ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
207    ertl_st_get_hdw tmpr RegisterSPH start_lbl;
208    ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
209    ertl_st_load destr addr1 addr2 start_lbl
210  ] start_lbl dest_lbl def.
211 
212definition get_params_stack ≝
213  λparams.
214  match params with
215  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ]
216  | _ ⇒
217    let f ≝ λi. λr. get_param_stack i r in
218      mapi ? ? f params
219  ].
220
221definition get_params ≝
222  λparams.
223  let n ≝ min (length ? params) (length ? RegisterParams) in
224  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
225  let hdw_params ≝ get_params_hdw hdw_params in
226    hdw_params @ (get_params_stack stack_params).
227 
228definition add_prologue ≝
229  λparams: list register.
230  λsral.
231  λsrah.
232  λsregs.
233  λdef.
234  let start_lbl ≝ ertl_if_entry def in
235  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
236  match lookup ? ? (ertl_if_graph def) start_lbl
237    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_function with
238  [ None ⇒ λnone_absrd. ?
239  | Some last_stmt ⇒ λsome_prf.
240    let def ≝
241      add_translates
242         ((adds_graph [
243                     ertl_st_new_frame start_lbl
244                   ]) ::
245         (adds_graph [
246                      ertl_st_pop sral start_lbl;
247                      ertl_st_pop srah start_lbl
248                   ]) ::
249         (save_hdws sregs) @
250         (get_params params))
251        start_lbl tmp_lbl def
252    in
253      add_graph tmp_lbl last_stmt def
254  ] ?.
255  cases not_implemented (* dep. types here *)
256qed.
257
258definition save_return ≝
259  λret_regs.
260  λstart_lbl: label.
261  λdest_lbl: label.
262  λdef: ertl_internal_function.
263  let 〈def, tmpr〉 ≝ fresh_reg def in
264  match reduce_strong ? ? RegisterSTS ret_regs with
265  [ dp crl crl_proof ⇒
266    let commonl ≝ \fst (\fst crl) in
267    let commonr ≝ \fst (\snd crl) in
268    let restl ≝ \snd (\fst crl) in
269    let restr ≝ \snd (\snd crl) in
270    let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
271    let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
272    let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
273    let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
274    let defaults ≝ map ? ? f_default restl in
275      adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
276  ].
277
278definition assign_result ≝
279  λstart_lbl: label.
280  match reduce_strong ? ? RegisterRets RegisterSTS with
281  [ dp crl crl_proof ⇒
282    let commonl ≝ \fst (\fst crl) in
283    let commonr ≝ \fst (\snd crl) in
284    let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in
285    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
286      adds_graph insts start_lbl
287  ].
288
289definition add_epilogue ≝
290  λret_regs.
291  λsral.
292  λsrah.
293  λsregs.
294  λdef.
295  let start_lbl ≝ ertl_if_exit def in
296  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
297  match lookup ? ? (ertl_if_graph def) start_lbl
298    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with
299  [ None ⇒ λnone_absd. ?
300  | Some last_stmt ⇒ λsome_prf.
301    let def ≝
302      add_translates (
303        [save_return ret_regs] @
304        restore_hdws sregs @
305        [adds_graph [
306          ertl_st_push srah start_lbl;
307          ertl_st_push sral start_lbl
308        ]] @
309        [adds_graph [
310          ertl_st_del_frame start_lbl
311        ]] @
312        [assign_result]
313      ) start_lbl tmp_lbl def
314    in
315    let def ≝ add_graph tmp_lbl last_stmt def in
316      set_joint_if_exit … tmp_lbl def ?
317  ] ?.
318  cases not_implemented (* dep types here, bug in matita too! *)
319qed.
320 
321definition allocate_regs_internal ≝
322  λr: Register.
323  λdef_sregs.
324  let 〈def, sregs〉 ≝ def_sregs in
325  let 〈def, r'〉 ≝ fresh_reg def in
326    〈def, 〈r', r〉 :: sregs〉.
327 
328definition allocate_regs ≝
329  λrs.
330  λsaved: rs_set rs.
331  λdef.
332    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
333   
334definition add_pro_and_epilogue ≝
335  λparams.
336  λret_regs.
337  λdef.
338  match fresh_regs_strong def 2 with
339  [ dp def_sra def_sra_proof ⇒
340    let def ≝ \fst def_sra in
341    let sra ≝ \snd def_sra in
342    let sral ≝ nth_safe ? 0 sra ? in
343    let srah ≝ nth_safe ? 1 sra ? in
344    let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
345    let def ≝ add_prologue params sral srah sregs def in
346    let def ≝ add_epilogue ret_regs sral srah sregs def in
347      def
348  ].
349  [1: >def_sra_proof //
350  |2: >def_sra_proof //
351  ]
352qed.
353
354definition set_params_hdw ≝
355  λparams.
356  match params with
357  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
358  | _ ⇒
359    let l ≝ zip_pottier ? ? params RegisterParams in
360      restore_hdws l
361  ].
362
363definition set_param_stack ≝
364  λoff.
365  λsrcr.
366  λstart_lbl: label.
367  λdest_lbl: label.
368  λdef: ertl_internal_function.
369  let 〈def, addr1〉 ≝ fresh_reg def in
370  let 〈def, addr2〉 ≝ fresh_reg def in
371  let 〈def, tmpr〉 ≝ fresh_reg def in
372  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
373    adds_graph [
374      ertl_st_int addr1 int_off start_lbl;
375      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
376      ertl_st_clear_carry start_lbl;
377      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
378      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
379      ertl_st_int addr2 (zero ?) start_lbl;
380      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
381      ertl_st_store addr1 addr2 srcr start_lbl
382    ] start_lbl dest_lbl def.   
383
384definition set_params_stack ≝
385  λparams.
386  match params with
387  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
388  | _ ⇒
389    let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in
390      mapi ? ? f params
391  ].
392
393axiom min_fst:
394  ∀m, n: nat.
395    min m n ≤ m.
396
397definition set_params ≝
398  λparams.
399  let n ≝ min (|params|) (|RegisterParams|) in
400  let hdw_stack_params ≝ split ? params n ? in
401  let hdw_params ≝ \fst hdw_stack_params in
402  let stack_params ≝ \snd hdw_stack_params in
403    set_params_hdw hdw_params @ set_params_stack stack_params.
404  @min_fst
405qed.
406
407definition fetch_result ≝
408  λret_regs.
409  λstart_lbl: label.
410  match reduce_strong ? ? RegisterSTS RegisterRets with
411  [ dp crl first_crl_proof ⇒
412    let commonl ≝ \fst (\fst crl) in
413    let commonr ≝ \fst (\snd crl) in
414    let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lbl in
415    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
416    match reduce_strong ? ? ret_regs RegisterSTS with
417    [ dp crl second_crl_proof ⇒
418      let commonl ≝ \fst (\fst crl) in
419      let commonr ≝ \fst (\snd crl) in
420      let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lbl in
421      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
422        adds_graph (saves @ restores) start_lbl
423    ]
424  ].
425  [ normalize nodelta; @second_crl_proof
426  | @first_crl_proof
427  ]
428qed.
429
430definition translate_call_id ≝
431  λf.
432  λargs.
433  λret_regs.
434  λstart_lbl.
435  λdest_lbl.
436  λdef.
437  let nb_args ≝ |args| in
438    add_translates (
439      set_params args @ [
440      adds_graph [ ertl_st_call_id f nb_args start_lbl ];
441      fetch_result ret_regs
442      ]
443    ) start_lbl dest_lbl def.
444
445definition translate_stmt ≝
446  λlbl.
447  λstmt.
448  λdef.
449  match stmt with
450  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
451  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
452  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
453  | rtl_st_stack_addr r1 r2 lbl' ⇒
454    adds_graph [
455      ertl_st_get_hdw r1 RegisterSPL lbl;
456      ertl_st_get_hdw r2 RegisterSPH lbl
457    ] lbl lbl' def
458  | rtl_st_int r i lbl' ⇒  add_graph lbl (ertl_st_int r i lbl') def
459  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
460  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
461      add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
462(* XXX: change from o'caml
463    adds_graph [
464      ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
465      ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
466      ] lbl lbl' def
467*)
468  | rtl_st_op1 op1 destr srcr lbl' ⇒
469    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
470  | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
471    add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
472  | rtl_st_clear_carry lbl' ⇒
473    add_graph lbl (ertl_st_clear_carry lbl') def
474  | rtl_st_set_carry lbl' ⇒
475    add_graph lbl (ertl_st_set_carry lbl') def
476  | rtl_st_load destr addr1 addr2 lbl' ⇒
477    add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def
478  | rtl_st_store addr1 addr2 srcr lbl' ⇒
479    add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def
480  | rtl_st_call_id f args ret_regs lbl' ⇒
481    translate_call_id f args ret_regs lbl lbl' def
482  | rtl_st_cond srcr lbl_true lbl_false ⇒
483    add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def
484  | rtl_st_return ⇒
485    add_graph lbl ertl_st_return def
486  | _ ⇒ ? (* assert false: not implemented or should not happen *)
487  ].
488  cases not_implemented
489qed.   
490
491(* hack with empty graphs used here *)
492definition translate_funct_internal ≝
493  λdef.
494  let nb_params ≝ |rtl_if_params def| in
495  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
496  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
497  let entry' ≝ rtl_if_entry def in
498  let exit' ≝ rtl_if_exit def in
499  let graph' ≝ add ? ? (empty_map ? ?) entry' (ertl_st_skip entry') in
500  let graph' ≝ add ? ? graph' exit' (ertl_st_skip exit') in
501  let def' ≝
502    mk_ertl_internal_function
503      (rtl_if_luniverse def) (rtl_if_runiverse def)
504      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
505      graph' ? ? in
506  let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in
507  let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
508    def'.
509  [1: %
510      [1: @entry'
511      |2: normalize nodelta
512          @graph_add_lookup
513          @graph_add
514      ]
515  |2: %
516      [1: @exit'
517      |2: normalize nodelta
518          @graph_add
519      ]
520  ]
521qed.
522   
523definition translate_funct ≝
524  λid_def: ident × ?.
525  let 〈id, def〉 ≝ id_def in
526  let def' ≝
527    match def with
528    [ Internal def ⇒ Internal ? (translate_funct_internal def)
529    | External def ⇒ External ? def
530    ] in
531  〈id, def'〉.
532
533definition generate ≝
534  λstmt.
535  λdef.
536  let 〈entry, nuniv〉 ≝ fresh_label def in
537  let graph ≝ add ? ? (ertl_if_graph def) entry stmt in
538    mk_ertl_internal_function
539      nuniv (ertl_if_runiverse def) (ertl_if_params def)
540      (ertl_if_locals def) (ertl_if_stacksize def) graph
541      ? ?.
542  [1: %
543    [1: @entry
544    |2: normalize nodelta;
545        @graph_add
546    ]
547  |2: generalize in match (ertl_if_exit def)
548      #HYP
549      cases HYP
550      #LBL #LBL_PRF
551      %
552      [1: @LBL
553      |2: normalize nodelta;
554          @graph_add_lookup
555          @LBL_PRF
556      ]
557  ]
558qed.
559   
560let rec find_and_remove_first_cost_label_internal
561  (def: ertl_internal_function) (lbl: label) (num_nodes: nat)
562    on num_nodes ≝
563  match num_nodes with
564  [ O ⇒ 〈None ?, def〉
565  | S num_nodes' ⇒
566    match lookup ? ? (ertl_if_graph def) lbl with
567    [ None ⇒ 〈None ?, def〉
568    | Some stmt ⇒
569      match stmt with
570      [ ertl_st_cost cost_lbl next_lbl ⇒
571          〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉
572      | ertl_st_cond _ _ _ ⇒ 〈None ?, def〉
573      | ertl_st_return ⇒ 〈None ?, def〉
574      | ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
575      | ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
576      | ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
577      | ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
578      | ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
579      | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
580      | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
581      | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
582      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
583      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
584      | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
585      | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
586      | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
587      | ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
588      | ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
589      | ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
590      | ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
591      | ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
592      | ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
593      | ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
594      | ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
595      ]
596    ]
597  ].
598   
599definition find_and_remove_first_cost_label ≝
600  λdef. 
601    find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graph def)).
602
603definition move_first_cost_label_up_internal ≝
604  λdef.
605  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in
606  match cost_label with
607  [ None ⇒ def
608  | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
609  ].
610
611definition move_first_cost_label_up ≝
612  λA: Type[0].
613  λid_def: A × ?.
614  let 〈id, def〉 ≝ id_def in
615  let def' ≝
616    match def with
617    [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun)
618    | External ext ⇒ def
619    ]
620  in
621    〈id, def'〉.
622
623definition translate ≝
624  λp.
625  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
626  let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in
627  let vars ≝ map ? ? f (rtl_pr_functs p) in
628    mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
Note: See TracBrowser for help on using the repository browser.