CristalCaveGem » LustreC

(** Exception for unsupported features in Ada backend **)

(** Print the name of the state variable.

   @param fmt the formater to print on

**)

(** Print the type of the state variable.

   @param fmt the formater to print on

**)

 (** Print the name of the reset procedure

   @param fmt the formater to print on

**)

 (** Print the name of the step procedure

   @param fmt the formater to print on

**)

 (** Print the name of the main procedure.

   @param fmt the formater to print on

**)

 (** Print the name of the arrow package.

   @param fmt the formater to print on

**)

 (** Print the type of a polymorphic type.

   @param fmt the formater to print on

   @param id the id of the polymorphic type

**)

(*TODO Check all this function with unit test, improve this system and

   add support for : "cbrt", "erf", "log10", "pow", "atan2".

*)

  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));

   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));

   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));

   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));

   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));

   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));

   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));

   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));

   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));

   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));

   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));

   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));

   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));

   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));

   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));

   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));

   ("ceil",  ("", "Float'Ceiling"));

   ("floor", ("", "Float'Floor"));

   ("fmod",  ("", "Float'Remainder"));

   ("round", ("", "Float'Rounding"));

   ("trunc", ("", "Float'Truncation"));

   ("fabs", ("", "abs"));]

  List.mem ident Basic_library.internal_funs ||

    List.mem_assoc ident ada_supported_funs

(** Print the name of a package associated to a machine.

   @param fmt the formater to print on

   @param machine the machine

**)

  if is_arrow machine then

      fprintf fmt "%t" pp_arrow_package_name

  else

      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id

(** Print a type.

   @param fmt the formater to print on

   @param type the type

**)

let pp_type fmt typ = 

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

    | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt

    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt

    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt

    | Types.Tunivar                  -> pp_polymorphic_type typ.Types.tid fmt

    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)

    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)

    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)

    | Types.Tarrow _                 -> eprintf "Tarrow@."; assert false (*TODO*)

    | Types.Ttuple l                 -> eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; assert false (*TODO*)

    | Types.Tenum _                  -> eprintf "Tenum@.";  assert false (*TODO*)

    | Types.Tstruct _                -> eprintf "Tstruct@.";assert false (*TODO*)

    | Types.Tarray _                 -> eprintf "Tarray@."; assert false (*TODO*)

    | Types.Tstatic _                -> eprintf "Tstatic@.";assert false (*TODO*)

    | Types.Tlink _                  -> eprintf "Tlink@.";  assert false (*TODO*)

    | Types.Tvar                     -> eprintf "Tvar@.";   assert false (*TODO*)

    (*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)

  )

(** Return a default ada constant for a given type.

   @param cst_typ the constant type

**)

let default_ada_cst cst_typ = match cst_typ with

  | Types.Basic.Tint  -> Const_int 0

  | Types.Basic.Treal -> Const_real Real.zero

  | Types.Basic.Tbool -> Const_tag tag_false

  | _ -> assert false

(** Make a default value from a given type.

   @param typ the type

**)

    | Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ

    | _                              -> assert false (*TODO*)

(** Print the type of a variable.

   @param fmt the formater to print on

   @param id the variable

**)

let pp_var_type fmt id = 

  pp_type fmt id.var_type

(** Print a package name with polymorphic types specified.

   @param substitution correspondance between polymorphic type id and their instantiation

   @param fmt the formater to print on

   @param machine the machine

**)

  assert(List.length polymorphic_types = List.length substitution);

  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)

            polymorphic_types substituion);

  fprintf fmt "%t%t%a"

    (pp_package_name machine)

    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types

(** Print the name of a variable.

   @param fmt the formater to print on

   @param id the variable

**)

let pp_var_name id fmt =

  fprintf fmt "%a" pp_clean_ada_identifier id.var_id

(** Print the complete name of variable.

   @param m the machine to check if it is memory

   @param fmt the formater to print on

   @param var the variable

**)

    | None -> pp_var_name var fmt

    | Some pp_state -> pp_access pp_state (pp_var_name var) fmt

