source: src/RTL/RTLtoERTL.ma @ 1238

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

changes to get everything type checking again after changing names of registers in i8051

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