source: src/ERTL/ERTLToLTL.ma @ 1256

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

changes: added a mapi for graphs

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