source: src/RTL/RTLtoERTL.ma @ 1250

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