source: src/RTL/RTLtoERTL.ma @ 1071

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

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

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