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

definition build ≝
  λint_fun: ertl_internal_function.
  let liveafter ≝ analyse int_fun in
  let graph ≝ ig_create (ertl_if_locals int_fun) in
  let graph ≝ ig_mkiph graph (ertl_if_locals int_fun) forbidden_registers in
  let graph ≝
    foldi ? ? ? (λlabel. λstmt. λgraph.
      let live ≝ liveafter label in 
      match eliminable live stmt with
      [ Some _ ⇒ graph
      | None   ⇒
        let defined ≝ defined stmt in
        let exceptions ≝
          match stmt with
          [ ertl_st_move _ sr _    ⇒ lattice_psingleton sr
          | ertl_st_set_hdw _ sr _ ⇒ lattice_psingleton sr
          | ertl_st_get_hdw _ sr _ ⇒ lattice_hsingleton sr
          | _                      ⇒ ?
          ]
        in
        let graph ≝ ig_mki graph (lattice_diff live exceptions) defined in
        let graph ≝
          match stmt with
          [ ertl_st_move r1 r2 _    ⇒ ig_mkppp graph r1 r2
          | ertl_st_get_hdw r hwr _ ⇒ ig_mkpph graph r hwr
          | ertl_st_set_hdw hwr r _ ⇒ ig_mkpph graph r hwr
          | _                       ⇒ graph
          ]
        in graph
      ]) (ertl_if_graph int_fun) graph
  in
    〈liveafter, graph〉.
  [*: @lattice_bottom ] (* XXX: matita bug here! *)
qed.