source: src/RTL/RTLTailcall.ma @ 1240

Last change on this file since 1240 was 1240, checked in by sacerdot, 8 years ago

Ported to common definitions.

File size: 1.8 KB
Line 
1include "RTL/RTL.ma".
2
3definition simplify_stmt ≝
4  λexit: label.
5  λlbl: label.
6  λstmt.
7  λgraph: rtl_statement_graph.
8  match stmt with
9  [ rtl_st_tailcall_id f args ⇒
10      add ? ? graph lbl (rtl_st_call_id f args [ ] exit)
11  | rtl_st_tailcall_ptr f1 f2 args ⇒
12      add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit)
13  | _ ⇒ graph
14  ].
15
16definition simplify_graph ≝
17  λexit: label.
18  λgraph: rtl_statement_graph.
19    foldi ? ? ? (simplify_stmt exit) graph graph.
20
21axiom simplify_graph_preserves_labels:
22  ∀g: rtl_statement_graph.
23  ∀l: label.
24  ∀exit: label.
25    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.
26   
27definition simplify_internal ≝
28  λdef.
29    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
30    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
31    let rtl_if_result' ≝ rtl_if_result def in
32    let rtl_if_params' ≝ rtl_if_params def in
33    let rtl_if_locals' ≝ rtl_if_locals def in
34    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
35    let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in
36    let rtl_if_entry' ≝ rtl_if_entry def in
37    let rtl_if_exit' ≝ rtl_if_exit def in
38      mk_rtl_internal_function
39        rtl_if_luniverse' rtl_if_runiverse'
40        rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
41        rtl_if_graph' ? ?.
42  normalize nodelta
43  [1: cases rtl_if_entry'
44      #ENTRY #ENTRY_PRF
45      %
46      [1: @ENTRY
47      |2: @simplify_graph_preserves_labels
48          @ENTRY_PRF
49      ]
50  |2: cases rtl_if_exit'
51      #EXIT #EXIT_PRF
52      %
53      [1: @EXIT
54      |2: @simplify_graph_preserves_labels
55          @EXIT_PRF
56      ]
57  ]
58qed.
59
60definition tailcall_simplify : rtl_program → rtl_program ≝
61 λp. transform_program … p (transf_fundef … simplify_internal).
Note: See TracBrowser for help on using the repository browser.