CristalCaveGem » LustreC

open Format

let with_out_file file f =

  let oc = open_out file in

  let fmt = formatter_of_out_channel oc in

  f fmt;

  close_out oc

open Format

let print_version fmt =

  Format.fprintf fmt 

    "/* @[<v>C code generated by %s@,Version number %s@,Code is %s compliant@,Using %s numbers */@,@]@."

       (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)

    || (List.exists (fun v -> v.var_id = name) m.mstep.step_outputs)

    || (List.exists (fun v -> v.var_id = name) m.mstep.step_locals)

    || (List.exists (fun v -> v.var_id = name) m.mmemory) in

       (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)

    || (List.exists (fun v -> v.var_id = name) m.mmemory) in

       (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)

    || (List.exists (fun v -> v.var_id = name) m.mmemory) in

  let vars = m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory in

    let s = Printf.sprintf "__%s_%d" "i" !loop_cpt in

    if List.exists (fun v -> v.var_id = s) vars then aux () else s

    Format.fprintf fmt "((%a %% %a) + ((%a %% %a) < 0?(abs(%a)):0))"

    Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

    Format.fprintf fmt "(%a - %t) / %a"

    Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2

  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)

  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v

  | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v

  | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2

  | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2

       Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

  | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2

  | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2

       Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2

  | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2

  | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)

  match dim.Dimension.dim_desc with

  | Dimension.Dident id       ->

     fprintf fmt "%s" id

  | Dimension.Dint i          ->

     fprintf fmt "%d" i

  | Dimension.Dbool b         ->

     fprintf fmt "%B" b

  | Dimension.Dite (i, t, e)  ->

     fprintf fmt "((%a)?%a:%a)"

       pp_c_dimension i pp_c_dimension t pp_c_dimension e

  | Dimension.Dappl (f, args) ->

     fprintf fmt "%a" (pp_basic_lib_fun (Basic_library.is_numeric_operator f) f pp_c_dimension) args

  | Dimension.Dlink dim' -> fprintf fmt "%a" pp_c_dimension dim'

  | Dimension.Dvar       -> fprintf fmt "_%s" (Utils.name_of_dimension dim.Dimension.dim_id)

  | Dimension.Dunivar    -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)

  Types.is_int_type t || Types.is_real_type t || Types.is_bool_type t

	 (pp_basic_c_type ~var_opt) t

	 var_id

	 pp_suffix ()

      match (Types.repr t).Types.tdesc with

      | Types.Tclock t'       -> aux t' pp_suffix

      | Types.Tarray (d, t')  ->

	 let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in

	 aux t' pp_suffix'

      | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix

      | Types.Tconst ty       -> fprintf fmt "%s %s" ty var_id

      | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var_id

      | _                     -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false

 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)

    | Const_int i     -> pp_print_int fmt i

    | Const_real r -> Real.pp fmt r

    (* | Const_float r   -> pp_print_float fmt r *)

    | Const_tag t     -> pp_c_tag fmt t

    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca

    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_c_const fmt c)) fl

    | Const_string _ | Const_modeid _ -> assert false (* string occurs in annotations not in C *)

  | Cst c         -> pp_c_const fmt c

  | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " pp_c_val) vl

  | Access (t, i) -> fprintf fmt "%a[%a]" pp_c_val t pp_c_val i

  | Power (v, _)  -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." (Machine_code_common.pp_val m) v; assert false)

  | Var v    ->

     if Machine_code_common.is_memory m v then (

       (* array memory vars are represented by an indirection to a local var with the right type,

          in order to avoid casting everywhere. *)

       if Types.is_array_type v.var_type && not (Types.is_real_type v.var_type && !Options.mpfr)

     )

  | Fun (n, vl)   -> pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl

    if Machine_code_common.is_memory m id && not (Types.is_real_type id.var_type && !Options.mpfr)

  then pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)

  else pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type

  then pp_c_type  ~var_opt:(Some id)                  id.var_id  fmt id.var_type

  else pp_c_type  ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)

    Format.fprintf fmt "%a = %a"

      (pp_c_type  ~var_opt:(Some id) id.var_id) id.var_type

      (pp_c_val m "" (pp_c_var_read m)) (Machine_code_common.get_const_assign m id)

    Format.fprintf fmt "%a"

      (pp_c_type  ~var_opt:(Some id) id.var_id) id.var_type

