include "ERTL/ERTL.ma".
include "ERTL/ERTLToLTLI.ma".
include "LTL/LTL.ma".
include "ERTL/spill.ma".

definition translate_internal ≝
  λf.
  λint_fun: ertl_internal_function.

  let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in

  let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in

  let generate stmt =
    let l = fresh_label () in
    add_graph l stmt ;
    l in

  (* Build an interference graph for this function, and color
     it. Define a function that allows consulting the coloring. *)

  let module G = struct
    let liveafter, graph = Build.build int_fun
    let uses = Uses.examine_internal int_fun
    let verbose = false
    let () =
      if verbose then
	Printf.printf "Starting hardware register allocation for %s.\n" f
  end in

  let module C = Coloring.Color (G) in

  let lookup r =
    Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring
  in

  (* Restrict the interference graph to concern spilled vertices only,
     and color it again, this time using stack slots as colors. *)

  let module H = struct
    let graph = Interference.droph (Interference.restrict G.graph (fun v ->
      match Interference.Vertex.Map.find v C.coloring with
      | Coloring.Spill ->
	  true
      | Coloring.Color _ ->
	  false
    ))
    let verbose = false
    let () =
      if verbose then
	Printf.printf "Starting stack slot allocation for %s.\n" f
  end in

  let module S = Spill.Color (H) in

  (* Define a new function that consults both colorings at once. *)

  let lookup r =
    match lookup r with
    | Coloring.Spill ->
	ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
    | Coloring.Color color ->
	ERTLToLTLI.Color color
  in

  (* We are now ready to instantiate the functor that deals with the
     translation of instructions. The reason why we make this a
     separate functor is purely pedagogical. Smaller modules are
     easier to understand. *)

  (* We add the additional stack size required for spilled register to the stack
     size previously required for the function: this is the final stack size
     required for the locals. *)

  let locals = S.locals + int_fun.ERTL.f_stacksize in

  (* The full stack size is then the size of the locals in the stack plus the
     size of the formal parameters of the function. *)

  let stacksize = int_fun.ERTL.f_params + locals in

  let module I = ERTLToLTLI.Make (struct
    let lookup = lookup
    let generate = generate
    let fresh_label = fresh_label
    let add_graph = add_graph
    let locals = locals
    let stacksize = stacksize
  end) in

  (* Translate the instructions in the existing control flow graph.
     Pure instructions whose destination pseudo-register is dead are
     eliminated on the fly. *)

  let () =
    Label.Map.iter (fun label stmt ->
      let stmt =
	match Liveness.eliminable (G.liveafter label) stmt with
	| Some successor ->
	    LTL.St_skip successor
	| None ->
	    I.translate_statement stmt
      in
      graph := Label.Map.add label stmt !graph
    ) int_fun.ERTL.f_graph
  in

  (* Build a [LTL] function. *)

  {
    LTL.f_luniverse = int_fun.ERTL.f_luniverse;
    LTL.f_stacksize = stacksize ;
    LTL.f_entry = int_fun.ERTL.f_entry;
    LTL.f_exit = int_fun.ERTL.f_exit;
    LTL.f_graph = !graph
  }

definition translate_funct ≝
  λname_def.
  let 〈name, def〉 ≝ name_def in
  let def' ≝
    match def with
    [ Internal def ⇒ Internal ? (translate_internal name def)
    | External def ⇒ External ? def
    ]
  in
    〈name, def'〉.

definition translate ≝
  λp.
  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).