(**********************************************************************)
(* (c) Greg Morrisett, Neal Glew,                                     *)
(*     June 1998, all rights reserved.                                *)
(**********************************************************************)

(* talpp.ml
 *
 * Pretty printer for x86 tal language.
 *
 * TODO: 1. GAS support
 *       2. Movsx/movzx instructions
 *)

open Utilities;;
open Format;;
open Identifier;;
open Tal;;

type options = {style : style; kinds : bool; cons : bool}
and style = MASM | GAS;;

let std_options = {style=MASM; kinds=true; cons=true};;

(* Utilities *)

let rec sepi fmt i s p l =
  match l with
    [] -> ()
  | [x] -> p x
  | x::l ->
      p x; pp_print_string fmt s; pp_print_break fmt 0 i; sepi fmt i s p l
;;

let rec sepb fmt s p l =
  match l with
    [] -> ()
  | [x] -> p x
  | x::l ->
      p x; pp_print_break fmt 1 0; pp_print_string fmt s; sepb fmt s p l
;;

let sep fmt s p l = sepi fmt 0 s p l;;
let sepc fmt p l = sepi fmt 0 "," p l;;
let sepci fmt i p l = sepi fmt i "," p l;;

(* Misc *)

let print_scale fmt s = 
  match s with
    Byte1 -> pp_print_char fmt '1'
  | Byte2 -> pp_print_char fmt '2'
  | Byte4 -> pp_print_char fmt '4'
  | Byte8 -> pp_print_char fmt '8'
;;

let string_of_reg r =
  match r with
    Eax -> "eax"
  | Ebx -> "ebx"
  | Ecx -> "ecx"
  | Edx -> "edx"
  | Esi -> "esi"
  | Edi -> "edi"
  | Ebp -> "ebp"
  | Esp -> "esp"
  | Virt i -> "R("^(id_to_string i)^")"
;;

let print_reg fmt o r =
 (match o.style with
    MASM ->
      (match r with
      | Virt i ->
	  pp_print_string fmt "R("; id_prn fmt i;
	  pp_print_string fmt ")"
      |	_ -> pp_print_string fmt (String.uppercase (string_of_reg r)))
  | GAS -> failwith "GAS unimplemented")
;;

let print_low_byte_reg fmt o r =
 (match o.style with
    MASM ->
      (match r with
      	Eax -> pp_print_string fmt "AL"
      |	Ebx -> pp_print_string fmt "BL"
      |	Ecx -> pp_print_string fmt "CL"
      |	Edx -> pp_print_string fmt "DL"
      |	Virt i ->
	  pp_print_string fmt "RL("; id_prn fmt i;
	  pp_print_string fmt ")"
      |	_ -> invalid_arg "bad low byte register")
  | GAS -> failwith "GAS unimplemented")
;;

(* Kinds *)

let rec print_kind_a fmt k =
  match k with
    Kbyte s -> pp_print_char fmt 'T'; print_scale fmt s
  | Ktype -> pp_print_char fmt 'T'
  | Kmemi i -> pp_print_string fmt "Tm"; pp_print_int fmt i
  | Kmem -> pp_print_string fmt "Tm"
  | Kstack -> pp_print_string fmt "Ts"
  | Kint -> pp_print_string fmt "Sint"
  | Karrow (k1,k2) ->
      print_kind_b fmt true k1;
      pp_print_string fmt "-!>";
      pp_print_cut fmt ();
      (match k2 with
	Karrow (_,_) -> print_kind_a fmt k2
      | _ -> print_kind_b fmt false k2)
  | Kprod ks ->
      pp_print_string fmt "*[";
      sepci fmt 2 (print_kind_b fmt false) ks;
      pp_print_string fmt "]"
and print_kind_b fmt p k =
  match k with
    Karrow (_,_) ->
      if p then pp_print_string fmt "(";
      pp_open_hvbox fmt 0; print_kind_a fmt k; pp_close_box fmt ();
      if p then pp_print_string fmt ")"
  | _ -> pp_open_hvbox fmt 0; print_kind_a fmt k; pp_close_box fmt ()
and print_kind fmt o k =
  if o.kinds then print_kind_b fmt false k
and print_ckind fmt o k =
  if o.kinds then begin
    pp_print_string fmt ":"; print_kind_b fmt false k
  end
;;

(* Constructors *)

let print_primcon fmt pc =
  match pc with
    PCbytes Byte1 -> pp_print_string fmt "B1"
  | PCbytes Byte2 -> pp_print_string fmt "B2"
  | PCbytes Byte4 -> pp_print_string fmt "B4"
  | PCbytes Byte8 -> pp_print_string fmt "B8"
  | PCjunk i -> pp_print_string fmt "junk "; pp_print_int fmt i
  | PCexn -> pp_print_string fmt "exn"
  | PCexnname -> pp_print_string fmt "exnname"
  | PCint i -> pp_print_int fmt i
;;

let print_variance fmt v =
  match v with
    Read -> pp_print_string fmt "^r"
  | Write -> pp_print_string fmt "^w"
  | ReadWrite -> pp_print_string fmt "^rw"
  | Uninit -> pp_print_string fmt "^u"
;;

let prec c =
  match c with
    Cvar _ -> 100
  | Clam (_,_,_) -> 1
  | Capp (_,_) -> 2
  | Ctuple _ -> 100
  | Cproj (_,_) -> 3
  | Clab _ -> 100
  | Cprim _ -> 100
  | Crec _ -> 100
  | Cforall (_,_,_) -> 4
  | Cexist (_,_,_) -> 4
  | Ccode _ -> 100
  | Chptr (_,_) -> 4
  | Cfield (_,_) -> 7
  | Cprod _ -> 100
  | Csum _ -> 100
  | Carray _ -> 100
  | Csing _ -> 100
  | Csptr _ -> 2
  | Cempty -> 100
  | Ccons (_,_) -> 6
  | Cappend (_,_) -> 5
;;

