source: src/ERTL/Interference.ma @ 1415

Last change on this file since 1415 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 
1include "ERTL/ERTL.ma".
2include "ERTL/liveness.ma".
3
4definition vertex ≝ register ⊎ Register.
5
6inductive decision: Type[0] ≝
7  | decision_spill: nat → decision
8  | decision_colour: Register → decision.
9
10definition 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
19record 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
26axiom build: ∀valuation. coloured_graph valuation.
Note: See TracBrowser for help on using the repository browser.