(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Pretty-printer for Csyntax *)

open Format
open Extracted.AST
open Extracted.Csyntax
open Extracted.Glue

let freshNameCounter = ref 0
let nameof id =
  try
    Hashtbl.find ClightFromC.symTable id
  with Not_found ->
    freshNameCounter := !freshNameCounter + 1;
    let name = "_cerco" ^ string_of_int (!freshNameCounter) in
    Hashtbl.add ClightFromC.symTable id name;
    name

let rec mListIter f l =
match l with
| Extracted.List.Nil -> ()
| Extracted.List.Cons (h,t) -> f h; mListIter f t

let rec mlist l =
match l with
| Extracted.List.Nil -> []
| Extracted.List.Cons (h,t) -> h::(mlist t)

let stack_cost_for scm id =
  let check ids = 
    let id' = Extracted.Types.fst ids in
    match Extracted.Identifiers.eq_identifier Extracted.PreIdentifiers.SymbolTag id id' with
    | Extracted.Bool.True -> Extracted.Types.Some (Extracted.Types.snd ids)
    | _ -> Extracted.Types.None
  in
  match Extracted.List.find check scm with
  | Extracted.Types.None -> 0
  | Extracted.Types.Some n -> int_of_matitanat n


let rec flist l =
match l with
| Fnil -> []
| Fcons (id, ty, tl) -> (nameof id,ty)::(flist tl)

type cost_style =
| Cost_plain
| Cost_numbered of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat
| Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat

(* Not ideal, but convenient for now *)
let style = ref Cost_plain

let namecost l =
  "_cost" ^ string_of_int (int_of_matitapos l)

let name_unop = function
  | Onotbool -> "!"
  | Onotint  -> "~"
  | Oneg     -> "-"


let name_binop = function
  | Oadd -> "+"
  | Osub -> "-"
  | Omul -> "*"
  | Odiv -> "/"
  | Omod -> "%"
  | Oand -> "&"
  | Oor  -> "|"
  | Oxor -> "^"
  | Oshl -> "<<"
  | Oshr -> ">>"
  | Oeq  -> "=="
  | One  -> "!="
  | Olt  -> "<"
  | Ogt  -> ">"
  | Ole  -> "<="
  | Oge  -> ">="

let name_inttype sz sg =
  match sz, sg with
  | I8, Signed -> "signed char"
  | I8, Unsigned -> "unsigned char"
  | I16, Signed -> "short"
  | I16, Unsigned -> "unsigned short"
  | I32, Signed -> "int"
  | I32, Unsigned -> "unsigned int"

(*
let name_floattype sz =
  match sz with
  | F32 -> "float"
  | F64 -> "double"
*)

(* Collecting the names and fields of structs and unions *)

module StructUnionSet = Set.Make(struct
  type t = string * fieldlist
  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
end)

let struct_unions = ref StructUnionSet.empty

let register_struct_union id fld =
  struct_unions := StructUnionSet.add (id, fld) !struct_unions

(* Declarator (identifier + type) *)

let name_optid id =
  if id = "" then "" else " " ^ id

let parenthesize_if_pointer id =
  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id

let rec name_cdecl id ty =
  match ty with
  | Tvoid ->
      "void" ^ name_optid id
  | Tint(sz, sg) ->
      name_inttype sz sg ^ name_optid id
  (*| Tfloat sz ->
      name_floattype sz ^ name_optid id*)
  | Tpointer t ->
      name_cdecl ("*" ^ id) t
  | Tarray(t, n) ->
      name_cdecl
        (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int (int_of_matitanat n)))
        t
  | Tfunction(args, res) ->
      let b = Buffer.create 20 in
      if id = ""
      then Buffer.add_string b "(*)"
      else Buffer.add_string b (parenthesize_if_pointer id);
      Buffer.add_char b '(';
      begin match args with
      | Tnil ->
          Buffer.add_string b "void"
      | _ ->
          let rec add_args first = function
          | Tnil -> ()
          | Tcons (t1, tl) ->
              if not first then Buffer.add_string b ", ";
              Buffer.add_string b (name_cdecl "" t1);
              add_args false tl in
          add_args true args
      end;
      Buffer.add_char b ')';
      name_cdecl (Buffer.contents b) res
  | Tstruct(name, fld) ->
      (nameof name) ^ name_optid id
  | Tunion(name, fld) ->
      (nameof name) ^ name_optid id
  | Tcomp_ptr name ->
      (nameof name) ^ " *" ^ id