(* TODO: refactor code -> use let rec and for basic pretty printing

   function *)

    @param fmt the formater to use

    @param t the tag to print

 **)

(** Printing function for machine type constants. For the moment,

    arrays are not supported.

    @param fmt the formater to use

    @param c the constant to print

 **)

  | Const_int i                     -> pp_print_int fmt i

  | Const_real r                    -> Real.pp_ada fmt r

  | Const_tag t                     -> pp_ada_tag fmt t

    (Format.eprintf

       "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";

     assert false)

  | _                               ->

    raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not

    support this constant")

(** Printing function for expressions [v1 modulo v2]. Depends

    on option [integer_div_euclidean] to choose between mathematical

    modulo or remainder ([rem] in Ada).

    @param pp_value pretty printer for values

    @param v1 the first value in the expression

    @param v2 the second value in the expression

    @param fmt the formater to print on

 **)

      "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"

      pp_value v1 pp_value v2

      pp_value v1 pp_value v2

      pp_value v2

  else (* Ada behavior for rem *)

(** Printing function for expressions [v1 div v2]. Depends on

    option [integer_div_euclidean] to choose between mathematic

    division or Ada division.

    @param pp_value pretty printer for values

    @param v1 the first value in the expression

    @param v2 the second value in the expression

    @param fmt the formater to print in

 **)

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

      pp_value v1

      (pp_mod pp_value v1 v2)

  else (* Ada behavior for / *)

    @param pp_value pretty printer for values

    @param i a string representing the function

    @param fmt the formater to print on

    @param vl the list of operands

 **)

  | "uminus", [v]    ->

  | "not", [v]       ->

  | "impl", [v1; v2] ->

  | "=", [v1; v2]    ->

  | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt

  | "equi", [v1; v2] ->

  | "xor", [v1; v2]  ->

  | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt

  | "&&", [v1; v2]    ->

  | "||", [v1; v2]    ->

  | "!=", [v1; v2]    ->

  | "ite", [v1; v2; v3]    ->

    Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3

  | op, [v1; v2]     ->

  | _, [v1] when  List.mem_assoc ident ada_supported_funs ->

    let pkg, name = try List.assoc ident ada_supported_funs

      with Not_found -> assert false in

    let pkg = pkg^(if String.equal pkg "" then "" else ".") in

      Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1

  | fun_name, _      ->

    (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)

    @param m the machine to know the state variable

    @param fmt the formater to use

    @param value the value to print. Should be a

           {!type:Machine_code_types.value_t} value

 **)

  | Cst c             -> pp_ada_const fmt c

  | Var var      -> pp_var env fmt var (* Find better to test if it is memory or not *)

  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl

  | _                 ->

    raise (Ada_not_supported

             "unsupported: Ada_backend.adb.pp_value does not support this value type")

(** Print the filename of a machine package.

   @param extension the extension to append to the package name

   @param fmt the formatter

   @param machine the machine corresponding to the package

**)

   @param machine the machine

   @param fmt the formater to print on

   @param substitution correspondance between polymorphic type id and their instantiation

   @param ident the identifier of the subinstance

   @param submachine the submachine of the subinstance

**)

let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) =

  (mode, pp_name, pp_type, with_statement)

(** Print variable declaration for a local state variable

   @param fmt the formater to print on

   @param mode input/output mode of the parameter

**)

  (mode, pp_state_name, pp_state_type, with_statement)

  (mode, pp_name, pp_type, with_statement)

  if m.mstep.step_inputs=[] then [] else

    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]

  if m.mstep.step_outputs=[] then [] else

    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]

  if m.mstatic=[] then [] else

    [List.map (build_pp_var_decl mode with_statement) m.mstatic]

  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])

    @ (build_pp_var_decl_step_input AdaIn None m)

    @ (build_pp_var_decl_step_output AdaOut None m)

  (if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])

    @ (build_pp_var_decl_static AdaIn None m)