source: src/RTL/RTLtoERTL.ma @ 936

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