source: src/RTL/RTLtoERTL.ma @ 939

Last change on this file since 939 was 783, checked in by mulligan, 10 years ago

rtl to ertl pass complete (modulo some straightforward axioms that need filling in) and refactoring to get rid of all the option types.

File size: 21.3 KB
Line 
1include "RTL/RTL.ma".
2include "RTL/RTLTailcall.ma".
3include "ERTL/ERTL.ma".
4include "utilities/RegisterSet.ma".
5
6definition change_exit_label ≝
7  λl: label.
8  λp: ertl_internal_function.
9  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
10  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
11  let ertl_if_params' ≝ ertl_if_params p in
12  let ertl_if_locals' ≝ ertl_if_locals p in
13  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
14  let ertl_if_graph' ≝ ertl_if_graph p in
15  let ertl_if_entry' ≝ ertl_if_entry p in
16  let ertl_if_exit' ≝ l in
17    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
18                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
19                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
20
21definition change_entry_label ≝
22  λl: label.
23  λp: ertl_internal_function.
24  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
25  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
26  let ertl_if_params' ≝ ertl_if_params p in
27  let ertl_if_locals' ≝ ertl_if_locals p in
28  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
29  let ertl_if_graph' ≝ ertl_if_graph p in
30  let ertl_if_entry' ≝ l in
31  let ertl_if_exit' ≝ ertl_if_exit p in
32    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
33                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
34                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
35                             
36definition add_graph ≝
37  λl: label.
38  λstmt.
39  λp.
40  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
41  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
42  let ertl_if_params' ≝ ertl_if_params p in
43  let ertl_if_locals' ≝ ertl_if_locals p in
44  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
45  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
46  let ertl_if_entry' ≝ ertl_if_entry p in
47  let ertl_if_exit' ≝ ertl_if_exit p in
48    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
49                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
50                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
51                             
52definition fresh_label ≝
53  λdef.
54    match fresh LabelTag (ertl_if_luniverse def) with
55    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
56    | Error ⇒ None ?
57    ].
58   
59definition change_label ≝
60  λl.
61  λe: ertl_statement.
62  match e with
63  [ ertl_st_skip _ ⇒ ertl_st_skip l
64  | ertl_st_comment s _ ⇒ ertl_st_comment s l
65  | ertl_st_cost c _ ⇒ ertl_st_cost c l
66  | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
67  | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
68  | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
69  | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
70  | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
71  | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
72  | ertl_st_pop r _ ⇒ ertl_st_pop r l
73  | ertl_st_push r _ ⇒ ertl_st_push r l
74  | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
75  | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
76  | ertl_st_int r i _ ⇒ ertl_st_int r i l
77  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
78  | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
79  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
80  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
81  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
82  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
83  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
84  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
85  | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
86  | ertl_st_return a ⇒ ertl_st_return a
87  ].
88 
89let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
90  match stmt_list with
91  [ nil ⇒ Some ? def
92  | cons hd tl ⇒
93    match tl with
94    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
95    | _ ⇒
96      let tmp_lbl ≝ fresh_label def in
97      match tmp_lbl with
98      [ Some tmp_lbl ⇒
99        let stmt ≝ change_label tmp_lbl hd in
100        let def ≝ add_graph start_lbl hd def in
101          adds_graph tl tmp_lbl dest_lbl def
102      | None ⇒ None ?
103      ]
104    ]
105  ].
106
107let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function))
108                       (start_lbl: label) (dest_lbl: label)
109                       (def: ertl_internal_function): option ertl_internal_function ≝
110  match translate_list with
111  [ nil ⇒ Some ? def
112  | cons hd tl ⇒
113    match tl with
114    [ nil ⇒ hd start_lbl dest_lbl def
115    | _ ⇒
116      let tmp_lbl ≝ fresh_label def in
117      match tmp_lbl with
118      [ Some tmp_lbl ⇒
119        match hd start_lbl tmp_lbl def with
120        [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def
121        | None ⇒ None ?
122        ]
123      | None ⇒ None ?
124      ]
125    ]
126  ].
127 
128axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
129
130let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
131  match n with
132  [ O ⇒ 〈def, [ ]〉
133  | S n' ⇒
134    let 〈def', regs'〉 ≝ fresh_regs def n' in
135    let 〈def', reg〉 ≝ fresh_reg def' in
136      〈def', reg :: regs'〉
137  ].
138 
139definition save_hdws_internal ≝
140  λdestr_srcr: register × hardware_register.
141  λstart_lbl: label.
142    let 〈destr, srcr〉 ≝ destr_srcr in
143      adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
144 
145definition save_hdws ≝
146  λl.
147    map ? ? save_hdws_internal l.
148   
149definition restore_hdws_internal ≝
150  λdestr_srcr: hardware_register × register.
151  λstart_lbl: label.
152    let 〈destr, srcr〉 ≝ destr_srcr in
153    adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
154   
155definition swap_components ≝
156  λA, B: Type[0].
157  λp: A × B.
158  let 〈l, r〉 ≝ p in
159  〈r, l〉.
160   
161definition restore_hdws ≝
162  λl.
163    map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
164
165definition get_params_hdw_internal ≝
166  λstart_lbl: label.
167    adds_graph [ ertl_st_skip start_lbl ] start_lbl.
168
169definition get_params_hdw ≝
170  λparams: list register.
171  match length ? params with
172  [ O ⇒ Some ? [ get_params_hdw_internal ]
173  | _ ⇒
174    match zip ? ? params parameters with
175    [ None ⇒ None ?
176    | Some l ⇒ Some ? (save_hdws l)
177    ]
178  ].
179
180definition get_param_stack ≝
181  λoff: nat.
182  λdestr.
183  λstart_lbl, dest_lbl: label.
184  λdef.
185  let 〈def, addr1〉 ≝ fresh_reg def in
186  let 〈def, addr2〉 ≝ fresh_reg def in
187  let 〈def, tmpr〉 ≝ fresh_reg def in
188  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
189  adds_graph [
190    ertl_st_frame_size addr1 start_lbl;
191    ertl_st_int tmpr int_offset start_lbl;
192    ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
193    ertl_st_get_hdw tmpr RegisterSPL start_lbl;
194    ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
195    ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
196    ertl_st_get_hdw tmpr RegisterSPH start_lbl;
197    ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
198    ertl_st_load destr addr1 addr2 start_lbl
199  ] start_lbl dest_lbl def.
200 
201definition get_params_stack_internal ≝
202  λi.
203  λr.
204    get_param_stack i r.
205 
206definition get_params_stack ≝
207  λparams.
208  match length ? params with
209  [ O ⇒ [ get_params_hdw_internal ]
210  | _ ⇒ mapi ? ? get_params_stack_internal params
211  ].
212
213definition get_params ≝
214  λparams.
215  let n ≝ min (length ? params) (length ? parameters) in
216  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
217  match get_params_hdw hdw_params with
218  [ None ⇒ None ?
219  | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params))
220  ].
221 
222definition add_prologue ≝
223  λparams.
224  λsral.
225  λsrah.
226  λsregs.
227  λdef.
228  let start_lbl ≝ ertl_if_entry def in
229  let tmp_lbl ≝ fresh_label def in
230  match tmp_lbl with
231  [ None ⇒ None ?
232  | Some tmp_lbl ⇒
233    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
234    let params ≝
235      match get_params params with
236      [ Some params ⇒ params
237      | None ⇒ [ ] (* dpm: is this ok? *)
238      ] in
239    let def ≝
240      add_translates (
241        adds_graph [ ertl_st_new_frame start_lbl ] ::
242        adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] ::
243        save_hdws sregs @
244        params) start_lbl tmp_lbl def in
245    match def with
246    [ Some def ⇒
247      match last_stmt with
248      [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def)
249      | None ⇒ None ?
250      ]
251    | None ⇒ None ?
252    ]
253  ].
254 
255definition allocate_regs_internal ≝
256  λr: register.
257  λdef_sregs.
258  let 〈def, sregs〉 ≝ def_sregs in
259  let 〈def, r'〉 ≝ fresh_reg def in
260    〈def, 〈r', r〉 :: sregs〉.
261 
262definition allocate_regs ≝
263  λrs: register_set.
264  λsaved: rs_set rs.
265  λdef.
266    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
267   
268definition save_return_internal ≝
269  λr.
270  λstart_lbl.
271  λdest_lbl.
272  λdef.
273  let 〈def, r_tmp〉 ≝ fresh_reg def in
274  adds_graph [
275    ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl;
276    ertl_st_set_hdw RegisterST0 r start_lbl;
277    ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def.
278   
279definition save_return_internal' ≝
280  λr1, r2.
281  λstart_lbl.
282  adds_graph [
283    ertl_st_set_hdw RegisterST0 r1 start_lbl;
284    ertl_st_set_hdw RegisterST1 r2 start_lbl
285  ] start_lbl.
286   
287definition save_return ≝
288  λret_regs.
289  match ret_regs with
290  [ nil ⇒ [ get_params_hdw_internal ]
291  | cons hd tl ⇒
292    match tl with
293    [ nil ⇒ [ save_return_internal hd ]
294    | cons hd' tl' ⇒ [ save_return_internal' hd hd' ]
295    ]
296  ].
297   
298definition add_epilogue ≝
299  λret_regs.
300  λsral.
301  λsrah.
302  λsregs.
303  λdef.
304  let start_lbl ≝ ertl_if_exit def in
305  let tmp_lbl ≝ fresh_label def in
306  match tmp_lbl with
307  [ None ⇒ None ?
308  | Some tmp_lbl ⇒
309    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
310    match last_stmt with
311    [ None ⇒ None ?
312    | Some last_stmt ⇒
313      let def ≝
314        add_translates (
315          save_return ret_regs @
316          restore_hdws sregs @
317          [adds_graph [
318            ertl_st_push srah start_lbl;
319            ertl_st_push sral start_lbl
320          ]] @
321          [adds_graph [
322            ertl_st_del_frame start_lbl
323          ]] @
324          [adds_graph [
325            ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl;
326            ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl
327          ]]) start_lbl tmp_lbl def in
328      match def with
329      [ None ⇒ None ?
330      | Some def ⇒
331        let def ≝ add_graph tmp_lbl last_stmt def in
332          Some ? (change_exit_label tmp_lbl def)
333      ]
334    ]
335  ].
336 
337axiom add_pro_and_epilogue:
338  ∀rs: register_set.
339  ∀params: list register.
340  ∀ret_args: list register.
341  ∀def: ertl_internal_function.
342    option ertl_internal_function.
343   
344(*
345  dpm: address callee_saved problem   
346definition add_pro_and_epilogue ≝
347  λrs: register_set.
348  λparams.
349  λret_args.
350  λdef.
351  let 〈def, sra〉 ≝ fresh_regs def 2 in
352  let sral ≝ safe_nth ? 0 sra ? in
353  let srah ≝ safe_nth ? 1 sra ? in
354  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
355  let def ≝ add_prologue params sral srah sregs def in
356  let def ≝ add_epilogue ret_args sral srah sregs def in
357    def. 
358*)
359
360definition set_params_hdw ≝
361  λparams.
362  match length ? params with
363  [ O ⇒ Some ? [ get_params_hdw_internal ]
364  | _ ⇒
365    match zip ? ? params parameters with
366    [ None ⇒ None ?
367    | Some zipped_params ⇒ Some ? (restore_hdws zipped_params)
368    ]
369  ].
370 
371definition set_param_stack ≝
372  λoff: nat.
373  λsrcr.
374  λstart_lbl, dest_lbl: label.
375  λdef.
376  let 〈def, addr1〉 ≝ fresh_reg def in
377  let 〈def, addr2〉 ≝ fresh_reg def in
378  let 〈def, tmpr〉 ≝ fresh_reg def in
379  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
380    adds_graph [
381      ertl_st_int addr2 int_offset start_lbl;
382      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
383      ertl_st_clear_carry start_lbl;
384      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
385      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
386      ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl;
387      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
388      ertl_st_store addr1 addr2 srcr start_lbl
389    ] start_lbl dest_lbl def.
390
391definition set_params_stack ≝
392  λparams.
393  match length ? params with
394  [ O ⇒ [ get_params_hdw_internal ]
395  | _ ⇒ mapi ? ? set_param_stack params
396 
397  ].
398 
399definition set_params ≝
400  λparams.
401  let n ≝ min (length ? params) (length ? parameters) in
402  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
403    match set_params_hdw hdw_params with
404    [ None ⇒ None ?
405    | Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params))
406    ].
407   
408definition fetch_result ≝
409  λret_regs.
410  λstart_lbl.
411  match ret_regs with
412  [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl
413  | cons hd tl ⇒
414    match tl with
415    [ nil ⇒
416      adds_graph [
417        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
418        ertl_st_get_hdw hd RegisterST0 start_lbl
419      ] start_lbl
420    | cons hd' tl' ⇒
421      adds_graph [
422        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
423        ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl;
424        ertl_st_get_hdw hd RegisterST0 start_lbl;
425        ertl_st_get_hdw hd' RegisterST1 start_lbl
426      ] start_lbl
427    ]
428  ].
429 
430definition translate_call_id ≝
431  λf.
432  λargs.
433  λret_regs.
434  λstart_lbl, dest_lbl: label.
435  λdef.
436  let nb_args ≝ bitvector_of_nat ? (length ? args) in
437  match set_params args with
438  [ None ⇒ None ?
439  | Some params_args ⇒
440    add_translates (
441      params_args @ [
442        adds_graph [ ertl_st_call_id f nb_args start_lbl ] ;
443        fetch_result ret_regs
444      ]) start_lbl dest_lbl def
445  ].
446 
447definition translate_stmt ≝
448  λlbl: label.
449  λstmt: rtl_statement.
450  λdef: ertl_internal_function.
451  match stmt with
452  [ rtl_st_skip lbl' ⇒
453    Some ? (add_graph lbl (ertl_st_skip lbl') def)
454  | rtl_st_cost cost_lbl lbl' ⇒
455    Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def)
456  | rtl_st_addr r1 r2 x lbl' ⇒
457    adds_graph [
458      ertl_st_addr_l r1 x lbl;
459      ertl_st_addr_h r2 x lbl
460    ] lbl lbl' def
461  | rtl_st_stack_addr r1 r2 lbl' ⇒
462    adds_graph [
463      ertl_st_get_hdw r1 RegisterSPL lbl;
464      ertl_st_get_hdw r2 RegisterSPH lbl
465    ] lbl lbl' def
466  | rtl_st_int r i lbl' ⇒
467    Some ? (add_graph lbl (ertl_st_int r i lbl') def)
468  | rtl_st_move r1 r2 lbl' ⇒
469    Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def)
470  | rtl_st_opaccs opaccs d s1 s2 lbl' ⇒
471    Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def)
472  | rtl_st_op1 op1 d s lbl' ⇒
473    Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def)
474  | rtl_st_op2 op2 d s1 s2 lbl' ⇒
475    Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def)
476  | rtl_st_clear_carry lbl' ⇒
477    Some ? (add_graph lbl (ertl_st_clear_carry lbl') def)
478  | rtl_st_load d a1 a2 lbl' ⇒
479    Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def)
480  | rtl_st_store a1 a2 s lbl' ⇒
481    Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def)
482  | rtl_st_call_id f args ret_regs lbl' ⇒
483    translate_call_id f args ret_regs lbl lbl' def
484  | rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *)
485  | rtl_st_cond_acc src lbl_true lbl_false ⇒
486    Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def)
487  | rtl_st_return ret_regs ⇒
488    Some ? (add_graph lbl (ertl_st_return ret_regs) def)
489  | rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *)
490  | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
491  ].
492   
493definition translate_funct_internal ≝
494  λdef.
495  let nb_params ≝ length ? (rtl_if_params def) in
496  let added_stacksize ≝ max 0 (nb_params - (length ? parameters)) in
497  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
498  let def' ≝
499    mk_ertl_internal_function
500      (rtl_if_luniverse def) (rtl_if_runiverse def)
501      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
502      (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
503  let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in
504  let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in
505    def'.
506   
507definition translate_funct ≝
508  λid_def: ident × ?.
509  let 〈id, def〉 ≝ id_def in
510  let def' ≝
511    match def with
512    [ rtl_f_internal def ⇒
513      match translate_funct_internal def with
514      [ None ⇒ None ?
515      | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
516      ]
517    | rtl_f_external def ⇒ Some ? (ertl_f_external def)
518    ] in
519  〈id, def'〉.
520
521definition generate ≝
522  λstmt.
523  λdef.
524  let entry ≝ fresh_label def in
525  match entry with
526  [ None ⇒ None ?
527  | Some entry ⇒
528    let def ≝ add_graph entry stmt def in
529      Some ? (change_entry_label entry def)
530  ].
531 
532let rec find_and_remove_first_cost_label_internal (def: ertl_internal_function)
533                                                  (lbl: label) (n: nat) on n ≝
534  match n with
535  [ O ⇒ None ?
536  | S n' ⇒
537    let statement_at_label ≝ lookup ? ? (ertl_if_graph def) lbl in
538    match statement_at_label with
539    [ None ⇒ None ?
540    | Some statement ⇒
541      match statement with
542      [ ertl_st_cost cost_lbl next_lbl ⇒
543        let def' ≝ add_graph lbl (ertl_st_skip next_lbl) def in
544          Some ? 〈Some ? cost_lbl, def'〉
545      | ertl_st_cond_acc _ _ _ ⇒ Some ? 〈None ?, def〉
546      | ertl_st_return _⇒ Some ? 〈None ?, def〉
547      | ertl_st_skip lbl' ⇒ find_and_remove_first_cost_label_internal def lbl' n'
548      | ertl_st_comment _ lbl' ⇒
549        find_and_remove_first_cost_label_internal def lbl' n'
550      | ertl_st_get_hdw _ _ lbl' ⇒
551        find_and_remove_first_cost_label_internal def lbl' n'
552      | ertl_st_set_hdw _ _ lbl' ⇒
553        find_and_remove_first_cost_label_internal def lbl' n'
554      | ertl_st_hdw_to_hdw _ _ lbl' ⇒
555        find_and_remove_first_cost_label_internal def lbl' n'
556      | ertl_st_pop _ lbl' ⇒
557        find_and_remove_first_cost_label_internal def lbl' n'
558      | ertl_st_push _ lbl' ⇒
559        find_and_remove_first_cost_label_internal def lbl' n'
560      | ertl_st_addr_h _ _ lbl' ⇒
561        find_and_remove_first_cost_label_internal def lbl' n'
562      | ertl_st_addr_l _ _ lbl' ⇒
563        find_and_remove_first_cost_label_internal def lbl' n'
564      | ertl_st_int _ _ lbl' ⇒
565        find_and_remove_first_cost_label_internal def lbl' n'
566      | ertl_st_move _ _ lbl' ⇒
567        find_and_remove_first_cost_label_internal def lbl' n'
568      | ertl_st_opaccs _ _ _ _ lbl' ⇒
569        find_and_remove_first_cost_label_internal def lbl' n'
570      | ertl_st_op2 _ _ _ _ lbl' ⇒
571        find_and_remove_first_cost_label_internal def lbl' n'
572      | ertl_st_op1 _ _ _ lbl' ⇒
573        find_and_remove_first_cost_label_internal def lbl' n'
574      | ertl_st_clear_carry lbl' ⇒
575        find_and_remove_first_cost_label_internal def lbl' n'
576      | ertl_st_load _ _ _ lbl' ⇒
577        find_and_remove_first_cost_label_internal def lbl' n'
578      | ertl_st_store _ _ _ lbl' ⇒
579        find_and_remove_first_cost_label_internal def lbl' n'
580      | ertl_st_call_id _ _ lbl' ⇒
581        find_and_remove_first_cost_label_internal def lbl' n'
582      | ertl_st_new_frame lbl' ⇒
583        find_and_remove_first_cost_label_internal def lbl' n'
584      | ertl_st_del_frame lbl' ⇒
585        find_and_remove_first_cost_label_internal def lbl' n'
586      | ertl_st_frame_size _ lbl' ⇒
587        find_and_remove_first_cost_label_internal def lbl' n'
588      ]
589    ]
590  ].
591 
592axiom num_entries:
593  ∀A: Type[0].
594  ∀g: graph A.
595    nat.
596 
597definition find_and_remove_first_cost_label ≝
598  λdef.
599    find_and_remove_first_cost_label_internal def (ertl_if_entry def) (num_entries ? (ertl_if_graph def)).
600
601definition move_first_cost_label_up_internal ≝
602  λdef.
603  let cost_label_def ≝ find_and_remove_first_cost_label def in
604  match cost_label_def with
605  [ None ⇒ None ?
606  | Some cost_label_def ⇒
607    let 〈cost_label, def〉 ≝ cost_label_def in
608    match cost_label with
609    [ None ⇒ Some ? def
610    | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
611    ]
612  ].
613 
614definition move_first_cost_label_up ≝
615  λid_def: ident × ?.
616  let 〈id, def〉 ≝ id_def in
617  let def' ≝
618    match def with 
619    [ ertl_f_internal int_fun ⇒
620      let cost_label_def ≝ move_first_cost_label_up_internal int_fun in
621      match cost_label_def with
622      [ None ⇒ None ?
623      | Some cost_label_def ⇒
624          Some ? (ertl_f_internal cost_label_def)
625      ]
626    | ertl_f_external _ ⇒ Some ? def
627    ] in
628  match def' with
629  [ None ⇒ None ?
630  | Some def' ⇒ Some ? 〈id, def'〉
631  ].
632 
633definition translate_internal ≝
634  λfunct.
635    let 〈id, funct〉 ≝ translate_funct funct in
636    match funct with
637    [ None ⇒ None ?
638    | Some funct ⇒ move_first_cost_label_up 〈id, funct〉
639    ].
640
641let rec strip_none (A: Type[0]) (l: list (option A)) on l: list A ≝
642  match l with
643  [ nil ⇒ nil ?
644  | cons hd tl ⇒
645    match hd with
646    [ None ⇒ strip_none A tl
647    | Some hd ⇒ hd :: strip_none A tl
648    ]
649  ].
650 
651definition translate: rtl_program → ertl_program ≝
652  λp.
653  let p ≝ tailcall_simplify p in
654  let rtl_pr_vars' ≝ rtl_pr_vars p in
655  let rtl_pr_functs' ≝ map … translate_internal (rtl_pr_functs p) in
656  let rtl_pr_functs_filtered ≝ strip_none ? rtl_pr_functs' in
657  let rtl_pr_main' ≝ rtl_pr_main p in
658    mk_ertl_program rtl_pr_vars' rtl_pr_functs_filtered rtl_pr_main'.
Note: See TracBrowser for help on using the repository browser.