CristalCaveGem » LustreC

open Utils.Format

module type MODIFIERS_SRC = sig

module EmptyMod = struct

module Main = functor (Mod: MODIFIERS_SRC) -> struct

  (********************************************************************************************)

  (*                    Instruction Printing functions                                        *)

  (********************************************************************************************)

  (* Computes the depth to which multi-dimension array assignments should be expanded.

     It equals the maximum number of nested static array constructions accessible from root [v].

  *)

    | Const_array cl ->

      1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0

  (* Returns a list of bool values, indicating whether the indices must be static or not *)

    | Fun (_, vl) ->

      List.fold_right

        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []

    | Array vl    ->

      true :: List.fold_right

        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []

    | Access (v, _) ->

      begin match static_loop_profile v with [] -> [] | _ :: q -> q end

    | Power (v, _) -> false :: static_loop_profile v

      Const_array cl ->

      List.fold_right

        (fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))

        cl []

  let rec is_const_index v =

    match v.value_desc with

    | Cst (Const_int _) -> true

    | Fun (_, vl)       -> List.for_all is_const_index vl

    | _                 -> false

  type loop_index = LVar of ident | LInt of int ref | LAcc of value_t

  (* Computes the list of nested loop variables together with their dimension bounds.

     - LInt r stands for loop expansion (no loop variable, but int loop index)

     - LVar v stands for loop variable v

  *)

  let rec mk_loop_variables m ty depth =

    match (Types.repr ty).Types.tdesc, depth with

    | Types.Tarray (d, ty'), 0 ->

      let v = mk_loop_var m () in

      (d, LVar v) :: mk_loop_variables m ty' 0

    | Types.Tarray (d, ty'), _ ->

      let r = ref (-1) in

      (d, LInt r) :: mk_loop_variables m ty' (depth - 1)

    | _, 0 -> []

    | _ -> assert false

  let reorder_loop_variables loop_vars =

    let (int_loops, var_loops) =

      List.partition (function (_, LInt _) -> true | _ -> false) loop_vars

    in

    var_loops @ int_loops

  (* Prints a one loop variable suffix for arrays *)

  let pp_loop_var pp_val fmt lv =

    match snd lv with

    | LVar v -> fprintf fmt "[%s]" v

    | LInt r -> fprintf fmt "[%d]" !r

    | LAcc i -> fprintf fmt "[%a]" pp_val i

  (* Prints a suffix of loop variables for arrays *)

  let pp_suffix pp_val =

    pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)

  (* Prints a value expression [v], with internal function calls only.

     [pp_var] is a printer for variables (typically [pp_c_var_read]),

     but an offset suffix may be added for array variables

  *)

  (* Prints a constant value before a suffix (needs casting) *)

  let rec pp_c_const_suffix var_type fmt c =

    match c with

    | Const_int i ->

      pp_print_int fmt i

    | Const_real r ->

      Real.pp fmt r

    | Const_tag t ->

      pp_c_tag fmt t

    | Const_array ca ->

      let var_type = Types.array_element_type var_type in

      fprintf fmt "(%a[])%a"

        (pp_c_type "") var_type

        (pp_print_braced (pp_c_const_suffix var_type)) ca

    | Const_struct fl ->

      pp_print_braced

        (fun fmt (f, c) ->

           (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)

        fmt fl

    | Const_string _

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

  (* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)

  let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =

    (*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)

    let pp_suffix = pp_suffix (pp_value_suffix m self var_type [] pp_var) in

      let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in

      pp_value_suffix m self var_type ((x, LInt r)::q) pp_var fmt value

      let var_type = Types.array_element_type var_type in

      pp_value_suffix m self var_type q pp_var fmt

        (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)

    | (_, LInt r) :: q, Array vl ->

      let var_type = Types.array_element_type var_type in

      pp_value_suffix m self var_type q pp_var fmt (List.nth vl !r)

    | loop_var :: q, Array vl      ->

      let var_type = Types.array_element_type var_type in

      fprintf fmt "(%a[])%a%a"

        (pp_c_type "") var_type

        (pp_print_braced (pp_value_suffix m self var_type q pp_var)) vl

        pp_suffix [loop_var]

    | [], Array vl      ->

      let var_type = Types.array_element_type var_type in

      fprintf fmt "(%a[])%a"

        (pp_c_type "") var_type

        (pp_print_braced (pp_value_suffix m self var_type [] pp_var)) vl

    | _ :: q, Power (v, _)  ->

      pp_value_suffix m self var_type q pp_var fmt v

    | _, Fun (n, vl)   ->

      pp_basic_lib_fun (Types.is_int_type value.value_type) n

        (pp_value_suffix m self var_type loop_vars pp_var) fmt vl

    | _, Access (v, i) ->

      let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in

      pp_value_suffix m self var_type

        ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v

    | _, Var v ->

      if 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

        then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars

        else fprintf fmt "%s->_reg.%a%a" self pp_var v pp_suffix loop_vars

      else

        fprintf fmt "%a%a" pp_var v pp_suffix loop_vars

    | _, Cst cst ->

      pp_c_const_suffix var_type fmt cst

    | _, _ ->

      eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."

        Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;

      assert false

  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution

     which may yield constant arrays in expressions.

     Type is needed to correctly print constant arrays.

  *)

  let pp_c_val m self pp_var fmt v =

    pp_value_suffix m self v.value_type [] pp_var fmt v

  let pp_basic_assign pp_var fmt typ var_name value =

    if Types.is_real_type typ && !Options.mpfr

    then

      Mpfr.pp_inject_assign pp_var fmt (var_name, value)

    else

      fprintf fmt "%a = %a;"

        pp_var var_name

        pp_var value

  (* type_directed assignment: array vs. statically sized type

     - [var_type]: type of variable to be assigned

     - [var_name]: name of variable to be assigned

     - [value]: assigned value

     - [pp_var]: printer for variables

  *)

  let pp_assign m self pp_var fmt var_type var_name value =

    let depth = expansion_depth value in

    (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)

    let loop_vars = mk_loop_variables m var_type depth in

    let reordered_loop_vars = reorder_loop_variables loop_vars in

    let rec aux typ fmt vars =

      match vars with

      | [] ->

        pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)

          fmt typ var_name value

      | (d, LVar i) :: q ->

        let typ' = Types.array_element_type typ in

        (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)

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

          i i i pp_c_dimension d i

          (aux typ') q

      | (d, LInt r) :: q ->

        (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)

        let typ' = Types.array_element_type typ in

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

        fprintf fmt "@[<v 2>{@,%a@]@,}"

          (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl

      | _ -> assert false

    in

    begin

      reset_loop_counter ();

      (*reset_addr_counter ();*)

      aux var_type fmt reordered_loop_vars;

      (*eprintf "end pp_assign@.";*)

    end

  let pp_machine_ pp_machine_name fn_name m self fmt inst =

    let (node, static) = try List.assoc inst m.minstances with Not_found ->

      eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;

      raise Not_found

    in

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

      pp_machine_name (node_name node)

      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma

         Dimension.pp_dimension) static

      self inst

  let pp_machine_reset =

    pp_machine_ pp_machine_reset_name "pp_machine_reset"

  let pp_machine_init =

    pp_machine_ pp_machine_init_name "pp_machine_init"

  let pp_machine_clear =

    pp_machine_ pp_machine_clear_name "pp_machine_clear"

  let has_c_prototype funname dependencies =

    (* We select the last imported node with the name funname.

       The order of evaluation of dependencies should be

       compatible with overloading. (Not checked yet) *)

    let imported_node_opt =

      List.fold_left

        (fun res dep ->

           match res with

           | Some _ -> res

           | None ->

             let decls = dep.content in

             let matched = fun t -> match t.top_decl_desc with

               | ImportedNode nd -> nd.nodei_id = funname

               | _ -> false

             in

             if List.exists matched decls then

               match (List.find matched decls).top_decl_desc with

               | ImportedNode nd -> Some nd

               | _ -> assert false

             else

               None) None dependencies in

    match imported_node_opt with

    | None -> false

    | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)

  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%a%s->%s);"

        pp_machine_step_name (node_name n)

        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma

           (pp_c_val m self pp_read)) inputs

        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma

           pp_write) outputs

        self

        i

    with Not_found -> (* stateless node instance *)

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

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

        pp_machine_step_name (node_name n)

        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma

           (pp_c_val m self pp_read)) inputs

        (pp_print_list ~pp_sep:pp_print_comma pp_write) outputs

  let pp_basic_instance_call m self =

    pp_call m self (pp_c_var_read m) (pp_c_var_write m)

  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 =

      fprintf fmt "%a%a"

        pp_var var

        (pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))

        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

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

  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =

    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"

      (pp_c_val m self (pp_c_var_read m)) c

      (pp_print_list ~pp_prologue:pp_print_cut

         (pp_machine_instr dependencies m self)) tl

      (pp_print_list ~pp_prologue:pp_print_cut

         (pp_machine_instr dependencies m self)) el

  and pp_machine_instr dependencies (m: machine_t) self fmt instr =

    match get_instr_desc instr with

    | MNoReset _ -> ()

    | MReset i ->

      pp_machine_reset m self fmt i

    | MLocalAssign (i,v) ->

      pp_assign

        m self (pp_c_var_read m) fmt

        i.var_type (mk_val (Var i) i.var_type) v

    | MStateAssign (i,v) ->

      pp_assign

        m self (pp_c_var_read m) fmt

        i.var_type (mk_val (Var i) i.var_type) v

    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->

      pp_machine_instr dependencies m self fmt

        (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))

    | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->

      pp_instance_call m self fmt i vl il

    | MStep ([i0], i, vl) when has_c_prototype i dependencies ->

      fprintf fmt "%a = %s%a;"

        (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)

        i

        (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl

    | MStep (il, i, vl) ->

      pp_basic_instance_call m self fmt i vl il

    | MBranch (_, []) ->

      eprintf "internal error: C_backend_src.pp_machine_instr %a@."

        (pp_instr m) instr;

      assert false

    | MBranch (g, hl) ->

      if let t = fst (List.hd hl) in t = tag_true || t = tag_false

      then (* boolean case, needs special treatment in C because truth value is not unique *)

        (* may disappear if we optimize code by replacing last branch test with default *)

        let tl = try List.assoc tag_true  hl with Not_found -> [] in

        let el = try List.assoc tag_false hl with Not_found -> [] in

        pp_conditional dependencies m self fmt g tl el

      else (* enum type case *)

        (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)

        fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"

          (pp_c_val m self (pp_c_var_read m)) g

          (pp_print_list ~pp_open_box:pp_open_vbox0

             (pp_machine_branch dependencies m self)) hl

    | MSpec s ->

      fprintf fmt "@[/*@@ %s */@]@ " s

    | MComment s  ->

      fprintf fmt "/*%s*/@ " s

  and pp_machine_branch dependencies m self fmt (t, h) =

    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"

      pp_c_tag t

      (pp_print_list ~pp_open_box:pp_open_vbox0

         (pp_machine_instr dependencies m self)) h

  (********************************************************************************************)

  (*                         C file Printing functions                                        *)

  (********************************************************************************************)

  let print_const_def fmt tdecl =

    let cdecl = const_of_top tdecl in

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

    then

      fprintf fmt "%a;"

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

      fprintf fmt "%a = %a;"

        (pp_c_type cdecl.const_id) cdecl.const_type

        pp_c_const cdecl.const_value

  let print_alloc_instance fmt (i, (m, static)) =

    fprintf fmt "_alloc->%s = %a %a;"

      pp_machine_alloc_name (node_name m)

      (pp_print_parenthesized Dimension.pp_dimension) static

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

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

      pp_machine_dealloc_name (node_name m)

      i

  let const_locals m =

    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals

  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

  let print_alloc_const fmt m =

    pp_print_list

      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")

      (pp_c_decl_local_var m) fmt (const_locals m)

  let print_alloc_array fmt vdecl =

    let base_type = Types.array_base_type vdecl.var_type in

    let size_types = Types.array_type_multi_dimension vdecl.var_type in

    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in

    fprintf fmt

      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\

       assert(_alloc->%s);"

      vdecl.var_id

      (pp_c_type "") base_type

      Dimension.pp_dimension size_type

      (pp_c_type "") base_type

      vdecl.var_id

  let print_dealloc_array fmt vdecl =

    fprintf fmt "free (_alloc->_reg.%s);"

      vdecl.var_id

  let array_mems m =

    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory

  let print_alloc_code fmt m =

    fprintf fmt

      "%a *_alloc;@,\

       _alloc = (%a *) malloc(sizeof(%a));@,\

       assert(_alloc);@,\

       %a%areturn _alloc;"

      pp_machine_memtype_name m.mname.node_id

      pp_machine_memtype_name m.mname.node_id

      pp_machine_memtype_name m.mname.node_id

      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)

      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances

  let print_dealloc_code fmt m =

    fprintf fmt

      "%a%afree (_alloc);@,\

       return;"

      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)

      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances

  (* let print_stateless_init_code fmt m self =

   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in

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

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

   *     (print_init_prototype self) (m.mname.node_id, m.mstatic)

   *     (\* array mems *\)

   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems

   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)

   *     (\* memory initialization *\)

   *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory

   *     (Utils.pp_newline_if_non_empty m.mmemory)

   *     (\* sub-machines initialization *\)

   *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit

   *     (Utils.pp_newline_if_non_empty m.minit)

   *

   * let print_stateless_clear_code fmt m self =

   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in

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

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

   *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)

   *     (\* array mems *\)

   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems

   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)

   *     (\* memory clear *\)

   *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory

   *     (Utils.pp_newline_if_non_empty m.mmemory)

   *     (\* sub-machines clear*\)

   *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit

   *     (Utils.pp_newline_if_non_empty m.minit) *)

  let pp_c_check m self 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

  let pp_print_function

      ~pp_prototype ~prototype

      ?(pp_local=pp_print_nothing) ?(base_locals=[])

      ?(pp_array_mem=pp_print_nothing) ?(array_mems=[])

      ?(pp_init_mpfr_local=pp_print_nothing)

      ?(pp_clear_mpfr_local=pp_print_nothing)

      ?(mpfr_locals=[])

      ?(pp_check=pp_print_nothing) ?(checks=[])

      ?(pp_extra=pp_print_nothing)

      ?(pp_instr=pp_print_nothing) ?(instrs=[])

      fmt =

    fprintf fmt

      "@[<v 2>%a {@,\

       %a%a\

       %a%a%a%a%areturn;@]@,\

       }"

      pp_prototype prototype

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_sep:pp_print_semicolon

         ~pp_eol:pp_print_semicolon

         pp_local)

      base_locals

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_sep:pp_print_semicolon

         ~pp_eol:pp_print_semicolon

         pp_array_mem)

      array_mems

      (pp_print_list

         ~pp_epilogue:pp_print_cut

         pp_init_mpfr_local) (mpfr_vars mpfr_locals)

      (pp_print_list pp_check) checks

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_epilogue:pp_print_cut

         pp_instr) instrs

      (pp_print_list

         ~pp_epilogue:pp_print_cut

         pp_clear_mpfr_local) (mpfr_vars mpfr_locals)

      (* extra *)

      pp_extra ()

  let node_of_machine m = {

    top_decl_desc = Node m.mname;

    top_decl_loc = Location.dummy_loc;

    top_decl_owner = "";

    top_decl_itf = false

  }

  let print_stateless_code dependencies fmt m =

    let self = "__ERROR__" in

    if not (!Options.ansi && is_generic_node (node_of_machine m))

    then

      (* C99 code *)

      pp_print_function

        ~pp_prototype:print_stateless_prototype

        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)

        ~pp_local:(pp_c_decl_local_var m)

        ~base_locals:m.mstep.step_locals

        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))

        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))

        ~mpfr_locals:m.mstep.step_locals

        ~pp_check:(pp_c_check m self)

        ~checks:m.mstep.step_checks

        ~pp_instr:(pp_machine_instr dependencies m self)

        ~instrs:m.mstep.step_instrs

        fmt

    else

      (* C90 code *)

      let gen_locals, base_locals = List.partition (fun v ->

          Types.is_generic_type v.var_type) m.mstep.step_locals in

      let gen_calls = List.map (fun e ->

          let (id, _, _) = call_of_expr e

          in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in

      pp_print_function

        ~pp_prototype:print_stateless_prototype

        ~prototype:(m.mname.node_id,

                    m.mstep.step_inputs @ gen_locals @ gen_calls,

                    m.mstep.step_outputs)

        ~pp_local:(pp_c_decl_local_var m)

        ~base_locals

        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))

        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))

        ~mpfr_locals:m.mstep.step_locals

        ~pp_check:(pp_c_check m self)

        ~checks:m.mstep.step_checks

        ~pp_instr:(pp_machine_instr dependencies m self)

        ~instrs:m.mstep.step_instrs

        fmt

  let print_reset_code dependencies self fmt m =

    pp_print_function

      ~pp_prototype:(print_reset_prototype self)

      ~prototype:(m.mname.node_id, m.mstatic)

      ~pp_local:(pp_c_decl_local_var m)

      ~base_locals:(const_locals m)

      ~pp_instr:(pp_machine_instr dependencies m self)

      ~instrs:m.minit

      fmt

  let print_init_code self fmt m =

    let minit = List.map (fun i ->

        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in

    pp_print_function

      ~pp_prototype:(print_init_prototype self)

      ~prototype:(m.mname.node_id, m.mstatic)

      ~pp_array_mem:(pp_c_decl_array_mem self)

      ~array_mems:(array_mems m)

      ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))

      ~mpfr_locals:m.mmemory

      ~pp_extra:(fun fmt () ->

          pp_print_list

            ~pp_open_box:pp_open_vbox0

            ~pp_epilogue:pp_print_cut

            (pp_machine_init m self)

            fmt minit)

      fmt

  let print_clear_code self fmt m =

    let minit = List.map (fun i ->

        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in

    pp_print_function

      ~pp_prototype:(print_clear_prototype self)

      ~prototype:(m.mname.node_id, m.mstatic)

      ~pp_array_mem:(pp_c_decl_array_mem self)

      ~array_mems:(array_mems m)

      ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))

      ~mpfr_locals:m.mmemory

      ~pp_extra:(fun fmt () ->

          pp_print_list

            ~pp_open_box:pp_open_vbox0

            ~pp_epilogue:pp_print_cut

            (pp_machine_clear m self)

            fmt minit)

      fmt

  let print_step_code dependencies self fmt m =

    if not (!Options.ansi && is_generic_node (node_of_machine m))

    then

      (* C99 code *)

      pp_print_function

        ~pp_prototype:(print_step_prototype self)

        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)

        ~pp_local:(pp_c_decl_local_var m)

        ~base_locals:m.mstep.step_locals

        ~pp_array_mem:(pp_c_decl_array_mem self)

        ~array_mems:(array_mems m)

        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))

        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))

        ~mpfr_locals:m.mstep.step_locals

        ~pp_check:(pp_c_check m self)

        ~checks:m.mstep.step_checks

        ~pp_instr:(pp_machine_instr dependencies m self)

        ~instrs:m.mstep.step_instrs

        fmt

    else

      (* C90 code *)

      let gen_locals, base_locals = List.partition (fun v ->

          Types.is_generic_type v.var_type) m.mstep.step_locals in

      let gen_calls = List.map (fun e ->

          let id, _, _ = call_of_expr e in

          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in

      pp_print_function

        ~pp_prototype:(print_step_prototype self)

        ~prototype:(m.mname.node_id,

                    m.mstep.step_inputs @ gen_locals @ gen_calls,

                    m.mstep.step_outputs)

        ~pp_local:(pp_c_decl_local_var m)

        ~base_locals

        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))

        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))

        ~mpfr_locals:m.mstep.step_locals

        ~pp_check:(pp_c_check m self)

        ~checks:m.mstep.step_checks

        ~pp_instr:(pp_machine_instr dependencies m self)

        ~instrs:m.mstep.step_instrs

        fmt

  (********************************************************************************************)

  (*                     MAIN C file Printing functions                                       *)

  (********************************************************************************************)

  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

        pp_print_list

          (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt 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

        fprintf fmt "%a@,%a"

          (Mpfr.pp_inject_init pp_var_suffix) var

          (Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value)

    in

    reset_loop_counter ();

    aux [] const.const_value fmt const.const_type

  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

    reset_loop_counter ();

    aux [] fmt var.var_type

  let print_import_init fmt dep =

    let baseNAME = file_to_module_name dep.name in

    fprintf fmt "%a();" pp_global_init_name baseNAME

  let print_import_clear fmt dep =

    let baseNAME = file_to_module_name dep.name in

    fprintf fmt "%a();" pp_global_clear_name baseNAME

  let print_global_init_code fmt (basename, prog, dependencies) =

    let baseNAME = file_to_module_name basename in

    let constants = List.map const_of_top (get_consts prog) in

    fprintf fmt

      "@[<v 2>%a {@,\

       static %s init = 0;@,\

       @[<v 2>if (!init) { @,\

       init = 1;%a%a@]@,\

       }@,\

       return;@]@,\

       }"

      print_global_init_prototype baseNAME

      (pp_c_basic_type_desc Type_predef.type_bool)

      (* constants *)

      (pp_print_list

         ~pp_prologue:pp_print_cut

         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))

      (mpfr_consts constants)

      (* dependencies initialization *)

      (pp_print_list

         ~pp_prologue:pp_print_cut

         print_import_init) (List.filter (fun dep -> dep.local) dependencies)

  let print_global_clear_code fmt (basename, prog, dependencies) =

    let baseNAME = file_to_module_name basename in

    let constants = List.map const_of_top (get_consts prog) in

    fprintf fmt

      "@[<v 2>%a {@,\

       static %s clear = 0;@,\

       @[<v 2>if (!clear) { @,\

       clear = 1;%a%a@]@,\

       }@,\

       return;@]@,\

       }"

      print_global_clear_prototype baseNAME

      (pp_c_basic_type_desc Type_predef.type_bool)

      (* constants *)

      (pp_print_list

         ~pp_prologue:pp_print_cut

         (pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants)

      (* dependencies initialization *)

      (pp_print_list

         ~pp_prologue:pp_print_cut

         print_import_clear) (List.filter (fun dep -> dep.local) dependencies)

  let print_alloc_function fmt m =

    if (not !Options.static_mem) then

      (* Alloc functions, only if non static mode *)

      fprintf fmt

        "@[<v 2>%a {@,\

         %a%a@]@,\

         }@,\

         @[<v 2>%a {@,\

         %a%a@]@,\

         @,"

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

        print_alloc_const m

        print_alloc_code m

        print_dealloc_prototype m.mname.node_id

        print_alloc_const m

        print_dealloc_code m

  let print_mpfr_code self fmt m =

    if !Options.mpfr then

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

        (* Init function *)

        (print_init_code self) m

        (* Clear function *)

        (print_clear_code self) m

  (* TODO: ACSL

     - a contract machine shall not be directly printed in the C source

     - but a regular machine associated to a contract machine shall integrate

       the associated statements, updating its memories, at the end of the

       function body.

     - last one may print intermediate comment/acsl if/when they are present in

       the sequence of instruction

  *)

  let print_machine dependencies fmt m =

    if fst (get_stateless_status m) then

    else

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

        print_alloc_function m

        (* Reset function *)

        (print_reset_code dependencies self) m

        (* Step function *)

        (print_step_code dependencies self) m

        (print_mpfr_code self) m

  let print_import_standard source_fmt () =

    fprintf source_fmt

      "@[<v>#include <assert.h>@,%a%a%a@]"

      (if Machine_types.has_machine_type ()

       then pp_print_endcut "#include <stdint.h>"

       else pp_print_nothing) ()

      (if not !Options.static_mem

       then pp_print_endcut "#include <stdlib.h>"

       else pp_print_nothing) ()

      (if !Options.mpfr

       then pp_print_endcut "#include <mpfr.h>"

       else pp_print_nothing) ()

  let print_extern_alloc_prototype fmt ind =

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

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

      print_alloc_prototype (ind.nodei_id, static)

      print_dealloc_prototype ind.nodei_id

  let print_lib_c source_fmt basename prog machines dependencies =

    fprintf source_fmt

      "@[<v>\

       %a\

       %a@,\

       @,\

       %a@,\

       %a\

       %a\

       %a\

       %a\

       %a\

       %a\

       @]@."

      print_import_standard ()

      print_import_prototype

      {

        local = true;

        name = basename;

        content = [];

        is_stateful=true (* assuming it is stateful *);

      }

      (* Print the svn version number and the supported C standard (C90 or C99) *)

      pp_print_version ()

      (* Print dependencies *)

      (pp_print_list

         ~pp_open_box:pp_open_vbox0