(* Type *)

let name_type ty = name_cdecl "" ty

(* Expressions *)

let parenthesis_level (Expr (e, ty)) =
  match e with
  | Econst_int _ -> 0
  (*| Econst_float _ -> 0*)
  | Evar _ -> 0
  | Eunop(_, _) -> 30
  | Ederef _ -> 20
  | Eaddrof _ -> 30
  | Ebinop(op, _, _) ->
      begin match op with
      | Oand | Oor | Oxor -> 75
      | Oeq | One | Olt | Ogt | Ole | Oge -> 70
      | Oadd | Osub | Oshl | Oshr -> 60
      | Omul | Odiv | Omod -> 40
      end
  | Ecast _ -> 30
  | Econdition(_, _, _) -> 80
  | Eandbool(_, _) -> 80
  | Eorbool(_, _) -> 80
  | Esizeof _ -> 20
  | Efield _ -> 20
  | Ecost (_,_) -> 20 
  (*| Ecall (_,_,_) -> 20*)

let rec print_expr p (Expr (eb, ty) as e) =
  let level = parenthesis_level e in
  match eb with
  | Econst_int (_,n) ->
      fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
  (*| Econst_float f ->
      fprintf p "%F" f*)
  | Evar id ->
      fprintf p "%s" (nameof id)
  | Eunop(op, e1) ->
      fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1)
  | Ederef (Expr (Ebinop(Oadd, e1, e2), _)) ->
      fprintf p "@[<hov 2>%a@,[%a]@]"
                print_expr_prec (level, e1)
                print_expr_prec (level, e2)
  | Ederef (Expr (Efield(e1, id), _)) ->
      fprintf p "%a->%s" print_expr_prec (level, e1) (nameof id)
  | Ederef e ->
      fprintf p "*%a" print_expr_prec (level, e)
  | Eaddrof e ->
      fprintf p "&%a" print_expr_prec (level, e)
  | Ebinop(op, e1, e2) ->
      fprintf p "@[<hov 0>%a@ %s %a@]"
                print_expr_prec (level, e1)
                (name_binop op)
                print_expr_prec (level, e2)
  | Ecast(ty, e1) ->
      fprintf p "@[<hov 2>(%s)@,%a@]"
                (name_type ty)
                print_expr_prec (level, e1)
  | Econdition(e1, e2, e3) ->
      fprintf p "@[<hov 0>%a@ ? %a@ : %a@]"
                print_expr_prec (level, e1)
                print_expr_prec (level, e2)
                print_expr_prec (level, e3)
  | Eandbool(e1, e2) ->
      fprintf p "@[<hov 0>%a@ && %a@]"
                print_expr_prec (level, e1)
                print_expr_prec (level, e2)
  | Eorbool(e1, e2) ->
      fprintf p "@[<hov 0>%a@ || %a@]"
                print_expr_prec (level, e1)
                print_expr_prec (level, e2)
  | Esizeof ty ->
      fprintf p "sizeof(%s)" (name_type ty)
  | Efield(e1, id) ->
      fprintf p "%a.%s" print_expr_prec (level, e1) (nameof id)
  | Ecost (lbl,e1) ->
      match !style with
      | Cost_plain ->
        fprintf p "(/* %s */ %a)" (namecost lbl) print_expr e1
      | Cost_numbered (cm,_,_,_) ->
        fprintf p "(/* %s = %d */ %a)" (namecost lbl) (int_of_matitanat (cm lbl)) print_expr e1
      | Cost_instrumented (cm,_,_,_) ->
        fprintf p "(__cost_incr(%d), %a)" (int_of_matitanat (cm lbl)) print_expr e1
  (*| Ecall (f, arg, e) ->
      fprintf p "(%s(%a), %a)" f print_expr arg print_expr e*)

