source: src/RTL/RTLTailcall_paolo.ma @ 2211

Last change on this file since 2211 was 2162, checked in by tranquil, 9 years ago
  • yet another correction to joint
  • added functions adding prologues and epilogues in TranslateUtils?. Adding a prologue will preserve the invariant of having a cost label at the start of the function, without needing transformations later
  • redefined ERTL and rewritten RTLToERTL (with suffix "_paolo")
File size: 1.8 KB
Line 
1include "RTL/RTL_paolo.ma".
2
3definition simplify_stmt ≝
4  λglobals.
5  λexit: label.
6  λlbl: label.
7  λstmt: rtl_statement globals.
8  λgraph: codeT rtlntc_params globals.
9  match stmt with
10  [ final fin ⇒
11     match fin with
12      [ tailcall ext ⇒
13         match ext with
14          [ rtl_tailcall_id f args ⇒
15              add … graph lbl (sequential … (CALL_ID rtlntc_params ? f args [ ]) exit)
16          | rtl_tailcall_ptr f1 f2 args ⇒
17              add … graph lbl (sequential rtlntc_params ? (rtl_call_ptr f1 f2 args [ ] : ext_call rtlntc_params) exit)
18          ]
19      | _ ⇒ graph ]
20  | _ ⇒ graph ].
21
22definition simplify_graph ≝
23  λglobals.
24  λexit: label.
25  λgraph: codeT rtl_params globals.
26    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
27
28axiom simplify_graph_preserves_labels:
29  ∀globals.
30  ∀g: codeT rtl_params globals.
31  ∀exit: label.
32  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
33   
34definition simplify_internal :
35 ∀globals.
36  joint_internal_function globals rtl_params →
37   joint_internal_function globals rtlntc_params
38
39  λglobals,def.
40    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
41      mk_joint_internal_function …
42       (joint_if_luniverse … def) (joint_if_runiverse … def)
43       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
44       (joint_if_stacksize … def) graph
45       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
46 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
47 #l #IH @simplify_graph_preserves_labels @IH
48qed.
49
50definition tailcall_simplify : rtl_program → rtlntc_program ≝
51 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracBrowser for help on using the repository browser.