let rec print_con_a fmt o inprec con =
  let c = con.rcon in
  let myprec = prec c in
  let lp () =
    if inprec > myprec then pp_print_string fmt "("; pp_open_hvbox fmt 0 in
  let rp () =
    pp_close_box fmt (); if inprec > myprec then pp_print_string fmt ")" in
  match c with
    Cvar v -> id_prn fmt v
  | Clam (v,k,c) -> 
      lp ();
      pp_print_string fmt "fn "; pp_open_hovbox fmt 0;
      print_con_b fmt o myprec v k c;
      rp ()
  | Capp (c1,c2) ->
      lp (); print_con_a fmt o myprec c1; pp_print_break fmt 1 2;
      print_con_a fmt o (myprec+1) c2; rp ()
  | Ctuple cs ->
      pp_open_hvbox fmt 0; pp_print_char fmt '[';
      sepci fmt 1 (print_con_a fmt o 0) cs;
      pp_print_char fmt ']'; pp_close_box fmt ()
  | Cproj (i,c) ->
      lp ();
      print_con_a fmt o myprec c; pp_print_string fmt ("."^(string_of_int i));
      rp ()
  | Clab l -> pp_print_char fmt '`'; id_prn fmt l
  | Cprim pc -> print_primcon fmt pc
  | Crec vkcs ->
      let f (v,k,c) =
	pp_open_hvbox fmt 0; id_prn fmt v; print_ckind fmt o k;
 	pp_print_char fmt '.'; pp_print_break fmt 0 2; print_con_a fmt o 0 c;
 	pp_close_box fmt () in
      pp_print_string fmt "rec(";
      pp_open_hvbox fmt 0; sepc fmt f vkcs;  pp_close_box fmt ();
      pp_print_string fmt ")"
  | Cforall (v,k,c) ->
      lp ();
      pp_print_string fmt "All["; pp_open_hovbox fmt 0;
      print_con_c fmt o myprec v k c;
      rp ()
  | Cexist (v,k,c) ->
      lp ();
      pp_print_string fmt "Exist["; pp_open_hovbox fmt 0;
      print_con_d fmt o myprec v k c;
      rp ()
  | Ccode rs -> print_register_state fmt o rs
  | Chptr (is,co) ->
      lp ();
      pp_print_char fmt '^';
      if is<>[] then begin
	let (o,c) = if co=None then ".[","]" else ".(",")" in
	pp_print_string fmt o; pp_open_hovbox fmt 0;
	sepc fmt (pp_print_int fmt) is;
	pp_close_box fmt (); pp_print_string fmt c
      end;
      (match co with
	None -> ()
      |	Some c -> print_con_a fmt o myprec c);
      rp ()
  | Cfield (c,v) ->
      lp (); print_con_a fmt o myprec c; print_variance fmt v; rp ()
  | Cprod cs ->
      pp_print_string fmt "*[";
      pp_open_hvbox fmt 0; sepc fmt (print_con_a fmt o 0) cs;
      pp_close_box fmt (); pp_print_char fmt ']';
  | Csum cs ->
      pp_print_string fmt "+[";
      pp_open_hvbox fmt 0; sepc fmt (print_con_a fmt o 0) cs;
      pp_close_box fmt (); pp_print_char fmt ']';
  | Carray(cl,ce) ->
      pp_open_hvbox fmt 0; pp_print_string fmt "array(";
      print_con_a fmt o 0 cl; pp_print_char fmt ','; pp_print_break fmt 0 2;
      print_con_a fmt o 0 ce; pp_print_string fmt ")"; pp_close_box fmt ()
  | Csing c ->
      pp_print_string fmt "S("; print_con_a fmt o 0 c; pp_print_string fmt ")"
  | Csptr c ->
      lp (); pp_print_string fmt "sptr"; pp_print_break fmt 1 2;
      print_con_a fmt o (myprec+1) c; rp ()
  | Cempty -> pp_print_string fmt "se"
  | Ccons (c1, c2) ->
      lp ();
      print_con_a fmt o (myprec+1) c1; pp_print_string fmt "::";
      pp_print_cut fmt (); print_con_a fmt o myprec c2;
      rp ()
  | Cappend (c1,c2) -> 
      lp ();
      print_con_a fmt o (myprec+1) c1; pp_print_string fmt "@";
      pp_print_cut fmt ();
      print_con_a fmt o myprec c2;
      rp ()
and print_con_b fmt o myprec v k con =
  let c = con.rcon in
  id_prn fmt v; print_ckind fmt o k; pp_print_break fmt 1 0;
  match c with
    Clam (v,k,c) -> print_con_b fmt o myprec v k c
  | _ ->
      pp_close_box fmt (); pp_print_char fmt '.'; pp_print_break fmt 1 2;
      print_con_a fmt o myprec con
and print_con_c fmt o myprec v k con =
  let c = con.rcon in
  id_prn fmt v; print_ckind fmt o k;
  match c with
    Cforall (v,k,c) -> pp_print_break fmt 1 0; print_con_c fmt o myprec v k c
  | _ ->
      pp_close_box fmt (); pp_print_string fmt "]."; pp_print_break fmt 0 2;
      print_con_a fmt o myprec con
and print_con_d fmt o myprec v k con =
  let c = con.rcon in
  id_prn fmt v; print_ckind fmt o k;
  match c with
    Cexist (v,k,c) -> pp_print_break fmt 1 0; print_con_d fmt o myprec v k c
  | _ ->
      pp_close_box fmt (); pp_print_string fmt "]."; pp_print_break fmt 0 2;
      print_con_a fmt o myprec con
and print_register_state fmt o rs =
  pp_print_string fmt "{"; pp_open_hvbox fmt 0;
  let f (r,c) =
    print_reg fmt o r; pp_print_string fmt ": "; print_con_a fmt o 0 c in
  let rlist = rs_fold_reg (fun r c rl -> (r,c)::rl) rs [] in
  sepc fmt f rlist; pp_close_box fmt (); pp_print_string fmt "}"
;;

let print_con fmt o c =
  if o.cons then print_con_a fmt o 0 c
and print_ccon fmt o c =
  if o.cons then begin pp_print_string fmt ":"; print_con_a fmt o 0 c end
