source: src/RTL/RTLtoERTL.ma @ 1071

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