and print_expr_prec p (context_prec, e) =
  let this_prec = parenthesis_level e in
  if this_prec >= context_prec
  then fprintf p "(%a)" print_expr e
  else print_expr p e

let rec print_expr_list p (first, el) =
  match el with
  | Extracted.List.Nil -> ()
  | Extracted.List.Cons (e1, et) ->
      if not first then fprintf p ",@ ";
      print_expr p e1;
      print_expr_list p (false, et)

(* Another quick hack :( *)
let return_cost = ref None
let print_return_cost p =
  match !return_cost with
  | None -> ()
  | Some s -> fprintf p "@ __stack_size_incr(-%d);@ " s

let rec print_stmt p s =
  match s with
  | Sskip ->
      fprintf p "/*skip*/;"
  | Sassign(e1, e2) ->
      fprintf p "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2
  | Scall(Extracted.Types.None, e1, el) ->
      fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]"
                print_expr e1
                print_expr_list (true, el)
  | Scall(Extracted.Types.Some lhs, e1, el) ->
      fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@]);@]"
                print_expr lhs
                print_expr e1
                print_expr_list (true, el)
  | Ssequence(s1, s2) ->
      fprintf p "%a@ %a" print_stmt s1 print_stmt s2
  | Sifthenelse(e, s1, Sskip) ->
      fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
              print_expr e
              print_stmt s1
  | Sifthenelse(e, s1, s2) ->
      fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
              print_expr e
              print_stmt s1
              print_stmt s2
  | Swhile(e, s) ->
      fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
              print_expr e
              print_stmt s
  | Sdowhile(e, s) ->
      fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
              print_stmt s
              print_expr e
  | Sfor(s_init, e, s_iter, s_body) ->
      fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
              print_stmt_for s_init
              print_expr e
              print_stmt_for s_iter
              print_stmt s_body
  | Sbreak ->
      fprintf p "break;"
  | Scontinue ->
      fprintf p "continue;"
  | Sswitch(e, cases) ->
      fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
              print_expr e
              print_cases cases
  | Sreturn Extracted.Types.None ->
      print_return_cost p;
      fprintf p "return;"
  | Sreturn (Extracted.Types.Some e) ->
      print_return_cost p;
      fprintf p "return %a;" print_expr e
  | Slabel(lbl, s1) ->
      fprintf p "%s:@ %a" (nameof lbl) print_stmt s1
  | Sgoto lbl ->
      fprintf p "goto %s;" (nameof lbl)
 | Scost (lbl,s1) ->
      match !style with
      | Cost_plain ->
        fprintf p "%s:@ %a" (namecost lbl) print_stmt s1
      | Cost_numbered (cm,_,_,_) ->
        fprintf p "/* %s = %d */@ %a" (namecost lbl) (int_of_matitanat (cm lbl)) print_stmt s1
      | Cost_instrumented (cm,_,_,_) ->
        fprintf p "__cost_incr(%d);@ %a" (int_of_matitanat (cm lbl)) print_stmt s1

and print_cases p cases =
  match cases with
  | LSdefault Sskip ->
      ()
  | LSdefault s ->
      fprintf p "@[<v 2>default:@ %a@]" print_stmt s
  | LScase(_, lbl, Sskip, rem) ->
      fprintf p "case %ld:@ %a"
        (Int32.of_int (int_of_bitvector lbl))
        print_cases rem
  | LScase(_, lbl, s, rem) ->
      fprintf p "@[<v 2>case %ld:@ %a@]@ %a"
              (Int32.of_int (int_of_bitvector lbl))
              print_stmt s
              print_cases rem

and print_stmt_for p s =
  match s with
  | Sskip ->
      fprintf p "/*nothing*/"
  | Sassign(e1, e2) ->
      fprintf p "%a = %a" print_expr e1 print_expr e2
  | Ssequence(s1, s2) ->
      fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2
  | Scall(Extracted.Types.None, e1, el) ->
      fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@])@]"
                print_expr e1
                print_expr_list (true, el)
  | Scall(Extracted.Types.Some lhs, e1, el) ->
      fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@])@]"
                print_expr lhs
                print_expr e1
                print_expr_list (true, el)
  | _ ->
      fprintf p "({ %a })" print_stmt s

