open Maps
open BTL
open RTL
open Camlcoq
open RTLcommonaux
open DebugPrint
open PrintBTL
open BTLcommonaux
open BTLtypes
open BTLRenumber

let get_inumb iinfo = P.of_int iinfo.inumb

let get_ib_num ib = P.of_int (get_inumb_or_next ib)

let translate_function btl entry =
  let rtl_code = ref PTree.empty in
  let rec translate_btl_block ib k =
    debug "Entering translate_btl_block...\n";
    print_btl_inst stderr ib;
    let rtli =
      match ib with
      | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) ->
          Some
            ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.opt_info),
              get_inumb iinfo )
      | Bcond (_, _, _, _, _) ->
          failwith "translate_function: unsupported Bcond"
      | Bseq (ib1, ib2) ->
          translate_btl_block ib1 (Some ib2);
          translate_btl_block ib2 None;
          None
      | Bnop (Some iinfo) ->
          Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
      | Bnop None ->
          failwith
            "translate_function: Bnop None can only be in the right child of \
             Bcond"
      | Bop (op, lr, rd, iinfo) ->
          Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo)
      | Bload (trap, chk, addr, lr, rd, iinfo) ->
          Some
            ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)),
              get_inumb iinfo )
      | Bstore (chk, addr, lr, src, iinfo) ->
          Some
            ( Istore (chk, addr, lr, src, get_ib_num (get_some k)),
              get_inumb iinfo )
      | BF (Bcall (sign, fn, lr, rd, s), iinfo) ->
          Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo)
      | BF (Btailcall (sign, fn, lr), iinfo) ->
          Some (Itailcall (sign, fn, lr), get_inumb iinfo)
      | BF (Bbuiltin (ef, lr, rd, s), iinfo) ->
          Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
      | BF (Bjumptable (arg, tbl), iinfo) ->
          Some (Ijumptable (arg, tbl), get_inumb iinfo)
      | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo)
      | BF (Bgoto s, iinfo) -> None
    in
    match rtli with
    | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code
    | None -> ()
  in
  List.iter
    (fun (n, ibf) ->
      ibf.binfo.visited <- true;
      let ib = ibf.entry in
      translate_btl_block ib None)
    (PTree.elements btl);
  !rtl_code

let btl2rtl (f : BTL.coq_function) =
  (*debug_flag := true;*)
  let btl = f.fn_code in
  let entry = f.fn_entrypoint in
  let obne, dm = renumber btl entry in
  let ordered_btl, new_entry = obne in
  let rtl = translate_function ordered_btl new_entry in
  debug "Entry %d\n" (p2i new_entry);
  debug "BTL Code:\n";
  print_btl_code stderr ordered_btl;
  debug "RTL Code: ";
  print_code rtl;
  debug "Dupmap:\n";
  print_ptree print_pint dm;
  debug "\n";
  (*debug_flag := false;*)
  ((rtl, new_entry), dm)