source: src/RTL/RTLtoERTL.ma @ 1278

Last change on this file since 1278 was 1278, checked in by sacerdot, 10 years ago

oppargs requires two more arguments. RTLtoERTL to be fixed since it was
bugged anyway

File size: 20.5 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 … (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  λglobals.
187  λret_regs.
188  λstart_lbl: label.
189  λdest_lbl: label.
190  λdef: ertl_internal_function globals.
191  let 〈def, tmpr〉 ≝ fresh_reg … def in
192  match reduce_strong ? ? RegisterSTS ret_regs with
193  [ dp crl crl_proof ⇒
194    let commonl ≝ \fst (\fst crl) in
195    let commonr ≝ \fst (\snd crl) in
196    let restl ≝ \snd (\fst crl) in
197    let restr ≝ \snd (\snd crl) in
198    let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero ?)) start_lbl in
199    let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in
200    let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
201    let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in
202    let defaults ≝ map ? ? f_default restl in
203      adds_graph … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
204  ].
205
206definition assign_result ≝
207  λglobals.λstart_lbl: label.
208  match reduce_strong ? ? RegisterRets RegisterSTS with
209  [ dp crl crl_proof ⇒
210    let commonl ≝ \fst (\fst crl) in
211    let commonr ≝ \fst (\snd crl) in
212    let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in
213    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
214      adds_graph … insts start_lbl
215  ].
216
217definition add_epilogue ≝
218  λglobals.
219  λret_regs.
220  λsral.
221  λsrah.
222  λsregs.
223  λdef.
224  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
225  let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
226  match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
227    return λx. x ≠ None ? → ertl_internal_function globals with
228  [ None ⇒ λnone_absrd. ⊥
229  | Some last_stmt ⇒ λsome_prf.
230    let def ≝
231      add_translates … (
232        [save_return globals ret_regs] @
233        restore_hdws … sregs @
234        [adds_graph … [
235          joint_st_sequential … (joint_instr_push … srah) start_lbl;
236          joint_st_sequential … (joint_instr_push … sral) start_lbl
237        ]] @
238        [adds_graph … [
239          joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl
240        ]] @
241        [assign_result globals]
242      ) start_lbl tmp_lbl def
243    in
244    let def' ≝ add_graph … tmp_lbl last_stmt def in
245      set_joint_if_exit … tmp_lbl def' ?
246  ] ?.
247[ cases start_lbl #x #H @H
248| cases (none_absrd) /2/
249| cases daemon (* CSC: XXXXX *)
250]
251qed.
252 
253
254definition allocate_regs ≝
255  λglobals.
256  λrs.
257  λsaved: rs_set rs.
258  λdef.
259   let allocate_regs_internal ≝
260    λr: Register.
261    λdef_sregs.
262    let 〈def, sregs〉 ≝ def_sregs in
263    let 〈def, r'〉 ≝ fresh_reg globals def in
264      〈def, 〈r', r〉 :: sregs〉
265   in
266    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
267   
268definition add_pro_and_epilogue ≝
269  λglobals.
270  λparams.
271  λret_regs.
272  λdef.
273  match fresh_regs_strong globals def 2 with
274  [ dp def_sra def_sra_proof ⇒
275    let def ≝ \fst def_sra in
276    let sra ≝ \snd def_sra in
277    let sral ≝ nth_safe ? 0 sra ? in
278    let srah ≝ nth_safe ? 1 sra ? in
279    let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
280    let def ≝ add_prologue … params sral srah sregs def in
281    let def ≝ add_epilogue … ret_regs sral srah sregs def in
282      def
283  ].
284>def_sra_proof //
285qed.
286
287definition set_params_hdw ≝
288  λglobals,params.
289  match params with
290  [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl]
291  | _ ⇒
292    let l ≝ zip_pottier ? ? params RegisterParams in
293      restore_hdws globals l
294  ].
295
296definition set_param_stack ≝
297  λglobals.
298  λoff.
299  λsrcr.
300  λstart_lbl: label.
301  λdest_lbl: label.
302  λdef: ertl_internal_function globals.
303  let 〈def, addr1〉 ≝ fresh_reg … def in
304  let 〈def, addr2〉 ≝ fresh_reg … def in
305  let 〈def, tmpr〉 ≝ fresh_reg … def in
306  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
307    adds_graph ? [
308      joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl;
309      joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
310      joint_st_sequential … (joint_instr_clear_carry …) start_lbl;
311      joint_st_sequential … (joint_instr_op2 … Sub addr1 tmpr addr1) start_lbl;
312      joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
313      joint_st_sequential … (joint_instr_int … addr2 (zero ?)) start_lbl;
314      joint_st_sequential … (joint_instr_op2 … Sub addr2 tmpr addr2) start_lbl;
315      joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) start_lbl
316    ] start_lbl dest_lbl def.   
317
318definition set_params_stack ≝
319  λglobals,params.
320  match params with
321  [ nil ⇒ [ λstart_lbl. adds_graph globals [joint_st_goto … start_lbl] start_lbl]
322  | _ ⇒
323    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
324      mapi ? ? f params].
325
326definition set_params ≝
327  λglobals,params.
328  let n ≝ min (|params|) (|RegisterParams|) in
329  let hdw_stack_params ≝ split ? params n ? in
330  let hdw_params ≝ \fst hdw_stack_params in
331  let stack_params ≝ \snd hdw_stack_params in
332    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
333/2/
334qed.
335
336definition fetch_result ≝
337  λglobals.
338  λret_regs.
339  λstart_lbl: label.
340  match reduce_strong ? ? RegisterSTS RegisterRets with
341  [ dp crl first_crl_proof ⇒
342    let commonl ≝ \fst (\fst crl) in
343    let commonr ≝ \fst (\snd crl) in
344    let f_save ≝ λst. λret. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware st, hardware ret〉) start_lbl in
345    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
346    match reduce_strong ? ? ret_regs RegisterSTS with
347    [ dp crl second_crl_proof ⇒
348      let commonl ≝ \fst (\fst crl) in
349      let commonr ≝ \fst (\snd crl) in
350      let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in
351      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
352        adds_graph … (saves @ restores) start_lbl]].
353[@second_crl_proof | @first_crl_proof]
354qed.
355
356definition translate_call_id ≝
357  λglobals,f.
358  λargs.
359  λret_regs.
360  λstart_lbl.
361  λdest_lbl.
362  λdef.
363  let nb_args ≝ |args| in
364    add_translates globals (
365      set_params … args @ [
366      adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
367      fetch_result … ret_regs
368      ]
369    ) start_lbl dest_lbl def.
370
371definition translate_stmt :
372 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
373 ≝
374  λglobals.
375  λlbl.
376  λstmt.
377  λdef.
378  match stmt with
379  [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
380  | joint_st_return ⇒ add_graph … lbl (joint_st_return …) def
381  | joint_st_sequential seq lbl' ⇒
382     match seq with
383      [ joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
384      | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
385      | joint_instr_call_id f args ret_regs ⇒
386         translate_call_id … f args ret_regs lbl lbl' def
387      | joint_instr_move rs ⇒
388         let 〈r1,r2〉 ≝ rs in
389         let rs ≝ 〈pseudo r1, pseudo r2〉 in
390          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_move … rs) lbl') def
391      | joint_instr_extension ext ⇒
392         match ext with
393          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
394          | rtlntc_st_ext_address r1 r2 ⇒
395             adds_graph … [
396              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
397              joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
398             ] lbl lbl' def]
399      (*CSC: everything is just copied to re-type it from now on;
400        the problem is call_id that takes different parameters, but that is pattern-matched
401        above. It could be made nicer at the cost of making all the rest of the code uglier *)
402      | joint_instr_cost_label cost_lbl ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cost_label … cost_lbl) lbl') def
403      | joint_instr_address x prf r1 r2 ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_address … x prf r1 r2) lbl') def
404      | joint_instr_int r i ⇒  add_graph … lbl (joint_st_sequential ertl_params_ globals (joint_instr_int … r i) lbl') def
405      | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
406          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
407      | joint_instr_op1 op1 destr srcr ⇒
408        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op1 … op1 destr srcr) lbl') def
409      | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
410        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
411      | joint_instr_clear_carry ⇒
412        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_clear_carry …) lbl') def
413      | joint_instr_set_carry ⇒
414        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_set_carry …) lbl') def
415      | joint_instr_load destr addr1 addr2 ⇒
416        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_load … destr addr1 addr2) lbl') def
417      | joint_instr_store addr1 addr2 srcr ⇒
418        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_store … addr1 addr2 srcr) lbl') def
419      | joint_instr_cond srcr lbl_true ⇒
420        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cond … srcr lbl_true) lbl') def
421      | joint_instr_comment msg ⇒
422        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_comment … msg) lbl') def
423      ]].
424  cases not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
425qed.
426
427(* hack with empty graphs used here *)
428definition translate_funct_internal ≝
429  λglobals.λdef:rtlntc_internal_function globals.
430  let nb_params ≝ |joint_if_params ?? def| in
431  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
432  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
433  let entry' ≝ joint_if_entry … def in
434  let exit' ≝ joint_if_exit … def in
435  let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in
436  let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in
437  let def' ≝
438    mk_joint_internal_function globals (ertl_params globals)
439      (joint_if_luniverse … def) (joint_if_runiverse … def) it
440      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
441      graph' ? ? in
442  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
443   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
444whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
445                                 makes the next application fail. Why? *)   
446%
447 [ @entry' | @graph_add_lookup @graph_add
448 | @exit'  | @graph_add ]
449qed.
450
451definition generate ≝
452  λglobals.
453  λstmt.
454  λdef.
455  let 〈entry, nuniv〉 ≝ fresh_label … def in
456  let graph ≝ add ? ? (joint_if_code … def) entry stmt in
457    mk_joint_internal_function ? (ertl_params globals)
458      nuniv (joint_if_runiverse … def) it (joint_if_params … def)
459      (joint_if_locals … def) (joint_if_stacksize … def) graph
460      ? ?.     
461  [ % [ @entry | @graph_add ]
462  | cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF ]
463qed.
464
465let rec find_and_remove_first_cost_label_internal (globals: list ident)
466  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
467    on num_nodes ≝
468  match num_nodes with
469  [ O ⇒ 〈None ?, def〉
470  | S num_nodes' ⇒
471    match lookup … (joint_if_code … def) lbl with
472    [ None ⇒ 〈None ?, def〉
473    | Some stmt ⇒
474      match stmt with
475      [ joint_st_sequential inst lbl ⇒
476         match inst with
477          [ joint_instr_cost_label cost_lbl ⇒
478             〈Some … cost_lbl, add_graph ertl_params_ globals lbl (joint_st_goto … lbl) def〉
479          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
480      | joint_st_return ⇒ 〈None …, def〉
481      | joint_st_goto lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
482      ]]].
483   
484definition find_and_remove_first_cost_label ≝
485  λglobals,def. 
486    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
487
488definition move_first_cost_label_up_internal ≝
489  λglobals,def.
490  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
491  match cost_label with
492  [ None ⇒ def
493  | Some cost_label ⇒ generate … (joint_st_sequential ertl_params_ globals (joint_instr_cost_label … cost_label) (joint_if_entry … def)) def
494  ].
495
496definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
497
498definition translate : rtl_program → ertl_program ≝
499 λp.
500  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
501    transform_program ??? p (transf_fundef ?? (translate_funct …)).
Note: See TracBrowser for help on using the repository browser.