source: src/RTL/RTLtoERTL.ma @ 1252

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

graph_params added to joint/Joint.ma, together with useful common setters/getters

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