source: src/ERTL/ERTLToLTL.ma @ 1415

Last change on this file since 1415 was 1352, checked in by sacerdot, 9 years ago

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

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