[784] | 1 | include "RTL/RTL.ma". |
---|
| 2 | |
---|
| 3 | definition simplify_stmt ≝ |
---|
[1270] | 4 | λglobals. |
---|
[784] | 5 | λexit: label. |
---|
[2286] | 6 | λstmt: joint_statement RTL globals. |
---|
[784] | 7 | match stmt with |
---|
[2286] | 8 | [ final fin ⇒ |
---|
| 9 | match fin with |
---|
[2490] | 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 | ]. |
---|
[1081] | 38 | |
---|
[2490] | 39 | definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝ |
---|
| 40 | λtag,A,B,f,m. |
---|
| 41 | match m with |
---|
| 42 | [ an_id_map m ⇒ an_id_map … (map … f m) |
---|
| 43 | ]. |
---|
| 44 | |
---|
[784] | 45 | definition simplify_graph ≝ |
---|
[1270] | 46 | λglobals. |
---|
[1081] | 47 | λexit: label. |
---|
[2286] | 48 | λgraph: codeT RTL globals. |
---|
[2490] | 49 | id_map_map … (simplify_stmt globals exit) graph. |
---|
[1081] | 50 | |
---|
| 51 | axiom simplify_graph_preserves_labels: |
---|
[1270] | 52 | ∀globals. |
---|
[2286] | 53 | ∀g: codeT RTL globals. |
---|
[1081] | 54 | ∀exit: label. |
---|
[2286] | 55 | ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g. |
---|
[784] | 56 | |
---|
[1270] | 57 | definition simplify_internal : |
---|
| 58 | ∀globals. |
---|
[2490] | 59 | joint_closed_internal_function RTL globals → |
---|
| 60 | joint_closed_internal_function RTL_ntc globals |
---|
[1270] | 61 | ≝ |
---|
| 62 | λglobals,def. |
---|
| 63 | let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in |
---|
[2490] | 64 | «mk_joint_internal_function … |
---|
[1270] | 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 |
---|
[2490] | 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) ] |
---|
[1270] | 71 | #l #IH @simplify_graph_preserves_labels @IH |
---|
[1081] | 72 | qed. |
---|
[784] | 73 | |
---|
[2286] | 74 | definition tailcall_simplify : rtl_program → rtl_ntc_program ≝ |
---|
[2103] | 75 | λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)). |
---|