source: src/RTL/RTLtoERTL.ma @ 1257

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

More progress in porting to joint datatype.

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