source: src/RTL/RTLTailcall.ma @ 1081

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

completed rtl-ertl pass

File size: 2.1 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 simplify_funct ≝
61  λid_def: ident × ?.
62  let 〈id, def〉 ≝ id_def in
63  let def' ≝
64    match def with
65    [ Internal def ⇒ Internal ? (simplify_internal def)
66    | External def ⇒ External ? def
67    ]
68  in
69    〈id, def'〉.
70 
71definition tailcall_simplify ≝
72  λp.
73  let rtl_pr_vars' ≝ rtl_pr_vars p in
74  let rtl_pr_functs' ≝ map ? ? simplify_funct (rtl_pr_functs p) in
75  let rtl_pr_main' ≝ rtl_pr_main p in
76    mk_rtl_program rtl_pr_vars' rtl_pr_functs' rtl_pr_main'.
Note: See TracBrowser for help on using the repository browser.