source: src/ERTL/ERTLToLTL.ma @ 1167

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

moved joint ltl lin files into their own directory. more changes to ltl and lin passes to help type checker in ertl pass

File size: 21.6 KB
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3include "ERTL/spill.ma".
4include "ASM/Arithmetic.ma".
5
6(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
7
8inductive decision: Type[0] ≝
9  | decision_spill: Byte → decision
10  | decision_colour: Register → decision.
11 
12axiom lookup: register → decision.
13
14definition fresh_label ≝
15  λglobals: list ident.
16  λluniv.
17    fresh LabelTag luniv.
18
19definition add_graph ≝
20  λglobals.
21  λlabel.
22  λstmt: ltl_statement globals.
23  λgraph: ltl_statement_graph globals.
24    add LabelTag ? graph label stmt.
25
26definition generate ≝
27  λglobals: list ident.
28  λluniv.
29  λgraph: ltl_statement_graph globals.
30  λstmt: ltl_statement globals.
31  let 〈l, luniv〉 ≝ fresh_label globals luniv in
32  let graph ≝ add_graph globals l stmt graph in
33    〈l, graph, luniv〉.
34
35definition num_locals ≝
36  λglobals.
37  λint_fun.
38    colour_locals + (ertl_if_stacksize globals int_fun).
39
40definition stacksize ≝
41  λglobals.
42  λint_fun.
43    colour_locals + (ertl_if_stacksize globals int_fun).
44
45definition adjust_off ≝
46  λglobals.
47  λint_fun.
48  λoff.
49  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
50  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
51    sub.
52
53definition get_stack ≝
54  λglobals: list ident.
55  λint_fun.
56  λgraph: graph (ltl_statement (globals)).
57  λr.
58  λoff.
59  λl.
60    let off ≝ adjust_off globals int_fun off in
61    let luniv ≝ ertl_if_luniverse globals int_fun in
62    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ??????? globals (joint_instr_move … globals (from_acc r)) l) in
63    ?.
64   
65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
66    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
67    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
68    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
69    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
70    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
71      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
72
73definition set_stack ≝
74  λint_fun.
75  λglobals.
76  λgraph: graph (ltl_statement (globals)).
77  λoff.
78  λr.
79  λl.
80  let off ≝ adjust_off int_fun off in
81  let luniv ≝ ertl_if_luniverse int_fun in
82  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
83  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
84  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
86  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
87  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
88  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
89    〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
90
91definition write ≝
92  λint_fun.
93  λglobals.
94  λgraph: graph (ltl_statement (globals)).
95  λr: register.
96  λl: label.
97  match lookup r with
98  [ decision_spill off ⇒
99    let 〈stmt, graph, luniv〉 ≝ set_stack int_fun globals graph off RegisterSST l in
100    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
101      〈RegisterSST, 〈l, 〈graph, luniv〉〉〉
102  | decision_colour hwr ⇒
103    let luniv ≝ ertl_if_luniverse int_fun in
104      〈hwr, 〈l, 〈graph, luniv〉〉〉
105  ].
106
107definition read ≝
108  λint_fun.
109  λglobals.
110  λgraph: graph (ltl_statement (globals)).
111  λr: register.
112  λstmt: Register → ltl_statement globals.
113  match lookup r with
114  [ decision_colour hwr ⇒ generate globals graph (stmt hwr)
115  | decision_spill off ⇒
116    let temphwr ≝ RegisterSST in
117    let 〈l, graph〉 ≝ generate globals graph (stmt temphwr) in
118    let 〈stmt, graph〉 ≝ get_stack int_fun globals graph temphwr off l in
119      generate globals graph stmt
120  ].
121
122definition move ≝
123  λint_fun.
124  λglobals: list ident.
125  λgraph: graph (ltl_statement globals).
126  λdest: decision.
127  λsrc: decision.
128  λl: label.
129  match dest with
130  [ decision_colour dest_hwr ⇒
131    match src with
132    [ decision_colour src_hwr ⇒
133      if eq_Register dest_hwr src_hwr then
134        〈joint_st_goto ? globals l, graph〉
135      else
136        let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
137          〈joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l, graph〉
138    | decision_spill src_off ⇒ get_stack int_fun globals graph dest_hwr src_off l
139    ]
140  | decision_spill dest_off ⇒
141    match src with
142    [ decision_colour src_hwr ⇒ set_stack int_fun globals graph dest_off src_hwr l
143    | decision_spill src_off ⇒
144      if eq_bv ? dest_off src_off then
145        〈joint_st_goto ? globals l, graph〉
146      else
147        let temp_hwr ≝ RegisterSST in
148        let 〈stmt, graph〉 ≝ set_stack int_fun globals graph dest_off temp_hwr l in
149        let 〈l, graph〉 ≝ generate globals graph stmt in
150          get_stack int_fun globals graph temp_hwr src_off l
151    ]
152  ].
153
154definition newframe ≝
155  λint_fun.
156  λglobals.
157  λgraph: graph (ltl_statement globals).
158  λl.
159  if eq_nat (stacksize int_fun) 0 then
160    〈joint_st_goto ? globals l, graph〉
161  else
162    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
163    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
164    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
165    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
166    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
167    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
168    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
169    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in
170      〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph〉.
171
172definition delframe ≝
173  λint_fun.
174  λglobals.
175  λgraph: graph (ltl_statement globals).
176  λl.
177  if eq_nat (stacksize int_fun) 0 then
178    〈joint_st_goto ? globals l, graph〉
179  else
180    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
181    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
182    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
183    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
184    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
185      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉.
186
187definition translate_statement ≝
188  λint_fun.
189  λglobals: list ident.
190  λgraph: graph (ltl_statement globals).
191  λstmt: ertl_statement.
192  match stmt with
193  [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉
194  | ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
195  | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
196  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
197  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
198  | ertl_st_hdw_to_hdw r1 r2 l ⇒
199    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
200      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
201  | ertl_st_new_frame l ⇒ newframe int_fun globals graph l
202  | ertl_st_del_frame l ⇒ delframe int_fun globals graph l
203  | ertl_st_frame_size r l ⇒
204    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
205    let 〈l, graph〉 ≝ l in
206      〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉
207  | ertl_st_pop r l ⇒
208    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
209    let 〈l, graph〉 ≝ l in
210    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
211      〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉
212  | ertl_st_push r l ⇒
213    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in
214    let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
215      〈joint_st_goto ? globals l, graph〉
216  | ertl_st_addr rl rh x l ⇒
217    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
218    let 〈l, graph〉 ≝ l in
219    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
220    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
221    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
222    let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
223    let 〈l, graph〉 ≝ l in
224    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
225    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
226      〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
227(*  | ertl_st_addr_h r x l ⇒
228    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
229    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
230    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
231      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
232  | ertl_st_addr_l r x l ⇒
233    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
234    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
235    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
236      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
237*)
238  | ertl_st_int r i l ⇒
239    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
240    let 〈l, graph〉 ≝ l in
241      〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉
242  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
243  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
244    let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in
245    let 〈l, graph〉 ≝ l in
246    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
247    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
248    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
249    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
250    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
251    let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in
252    let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in
253    let 〈l, graph〉 ≝ l in
254    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
255    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
256    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
257    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
258    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
259    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
260      〈joint_st_goto ? globals l, graph〉
261(*
262  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
263    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
264    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
265    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
266    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
267    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
268    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
269      joint_st_goto ? globals l
270  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
271    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
272    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
273    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
274    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
275    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
276    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
277    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
278      joint_st_goto ? globals l
279*)
280  | ertl_st_op1 op1 destr srcr l ⇒
281    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
282    let 〈l, graph〉 ≝ l in
283    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
284    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
285    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
286      〈joint_st_goto ? globals l, graph〉
287  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
288    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
289    let 〈l, graph〉 ≝ l in
290    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
291    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
292    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
293    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
294    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
295      〈joint_st_goto ? globals l, graph〉
296  | ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉
297  | ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉
298  | ertl_st_load destr addr1 addr2 l ⇒
299    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
300    let 〈l, graph〉 ≝ l in
301    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
302    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
303    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
304    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
305    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
306    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
307    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
308    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
309      〈joint_st_goto ? globals l, graph〉
310  | ertl_st_store addr1 addr2 srcr l ⇒
311    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
312    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
313    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
314    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
315    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
316    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
317    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
318    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
319    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
320    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
321      〈joint_st_goto ? globals l, graph〉
322  | ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉
323  | ertl_st_cond srcr lbl_true lbl_false ⇒
324    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
325    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
326      〈joint_st_goto ? globals l, graph〉
327  | ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉
328  ].
329  cases daemon (* XXX: todo -- proofs regarding gvars *)
330qed.
331
332(* **** *)
333
334definition translate_internal ≝
335  λglobals: list ident.
336  λf.
337  λint_fun: ertl_internal_function.
338  let lookup ≝ λr.
339    match lookup r with
340    | colour_spill ->
341        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
342    | colour_colour color ->
343        ERTLToLTLI.Color color
344  in
345  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
346  let stacksize ≝ (ertl_if_params int_fun) + locals in
347    mk_ltl_internal_function
348      globals
349      (ertl_if_luniverse int_fun)
350      (ertl_if_runiverse int_fun)
351      stacksize.
352
353  let () =
354    Label.Map.iter (fun label stmt ->
355      let stmt =
356        match Liveness.eliminable (G.liveafter label) stmt with
357        | Some successor ->
358            LTL.St_skip successor
359        | None ->
360            I.translate_statement stmt
361      in
362      graph := Label.Map.add label stmt !graph
363    ) int_fun.ERTL.f_graph
364  in
365
366definition translate_funct ≝
367  λname_def.
368  let 〈name, def〉 ≝ name_def in
369  let def' ≝
370    match def with
371    [ Internal def ⇒ Internal ? (translate_internal name def)
372    | External def ⇒ External ? def
373    ]
374  in
375    〈name, def'〉.
376
377definition translate ≝
378  λp.
379  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
380    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.