source: src/RTL/RTLTailcall.ma @ 2640

Last change on this file since 2640 was 2490, checked in by tranquil, 7 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File size: 2.5 KB
Line 
1include "RTL/RTL.ma".
2
3definition simplify_stmt ≝
4  λglobals.
5  λexit: label.
6  λstmt: joint_statement RTL globals.
7  match stmt with
8  [ final fin ⇒
9     match fin with
10      [ TAILCALL _ f args ⇒ sequential … (CALL RTL_ntc ? f args [ ]) exit
11      | RETURN ⇒ RETURN RTL_ntc
12      | GOTO l ⇒ GOTO RTL_ntc l
13      ]
14  | sequential s next ⇒
15    sequential RTL_ntc ?
16    (match s return λ_.joint_step RTL_ntc globals with
17    [ step_seq s ⇒
18      match s return λ_.joint_seq RTL_ntc globals with
19      [ COMMENT s ⇒ COMMENT … s
20      | COST_LABEL l ⇒ COST_LABEL … l
21      | MOVE m ⇒ MOVE … m
22      | POP a ⇒ POP … a
23      | PUSH a ⇒ PUSH … a
24      | ADDRESS i prf dpl dph ⇒ ADDRESS … i prf dpl dph
25      | OPACCS op a b arg1 arg2 ⇒ OPACCS … op a b arg1 arg2
26      | OP1 op a arg ⇒ OP1 … op a arg
27      | OP2 op a arg1 arg2 ⇒ OP2 … op a arg1 arg2
28      | CLEAR_CARRY ⇒ CLEAR_CARRY ??
29      | SET_CARRY ⇒ SET_CARRY ??
30      | LOAD a dpl dph ⇒ LOAD … a dpl dph
31      | STORE dpl dph a ⇒ STORE … dpl dph a
32      | CALL f args dest ⇒ CALL … f args dest
33      | extension_seq s ⇒ extension_seq … s
34      ]
35    | COND a ltrue ⇒ COND … a ltrue
36    ]) next
37  ].
38
39definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝
40λtag,A,B,f,m.
41match m with
42[ an_id_map m ⇒ an_id_map … (map … f m)
43].
44
45definition simplify_graph ≝
46  λglobals.
47  λexit: label.
48  λgraph: codeT RTL globals.
49  id_map_map … (simplify_stmt globals exit) graph.
50
51axiom simplify_graph_preserves_labels:
52  ∀globals.
53  ∀g: codeT RTL globals.
54  ∀exit: label.
55  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
56   
57definition simplify_internal :
58 ∀globals.
59  joint_closed_internal_function RTL globals →
60   joint_closed_internal_function RTL_ntc globals
61
62  λglobals,def.
63    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
64    «mk_joint_internal_function …
65       (joint_if_luniverse … def) (joint_if_runiverse … def)
66       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
67       (joint_if_stacksize … def) graph
68       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)), ?».
69 [3: cases daemon (* TODO *)
70 | cases (joint_if_exit … def) | cases (joint_if_entry … def) ]
71 #l #IH @simplify_graph_preserves_labels @IH
72qed.
73
74definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
75 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracBrowser for help on using the repository browser.