|
Last change
on this file since 1379 was
1282,
checked in by sacerdot, 9 years ago
|
|
Cosmetic change: names of joint statements/instructions shortened and made
uppercase.
|
|
File size:
707 bytes
|
| Line | |
|---|
| 1 | include "ERTL/ERTL.ma". |
|---|
| 2 | include "ERTL/liveness.ma". |
|---|
| 3 | |
|---|
| 4 | definition vertex ≝ register ⊎ Register. |
|---|
| 5 | |
|---|
| 6 | inductive decision: Type[0] ≝ |
|---|
| 7 | | decision_spill: nat → decision |
|---|
| 8 | | decision_colour: Register → decision. |
|---|
| 9 | |
|---|
| 10 | definition is_member ≝ |
|---|
| 11 | λvertex. |
|---|
| 12 | λregister_lattice. |
|---|
| 13 | let 〈l, r〉 ≝ register_lattice in |
|---|
| 14 | match vertex with |
|---|
| 15 | [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l |
|---|
| 16 | | inr v ⇒ set_member ? eq_Register v r |
|---|
| 17 | ]. |
|---|
| 18 | |
|---|
| 19 | record coloured_graph (v: valuation): Type[1] ≝ |
|---|
| 20 | { |
|---|
| 21 | colouring: vertex → decision; |
|---|
| 22 | prop_colouring: ∀l. ∀v1, v2: vertex. |
|---|
| 23 | is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 |
|---|
| 24 | }. |
|---|
| 25 | |
|---|
| 26 | axiom build: ∀valuation. coloured_graph valuation. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
