source: src/RTL/RTLTailcall.ma @ 1396

Last change on this file since 1396 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
RevLine 
[784]1include "RTL/RTL.ma".
2
3definition simplify_stmt ≝
[1270]4  λglobals.
[784]5  λexit: label.
6  λlbl: label.
[1270]7  λstmt: rtl_statement globals.
[1275]8  λgraph: codeT … (rtlntc_params globals).
[784]9  match stmt with
[1282]10  [ sequential seq DUMMY ⇒
[1270]11     match seq with
[1282]12      [ extension ext ⇒
[1270]13         match ext with
14          [ rtl_st_ext_tailcall_id f args ⇒
[1282]15              add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)
[1270]16          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
[1282]17              add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
[1270]18          | _ ⇒ graph ]
19      | _ ⇒ graph ]
20  | _ ⇒ graph ].
[1081]21
[784]22definition simplify_graph ≝
[1270]23  λglobals.
[1081]24  λexit: label.
[1270]25  λgraph: codeT … (rtl_params globals).
[1275]26    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
[1081]27
28axiom simplify_graph_preserves_labels:
[1270]29  ∀globals.
30  ∀g: codeT … (rtl_params globals).
[1081]31  ∀l: label.
32  ∀exit: label.
[1270]33    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
[784]34   
[1270]35definition simplify_internal :
36 ∀globals.
37  joint_internal_function … (rtl_params globals) →
[1275]38   joint_internal_function … (rtlntc_params globals)
[1270]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
[1081]49qed.
[784]50
[1275]51definition tailcall_simplify : rtl_program → rtlntc_program ≝
[1282]52 λp. transform_program … p (transf_fundef … (simplify_internal …)).
Note: See TracBrowser for help on using the repository browser.