let name_function_parameters fun_name params =
  let b = Buffer.create 20 in
  Buffer.add_string b fun_name;
  Buffer.add_char b '(';
  begin match params with
  | Extracted.List.Nil ->
      Buffer.add_string b "void"
  | _ ->
      let rec add_params first = function
      | Extracted.List.Nil -> ()
      | Extracted.List.Cons ({Extracted.Types.fst = id; Extracted.Types.snd = ty}, rem) ->
          if not first then Buffer.add_string b ", ";
          Buffer.add_string b (name_cdecl (nameof id) ty);
          add_params false rem in
      add_params true params
  end;
  Buffer.add_char b ')';
  Buffer.contents b

let print_function p id f =
  fprintf p "%s@ "
            (name_cdecl (name_function_parameters (nameof id) f.fn_params)
                        f.fn_return);
  fprintf p "@[<v 2>{@ ";
  mListIter
    (fun ({Extracted.Types.fst = id; Extracted.Types.snd = ty}) ->
      fprintf p "%s;@ " (name_cdecl (nameof id) ty))
    f.fn_vars;
  (match !style with
  | Cost_plain -> return_cost := None
  | Cost_numbered (_,_,scm,_) ->
    let cost = stack_cost_for scm id in
    fprintf p "/* stack cost %d */@ " cost;
    return_cost := None (* No need to tell us the stack size again *)
  | Cost_instrumented (_,_,scm,_) ->
    let cost = stack_cost_for scm id in
    fprintf p "__stack_size_incr(%d);@ " cost;
    return_cost := Some cost
  );
  print_stmt p f.fn_body;
  (* We don't always need this (e.g., when it ends with a return), but
     better safe than sorry... *)
  print_return_cost p;
  fprintf p "@;<0 -2>}@]@ @ "

let print_fundef p {Extracted.Types.fst = id; Extracted.Types.snd = fd} =
  match fd with
  | CL_External(_, args, res) ->
      fprintf p "extern %s;@ @ "
                (name_cdecl (nameof id) (Tfunction(args, res)))
  | CL_Internal f ->
      print_function p id f

let string_of_init id =
  let b = Buffer.create (List.length id) in
  let add_init = function
  | Init_int8 n ->
      let n = int_of_bitvector n in
      if n >= 32 && n <= 126 && n <> Char.code '\"' && n <> Char.code '\\'
      then Buffer.add_char b (Char.chr n)
      else Buffer.add_string b (Printf.sprintf "\\%03o" n)
  | _ ->
      assert false
  in List.iter add_init id; Buffer.contents b

let eight = matitanat_of_int 8
let zero8 = Extracted.BitVector.zero eight

let chop_last_nul id =
  match List.rev id with
  | Init_int8 n :: tl when Extracted.BitVector.eq_bv eight n zero8 = Extracted.Bool.True -> List.rev tl
  | _ -> id

let print_init p = function
  | Init_int8 n -> fprintf p "%ld,@ " (Int32.of_int (int_of_bitvector n))
  | Init_int16 n -> fprintf p "%ld,@ " (Int32.of_int (int_of_bitvector n))
  | Init_int32 n -> fprintf p "%ld,@ " (Int32.of_int (int_of_bitvector n))
  (*| Init_float32 n -> fprintf p "%F,@ " n
  | Init_float64 n -> fprintf p "%F,@ " n*)
  | Init_space n -> fprintf p "/* skip %ld, */@ " (Int32.of_int (int_of_matitanat n))
  | Init_null  -> fprintf p "0,@ "
  | Init_addrof(symb, ofs) ->
      let symb = nameof symb in
      let ofs = Int32.of_int (int_of_matitanat ofs) in
      if ofs = Int32.zero
      then fprintf p "&%s,@ " symb
      else fprintf p "(void *)((char *)&%s + %ld),@ " symb ofs

