include "ASM/I8051.ma".
include "utilities/Interference.ma".
include "utilities/RegisterSet.ma".

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

definition colouring ≝ vertex_map decision.

(* XXX: was set data structure previously *)
definition colour_set ≝ rs_set.

definition add_colour ≝
  λrs: register_set.
  λc: colouring.
  λr: vertex.
  λcs: colour_set rs.
  match vm_find … r c with
  [ None ⇒ cs (* XXX: correct, or should we assert false? *)
  | Some decision ⇒
    match decision with
    [ decision_spill ⇒ cs
    | decision_colour colour ⇒ rs_insert rs colour cs
    ]
  ].

definition colours ≝ λrs. rs_from_list rs RegistersAllocatable.

definition k ≝ |RegistersAllocatable|.

definition forbidden_colours ≝
  λrs.
  λgraph.
  λcolouring.
  λv.
    vs_fold ? (add_colour rs colouring) (ig_ipp graph v) (rs_from_list rs (ig_iph graph v)).
    
definition high ≝
  λgraph.
  λv.
    geb (ig_degree graph v) k.

definition high_neighbours ≝
  λgraph.
  λv.
    vs_filter (high graph) (ig_ipp graph v).

definition georgepp ≝
  λrs.
  λgraph.
  λab.
  let 〈a, b〉 ≝ ab in
    vs_subset … (high_neighbours graph a) (ig_ipp graph b) ∧
      rs_subset rs (rs_from_list rs (ig_iph graph a)) (rs_from_list rs (ig_iph graph b)).