source: src/RTL/RTLTailcall.ma @ 1080

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

more added

File size: 2.1 KB
Line 
1include "RTL/RTL.ma".
2
3(* dpm: this should not be option, fix *)
4axiom 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
11definition 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 
24definition 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 
32definition simplify_graph ≝
33  λexit.
34  λgraph: rtl_statement_graph.
35    map_fold ? ? (lift_option3 ? ? ? ? (simplify_stmt exit)) graph graph.
36   
37definition 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
54definition 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 
64definition 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'.
Note: See TracBrowser for help on using the repository browser.