include "ERTL/liveness.ma".
(* include "utilities/Interference.ma". *)

(*
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. *)