source: src/RTL/RTLtoERTL.ma @ 763

Last change on this file since 763 was 763, checked in by mulligan, 10 years ago

Changes to RTL-ERTL pass.

File size: 4.9 KB
Line 
1include "RTL/RTL.ma".
2include "ERTL/ERTL.ma".
3
4definition change_exit_label ≝
5  λl: label.
6  λp: ertl_internal_function.
7  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
8  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
9  let ertl_if_params' ≝ ertl_if_params p in
10  let ertl_if_locals' ≝ ertl_if_locals p in
11  let ertl_if_graph' ≝ ertl_if_graph p in
12  let ertl_if_entry' ≝ ertl_if_entry p in
13  let ertl_if_exit' ≝ l in
14    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
15                              ertl_if_params' ertl_if_locals'
16                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
17
18definition change_entry_label ≝
19  λl: label.
20  λp: ertl_internal_function.
21  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
22  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
23  let ertl_if_params' ≝ ertl_if_params p in
24  let ertl_if_locals' ≝ ertl_if_locals p in
25  let ertl_if_graph' ≝ ertl_if_graph p in
26  let ertl_if_entry' ≝ l in
27  let ertl_if_exit' ≝ ertl_if_exit p in
28    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
29                              ertl_if_params' ertl_if_locals'
30                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
31                             
32definition add_graph ≝
33  λl: label.
34  λstmt.
35  λp.
36  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
37  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
38  let ertl_if_params' ≝ ertl_if_params p in
39  let ertl_if_locals' ≝ ertl_if_locals p in
40  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
41  let ertl_if_entry' ≝ ertl_if_entry p in
42  let ertl_if_exit' ≝ ertl_if_exit p in
43    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
44                              ertl_if_params' ertl_if_locals'
45                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
46                             
47definition fresh_label ≝
48  λdef.
49    fresh LabelTag (ertl_if_luniverse def).
50   
51definition change_label ≝
52  λl.
53  λe: ertl_statement.
54  match e with
55  [ ertl_st_skip _ ⇒ ertl_st_skip l
56  | ertl_st_comment s _ ⇒ ertl_st_comment s l
57  | ertl_st_cost c _ ⇒ ertl_st_cost c l
58  | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
59  | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
60  | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
61  | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
62  | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
63  | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
64  | ertl_st_pop r _ ⇒ ertl_st_pop r l
65  | ertl_st_push r _ ⇒ ertl_st_push r l
66  | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
67  | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
68  | ertl_st_int r i _ ⇒ ertl_st_int r i l
69  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
70  | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
71  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
72  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
73  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
74  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
75  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
76  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
77  | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
78  | ertl_st_return a ⇒ ertl_st_return a
79  ].
80 
81let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
82  match stmt_list with
83  [ nil ⇒ Some ? def
84  | cons hd tl ⇒
85    match tl with
86    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
87    | _ ⇒
88      let tmp_lbl ≝ fresh_label def in
89      match tmp_lbl with
90      [ OK o ⇒
91        let 〈lbl, univ〉 ≝ o in
92        let stmt ≝ change_label lbl hd in
93        let def ≝ add_graph start_lbl hd def in
94          adds_graph tl lbl dest_lbl def
95      | Error ⇒ None ?
96      ]
97    ]
98  ].
99
100let rec add_translates (translate_list: list (label → label → ertl_internal_function → ertl_internal_function))
101                       (start_lbl: label) (dest_lbl: label)
102                       (def: ertl_internal_function): option ertl_internal_function ≝
103  match translate_list with
104  [ nil ⇒ Some ? def
105  | cons hd tl ⇒
106    match tl with
107    [ nil ⇒ Some ? (hd start_lbl dest_lbl def)
108    | _ ⇒
109      let tmp_lbl ≝ fresh_label def in
110      match tmp_lbl with
111      [ OK o ⇒
112        let 〈lbl, univ〉 ≝ o in
113        let def ≝ hd start_lbl lbl def in
114          add_translates tl lbl dest_lbl def
115      | Error ⇒ None ?
116      ]
117    ]
118  ].
119 
120axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
121
122let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
123  match n with
124  [ O ⇒ 〈def, [ ]〉
125  | S n' ⇒
126    let 〈def', regs'〉 ≝ fresh_regs def n' in
127    let 〈def', reg〉 ≝ fresh_reg def' in
128      〈def', reg :: regs'〉
129  ].
130 
131definition save_hdws ≝
132  λ
Note: See TracBrowser for help on using the repository browser.