source: src/ERTL/Interference.ma @ 3255

include "ERTL/liveness.ma".

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

definition DeqRegister : DeqSet ≝
mk_DeqSet Register eq_Register ?.
#x #y % [2: #EQ destruct cases y % ]
cases x -x try (cases y -y normalize #EQ destruct %)
qed.

unification hint 0 ≔ ⊢ Register ≡ carr DeqRegister.

definition is_src_of_move :
∀globals.joint_statement ERTL globals → vertex → bool ≝
λglobals,s,v.
match s with
[ sequential s _ ⇒
  match s with
  [ step_seq s ⇒
    match s with
    [ MOVE pr ⇒
      match \snd pr with
      [ Reg r ⇒
        match r with
        [ PSD r ⇒ match v with [ inl r' ⇒ eq_identifier … r r' | _ ⇒ false ]
        | HDW r ⇒ match v with [ inr r' ⇒ eq_Register r r' | _ ⇒ false ]
        ]
      | _ ⇒ false
      ]
    | _ ⇒ false
    ]
  | _ ⇒ false
  ]
| _ ⇒ false
].

definition interferes_asym :
  ∀globals.joint_internal_function ERTL globals →
  valuation register_lattice →
  label → vertex → vertex → bool ≝
λglobals,fn,liveafter,l,v1,v2.
match v1 with
[ inr R ⇒
  match v2 with [ inl _ ⇒ R ∈ RegistersForbidden | _ ⇒ false ]
| _ ⇒ false ]
∨
match stmt_at … (joint_if_code … fn) l with
[ None ⇒ false
| Some s ⇒
  in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧
  ¬is_src_of_move … s v2
].

definition interferes ≝ λglobals,fn,liveafter,label,v1,v2.
interferes_asym globals fn liveafter label v1 v2 ∨
interferes_asym globals fn liveafter label v2 v1.

(* prop_colouring is the non interferece
   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
   registers *)
record coloured_graph (interferes : label → vertex → vertex → bool) : Type[1] ≝
{ colouring: vertex → decision
; spilled_no: nat
; prop_colouring: ∀l. ∀v1, v2: vertex.
  interferes l v1 v2 → colouring v1 = colouring v2 → v1 = v2
; prop_spilled_no: ∀v1:vertex.∀i.colouring v1 = decision_spill i → i < spilled_no
; hdw_same_colouring : ∀R.colouring (inr … R) = decision_colour R
}.

definition coloured_graph_computer ≝
 ∀globals.
  ∀fn:joint_internal_function ERTL globals.
   ∀liveafter.
    coloured_graph (interferes … fn liveafter).