let pp_c_decl_array_mem self fmt id =

  fprintf fmt "%a = (%a) (%s->_reg.%s)"

    (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type

    (pp_c_type "(*)") id.var_type

    self

    id.var_id

  then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)

  else pp_c_type                  id.var_id  fmt id.var_type

let pp_c_checks self fmt m =

  Utils.fprintf_list ~sep:"" 

    (fun fmt (loc, check) -> 

      fprintf fmt 

	"@[<v>%a@,assert (%a);@]@," 

	Location.pp_c_loc loc

	(pp_c_val m self (pp_c_var_read m)) check

    ) 

    fmt 

    m.mstep.step_checks

let pp_registers_struct fmt m =

  if m.mmemory <> []

  then

    fprintf fmt "@[%a {@[<v>%a;@ @]}@] _reg; "

      pp_machine_regtype_name m.mname.node_id

      (Utils.fprintf_list ~sep:";@ " pp_c_decl_struct_var) m.mmemory

  else

    ()

  if fst (Machine_code_common.get_stateless_status m) then

    begin

    end

  else

    begin

      (* Define struct *)

      fprintf fmt "@[%a {@[<v>%a%t%a%t@]};@]@."

	pp_machine_memtype_name m.mname.node_id

	pp_registers_struct m

	(Utils.pp_final_char_if_non_empty "@ " m.mmemory)

	(Utils.fprintf_list ~sep:";@ " pp_c_decl_instance_var) m.minstances

	(Utils.pp_final_char_if_non_empty ";@ " m.minstances)

    end

let print_machine_struct_from_header fmt inode =

  if inode.nodei_stateless then

    begin

    end

  else

    begin

      (* Declare struct *)

      fprintf fmt "@[%a;@]@."

	pp_machine_memtype_name inode.nodei_id

    end

  fprintf fmt "%a * %a (%a)"

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static

  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static

    (Utils.pp_final_char_if_non_empty ",@," static) 

  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static

    (Utils.pp_final_char_if_non_empty ",@," static) 

  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static

    (Utils.pp_final_char_if_non_empty ",@," static) 

  fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]@,@])"

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs

    (Utils.pp_final_char_if_non_empty ",@ " inputs) 

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs

  fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@])"

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs

    (Utils.pp_final_char_if_non_empty ",@ " inputs) 

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs

    (Utils.pp_final_char_if_non_empty ",@," outputs) 

let print_stateless_C_prototype fmt (name, inputs, outputs) =

  let output = 

    match outputs with

    | [hd] -> hd

    | _ -> assert false

  in

  fprintf fmt "%a %s (@[<v>@[%a@]@,@])"

    (pp_basic_c_type ~var_opt:None) output.var_type

    name

    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs

let print_import_init fmt dep =

  if dep.local then

    let baseNAME = file_to_module_name dep.name in

    fprintf fmt "%a();" pp_global_init_name baseNAME

  else ()

let print_import_clear fmt dep =

  if dep.local then

    let baseNAME = file_to_module_name dep.name in

    fprintf fmt "%a();" pp_global_clear_name baseNAME

  else ()

  fprintf fmt "#include \"%s.h\"@," dep.name

    fprintf fmt "#include \"%s_alloc.h\"@," dep.name

let print_extern_alloc_prototypes fmt dep =

  List.iter (fun decl -> match decl.top_decl_desc with

  | ImportedNode ind when not ind.nodei_stateless ->

    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in

    begin

      fprintf fmt "extern %a;@.@." print_alloc_prototype (ind.nodei_id, static);

      fprintf fmt "extern %a;@.@." print_dealloc_prototype ind.nodei_id;

    end

  | _                -> ()

  ) dep.content

let pp_c_main_var_input fmt id =  

  fprintf fmt "%s" id.var_id

let pp_c_main_var_output fmt id =

  if Types.is_address_type id.var_type

  then

    fprintf fmt "%s" id.var_id

  else

    fprintf fmt "&%s" id.var_id

let pp_main_call mname self fmt m (inputs: value_t list) (outputs: var_decl list) =

  if fst (Machine_code_common.get_stateless_status m)

  then

    fprintf fmt "%a (%a%t%a);"

      pp_machine_step_name mname

      (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_c_main_var_input)) inputs

      (Utils.pp_final_char_if_non_empty ", " inputs) 

      (Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs

  else

    fprintf fmt "%a (%a%t%a%t%s);"

      pp_machine_step_name mname

      (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_c_main_var_input)) inputs

      (Utils.pp_final_char_if_non_empty ", " inputs) 

      (Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs

      (Utils.pp_final_char_if_non_empty ", " outputs)

      self

let pp_array_suffix fmt loop_vars =

  Utils.fprintf_list ~sep:"" (fun fmt v -> fprintf fmt "[%s]" v) fmt loop_vars

	idx idx idx pp_c_dimension dim idx

	(aux (idx::indices)) (Types.array_element_type typ)

	fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in

  if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)

  then

    begin

      reset_loop_counter ();

      aux [] fmt var.var_type

    end

