|
Last change
on this file since 2286 was
2286,
checked in by tranquil, 9 years ago
|
|
Big update!
- merge of all _paolo variants
- reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
- split I8051.ma spawning new BackEndOps?.ma
compiler.ma broken at the moment, but not by these changes as far as I can tell
|
|
File size:
887 bytes
|
| Line | |
|---|
| 1 | include "ERTL/liveness.ma". |
|---|
| 2 | |
|---|
| 3 | inductive decision: Type[0] ≝ |
|---|
| 4 | | decision_spill: nat → decision |
|---|
| 5 | | decision_colour: Register → decision. |
|---|
| 6 | |
|---|
| 7 | (* prop_colouring is the non interferece |
|---|
| 8 | prop_colouring 2 and 3 together say that spilled_no is the number of spilled |
|---|
| 9 | registers *) |
|---|
| 10 | (* Wilmer: the generation of the destruct principle diverges; |
|---|
| 11 | Ctr-C make the file pass *) |
|---|
| 12 | record coloured_graph (after: valuation register_lattice): Type[1] ≝ |
|---|
| 13 | { colouring: vertex → decision |
|---|
| 14 | ; spilled_no: nat |
|---|
| 15 | ; prop_colouring: ∀l. ∀v1, v2: vertex. |
|---|
| 16 | lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2 |
|---|
| 17 | ; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *) |
|---|
| 18 | ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no |
|---|
| 19 | }. |
|---|
| 20 | |
|---|
| 21 | axiom build: ∀valuation. coloured_graph valuation. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
