source: src/ERTL/build.ma @ 1227

include "ERTL/liveness.ma".
include "utilities/Interference.ma".

definition vertex ≝ register ⊎ Register.

record graph: Type[0] ≝ 
{
  interferes: vertex → vertex → bool
}.

axiom create: ∀globals: list ident. ertl_internal_function globals → graph.

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

record coloured_graph (d: Type[0]): Type[1] ≝
{
  the_graph: graph;
  colouring: register → d;
  prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
}.

definition initial_colouring ≝ coloured_graph decision.
definition stack_colouring ≝ coloured_graph nat.

(*
definition build ≝
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  let liveafter ≝ analyse globals int_fun in
  let graph ≝ ig_create (ertl_if_locals globals int_fun) in
  let graph ≝ ig_mkiph graph (ertl_if_locals globals int_fun) RegistersForbidden in
  let graph ≝
    foldi ? ? ? (λlabel. λstmt. λgraph.
      let live ≝ liveafter label in 
      match eliminable globals live stmt with
      [ Some _ ⇒ graph
      | None   ⇒
        let defined ≝ defined globals stmt in
        let exceptions ≝
          match stmt with
          [ joint_st_sequential seq l ⇒
            match seq with
            [ joint_instr_move pair_reg ⇒
              let reg_r ≝ \snd pair_reg in
              match reg_r with
              [ hardware hw ⇒ lattice_hsingleton hw
              | pseudo   ps ⇒ lattice_psingleton ps
              ]
            | _                         ⇒ ?
            ]
          | _ ⇒ ?
          ]
        in
        let graph ≝ ig_mki graph (lattice_diff live exceptions) defined in
        let graph ≝
          match stmt with
          [ joint_st_sequential seq l ⇒
            match seq with
            [ joint_instr_move pair_reg ⇒
              let reg_l ≝ \fst pair_reg in
              let reg_r ≝ \snd pair_reg in
              match reg_l with
              [ pseudo ps1 ⇒
                match reg_r with
                [ pseudo ps2  ⇒ ig_mkppp graph ps1 ps2
                | hardware hw ⇒ ig_mkpph graph ps1 hw
                ]
              | hardware hw1 ⇒
                match reg_r with
                [ pseudo ps    ⇒ ig_mkpph graph ps hw1
                | hardware hw2 ⇒ graph
                ]
              ]
            | _ ⇒ graph
            ]
          | _ ⇒ graph
          ]
        in graph
      ]) (ertl_if_graph globals int_fun) graph
  in
    〈liveafter, graph〉.
  [*: @lattice_bottom ] (* XXX: matita bug here! *)
qed. *)