open Printf
open Camlcoq
open Datatypes
open Maps
open BTL
open PrintAST
open DebugPrint
open BTLtypes

(* Printing of BTL code *)

let reg pp r = fprintf pp "x%d" (P.to_int r)

let rec regs pp = function
  | [] -> ()
  | [ r ] -> reg pp r
  | r1 :: rl -> fprintf pp "%a, %a" reg r1 regs rl

let ros pp = function
  | Coq_inl r -> reg pp r
  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)

let print_succ pp s = fprintf pp "\tsucc %d\n" (P.to_int s)

let print_pref pp pref = fprintf pp "%s" pref

let rec print_iblock pp is_rec pref ib =
  match ib with
  | Bnop None ->
      print_pref pp pref;
      fprintf pp "??: Bnop None\n"
  | Bnop (Some iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bnop\n" iinfo.inumb
  | Bop (op, args, res, iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bop: %a = %a\n" iinfo.inumb reg res
        (PrintOp.print_operation reg)
        (op, args)
  | Bload (trap, chunk, addr, args, dst, iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bload: %a = %s[%a]%a\n" iinfo.inumb reg dst
        (name_of_chunk chunk)
        (PrintOp.print_addressing reg)
        (addr, args) print_trapping_mode trap
  | Bstore (chunk, addr, args, src, iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bstore: %s[%a] = %a\n" iinfo.inumb (name_of_chunk chunk)
        (PrintOp.print_addressing reg)
        (addr, args) reg src
  | BF (Bcall (sg, fn, args, res, s), iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bcall: %a = %a(%a)\n" iinfo.inumb reg res ros fn regs args;
      print_succ pp s
  | BF (Btailcall (sg, fn, args), iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Btailcall: %a(%a)\n" iinfo.inumb ros fn regs args
  | BF (Bbuiltin (ef, args, res, s), iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bbuiltin: %a = %s(%a)\n" iinfo.inumb
        (print_builtin_res reg) res (name_of_external ef)
        (print_builtin_args reg) args;
      print_succ pp s
  | Bcond (cond, args, ib1, ib2, iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bcond: (%a) (prediction: %s)\n" iinfo.inumb
        (PrintOp.print_condition reg)
        (cond, args)
        (match iinfo.opt_info with
        | None -> "none"
        | Some true -> "branch"
        | Some false -> "fallthrough");
      let pref' = pref ^ "  " in
      fprintf pp "%sifso = [\n" pref;
      if is_rec then print_iblock pp is_rec pref' ib1 else fprintf pp "...\n";
      fprintf pp "%s]\n" pref;
      fprintf pp "%sifnot = [\n" pref;
      if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n";
      fprintf pp "%s]\n" pref
  | BF (Bjumptable (arg, tbl), iinfo) ->
      let tbl = Array.of_list tbl in
      print_pref pp pref;
      fprintf pp "%d: Bjumptable: (%a)\n" iinfo.inumb reg arg;
      for i = 0 to Array.length tbl - 1 do
        fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i))
      done
  | BF (Breturn None, iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Breturn\n" iinfo.inumb
  | BF (Breturn (Some arg), iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Breturn: %a\n" iinfo.inumb reg arg
  | BF (Bgoto s, iinfo) ->
      print_pref pp pref;
      fprintf pp "%d: Bgoto: %d\n" iinfo.inumb (P.to_int s)
  | Bseq (ib1, ib2) ->
      if is_rec then (
        print_iblock pp is_rec pref ib1;
        print_iblock pp is_rec pref ib2)
      else fprintf pp "Bseq...\n"

let print_btl_inst pp ib =
  if !debug_flag then print_iblock pp false "  " ib else ()

let print_btl_code pp btl =
  if !debug_flag then (
    fprintf pp "\n";
    List.iter
      (fun (n, ibf) ->
        fprintf pp "[BTL Liveness] ";
        print_regset ibf.input_regs;
        fprintf pp "\n";
        fprintf pp "[BTL block %d with inumb %d]\n" (P.to_int n) ibf.binfo.bnumb;
        print_iblock pp true "  " ibf.entry;
        fprintf pp "\n")
      (PTree.elements btl);
    fprintf pp "\n")
  else ()