(* Pasted from Pottier's PP compiler *)

(* This module translates [ERTL] statements into [LTL] statements. It is
   parameterized over a module [Env], whose signature appears below, which
   provides support for mapping pseudo-registers to stack slots or hardware
   registers and for generating instructions (which requires allocating fresh
   control flow graph labels). *)

type decision =
  | Spill of AST.immediate
  | Color of I8051.register

module Make (Env : sig

  val lookup: Register.t -> decision

  (* [generate stmt] returns a fresh statement label, which it associates with
     [stmt] in the control flow graph. *)

  val generate: LTL.statement -> Label.t

  val fresh_label: unit -> Label.t

  val add_graph: Label.t -> LTL.statement -> unit

  val locals: int

  val stacksize: int

end) = struct

  open Env
  open I8051

  let adjust off = locals - (off + I8051.int_size)

  let get_stack r off l =
    let off = adjust off in
    let l = generate (LTL.St_from_acc (r, l)) in
    let l = generate (LTL.St_load l) in
    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
    let l = generate (LTL.St_int (I8051.a, 0, l)) in
    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
    LTL.St_int (I8051.a, off, l)

  let set_stack off r l =
    let off = adjust off in
    let l = generate (LTL.St_store l) in
    let l = generate (LTL.St_to_acc (r, l)) in
    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
    let l = generate (LTL.St_int (I8051.a, 0, l)) in
    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
    LTL.St_int (I8051.a, off, l)


  let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) =
    match lookup r with

      | Color hwr ->
	(* Pseudo-register [r] has been mapped to hardware register
	   [hwr]. Just write into [hwr] and branch to [l]. *)
	(hwr, l)

      | Spill off ->
	(* Pseudo-register [r] has been mapped to offset [off] in the local zone
	   of the stack. Then, write into [sst] (never allocated) and transfer
	   control to an instruction that copies [sst] in the designated
	   location of the stack before branching to [l]. *)
	(I8051.sst, generate (set_stack off I8051.sst l))


  let read (r : Register.t) (stmt : I8051.register -> LTL.statement) =
    match lookup r with
      | Color hwr ->
	(* Pseudo-register [r] has been mapped to hardware register [hwr]. Just
	   generate statement [stmt] with a reference to register [hwr]. *)
	generate (stmt hwr)

      | Spill off ->
	(* Pseudo-register [r] has been mapped to offset [off] in the local zone
	   of the stack. Issue a statement that copies the designated area in
	   the stack into the temporary unallocatable hardware register [sst],
	   then generate statement [stmt] with a reference to register
	   [sst]. *)
	let temphwr = I8051.sst in
	let l = generate (stmt temphwr) in
	generate (get_stack temphwr off l)


  let move (dest : decision) (src : decision) l =
    match dest, src with

      (* Both pseudo-registers are translated to hardware registers. Issue move
	 statements, or no statement at all if both pseudo-registers reside in
	 the same hardware register. *)
      | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr ->
	LTL.St_skip l
      | Color desthwr, Color sourcehwr ->
	let l = generate (LTL.St_from_acc (desthwr, l)) in
	LTL.St_to_acc (sourcehwr, l)

      (* One pseudo-register is translated to a hardware register, while the
	 other is spilled. Issue a single stack access instruction. *)
      | Color desthwr, Spill off -> get_stack desthwr off l
      | Spill off, Color sourcehwr -> set_stack off sourcehwr l

      (* Both pseudo-registers are spilled. Combine the previous two cases. Of
	 course, if the two pseudo-registers have been spilled into the same
	 stack slot, there is nothing to do. *)
      | Spill off1, Spill off2 when off1 = off2 ->
	LTL.St_skip l
      | Spill off1, Spill off2 ->
	let temphwr = I8051.sst in
	let l = generate (set_stack off1 temphwr l) in
	get_stack temphwr off2 l


  let newframe l =
    if stacksize = 0 then LTL.St_skip l
    else
      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
      let l = generate (LTL.St_op2 (I8051.Sub, I8051.dph, l)) in
      let l = generate (LTL.St_int (I8051.dph, 0, l)) in
      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
      let l = generate (LTL.St_op2 (I8051.Sub, I8051.dpl, l)) in
      let l = generate (LTL.St_clear_carry l) in
      let l = generate (LTL.St_int (I8051.dpl, stacksize, l)) in
      LTL.St_to_acc (I8051.spl, l)

  let delframe l =
    if stacksize = 0 then LTL.St_skip l
    else
      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
      let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
      let l = generate (LTL.St_int (I8051.a, 0, l)) in
      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
      let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
      LTL.St_int (I8051.a, stacksize, l)


  (* ------------------------------------------------------------------------ *)

  (* [translate_statement] turns a [ERTL] statement into a [LTL] statement, or
     sequence of statements, that transfers control to the same label(s).

     Existing statement labels are preserved, that is, the labels in the new
     control flow graph form a superset of the labels in the existing control
     flow graph. *)

  let translate_statement (stmt : ERTL.statement) : LTL.statement =
    match stmt with

      | ERTL.St_skip l ->
	LTL.St_skip l

      | ERTL.St_comment (s, l) ->
	LTL.St_comment (s, l)

      | ERTL.St_cost (cost_lbl, l) ->
	LTL.St_cost (cost_lbl, l)

      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
	move (lookup destr) (Color sourcehwr) l

      | ERTL.St_set_hdw (desthwr, sourcer, l) ->
	move (Color desthwr) (lookup sourcer) l

      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
	let l = generate (LTL.St_from_acc (r1, l)) in
	LTL.St_to_acc (r2, l)

      | ERTL.St_newframe l ->
	newframe l

      | ERTL.St_delframe l ->
	delframe l

      | ERTL.St_framesize (r, l) ->
	let (hdw, l) = write r l in
	LTL.St_int (hdw, stacksize, l)

      | ERTL.St_pop (r, l) ->
	let (hdw, l) = write r l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	LTL.St_pop l

      | ERTL.St_push (r, l) ->
	let l = generate (LTL.St_push l) in
	let l = read r (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_addrH (r, x, l) ->
	let (hdw, l) = write r l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	let l = generate (LTL.St_to_acc (I8051.dph, l)) in
	LTL.St_addr (x, l)

      | ERTL.St_addrL (r, x, l) ->
	let (hdw, l) = write r l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	let l = generate (LTL.St_to_acc (I8051.dpl, l)) in
	LTL.St_addr (x, l)

      | ERTL.St_int (r, i, l) ->
	let (hdw, l) = write r l in
	LTL.St_int (hdw, i, l)

      | ERTL.St_move (r1, r2, l) ->
	move (lookup r1) (lookup r2) l

      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
	let (hdw, l) = write destr l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	let l = generate (LTL.St_opaccs (opaccs, l)) in
	let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	let l = generate (LTL.St_from_acc (I8051.b, l)) in
	let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
	let (hdw, l) = write destr l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	let l = generate (LTL.St_to_acc (I8051.b, l)) in
	let l = generate (LTL.St_opaccs (opaccs, l)) in
	let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	let l = generate (LTL.St_from_acc (I8051.b, l)) in
	let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_op1 (op1, destr, srcr, l) ->
	let (hdw, l) = write destr l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	let l = generate (LTL.St_op1 (op1, l)) in
	let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
	let (hdw, l) = write destr l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
	let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	let l = generate (LTL.St_from_acc (I8051.b, l)) in
	let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_clear_carry l ->
	LTL.St_clear_carry l

      | ERTL.St_set_carry l ->
	LTL.St_set_carry l

      | ERTL.St_load (destr, addr1, addr2, l) ->
	let (hdw, l) = write destr l in
	let l = generate (LTL.St_from_acc (hdw, l)) in
	let l = generate (LTL.St_load l) in
	let l = generate (LTL.St_from_acc (I8051.dph, l)) in
	let l = generate (LTL.St_to_acc (I8051.st0, l)) in
	let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
	let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	let l = generate (LTL.St_from_acc (I8051.st0, l)) in
	let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_store (addr1, addr2, srcr, l) ->
	let l = generate (LTL.St_store l) in
	let l = generate (LTL.St_to_acc (I8051.st1, l)) in
	let l = generate (LTL.St_from_acc (I8051.dph, l)) in
	let l = generate (LTL.St_to_acc (I8051.st0, l)) in
	let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
	let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	let l = generate (LTL.St_from_acc (I8051.st0, l)) in
	let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	let l = generate (LTL.St_from_acc (I8051.st1, l)) in
	let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_call_id (f, _, l) ->
	LTL.St_call_id (f, l)

      | ERTL.St_call_ptr (f1, f2, _, l) ->
	let l = generate (LTL.St_call_ptr l) in
	let l = generate (LTL.St_from_acc (I8051.dph, l)) in
	let l = generate (LTL.St_to_acc (I8051.st0, l)) in
	let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
	let l = read f1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	let l = generate (LTL.St_from_acc (I8051.st0, l)) in
	let l = read f2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
	let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
	let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
	LTL.St_skip l

      | ERTL.St_return _ ->
	LTL.St_return

(* ------------------------------------------------------------------------- *)

end