include "ERTL/ERTL.ma".
include "ERTL/liveness.ma".

definition vertex ≝ register ⊎ Register.

inductive decision: Type[0] ≝
  | decision_spill: nat → decision
  | decision_colour: Register → decision.

definition is_member ≝
  λvertex.
  λregister_lattice.
  let 〈l, r〉 ≝ register_lattice in
  match vertex with
  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
  | inr v ⇒ set_member ? eq_Register v r
  ].

record coloured_graph (v: valuation): Type[1] ≝
{
  colouring: vertex → decision;
  prop_colouring: ∀l. ∀v1, v2: vertex.
    is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
}.

axiom build: ∀valuation. coloured_graph valuation.