source: src/ERTL/ERTLToLTL.ma @ 1241

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

changes for claudio

File size: 24.9 KB
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3include "ERTL/spill.ma".
4include "ERTL/build.ma".
5include "ERTL/uses.ma".
6include "ERTL/Interference.ma".
7include "ASM/Arithmetic.ma".
8
9(* XXX: define an interference graph for a function and colour it, allowing
10        the consultation of registers.
11definition initial_colouring ≝
12  λglobals.
13  λint_fun.
14  let 〈ignore, graph〉 ≝ build globals int_fun in
15  let coloured ≝ colour_initial graph in
16    coloured.
17
18definition interference_lookup ≝
19  λcoloured: initial_colouring.
20  λr.
21    colouring … coloured r.
22
23definition prepare_graph_for_second_colouring ≝
24  λglobals: list ident.
25  λcoloured: initial_colouring.
26    let g ≝ the_graph decision coloured in
27    let restricted ≝ ig_restrict g (λv.
28      match colouring decision coloured v with
29      [ decision_spill ⇒ true
30      | decision_colour _ ⇒ false
31      ]
32    )
33    in restricted.
34
35definition second_colouring ≝
36  λglobals: list ident.
37  λcoloured.
38    let prepared ≝ prepare_graph_for_second_colouring globals coloured in
39      colour_stack prepared.
40
41definition lookup ≝
42  λinitial.
43  λsecond.
44  λr.
45  match interference_lookup initial r with
46  [ decision_colour _ ⇒ ?
47  | decision_spill ⇒ ?
48  ].
49*)
50
51definition lookup ≝ colouring.
52
53definition fresh_label ≝
54  λglobals: list ident.
55  λluniv.
56    fresh LabelTag luniv.
57
58definition ltl_statement_graph ≝
59  λglobals.
60    graph … (ltl_statement globals).
61
62definition add_graph ≝
63  λglobals.
64  λlabel.
65  λstmt: ltl_statement globals.
66  λgraph: ltl_statement_graph globals.
67    add LabelTag ? graph label stmt.
68
69definition generate ≝
70  λglobals: list ident.
71  λluniv.
72  λgraph: ltl_statement_graph globals.
73  λstmt: ltl_statement globals.
74  let 〈l, luniv〉 ≝ fresh_label globals luniv in
75  let graph ≝ add_graph globals l stmt graph in
76    〈l, graph, luniv〉.
77
78definition num_locals ≝
79  λglobals.
80  λint_fun.
81    colour_locals + (joint_if_stacksize ertl_params globals int_fun).
82
83definition stacksize ≝
84  λglobals.
85  λint_fun.
86    colour_locals + (joint_if_stacksize ertl_params globals int_fun).
87
88definition adjust_off ≝
89  λglobals.
90  λint_fun.
91  λoff.
92  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
93  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
94    sub.
95
96definition get_stack:
97 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
98  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) ≝
99  λglobals: list ident.
100  λint_fun.
101  λgraph: graph (ltl_statement (globals)).
102  λr.
103  λoff.
104  λl.
105    let off ≝ adjust_off globals int_fun off in
106    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
108    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
109    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
110    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
111    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
112    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
113    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
114      〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
115
116definition set_stack:
117  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
118    → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝
119  λglobals: list ident.
120  λint_fun.
121  λgraph: graph (ltl_statement (globals)).
122  λoff.
123  λr.
124  λl.
125  let off ≝ adjust_off globals int_fun off in
126  let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
128  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
129  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
130  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
131  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
132  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
133  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
134    〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
135
136definition write ≝
137  λglobals: list ident.
138  λint_fun.
139  λvaluation.
140  λcoloured_graph.
141  λgraph.
142  λr.
143  λl.
144  match lookup valuation coloured_graph (inl … r) with
145  [ decision_spill off ⇒
146    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l in
147    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
148      〈RegisterSST, l, graph, luniv〉
149  | decision_colour hwr ⇒
150    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
151      〈hwr, l, graph, luniv〉
152  ].
153
154definition read ≝
155  λglobals: list ident.
156  λint_fun.
157  λvaluation.
158  λcoloured_graph.
159  λgraph.
160  λr.
161  λstmt.
162  match lookup valuation coloured_graph (inl … r) with
163  [ decision_colour hwr ⇒ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt hwr)
164  | decision_spill off ⇒
165    let temphwr ≝ RegisterSST in
166    let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt temphwr) in
167    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in
168      generate globals luniv graph stmt
169  ].
170
171definition move ≝
172  λglobals: list ident.
173  λint_fun.
174  λgraph: graph (ltl_statement globals).
175  λdest: decision.
176  λsrc: decision.
177  λl: label.
178  match dest with
179  [ decision_colour dest_hwr ⇒
180    match src with
181    [ decision_colour src_hwr ⇒
182      let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
183      if eq_Register dest_hwr src_hwr then
184        〈joint_st_goto … globals l, graph, luniv〉
185      else
186        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
187          〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
188    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l
189    ]
190  | decision_spill dest_off ⇒
191    match src with
192    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l
193    | decision_spill src_off ⇒
194      let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
195      if eq_nat dest_off src_off then
196        〈joint_st_goto … globals l, graph, luniv〉
197      else
198        let temp_hwr ≝ RegisterSST in
199        let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l in
200        let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
201          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l
202    ]
203  ].
204
205definition newframe ≝
206  λglobals: list ident.
207  λint_fun: ertl_internal_function globals.
208  λgraph: ltl_statement_graph globals.
209  λl: label.
210  if eq_nat (stacksize globals int_fun) 0 then
211    〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse ertl_params globals int_fun)〉
212  else
213    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
214    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
215    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
216    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
217    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
218    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
219    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
220    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
221    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
222      〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
223
224definition delframe ≝
225  λglobals.
226  λint_fun.
227  λgraph: graph (ltl_statement globals).
228  λl.
229  if eq_nat (stacksize globals int_fun) 0 then
230    〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse ertl_params globals int_fun〉
231  else
232    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
233    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
234    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
235    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
236    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
237    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
238      〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
239
240definition translate_statement ≝
241  λglobals: list ident.
242  λint_fun.
243  λvaluation.
244  λcoloured_graph: coloured_graph valuation.
245  λgraph: ltl_statement_graph globals.
246  λstmt: ertl_statement globals.
247  match stmt with
248  [ joint_st_sequential seq l ⇒
249    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
250    match seq with
251    [ joint_instr_comment c ⇒
252      〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
253    | joint_instr_cost_label cost_lbl ⇒
254      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
255    | joint_instr_pop r ⇒
256      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
257      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
258        〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
259    | joint_instr_push r ⇒
260      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
261      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
262      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
263        〈joint_st_goto ltl_params globals l, graph, luniv〉
264    | joint_instr_cond srcr lbl_true ⇒
265      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
266      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
267      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
268        〈joint_st_goto ltl_params globals l, graph, luniv〉
269    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
270    | joint_instr_store addr1 addr2 srcr ⇒
271      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
272      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
273      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
274      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
275      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
276      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
277      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
278      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
279      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
280      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
281      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
282      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
283        〈joint_st_goto ltl_params globals l, graph, luniv〉
284    | joint_instr_load destr addr1 addr2 ⇒
285      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
286      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
287      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
290      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
291      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
292      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
294      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
295      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
296        〈joint_st_goto ltl_params globals l, graph, luniv〉
297    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
298    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
299    | joint_instr_op2 op2 destr srcr ⇒
300      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
301      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
303      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
304      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
305      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
306      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
307      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
308        〈joint_st_goto ltl_params globals l, graph, luniv〉
309    | joint_instr_op1 op1 acc_a ⇒
310      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a l in
311      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
312      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
313      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
314      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
315        〈joint_st_goto ltl_params globals l, graph, luniv〉
316    | joint_instr_int r i ⇒
317      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
318        〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
319    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
320      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in
321      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
322      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
323      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
324      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
325      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
326      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
327      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
328      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
329      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
330      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in
331      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
333      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
334      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
335      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
337      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
338      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
339        〈joint_st_goto ltl_params globals l, graph, luniv〉
340    | joint_instr_move pair_regs ⇒
341      let regl ≝ \fst pair_regs in
342      let regr ≝ \snd pair_regs in
343      match regl with
344      [ pseudo p1  ⇒
345        match regr with
346        [ pseudo p2  ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (lookup valuation coloured_graph (inl … p2)) l
347        | hardware h ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (decision_colour h) l
348        ]
349      | hardware h1 ⇒
350        match regr with
351        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup valuation coloured_graph (inl … p)) l
352        | hardware h2 ⇒
353          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
354            〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l, graph, luniv〉
355        ]
356      ]
357    | joint_instr_address lbl prf dpl dph ⇒
358      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in
359      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
360      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
361      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
362      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
363      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in
364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
365      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
366        〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
367    ]
368  | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse ertl_params globals int_fun〉
369  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse ertl_params globals int_fun〉
370  | joint_st_extension ext ⇒
371    match ext with
372    [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
373    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
374    | ertl_st_ext_frame_size r l ⇒
375      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
376        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
377    ]
378  ].
379
380definition translate_internal ≝
381  λglobals.
382  λint_fun.
383  let uses ≝ examine_internal globals int_fun in ?.
384
385definition translate_funct ≝
386  λname_def.
387  let 〈name, def〉 ≝ name_def in
388  let def' ≝
389    match def with
390    [ Internal def ⇒ Internal ? (translate_internal name def)
391    | External def ⇒ External ? def
392    ]
393  in
394    〈name, def'〉.
395
396definition translate ≝
397  λp.
398  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
399    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.