1 | include "RTL/RTL.ma". |
---|
2 | |
---|
3 | (* dpm: this should not be option, fix *) |
---|
4 | axiom map_fold: |
---|
5 | ∀A, B: Type[0]. |
---|
6 | ∀f: label → A → B → option B. |
---|
7 | ∀m: rtl_statement_graph. |
---|
8 | ∀b: B. |
---|
9 | B. |
---|
10 | |
---|
11 | definition simplify_stmt ≝ |
---|
12 | λexit: label. |
---|
13 | λlbl: label. |
---|
14 | λstmt. |
---|
15 | λgraph: rtl_statement_graph. |
---|
16 | match stmt with |
---|
17 | [ rtl_st_tailcall_id f args ⇒ |
---|
18 | add ? ? graph lbl (rtl_st_call_id f args [ ] exit) |
---|
19 | | rtl_st_tailcall_ptr f1 f2 args ⇒ |
---|
20 | add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit) |
---|
21 | | _ ⇒ graph |
---|
22 | ]. |
---|
23 | |
---|
24 | definition lift_option3: ∀A, B, C, D. ∀f: A → B → C → D. A → B → C → option D ≝ |
---|
25 | λA, B, C, D: Type[0]. |
---|
26 | λf: A → B → C → D. |
---|
27 | λa: A. |
---|
28 | λb: B. |
---|
29 | λc: C. |
---|
30 | Some ? (f a b c). |
---|
31 | |
---|
32 | definition simplify_graph ≝ |
---|
33 | λexit. |
---|
34 | λgraph: rtl_statement_graph. |
---|
35 | map_fold ? ? (lift_option3 ? ? ? ? (simplify_stmt exit)) graph graph. |
---|
36 | |
---|
37 | definition simplify_internal ≝ |
---|
38 | λdef. |
---|
39 | let rtl_if_luniverse' ≝ rtl_if_luniverse def in |
---|
40 | let rtl_if_runiverse' ≝ rtl_if_runiverse def in |
---|
41 | let rtl_if_result' ≝ rtl_if_result def in |
---|
42 | let rtl_if_params' ≝ rtl_if_params def in |
---|
43 | let rtl_if_locals' ≝ rtl_if_locals def in |
---|
44 | let rtl_if_stacksize' ≝ rtl_if_stacksize def in |
---|
45 | let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in |
---|
46 | let rtl_if_entry' ≝ rtl_if_entry def in |
---|
47 | let rtl_if_exit' ≝ rtl_if_exit def in |
---|
48 | mk_rtl_internal_function |
---|
49 | rtl_if_luniverse' rtl_if_runiverse' |
---|
50 | rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize' |
---|
51 | rtl_if_graph' ? ?. |
---|
52 | [1: normalize nodelta; |
---|
53 | |
---|
54 | definition simplify_funct ≝ |
---|
55 | λid_def: ident × ?. |
---|
56 | let 〈id, def〉 ≝ id_def in |
---|
57 | let def' ≝ |
---|
58 | match def with |
---|
59 | [ rtl_f_internal def ⇒ rtl_f_internal (simplify_internal def) |
---|
60 | | rtl_f_external def ⇒ rtl_f_external def |
---|
61 | ] in |
---|
62 | 〈id, def'〉. |
---|
63 | |
---|
64 | definition tailcall_simplify ≝ |
---|
65 | λp. |
---|
66 | let rtl_pr_vars' ≝ rtl_pr_vars p in |
---|
67 | let rtl_pr_functs' ≝ map ? ? simplify_funct (rtl_pr_functs p) in |
---|
68 | let rtl_pr_main' ≝ rtl_pr_main p in |
---|
69 | mk_rtl_program rtl_pr_vars' rtl_pr_functs' rtl_pr_main'. |
---|