| 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'. |
|---|
