source: src/ERTL/ERTLToLTL.ma @ 1161

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

changes from today: merged ertl, ltl and lin into one datatype to simplify semantics

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