;;

(*** Code ***)

(* 'a Coerce *)

let rec strip_tapps clist cons =
  match clist with
    (Tapp con)::clist -> strip_tapps clist (con::cons)
  | _ -> (clist,cons)
;;

let rec print_coerce fmt f o (raw,clist) =
  match clist with
    [] -> f fmt o raw
  | (Pack (c1,c2))::clist ->
      (* c1 is hidden type, c2 is existential *)
      pp_open_hvbox fmt 0;
      pp_print_string fmt "pack(<"; print_con fmt o c1;
      pp_print_string fmt ">,"; pp_print_break fmt 0 2;
      print_coerce fmt f o (raw,clist);
      pp_print_char fmt ','; pp_print_break fmt 0 2;
      pp_print_char fmt '<'; print_con fmt o c2; pp_print_string fmt ">)";
      pp_close_box fmt ()
  | (Tapp con)::clist ->
      let (clist,cons) = strip_tapps clist [con] in
      pp_open_hvbox fmt 0;
      pp_print_string fmt "tapp(";
      print_coerce fmt f o (raw,clist);
      pp_print_char fmt ','; pp_print_break fmt 0 2; pp_print_char fmt '<';
      pp_open_hovbox fmt 0; sepc fmt (print_con fmt o) cons;
      pp_close_box fmt (); pp_print_string fmt ">)";
      pp_close_box fmt ();
  | (Roll t)::clist ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "roll(<"; print_con fmt o t;
      pp_print_string fmt ">,"; pp_print_break fmt 0 2;
      print_coerce fmt f o (raw,clist); pp_print_string fmt ")";
      pp_close_box fmt ()
  | (Unroll)::clist ->
      pp_print_string fmt "unroll("; print_coerce fmt f o (raw,clist);
      pp_print_string fmt ")"
  | (Tosum t)::clist -> 
      pp_open_hvbox fmt 0;
      pp_print_string fmt "sum("; pp_print_char fmt '<'; print_con fmt o t;
      pp_print_string fmt ">,"; pp_print_break fmt 0 2;
      print_coerce fmt f o (raw,clist); pp_print_string fmt ")";
      pp_close_box fmt ()
  | (RollTosum t)::clist -> 
      pp_open_hvbox fmt 0;
      pp_print_string fmt "rollsum("; pp_print_char fmt '<'; print_con fmt o t;
      pp_print_string fmt ">,"; pp_print_break fmt 0 2;
      print_coerce fmt f o (raw,clist); pp_print_string fmt ")";
      pp_close_box fmt ()
  | (Fromsum)::clist ->
      pp_print_string fmt "rec("; print_coerce fmt f o (raw,clist);
      pp_print_string fmt ")"
  | (Toexn)::clist ->
      pp_print_string fmt "exn("; print_coerce fmt f o (raw,clist);
      pp_print_string fmt ")"
  | (Toarray (off,d))::clist ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "array("; pp_print_int fmt off;
      pp_print_char fmt ','; pp_print_break fmt 0 2; pp_print_int fmt d;
      pp_print_char fmt ','; pp_print_break fmt 0 2;
      print_coerce fmt f o (raw,clist); pp_print_string fmt ")";
      pp_close_box fmt ()
  | (Slot (i,sz))::clist ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "slot("; pp_print_int fmt i; pp_print_char fmt ',';
      pp_print_break fmt 0 2; pp_print_int fmt sz; pp_print_char fmt ',';
      pp_print_break fmt 0 2; print_coerce fmt f o (raw,clist);
      pp_print_string fmt ")";
      pp_close_box fmt ()
  | (Subsume t)::clist ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "subsume("; pp_print_char fmt '<'; print_con fmt o t;
      pp_print_string fmt ">,"; pp_print_break fmt 0 2;
      print_coerce fmt f o (raw,clist); pp_print_string fmt ")";
      pp_close_box fmt ()
;;

let print_label_coerce fmt o lc =
  print_coerce fmt (fun fmt _ l -> id_prn fmt l) o lc
;;

let print_reg_coerce fmt o rc = print_coerce fmt print_reg o rc;;

let print_genop fmt o gop =
  if o.style=GAS then failwith "GAS unimplemented";
  match gop with
    Immed i -> pp_print_int fmt i
  | Tag i ->
      pp_print_string fmt "S("; pp_print_int fmt i; pp_print_string fmt ")"
  | Reg r -> print_reg fmt o r
  | Addr l -> id_prn fmt l
  | Prjr (r,i) ->
      pp_print_char fmt '['; print_reg_coerce fmt o r; pp_print_char fmt '+';
      pp_print_int fmt i; pp_print_char fmt ']'
  | Prjl (l,i) ->
      pp_print_char fmt '['; print_label_coerce fmt o l; pp_print_char fmt '+';
      pp_print_int fmt i; pp_print_char fmt ']'
;;

let print_genop_coerce fmt o cgop = print_coerce fmt print_genop o cgop;;

(* MASM gets projections of code labels wrong and also needs size information
 * in some instances.  Thus the phrase DWORD PTR must be inserted in certain
 * circumstances.
 *
 * print_unary_op, print_unary_op_coerce, print_anop, print_anop_coerce,
 * print_binop, and print_binop2 do these insertions
 *)

let print_unary_op fmt o gop =
  if o.style=GAS then failwith "GAS unimplemented";
  begin match gop with
    Prjr (_,_) | Prjl (_,_) -> pp_print_string fmt "DWORD PTR "
  | _ -> ()
  end;
  print_genop fmt o gop
;;

let print_unary_op_coerce fmt o (gop,_ as cgop) =
  if o.style=GAS then failwith "GAS unimplemented";
  begin match gop with
    Prjr (_,_) | Prjl (_,_) -> pp_print_string fmt "DWORD PTR "
  | _ -> ()
  end;
  print_genop_coerce fmt o cgop
;;

let print_anop fmt o gop =
  if o.style=GAS then failwith "GAS unimplemented";
  begin match gop with
    Prjl (_,_) -> pp_print_string fmt "DWORD PTR "
  | _ -> ()
  end;
  print_genop fmt o gop
;;

let print_anop_coerce fmt o (gop,_ as cgop) =
  if o.style=GAS then failwith "GAS unimplemented";
  begin match gop with
    Prjl (_,_) -> pp_print_string fmt "DWORD PTR "
  | _ -> ()
  end;
  print_genop_coerce fmt o cgop
;;

let print_binop fmt o o1 o2 =
  let ptr1 =
    match o1 with
      Prjl(_,_) -> true
    | Prjr(_,_) -> (match o2 with Immed _ | Tag _ -> true | _ -> false)
    | _ -> false
  and ptr2 =
    match o2 with
      Prjl(_,_) -> true
    | Prjr(_,_) -> (match o1 with Immed _ | Tag _ -> true | _ -> false)
    | _ -> false in
  if ptr1 then pp_print_string fmt "DWORD PTR ";
  print_genop fmt o o1; pp_print_char fmt ',';
  if ptr2 then pp_print_string fmt "DWORD PTR ";
  print_genop fmt o o2
;;

let print_binop2 fmt o o1 (o2,_ as co2) =
  let ptr1 =
    match o1 with
      Prjl(_,_) -> true
    | Prjr(_,_) -> (match o2 with Immed _ | Tag _ -> true | _ -> false)
    | _ -> false
  and ptr2 =
    match o2 with
      Prjl(_,_) -> true
    | Prjr(_,_) -> (match o1 with Immed _ | Tag _ -> true | _ -> false)
    | _ -> false in
  if ptr1 then pp_print_string fmt "DWORD PTR ";
  print_genop fmt o o1; pp_print_char fmt ',';
  if ptr2 then pp_print_string fmt "DWORD PTR ";
  print_genop_coerce fmt o co2
;;

let print_cc fmt o cc =
  if o.style=GAS then failwith "GAS unimplemented";
  let s =
    match cc with
      Above -> "A" | AboveEq -> "AE" | Below -> "B" | BelowEq -> "BE"
    | Eq -> "E" | Greater -> "G" | GreaterEq -> "GE" | Less -> "L"
    | LessEq -> "LE" | NotEq -> "NE" | NotOverflow -> "NO" | NotSign -> "NS"
    | Overflow -> "O" | ParityEven -> "PE" | ParityOdd -> "PO" | Sign -> "S"
  in pp_print_string fmt s
;;

let print_arithbin fmt o x =
  if o.style=GAS then failwith "GAS unimplemented";
  let s = 
    match x with
      Adc -> "ADC" | Add -> "ADD" | And -> "AND" | Imul2 -> "IMUL"
    | Or -> "OR" | Sbb -> "SBB" | Sub -> "SUB" | Xor -> "XOR"
  in pp_print_string fmt s
;;

let print_arithun fmt o x =
  if o.style=GAS then failwith "GAS unimplemented";
  let s = 
    match x with
      Dec -> "DEC" | Inc -> "INC" | Neg -> "NEG" | Not -> "NOT"
  in pp_print_string fmt s
;;

let print_arithmd fmt o x =
  if o.style=GAS then failwith "GAS unimplemented";
  let s = 
    match x with
      Div -> "DIV" | Idiv -> "IDIV" | Imul1 -> "IMUL" | Mul -> "MUL"
  in pp_print_string fmt s
;;

let print_arithsr fmt o x =
  if o.style=GAS then failwith "GAS unimplemented";
  let s = 
    match x with
      Rcl -> "RCL" | Rcr -> "RCR" | Rol -> "ROL" | Ror -> "ROR" | Sal -> "SAL"
    | Sar -> "SAR" | Shl -> "SHL" | Shr -> "SHR"
  in pp_print_string fmt s
;;

let print_conv fmt o c =
  if o.style=GAS then failwith "GAS unimplemented";
  match c with
    Cbw -> pp_print_string fmt "\tCBW"
  | Cdq -> pp_print_string fmt "\tCDQ"
  | Cwd -> pp_print_string fmt "\tCWD"
  | Cwde -> pp_print_string fmt "\tCWDE"
  | Movsx (r1,s1,r2,s2) -> failwith "Talpp.print_conv - movsx unimplemented"
  | Movzx (r1,s1,r2,s2) -> failwith "Talpp.print_conv - movzx unimplemented"
;;

let print_array_arg fmt o genop =
  match genop with
    Prjr (rc,n) ->
      print_reg_coerce fmt o rc; pp_print_char fmt '+'; pp_print_int fmt n
  | Prjl (lc,n) ->
      print_label_coerce fmt o lc; pp_print_char fmt '+'; pp_print_int fmt n
  | _ -> invalid_arg "Talpp.print_array_arg"
;;

let print_mallocarg fmt o ma =
  let rec aux ma =
    match ma with
      Mprod mas -> 
      	pp_print_char fmt '['; pp_open_hovbox fmt 0;
      	sepc fmt aux mas;
      	pp_close_box fmt (); pp_print_char fmt ']'
    | Mfield c -> pp_print_char fmt ':'; print_con fmt o c
    | Mbytearray (scale,size) ->
      	pp_print_string fmt "array("; pp_print_int fmt size;
 	pp_print_string fmt ",B"; print_scale fmt scale;
 	pp_print_string fmt ")"
    | Mexnname c ->
      	pp_print_string fmt "exnname("; print_con fmt o c;
      	pp_print_string fmt ")" in
  pp_print_char fmt '<'; aux ma; pp_print_char fmt '>'
;;

let print_instruction fmt o i =
  if o.style=GAS then failwith "GAS unimplemented";
  (match i with
    ArithBin (x,o1,o2) ->
      pp_print_char fmt '\t'; print_arithbin fmt o x; pp_print_char fmt '\t';
      print_binop fmt o o1 o2
  | ArithUn (x,op) ->
      pp_print_char fmt '\t'; print_arithun fmt o x; pp_print_char fmt '\t';
      print_unary_op fmt o op
  | ArithMD (x,op) ->
      pp_print_char fmt '\t'; print_arithmd fmt o x; pp_print_char fmt '\t';
      print_unary_op fmt o op
  | ArithSR (x,op,io) ->
      pp_print_char fmt '\t'; print_arithsr fmt o x; pp_print_char fmt '\t';
      print_unary_op fmt o op; pp_print_char fmt ',';
      (match io with None -> pp_print_string fmt "CL"
      | Some i -> pp_print_int fmt i)
  | Bswap r -> pp_print_string fmt "\tBSWAP\t"; print_reg fmt o r
  | Call op -> pp_print_string fmt "\tCALL\t"; print_unary_op_coerce fmt o op
  | Clc -> pp_print_string fmt "\tCLC"
  | Cmc -> pp_print_string fmt "\tCMC"
  | Cmovcc (cc,r,op) ->
      pp_print_string fmt "\tCMOV"; print_cc fmt o cc; pp_print_char fmt '\t';
      print_reg fmt o r; pp_print_char fmt ','; print_anop_coerce fmt o op
  | Cmp (o1,o2) -> pp_print_string fmt "\tCMP\t"; print_binop fmt o o1 o2
  | Conv c -> print_conv fmt o c
  | Imul3 (r,op,i) ->
      pp_print_string fmt "\tIMUL\t"; print_reg fmt o r;
      pp_print_char fmt ','; print_anop fmt o op;
      pp_print_char fmt ','; pp_print_int fmt i
  | Int n -> pp_print_string fmt "\tINT\t"; pp_print_int fmt n
  | Into -> pp_print_string fmt "\tINTO"
  | Jcc (cc,l) ->
      pp_print_string fmt "\tJ"; print_cc fmt o cc; pp_print_char fmt '\t';
      print_label_coerce fmt o l
  | Jecxz l -> pp_print_string fmt "\tJECXZ\t"; print_label_coerce fmt o l
  | Jmp op -> pp_print_string fmt "\tJMP\t"; print_anop_coerce fmt o op
  | Lahf -> pp_print_string fmt "\tLAHF"
  | Lea (r,op) ->
      pp_print_string fmt "\tLEA\t"; print_reg fmt o r; pp_print_char fmt ',';
      print_anop fmt o op
  | Loopd (l,bo) ->
      pp_print_string fmt "\tLOOP";
      (match bo with
 	None -> ()
      | Some false -> pp_print_string fmt "NE"
      | Some true -> pp_print_char fmt 'E');
      pp_print_string fmt "D\t"; print_label_coerce fmt o l
  | Mov (o1,o2) ->
      pp_print_string fmt "\tMOV\t"; 
      print_binop2 fmt o o1 o2
  | Nop -> pp_print_string fmt "\tNOP"
  | Pop op -> pp_print_string fmt "\tPOP\t"; print_unary_op fmt o op
  | Popad -> pp_print_string fmt "\tPOPAD"
  | Popfd -> pp_print_string fmt "\tPOPFD"
  | Push op -> pp_print_string fmt "\tPUSH\t"; print_unary_op_coerce fmt o op
  | Pushad -> pp_print_string fmt "\tPUSHAD"
  | Pushfd -> pp_print_string fmt "\tPUSHFD"
  | Retn no ->
      pp_print_string fmt "\tRETN";
      (match no with None -> ()
      | Some n -> pp_print_char fmt '\t'; pp_print_int fmt n)
  | Sahf -> pp_print_string fmt "\tSAHF"
  | Setcc (cc,op) ->
      pp_print_string fmt "\tSET"; print_cc fmt o cc; pp_print_char fmt '\t';
      (match op with Reg r -> print_low_byte_reg fmt o r
       | _ -> failwith "bad args to SETcc")
  | Shld (op,r,io) -> 
      pp_print_string fmt "\tSHLD\t"; print_anop fmt o op;
      pp_print_char fmt ','; print_reg fmt o r; pp_print_char fmt ',';
      (match io with None -> pp_print_string fmt "CL"
      | Some c -> pp_print_int fmt c)
  | Shrd (op,r,io) -> 
      pp_print_string fmt "\tSHRD\t"; print_anop fmt o op;
      pp_print_char fmt ','; print_reg fmt o r; pp_print_char fmt ',';
      (match io with None -> pp_print_string fmt "CL"
      | Some c -> pp_print_int fmt c)
  | Stc -> pp_print_string fmt "\tSTC"
  | Test (o1,o2) -> pp_print_string fmt "\tTEST\t"; print_binop fmt o o1 o2
  | Xchg (op,r) ->
      pp_print_string fmt "\tXCHG\t"; print_anop fmt o op;
      pp_print_char fmt ','; print_reg fmt o r
(* Abstract ops *)
  | Asub (r1,genop1,scale,r2,genop2) ->
      pp_print_string fmt "\tASUB\t"; print_reg fmt o r1;
      pp_print_char fmt ','; print_array_arg fmt o genop1;
      pp_print_char fmt ','; pp_print_int fmt scale;
      pp_print_char fmt ','; print_reg fmt o r2;
      pp_print_char fmt ','; print_genop fmt o genop2
  | Aupd (genop1,scale,r1,r2,genop2) ->
      pp_print_string fmt "\tAUPD\t"; print_array_arg fmt o genop1;
      pp_print_char fmt ','; pp_print_int fmt scale;
      pp_print_char fmt ','; print_reg fmt o r1;
      pp_print_char fmt ','; print_reg fmt o r2;
      pp_print_char fmt ','; print_genop fmt o genop2
  | Bexn (r,genop,lc) ->
      pp_print_string fmt "\tBEXN\t"; print_reg fmt o r; pp_print_char fmt ',';
      print_genop fmt o genop; pp_print_char fmt ',';
      print_label_coerce fmt o lc
  | Btagi (r,i,lc,cc) ->
      pp_print_string fmt "\tBTAGI\t"; print_cc fmt o cc;
      pp_print_char fmt ','; print_reg fmt o r; pp_print_char fmt ',';
      pp_print_int fmt i; pp_print_char fmt ','; print_label_coerce fmt o lc
  | Btagvar (r,offset,i,lc,cc) ->
      pp_print_string fmt "\tBTAGVAR\t"; print_cc fmt o cc;
      pp_print_string fmt ",["; print_reg fmt o r; pp_print_char fmt '+';
      pp_print_int fmt offset ; pp_print_string fmt "],";
      pp_print_int fmt i; pp_print_char fmt ','; print_label_coerce fmt o lc
  | Coerce rc ->
      pp_print_string fmt "\tCOERCE\t"; print_reg_coerce fmt o rc
  | Comment s ->
      pp_print_string fmt "; "; pp_print_string fmt s
  | Fallthru cons ->
      pp_print_string fmt "\tFALLTHRU";
      if cons<>[] then begin 
        pp_print_string fmt "\t<";
        pp_open_hovbox fmt 0; sepc fmt (print_con fmt o) cons;
        pp_close_box fmt (); pp_print_char fmt '>'
      end
  | Malloc (i,marg) ->
      pp_print_string fmt "\tMALLOC\t"; pp_print_int fmt i; 
      pp_print_char fmt ','; print_mallocarg fmt o marg
  | Unpack (v,r,op) ->
      pp_print_string fmt "\tUNPACK\t"; id_prn fmt v; pp_print_char fmt ',';
      print_reg fmt o r; pp_print_char fmt ','; print_anop_coerce fmt o op
	)
;;

let print_code_block fmt o (l,lc,is : code_block) =
  id_prn fmt l;
  pp_print_char fmt ':';
  pp_print_cut fmt ();
  if o.cons then begin
    pp_print_string fmt "LABELTYPE <";
    print_con fmt o lc;
    pp_print_char fmt '>'; 
    pp_print_cut fmt ()
  end;
  for i = 0 to (Array.length is)-1 do
    print_instruction fmt o is.(i);
    pp_print_cut fmt ()
  done;
;;

(*** Data ***)

let print_data_item fmt o di =
  match di with
    Dlabel cl ->
      pp_print_string fmt "\tDD\t"; print_label_coerce fmt o cl
  | Dtag ci ->
      let prn_tag fmt o i =
 	pp_print_string fmt "S("; pp_print_int fmt i;
 	pp_print_string fmt ")" in
      pp_print_string fmt "\tDD\t"; print_coerce fmt prn_tag o ci
  | Dbytes s ->
      pp_print_string fmt "\tDB\t";
      for i = 0 to String.length s - 1 do
	if i>0 then pp_print_char fmt ',';
	pp_print_int fmt (Char.code s.[i])
      done
  | D2bytes i -> pp_print_string fmt "\tDW\t"; pp_print_int fmt i
  | D4bytes i -> pp_print_string fmt "\tDD\t"; pp_print_int fmt i
  | Djunk -> pp_print_string fmt "\tDD\t?"
  | Dexnname c ->
      pp_print_string fmt "\texnname\t<"; print_con fmt o c;
      pp_print_char fmt '>'
  | Dup -> pp_print_string fmt "\tTAL_STRUCT"
  | Ddown -> pp_print_string fmt "\tTAL_ENDS"
;;

let print_data_block fmt o (l,lc,(dis,clist) : data_block) =
  id_prn fmt l;
  pp_print_char fmt ':';
  pp_print_cut fmt ();
  if o.cons then begin
    match lc with
      None -> ()
    | Some c ->
    	pp_print_string fmt "LABELTYPE <";
    	print_con fmt o c;
    	pp_print_char fmt '>'; 
    	pp_print_cut fmt ()
  end;
  if clist<>[] then begin
    pp_print_string fmt "COERCE\t<";
    print_coerce fmt (fun fmt _ _ -> pp_print_string fmt "?") o ((),clist);
    pp_print_char fmt '>'; pp_print_cut fmt ()
  end;
  let aux di = print_data_item fmt o di; pp_print_cut fmt () in
  List.iter aux dis
;;

(*** Compilation Units ***)

let print_tal_int fmt name o m =
  pp_open_vbox fmt 0;
  pp_print_string fmt ("; TAL INTERFACE "^name); pp_print_cut fmt ();
  pp_print_string fmt "; This file was generated by TALC"; pp_print_cut fmt ();
  for i = 0 to (Array.length m.int_includes) - 1 do
    pp_print_string fmt ("\tINCLUDE\t"^m.int_includes.(i)); pp_print_cut fmt ()
  done;
  if (Array.length m.int_includes)>0 then pp_print_cut fmt ();
  for i = 0 to (Array.length m.int_cons) - 1 do
    let (l,k,cd) = m.int_cons.(i) in
    pp_print_string fmt "\tTYPE\t";
    pp_print_char fmt '<'; pp_open_hovbox fmt 0; id_prn fmt l;
    pp_print_break fmt 1 2; print_char ':'; print_kind fmt o k;
    (match cd with
      AbsCon -> ()
    | BoundCon c ->
	pp_print_break fmt 1 2; print_string "<= "; print_con fmt o c
    | ConcCon c ->
 	pp_print_break fmt 1 2; print_string "= "; print_con fmt o c);
    pp_close_box fmt (); pp_print_char fmt '>';
    pp_print_cut fmt ()
  done;
  if (Array.length m.int_cons)>0 then pp_print_cut fmt ();
  for i = 0 to (Array.length m.int_vals) - 1 do
    let (l,c) = m.int_vals.(i) in
    pp_print_string fmt "\tVAL\t"; id_prn fmt l;
    pp_print_string fmt ",<"; print_con fmt o c; pp_print_char fmt '>';
    pp_print_cut fmt ()
  done;
  pp_close_box fmt ()
;;

let print_tal_int_type fmt o {it_cons=cons; it_vals=vals} =
  let prn_lkco (l,k,cd) =
    pp_open_hovbox fmt 0; id_prn fmt l; pp_print_break fmt 1 2;
    print_ckind fmt o k;
    (if o.cons then
      match cd with
      	AbsCon -> ()
      |	BoundCon c ->
	  pp_print_break fmt 1 2; pp_print_string fmt "<="; print_con fmt o c
      | ConcCon c ->
	  pp_print_break fmt 1 2; pp_print_char fmt '='; print_con fmt o c);
    pp_close_box fmt () in
  let prn_lc (l,c) =
    pp_open_hovbox fmt 0; id_prn fmt l; pp_print_break fmt 1 2;
    print_ccon fmt o c; pp_close_box fmt () in
  pp_print_char fmt '{'; pp_open_hvbox fmt 0;
  pp_open_hovbox fmt 0; sepc fmt prn_lkco cons; pp_close_box fmt ();
  pp_print_char fmt ';'; pp_print_break fmt 1 0; pp_open_hvbox fmt 0;
  sepc fmt prn_lc vals; pp_close_box fmt (); pp_close_box fmt ();
  pp_print_char fmt '}'
;;

let print_tal_imp fmt name o m = 
  pp_open_vbox fmt 0;
  pp_print_string fmt ("; TAL IMPLEMENTATION "^name); pp_print_cut fmt ();
  pp_print_string fmt "; This file was generated by TALC"; pp_print_cut fmt ();
  pp_print_string fmt "\tINCLUDE\tTAL.INC"; pp_print_cut fmt ();
  pp_print_string fmt "\t_begin_TAL"; pp_print_cut fmt (); pp_print_cut fmt ();
  for i = 0 to (Array.length m.imports) - 1 do
    pp_print_string fmt ("\tTAL_IMPORT\t"^m.imports.(i)); pp_print_cut fmt ()
  done;
  if (Array.length m.imports)>0 then pp_print_cut fmt ();
  for i = 0 to (Array.length m.exports) - 1 do
    pp_print_string fmt ("\tTAL_EXPORT\t"^m.exports.(i)); pp_print_cut fmt ()
  done;
  if (Array.length m.exports)>0 then pp_print_cut fmt ();
  for i = 0 to (Array.length m.imp_abbrevs) - 1 do
    let (l,c) = m.imp_abbrevs.(i) in
    pp_print_string fmt "\tTYPE\t";
    pp_print_char fmt '<'; pp_open_hovbox fmt 0; id_prn fmt l;
    pp_print_break fmt 1 2; print_string "= ";
    print_con fmt o c; pp_close_box fmt (); pp_print_char fmt '>';
    pp_print_cut fmt ()
  done;
  if (Array.length m.imp_abbrevs)>0 then pp_print_cut fmt ();
  for i = 0 to (Array.length m.con_blocks) - 1 do
    let (l,k,c) = m.con_blocks.(i) in
    pp_print_string fmt "\tTYPE\t";
    pp_print_char fmt '<'; pp_open_hovbox fmt 0; id_prn fmt l;
    pp_print_break fmt 1 2; print_char ':'; print_kind fmt o k;
    pp_print_break fmt 1 2; print_string "= ";
    print_con fmt o c; pp_close_box fmt (); pp_print_char fmt '>';
    pp_print_cut fmt ()
  done;
  if (Array.length m.con_blocks)>0 then pp_print_cut fmt ();
  pp_print_string fmt "\tCODE"; pp_print_cut fmt (); pp_print_cut fmt ();
  for i = 0 to (Array.length m.code_blocks) - 1 do
    print_code_block fmt o m.code_blocks.(i)
  done;
  if (Array.length m.code_blocks)>0 then pp_print_cut fmt ();
  pp_print_string fmt "\tDATA"; pp_print_cut fmt (); pp_print_cut fmt ();
  for i = 0 to (Array.length m.data_blocks) - 1 do
    print_data_block fmt o m.data_blocks.(i)
  done;
  if (Array.length m.data_blocks)>0 then pp_print_cut fmt ();
  pp_print_string fmt "\t_end_TAL"; pp_print_cut fmt ();
  pp_print_string fmt "\tEND"; pp_print_cut fmt ();
  pp_close_box fmt ()
;;

open Talctxt;;

let print_tal_loc fmt o l =
  match l with
    Loctop -> pp_print_string fmt "top level"
  | Loccon l -> pp_print_string fmt "abstract type "; id_prn fmt l
  | Locval l -> pp_print_string fmt "imported label "; id_prn fmt l
  | Loccb l -> pp_print_string fmt "concrete type "; id_prn fmt l
  | Locc (l,i) ->
      pp_print_string fmt "code block "; id_prn fmt l;
      pp_print_string fmt "("; pp_print_int fmt i; pp_print_string fmt ")"
  | Locd (l,i) ->
      pp_print_string fmt "data block "; id_prn fmt l;
      pp_print_string fmt "("; pp_print_int fmt i; pp_print_string fmt ")"
;;

let print_verify_error fmt o ve =
  match ve with
    Undefined_label l ->
      pp_print_string fmt "label "; id_prn fmt l;
      pp_print_string fmt " undefined"
  | Undefined_var v ->
      pp_print_string fmt "var "; id_prn fmt v;
      pp_print_string fmt " undefined"
  | Undefined_reg r ->
      pp_print_string fmt "reg "; print_reg fmt o r;
      pp_print_string fmt " undefined"
  | Redefined_label l ->
      pp_print_string fmt "label "; id_prn fmt l;
      pp_print_string fmt " redefined"
  | Kindleq (k1,k2) ->
      pp_open_hvbox fmt 0; print_kind fmt o k1; pp_print_space fmt ();
      pp_print_string fmt "! <="; pp_print_space fmt (); print_kind fmt o k2;
      pp_close_box fmt ()
  | Kindeq (k1,k2) ->
      pp_open_hvbox fmt 0; print_kind fmt o k1; pp_print_space fmt ();
      pp_print_string fmt "!="; pp_print_space fmt (); print_kind fmt o k2;
      pp_close_box fmt ()
  | Kindmeet (k1,k2) ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "no kind meet:"; pp_print_break fmt 1 2;
      print_kind fmt o k1; pp_print_char fmt ','; pp_print_break fmt 1 2;
      print_kind fmt o k2;
      pp_close_box fmt ()
  | Kindjoin (k1,k2) ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "no kind join:"; pp_print_break fmt 1 2;
      print_kind fmt o k1; pp_print_char fmt ','; pp_print_break fmt 1 2;
      print_kind fmt o k2;
      pp_close_box fmt ()
  | Conwf (c,s) ->
      pp_print_string fmt "malformed constructor:"; pp_print_break fmt 1 2;
      pp_print_string fmt s; pp_print_char fmt ':'; pp_print_break fmt 1 2;
      print_con fmt o c
  | Neqcon (c1,c2) ->
      pp_open_hvbox fmt 0; print_con fmt o c1; pp_print_space fmt ();
      pp_print_string fmt "!="; pp_print_space fmt (); print_con fmt o c2;
      pp_close_box fmt ()
  | Nleqcon (c1,c2) ->
      pp_open_hvbox fmt 0; print_con fmt o c1; pp_print_space fmt ();
      pp_print_string fmt "! <="; pp_print_space fmt (); print_con fmt o c2;
      pp_close_box fmt ()
  | Rsnleq (r,rs1,rs2) ->
      pp_open_hvbox fmt 0; print_register_state fmt o rs1;
      pp_print_space fmt (); pp_print_string fmt "! <="; pp_print_space fmt ();
      print_register_state fmt o rs2; pp_print_space fmt ();
      pp_print_string fmt "@ "; print_reg fmt o r; pp_close_box fmt ()
  | Conmeet (c1,c2) ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "no con meet:"; pp_print_break fmt 1 2;
      print_con fmt o c1; pp_print_char fmt ','; pp_print_break fmt 1 2;
      print_con fmt o c2;
      pp_close_box fmt ()
  | Conjoin (c1,c2) ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "no con join"; pp_print_break fmt 1 2;
      print_con fmt o c1; pp_print_char fmt ','; pp_print_break fmt 1 2;
      print_con fmt o c2;
      pp_close_box fmt ()
  | Rsmeet (rs1,rs2) ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "no register state meet:"; pp_print_break fmt 1 2;
      print_register_state fmt o rs1; pp_print_char fmt ',';
      pp_print_break fmt 1 2; print_register_state fmt o rs2;
      pp_close_box fmt ()
  | Rsjoin (rs1,rs2) ->
      pp_open_hvbox fmt 0;
      pp_print_string fmt "no register state join"; pp_print_break fmt 1 2;
      print_register_state fmt o rs1; pp_print_char fmt ',';
      pp_print_break fmt 1 2; print_register_state fmt o rs2;
      pp_close_box fmt ()
  | BadUnroll c ->
      pp_print_string fmt "cannot unroll:"; pp_print_break fmt 1 2;
      print_con fmt o c
  | Unknown_size c ->
      pp_print_string fmt "indeterminant size:"; pp_print_break fmt 1 2;
      print_con fmt o c
  | Bad_offset i ->
      pp_print_string fmt "bad tuple/stack offset "; pp_print_int fmt i
  | Bad_depth i ->
      pp_print_string fmt "bad tuple/stack depth "; pp_print_int fmt i
  | Not_tail (c,_) ->
      pp_print_string fmt "not tail of current stack:"; pp_print_break fmt 1 2;
      print_con fmt o c
  | Readonly -> pp_print_string fmt "field is readonly"
  | Stack_write_alignment -> pp_print_string fmt "stack slot write misaligned"
  | Coercion (c,s,_) -> pp_print_string fmt s; pp_print_break fmt 1 2;
      print_con fmt o c
  | No_stack_type -> pp_print_string fmt "stack currently undefined"
  | Genop (s,_) -> pp_print_string fmt s
  | Both_mem (_,_) -> pp_print_string fmt "both operands are for memory"
  | Inst_form s -> pp_print_string fmt s
  | Data_form s -> pp_print_string fmt s
  | Fallsthru -> pp_print_string fmt "code falls through"
  | Cyclic_imports s ->
      pp_print_string fmt s; pp_print_char fmt ':'; pp_print_break fmt 1 2;
      pp_print_string fmt "cyclic import"
  | Doesnt_export -> pp_print_string fmt "exported item not defined in module"
  | Ndisjoint_exports l ->
      pp_print_string fmt "non-disjoint exports: "; id_prn fmt l
  | Multiple_exports -> pp_print_string fmt "exported twice"
  | Con_def_nleq -> pp_print_string fmt "constructor definition not subtype"
  | Intt_nleq s ->
      pp_print_string fmt "interface not subtype:"; pp_print_break fmt 1 2;
      pp_print_string fmt s
;;

let print_ctxt fmt o ctxt =
  let rs = Talctxt.get_register_state ctxt in
  let kindmap = Talctxt.get_var_map ctxt in
  let pp_print_string = pp_print_string fmt in
  let print_map dom codom d =
    pp_open_hvbox fmt 0;
    Dict.app_dict (fun x v -> (dom x; 
			       pp_print_string ":"; 
			       codom v;
			       pp_print_break fmt 1 2)) d;
    pp_close_box fmt () in
  begin
    pp_open_hvbox fmt 0;
    pp_print_string "CTXT{"; pp_print_break fmt 0 2;
    pp_print_string "Delta{";
    print_map (id_prn fmt) (print_kind fmt o) kindmap;
    pp_print_string "}"; pp_print_break fmt 1 2;
    pp_print_string "Regs"; print_register_state fmt o rs;
    pp_print_break fmt 1 2;
    pp_print_string "}";
    pp_close_box fmt()
  end

let print_Talverify fmt o (ctxt,ve) =
  pp_open_hvbox fmt 0;
  print_tal_loc fmt o (get_loc ctxt);
  pp_print_char fmt ':'; pp_print_break fmt 1 2;
  pp_print_string fmt (get_verify_ctxt ctxt);
  pp_print_char fmt ':'; pp_print_break fmt 1 2;
  print_verify_error fmt o ve;
(*  pp_print_break fmt 1 2;
  print_ctxt fmt o ctxt;
*)
  pp_close_box fmt ()
;;

(* EOF: x86talpp.ml *)
