source: src/RTL/RTLTailcall.ma @ 1299

Last change on this file since 1299 was 1282, checked in by sacerdot, 9 years ago

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File size: 1.8 KB
Line 
1include "RTL/RTL.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  [ sequential seq DUMMY ⇒
11     match seq with
12      [ extension ext ⇒
13         match ext with
14          [ rtl_st_ext_tailcall_id f args ⇒
15              add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)
16          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
17              add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
18          | _ ⇒ graph ]
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  ∀l: label.
32  ∀exit: label.
33    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
34   
35definition simplify_internal :
36 ∀globals.
37  joint_internal_function … (rtl_params globals) →
38   joint_internal_function … (rtlntc_params globals)
39
40  λglobals,def.
41    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
42      mk_joint_internal_function …
43       (joint_if_luniverse … def) (joint_if_runiverse … def)
44       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
45       (joint_if_stacksize … def) graph
46       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
47 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
48 #l #IH @simplify_graph_preserves_labels @IH
49qed.
50
51definition tailcall_simplify : rtl_program → rtlntc_program ≝
52 λp. transform_program … p (transf_fundef … (simplify_internal …)).
Note: See TracBrowser for help on using the repository browser.