let print_init1 p = function
  | Init_int8 n -> fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
  | Init_int16 n -> fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
  | Init_int32 n -> fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
  (*| Init_float32 n -> fprintf p "%F" n
  | Init_float64 n -> fprintf p "%F" n*)
  | Init_space n -> fprintf p "/* skip %ld */" (Int32.of_int (int_of_matitanat n))
  | Init_null  -> fprintf p "0"
  | Init_addrof(symb, ofs) ->
      let symb = nameof symb in
      let ofs = Int32.of_int (int_of_matitanat ofs) in
      if ofs = Int32.zero
      then fprintf p "&%s" symb
      else fprintf p "(void *)((char *)&%s + %ld)" symb ofs

(* XXX From Misc.LexingExt *)
  let lex_num s pos =
    let rec num i = 
        if s.[i] >= '0' && s.[i] <= '9' then
          num (i + 1)
        else 
          i
    in
    let pos' = num pos in
    if pos = pos' then 
      None
    else 
      Some (pos, pos', int_of_string (String.sub s pos (pos' - pos)))


let match_string_literal s pos =
  let s_len = String.length s - 1 in
  let prefix = "__stringlit_" in
  let len_prefix = String.length prefix in
  s_len >= len_prefix
  && String.sub s 0 len_prefix = prefix  && 
      match lex_num s len_prefix with
	| None -> false
	| Some (pos, pos', v) -> pos' = String.length s - 1

let print_globvar p ({Extracted.Types.fst = 
                       {Extracted.Types.fst = id; Extracted.Types.snd = region};
                      Extracted.Types.snd =
                       {Extracted.Types.fst = init; Extracted.Types.snd = ty};
                     }) =
  let id = nameof id in
  let init = mlist init in
  match init with
  | [] ->
      fprintf p "extern %s;@ @ "
              (name_cdecl id ty)
  | [Init_space _] ->
      fprintf p "%s;@ @ "
              (name_cdecl id ty)
  | [init] ->
      fprintf p "@[<hov 2>%s = %a;@]@ @ "
              (name_cdecl id ty) print_init1 init
  | _ ->
      fprintf p "@[<hov 2>%s = "
              (name_cdecl id ty);
      if match_string_literal id 0 
      && List.for_all (function Init_int8 _ -> true | _ -> false) init
      then
        fprintf p "\"%s\"" (string_of_init (chop_last_nul init))
      else begin
        fprintf p "{@ ";
        List.iter (print_init p) init;
        fprintf p "}"
      end;
      fprintf p ";@]@ @ "

(* Collect struct and union types *)

let rec collect_type = function
  | Tvoid -> ()
  | Tint(sz, sg) -> ()
  (*| Tfloat sz -> ()*)
  | Tpointer t -> collect_type t
  | Tarray(t, n) -> collect_type t
  | Tfunction(args, res) -> collect_type_list args; collect_type res
  | Tstruct(id, fld) -> register_struct_union (nameof id) fld; collect_fields fld
  | Tunion(id, fld) -> register_struct_union (nameof id) fld; collect_fields fld
  | Tcomp_ptr _ -> ()

and collect_type_list = function
  | Tnil -> ()
  | Tcons (hd,tl) -> collect_type hd; collect_type_list tl

and collect_fields = function
  | Fnil -> ()
  | Fcons (id, hd, tl) -> collect_type hd; collect_fields tl

let rec collect_expr (Expr(ed, ty)) =
  match ed with
  | Econst_int _ -> ()
  (*| Econst_float f -> ()*)
  | Evar id -> ()
  | Eunop(op, e1) -> collect_expr e1
  | Ederef e -> collect_expr e
  | Eaddrof e -> collect_expr e
  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
  | Esizeof ty -> collect_type ty
  | Efield(e1, id) -> collect_expr e1
  | Ecost(_, e) -> collect_expr e
  (*| Ecall(_, arg, e) -> collect_expr arg; collect_expr e*)

let rec collect_expr_list = function
  | Extracted.List.Nil -> ()
  | Extracted.List.Cons (hd, tl) -> collect_expr hd; collect_expr_list tl

let rec collect_stmt = function
  | Sskip -> ()
  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
  | Scall(Extracted.Types.None, e1, el) -> collect_expr e1; collect_expr_list el
  | Scall(Extracted.Types.Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
  | Swhile(e, s) -> collect_expr e; collect_stmt s
  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
  | Sfor(s_init, e, s_iter, s_body) ->
      collect_stmt s_init; collect_expr e;
      collect_stmt s_iter; collect_stmt s_body
  | Sbreak -> ()
  | Scontinue -> ()
  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
  | Sreturn Extracted.Types.None -> ()
  | Sreturn (Extracted.Types.Some e) -> collect_expr e
  | Slabel(lbl, s) -> collect_stmt s
  | Sgoto lbl -> ()
  | Scost (_,s1) -> collect_stmt s1

and collect_cases = function
  | LSdefault s -> collect_stmt s
  | LScase(_, lbl, s, rem) -> collect_stmt s; collect_cases rem

let collect_function f =
  collect_type f.fn_return;
  mListIter (fun ({Extracted.Types.fst = id; Extracted.Types.snd = ty}) -> collect_type ty) f.fn_params;
  mListIter (fun ({Extracted.Types.fst = id; Extracted.Types.snd = ty}) -> collect_type ty) f.fn_vars;
  collect_stmt f.fn_body

let collect_fundef ({Extracted.Types.fst = id; Extracted.Types.snd = fd}) =
  match fd with
  | CL_External(_, args, res) -> collect_type_list args; collect_type res
  | CL_Internal f -> collect_function f

let collect_globvar v =
  collect_type (Extracted.Types.snd (Extracted.Types.snd v))

let collect_program p =
  mListIter collect_globvar p.prog_vars;
  mListIter collect_fundef p.prog_funct

let declare_struct_or_union p (name, fld) =
  fprintf p "%s;@ @ " name

let print_struct_or_union p (name, fld) =
  fprintf p "@[<v 2>%s {" name;
  let rec print_fields = function
  | Fnil -> ()
  | Fcons (id, ty, rem) ->
      fprintf p "@ %s;" (name_cdecl (nameof id) ty);
      print_fields rem in
  print_fields fld;
  fprintf p "@;<0 -2>};@]@ "

let print_program_2 p prog =
  struct_unions := StructUnionSet.empty;
  collect_program prog;
  fprintf p "@[<v 0>";
  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
  StructUnionSet.iter (print_struct_or_union p) !struct_unions;
  mListIter (print_globvar p) prog.prog_vars;
  mListIter (print_fundef p) prog.prog_funct;
  fprintf p "@]@."

let print_program cs prog =
  style := cs;
  (match cs with
  | Cost_instrumented (cm,initc,_,sinit) ->
     let cinit = int_of_matitanat (cm initc) in
     let sinit = int_of_float (2.0 ** 16.) - int_of_matitanat sinit in
      fprintf str_formatter "int __cost = %d;@\n@\n" cinit;
      fprintf str_formatter "int __stack_size = %d, __stack_size_max = %d;@\n@\n" sinit sinit;
      fprintf str_formatter "void __cost_incr(int incr) {@\n";
      fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n";
      fprintf str_formatter "void __stack_size_incr(int incr) {@\n";
      fprintf str_formatter "  __stack_size = __stack_size + incr;@\n";
      fprintf str_formatter "  __stack_size_max = __stack_size_max < __stack_size ? __stack_size : __stack_size_max;@\n}@\n@\n"
  | _ -> ());
  print_program_2 str_formatter prog;
  flush_str_formatter ()

let string_of_ctype = name_type

let print_expression cs e = 
  style := cs;
  print_expr str_formatter e;
  flush_str_formatter ()

let print_statement cs s = 
  style := cs;
  print_stmt str_formatter s;
  flush_str_formatter ()

let print_ctype_prot = name_type

let print_ctype_def = function
  | Tstruct (name, fld) | Tunion (name, fld) ->
    let f_fld s (id, t) = s ^ "  " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in
    let s_fld = List.fold_left f_fld "" in
    nameof name ^ " {\n" ^ (s_fld (flist fld)) ^ "};\n"
  | _ -> "" (* no definition associated to the other types *)

let string_of_unop = name_unop

let string_of_binop = name_binop