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_sig' ≝ rtl_if_sig def in |
---|

42 | let rtl_if_result' ≝ rtl_if_result def in |
---|

43 | let rtl_if_params' ≝ rtl_if_params def in |
---|

44 | let rtl_if_locals' ≝ rtl_if_locals def in |
---|

45 | let rtl_if_stacksize' ≝ rtl_if_stacksize def in |
---|

46 | let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in |
---|

47 | let rtl_if_entry' ≝ rtl_if_entry def in |
---|

48 | let rtl_if_exit' ≝ rtl_if_exit def in |
---|

49 | mk_rtl_internal_function |
---|

50 | rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' |
---|

51 | rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize' |
---|

52 | rtl_if_graph' rtl_if_entry' rtl_if_exit'. |
---|

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