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
  ].

(* prop_colouring is the non interferece
   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
   registers *)
(* Wilmer: the generation of the destruct principle diverges;
   Ctr-C make the file pass *)
record coloured_graph (v: valuation): Type[1] ≝
{ colouring: vertex → decision
; spilled_no: nat
; prop_colouring: ∀l. ∀v1, v2: vertex.
   is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
; prop_colouring2: (*CSC: the exist-guarded premise is just to make the proof more general *)
   ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no
(* CSC: useless for the proof and very weak
; prop_colouring3:
   spilled_no = 0 ∨
    ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
*)
}.

axiom build: ∀valuation. coloured_graph valuation.