source: src/RTL/RTLtoERTL.ma @ 1149

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