source: src/RTL/RTLtoERTL.ma @ 1081

Last change on this file since 1081 was 1081, checked in by mulligan, 9 years ago

completed rtl-ertl pass

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