let pp_const_initialize m pp_var fmt const =

  let var = Machine_code_common.mk_val (Var (Corelang.var_decl_of_const const)) const.const_type in

  let rec aux indices value fmt typ =

    if Types.is_array_type typ

    then

      let dim = Types.array_type_dimension typ in

      let szl = Utils.enumerate (Dimension.size_const_dimension dim) in

      let typ' = Types.array_element_type typ in

      let value = match value with

	| Const_array ca -> List.nth ca

	| _                      -> assert false in

      fprintf fmt "%a"

	(Utils.fprintf_list ~sep:"@," (fun fmt i -> aux (string_of_int i::indices) (value i) fmt typ')) szl

    else

      let indices = List.rev indices in

      let pp_var_suffix fmt var =

	fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in

      begin

	Mpfr.pp_inject_init pp_var_suffix fmt var;

	fprintf fmt "@,";

	Mpfr.pp_inject_real pp_var_suffix pp_c_const fmt var value

      end

  in

  if !Options.mpfr && Types.is_real_type (Types.array_base_type const.const_type)

  then

    begin

      reset_loop_counter ();

      aux [] const.const_value fmt const.const_type

    end

	idx idx idx pp_c_dimension dim idx

	(aux (idx::indices)) (Types.array_element_type typ)

	fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in

  if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)

  then

    begin

      reset_loop_counter ();

      aux [] fmt var.var_type

    end

let pp_const_clear pp_var fmt const =

  let m = Machine_code_common.empty_machine in

  let var = Corelang.var_decl_of_const const in

  let rec aux indices fmt typ =

    if Types.is_array_type typ

    then

      let dim = Types.array_type_dimension typ in

      let idx = mk_loop_var m () in

      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

	idx idx idx pp_c_dimension dim idx

	(aux (idx::indices)) (Types.array_element_type typ)

    else

      let indices = List.rev indices in

      let pp_var_suffix fmt var =

	fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in

      Mpfr.pp_inject_clear pp_var_suffix fmt var 

  in

  if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)

  then

    begin

      reset_loop_counter ();

      aux [] fmt var.var_type

    end

let pp_call m self pp_read pp_write fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =

 try (* stateful node instance *)

   let (n,_) = List.assoc i m.minstances in

   fprintf fmt "%a (%a%t%a%t%s->%s);"

     pp_machine_step_name (node_name n)

     (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_read)) inputs

     (Utils.pp_final_char_if_non_empty ", " inputs) 

     (Utils.fprintf_list ~sep:", " pp_write) outputs

     (Utils.pp_final_char_if_non_empty ", " outputs)

     self

     i

 with Not_found -> (* stateless node instance *)

   let (n,_) = List.assoc i m.mcalls in

   fprintf fmt "%a (%a%t%a);"

     pp_machine_step_name (node_name n)

     (Utils.fprintf_list ~sep:", " (pp_c_val m self pp_read)) inputs

     (Utils.pp_final_char_if_non_empty ", " inputs) 

     (Utils.fprintf_list ~sep:", " pp_write) outputs 

let pp_basic_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =

  pp_call m self (pp_c_var_read m) (pp_c_var_write m) fmt i inputs outputs

