source: src/RTL/RTLtoERTL.ma @ 1278

Last change on this file since 1278 was 1278, checked in by sacerdot, 9 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.