(*

 try (* stateful node instance *)

   let (n,_) = List.assoc i m.minstances in

   fprintf fmt "%a (%a%t%a%t%s->%s);"

     pp_machine_step_name (node_name n)

     (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) inputs

     (Utils.pp_final_char_if_non_empty ", " inputs) 

     (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs

     (Utils.pp_final_char_if_non_empty ", " outputs)

     self

     i

 with Not_found -> (* stateless node instance *)

   let (n,_) = List.assoc i m.mcalls in

   fprintf fmt "%a (%a%t%a);"

     pp_machine_step_name (node_name n)

     (Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) inputs

     (Utils.pp_final_char_if_non_empty ", " inputs) 

     (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs 

*)

let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =

  let pp_offset pp_var indices fmt var =

    match indices with

    | [] -> fprintf fmt "%a" pp_var var

    | _  -> fprintf fmt "%a[%a]" pp_var var (Utils.fprintf_list ~sep:"][" pp_print_string) indices in

  let rec aux indices fmt typ =

    if Types.is_array_type typ

    then

      let dim = Types.array_type_dimension typ in

      let idx = mk_loop_var m () in

      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

	idx idx idx pp_c_dimension dim idx

	(aux (idx::indices)) (Types.array_element_type typ)

    else

      let pp_read  = pp_offset (pp_c_var_read  m) indices in

      let pp_write = pp_offset (pp_c_var_write m) indices in

      pp_call m self pp_read pp_write fmt i inputs outputs

  in

  begin

    reset_loop_counter ();

    aux [] fmt (List.hd inputs).Machine_code_types.value_type

  end

let pp_print_file file_suffix fmt typ arg =

  fprintf fmt "@[<v 2>if (traces) {@ ";

  fprintf fmt "fprintf(f_%s, \"%%%s\\n\", %s);@ " file_suffix typ arg;

  fprintf fmt "fflush(f_%s);@ " file_suffix;

  fprintf fmt "@]}@ "

  if Types.is_int_type unclocked_t then (

    fprintf fmt "_put_int(\"%s\", %s);@ " name var_id;

    pp_file fmt "d" var_id

  )

  else if Types.is_bool_type unclocked_t then (

    fprintf fmt "_put_bool(\"%s\", %s);@ " name var_id;

    pp_file fmt "i" var_id

  )

  else if Types.is_real_type unclocked_t then

      if !Options.mpfr then (

        fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@ " name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double;

        pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", mpfr_get_d(" ^ var_id ^ ", MPFR_RNDN)")

      )

      else (

        fprintf fmt "_put_double(\"%s\", %s, %i);@ " name var_id !Options.print_prec_double;

        pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", " ^ var_id)

      )

  else

    (Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false)

let print_get_inputs fmt m =

  let pi fmt (id, v', v) =

    let pp_file = pp_print_file ("in" ^ (string_of_int id)) in

    let unclocked_t = Types.unclock_type v.var_type in

    if Types.is_int_type unclocked_t then (

      fprintf fmt "%s = _get_int(\"%s\");@ " v.var_id v'.var_id;

      pp_file fmt "d" v.var_id

    )

    else if Types.is_bool_type unclocked_t then (

      fprintf fmt "%s = _get_bool(\"%s\");@ " v.var_id v'.var_id;

      pp_file fmt "i" v.var_id

    )

    else if Types.is_real_type unclocked_t then

        if !Options.mpfr then (

	  fprintf fmt "double %s_tmp = _get_double(\"%s\");@ " v.var_id v'.var_id;

          pp_file fmt "f" (v.var_id ^ "_tmp");

          fprintf fmt "mpfr_set_d(%s, %s_tmp, %i);" v.var_id v.var_id (Mpfr.mpfr_prec ())

        )

        else (

	  fprintf fmt "%s = _get_double(\"%s\");@ " v.var_id v'.var_id;

          pp_file fmt "f" v.var_id

        )

    else

      begin

	Global.main_node := !Options.main_node;

	Format.eprintf "Code generation error: %a%a@."

	  Error.pp_error_msg Error.Main_wrong_kind

	  Location.pp_loc v'.var_loc;

	raise (Error.Error (v'.var_loc, Error.Main_wrong_kind))

      end

  in

  Utils.List.iteri2 (fun idx v' v ->

    fprintf fmt "@ %a" pi ((idx+1), v', v);

  ) m.mname.node_inputs m.mstep.step_inputs

  fprintf fmt "FILE *f_%s%i;@ " inout idx 

  fprintf fmt "const char* cst_char_suffix_%s%i = \"_simu.%s%i\";@ " inout idx inout idx;

  fprintf fmt "size_t l%s%i = strlen(dir) + strlen(prefix) + strlen(cst_char_suffix_%s%i);@ " inout idx inout idx;

  fprintf fmt "char* f_%s%i_name = malloc((l%s%i+2) * sizeof(char));@ " inout idx inout idx;

  fprintf fmt "strcpy (f_%s%i_name, dir);@ " inout idx;

  fprintf fmt "strcat(f_%s%i_name, \"/\");@ " inout idx;

  fprintf fmt "strcat(f_%s%i_name, prefix);@ " inout idx;

  fprintf fmt "strcat(f_%s%i_name, cst_char_suffix_%s%i);@ " inout idx inout idx;

  fprintf fmt "f_%s%i = fopen(f_%s%i_name, \"w\");@ " inout idx inout idx;

  fprintf fmt "free(f_%s%i_name);@ " inout idx;

  "f_" ^ inout ^ (string_of_int idx)

open Format 

module type MODIFIERS_HDR =

sig

module EmptyMod =

struct

module Main = functor (Mod: MODIFIERS_HDR) -> 

struct

let print_import_standard fmt =

  begin

    (*   begin *)

	fprintf fmt "#include <stdint.h>@.";

      (* end; *)

    if !Options.mpfr then

      begin

	fprintf fmt "#include <mpfr.h>@."

      end;

    if !Options.cpp then

      fprintf fmt "#include \"%s/arrow.hpp\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner

    else

      fprintf fmt "#include \"%s/arrow.h\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner

  end

let rec print_static_val pp_var fmt v =

  match v.value_desc with

  | Cst c         -> pp_c_const fmt c

  | Var v         -> pp_var fmt v

  | Fun (n, vl)   -> pp_basic_lib_fun (Types.is_int_type v.value_type) n (print_static_val pp_var) fmt vl

  | _             -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false)

let print_constant_decl (m, attr, inst) pp_var fmt v =

  Format.fprintf fmt "%s %a = %a"

    attr

    (pp_c_type (Format.sprintf "%s ## %s" inst v.var_id)) v.var_type

    (print_static_val pp_var) (get_const_assign m v)

let print_static_constant_decl (m, attr, inst) fmt const_locals =

  let pp_var fmt v =

    if List.mem v const_locals

    then

      Format.fprintf fmt "%s ## %s" inst v.var_id

    else 

      Format.fprintf fmt "%s" v.var_id in

  Format.fprintf fmt "%a%t"

    (Utils.fprintf_list ~sep:";\\@," (print_constant_decl (m, attr, inst) pp_var)) const_locals

    (Utils.pp_final_char_if_non_empty ";\\@," const_locals)

let print_static_declare_instance (m, attr, inst) const_locals fmt (i, (n, static)) =

  let pp_var fmt v =

    if List.mem v const_locals

    then

      Format.fprintf fmt "%s ## %s" inst v.var_id

    else 

      Format.fprintf fmt "%s" v.var_id in

  let values = List.map (value_of_dimension m) static in

  fprintf fmt "%a(%s, %a%t%s)"

    pp_machine_static_declare_name (node_name n)

    attr

    (Utils.fprintf_list ~sep:", " (print_static_val pp_var)) values

    (Utils.pp_final_char_if_non_empty ", " static)

    i

let print_static_declare_macro fmt (m, attr, inst) =

  let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in

  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in

  fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%a%s %a %s;\\@,%a%t%a;@,@]"

    pp_machine_static_declare_name m.mname.node_id

    attr

    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic

    (Utils.pp_final_char_if_non_empty ", " m.mstatic)

    inst

    (* constants *)

    (print_static_constant_decl (m, attr, inst)) const_locals

    attr

    pp_machine_memtype_name m.mname.node_id

    inst

    (Utils.fprintf_list ~sep:";\\@," (pp_c_decl_local_var m)) array_mem

    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)

    (Utils.fprintf_list ~sep:";\\@,"

       (fun fmt (i',m') ->

	 let path = sprintf "%s ## _%s" inst i' in

	 fprintf fmt "%a"

	   (print_static_declare_instance (m, attr, inst) const_locals) (path, m')

       )) m.minstances

let print_static_link_instance fmt (i, (m, _)) =

 fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i

(* Allocation of a node struct:

   - if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct)

*)

let print_static_link_macro fmt (m, _, inst) =

  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in

  fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"

    pp_machine_static_link_name m.mname.node_id

    inst

    (Utils.fprintf_list ~sep:";\\@,"

       (fun fmt v ->

	 fprintf fmt "%s._reg.%s = (%a*) &%s"

	   inst

	   v.var_id

           (fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v

	   v.var_id

       )) array_mem

    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)

    (Utils.fprintf_list ~sep:";\\@,"

       (fun fmt (i',m') ->

	 let path = sprintf "%s ## _%s" inst i' in

	 fprintf fmt "%a;\\@,%s.%s = &%s"

	   print_static_link_instance (path,m')

	   inst

	   i'

	   path

       )) m.minstances

let print_static_alloc_macro fmt (m, attr, inst) =

  fprintf fmt "@[<v>@[<v 2>#define %a(%s, %a%t%s)\\@,%a(%s, %a%t%s);\\@,%a(%s);@]@,@]@."

    pp_machine_static_alloc_name m.mname.node_id

    attr

    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic

    (Utils.pp_final_char_if_non_empty ", " m.mstatic)

    inst

    pp_machine_static_declare_name m.mname.node_id

    attr

    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic

    (Utils.pp_final_char_if_non_empty ", " m.mstatic)

    inst

    pp_machine_static_link_name m.mname.node_id

    inst

(* TODO: ACSL

we do multiple things:

- provide the semantics of the node as a predicate: function step and reset are associated to ACSL predicate

- the node is associated to a refinement contract, wrt its ACSL sem

- if the node is a regular node associated to a contract, print the contract as function contract.

- do not print anything if this is a contract node

*)

let print_machine_alloc_decl fmt m =

  Mod.print_machine_decl_prefix fmt m;

  if fst (get_stateless_status m) then

    begin

    end

  else

    begin

      if !Options.static_mem

      then

	begin

	  (* Static allocation *)

	  let inst = mk_instance m in

	  let attr = mk_attribute m in

	  fprintf fmt "%a@.%a@.%a@."

		  print_static_declare_macro (m, attr, inst)

		  print_static_link_macro (m, attr, inst)

		  print_static_alloc_macro (m, attr, inst)

	end

	begin 

          (* Dynamic allocation *)

	  fprintf fmt "extern %a;@.@."

	    print_alloc_prototype (m.mname.node_id, m.mstatic);

	  fprintf fmt "extern %a;@.@."

	    print_dealloc_prototype m.mname.node_id

	end

    end

let print_machine_decl_from_header fmt inode =

  (*Mod.print_machine_decl_prefix fmt m;*)

  if inode.nodei_prototype = Some "C" then

    if inode.nodei_stateless then

      begin

	fprintf fmt "extern %a;@.@."

	  print_stateless_C_prototype

	  (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)

      end

    else (Format.eprintf "internal error: print_machine_decl_from_header"; assert false)

  else

    if inode.nodei_stateless then

    begin

      fprintf fmt "extern %a;@.@."

	print_stateless_prototype 

	(inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)

    end

    else 

      begin

	let static_inputs = List.filter (fun v -> v.var_dec_const) inode.nodei_inputs in

	let used name =

	  (List.exists (fun v -> v.var_id = name) inode.nodei_inputs)

	  || (List.exists (fun v -> v.var_id = name) inode.nodei_outputs) in

	let self = mk_new_name used "self" in

	fprintf fmt "extern %a;@.@."

	  (print_reset_prototype self) (inode.nodei_id, static_inputs);

	fprintf fmt "extern %a;@.@."

	  (print_init_prototype self) (inode.nodei_id, static_inputs);

	fprintf fmt "extern %a;@.@."

	  (print_clear_prototype self) (inode.nodei_id, static_inputs);

	fprintf fmt "extern %a;@.@."

	  (print_step_prototype self)

	  (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)

let print_const_decl fmt cdecl =

  if !Options.mpfr &&  Types.is_real_type (Types.array_base_type cdecl.const_type)

  then

    fprintf fmt "extern %a;@." 

      (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type) 

  else

    fprintf fmt "extern %a;@." 

      (pp_c_type cdecl.const_id) cdecl.const_type

let rec pp_c_struct_type_field filename cpt fmt (label, tdesc) =

   fprintf fmt "%a;" (pp_c_type_decl filename cpt label) tdesc

and pp_c_type_decl filename cpt var fmt tdecl =

  match tdecl with

  | Tydec_any           -> assert false

  | Tydec_int           -> fprintf fmt "int %s" var

  | Tydec_real when !Options.mpfr

                        -> fprintf fmt "%s %s" Mpfr.mpfr_t var

  | Tydec_real          -> fprintf fmt "double %s" var

  (* | Tydec_float         -> fprintf fmt "float %s" var *)

  | Tydec_bool          -> fprintf fmt "_Bool %s" var

  | Tydec_clock ty      -> pp_c_type_decl filename cpt var fmt ty

  | Tydec_const c       -> fprintf fmt "%s %s" c var

  | Tydec_array (d, ty) -> fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d

  | Tydec_enum tl ->

    begin

      fprintf fmt "enum _enum_%s_%d { %a } %s" (protect_filename filename) !cpt (Utils.fprintf_list ~sep:", " pp_print_string) tl var

    end