diff --git a/src/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml
index 198807f2ab88ccf34ed0d026ce0e23234658b878..2d0cb4028d3ee9ed7d6ba285c22abcc75ad407f4 100644
--- a/src/backends/Ada/ada_backend.ml
+++ b/src/backends/Ada/ada_backend.ml
@@ -42,14 +42,6 @@ let write_file destname pp_filename pp_file arg =
close_out out
-(** 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
-**)
-let pp_machine_filename extension fmt machine =
- pp_filename extension fmt (function fmt -> pp_package_name fmt machine)
-
(** Exception raised when a machine contains a feature not supported by the
Ada backend*)
exception CheckFailed of string
@@ -64,13 +56,6 @@ let check machine =
| [] -> ()
| _ -> raise (CheckFailed "machine.mconst should be void")
-(** Print the name of the ada project file.
- @param fmt the formater to print on
- @param main_machine the machine associated to the main node
-**)
-let pp_project_name fmt main_machine =
- fprintf fmt "%a.gpr" pp_package_name main_machine
-
let get_typed_submachines machines m =
let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
@@ -83,7 +68,7 @@ let get_typed_submachines machines m =
(** Main function of the Ada backend. It calls all the subfunction creating all
the file and fill them with Ada code representing the machines list given.
- @param basename useless
+ @param basename name of the lustre file
@param prog useless
@param prog list of machines to translate
@param dependencies useless
@@ -98,7 +83,7 @@ let translate_to_ada basename prog machines dependencies =
let _machines = List.combine typed_submachines machines in
- let _pp_filename ext fmt (typed_submachines, machine) =
+ let _pp_filename ext fmt (typed_submachine, machine) =
pp_machine_filename ext fmt machine in
(* Extract the main machine if there is one *)
@@ -126,15 +111,13 @@ let translate_to_ada basename prog machines dependencies =
(* If a main node is given we generate a main adb file and a project file *)
log_str_level_two 1 "Generating wrapper files";
- match main_machine with
- | None -> log_str_level_two 2 "File not generated(no -node argument)";
+ (match main_machine with
+ | None -> ()
| Some machine ->
-begin
- let pp_main_filename fmt _ =
- pp_filename "adb" fmt pp_main_procedure_name in
- write_file destname pp_project_name Wrapper.pp_project_file machine;
- write_file destname pp_main_filename Wrapper.pp_main_adb machine;
-end
+ write_file destname pp_main_filename Wrapper.pp_main_adb machine;
+ write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file machines basename) main_machine);
+ write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
+ write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file machines basename) None;
(* Local Variables: *)
diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
index 44660e0b62af4785fef348d658cc938b0d4aacff..7ba82fa17e1f5c5ad828d9edb70f37c1318a3d45 100644
--- a/src/backends/Ada/ada_backend_adb.ml
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -170,13 +170,14 @@ struct
@param fmt the formater to print on
@param machine the machine
**)
- let pp_step_definition typed_submachines fmt m = pp_procedure_definition
- pp_step_procedure_name
- (pp_step_prototype m)
- (pp_machine_var_decl NoMode)
- (pp_machine_instr typed_submachines m)
- fmt
- (m.mstep.step_locals, m.mstep.step_instrs)
+ let pp_step_definition typed_submachines fmt m =
+ pp_procedure_definition
+ pp_step_procedure_name
+ (pp_step_prototype m)
+ (pp_machine_var_decl NoMode)
+ (pp_machine_instr typed_submachines m)
+ fmt
+ (m.mstep.step_locals, m.mstep.step_instrs)
(** Print the definition of the reset procedure from a machine.
@@ -184,13 +185,18 @@ struct
@param fmt the formater to print on
@param machine the machine
**)
- let pp_reset_definition typed_submachines fmt m = pp_procedure_definition
- pp_reset_procedure_name
- (pp_reset_prototype m)
- (pp_machine_var_decl NoMode)
- (pp_machine_instr typed_submachines m)
- fmt
- ([], m.minit)
+ let pp_reset_definition typed_submachines fmt m =
+ let build_assign = function var ->
+ mkinstr (MStateAssign (var, mk_default_value var.var_type))
+ in
+ let assigns = List.map build_assign m.mmemory in
+ pp_procedure_definition
+ pp_reset_procedure_name
+ (pp_reset_prototype m)
+ (pp_machine_var_decl NoMode)
+ (pp_machine_instr typed_submachines m)
+ fmt
+ ([], assigns@m.minit)
(** Print the package definition(ads) of a machine.
It requires the list of all typed instance.
diff --git a/src/backends/Ada/ada_backend_ads.ml b/src/backends/Ada/ada_backend_ads.ml
index 9a41c9af78c59d3b85a187b03c2b0422747c5627..e5466fd7ec9c7a419c6be67b89feb58f1eb2310b 100644
--- a/src/backends/Ada/ada_backend_ads.ml
+++ b/src/backends/Ada/ada_backend_ads.ml
@@ -106,8 +106,9 @@ struct
let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
match opt_contract with
| None -> pp_prototype fmt
- | Some contract ->
- fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
+ | Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)
+ | Some (Contract contract) ->
+ fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"
pp_prototype
(Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
(Utils.pp_final_char_if_non_empty ",@," contract.assume)
@@ -118,13 +119,11 @@ struct
@param machine the machine
**)
let pp_step_prototype_contract fmt m =
- ()
- (* Temporarily disabled while waiting for the code to stabilize
-pp_procedure_prototype_contract
- (pp_step_prototype m)
- fmt
- m.mspec
- *)
+ pp_procedure_prototype_contract
+ (pp_step_prototype m)
+ fmt
+ m.mspec
+
(** Remove duplicates from a list according to a given predicate.
@param eq the predicate defining equality
diff --git a/src/backends/Ada/ada_backend_common.ml b/src/backends/Ada/ada_backend_common.ml
index 2c6ed9b935a8892ba1170c663b05683588fde10a..037db2dee32d9723daddad7f1f419867159633ae 100644
--- a/src/backends/Ada/ada_backend_common.ml
+++ b/src/backends/Ada/ada_backend_common.ml
@@ -14,10 +14,34 @@ exception Ada_not_supported of string
let is_machine_statefull m = not m.mname.node_dec_stateless
+(*TODO Check all this function with unit test, improve this system and
+ add support for : "cbrt", "erf", "log10", "pow", "atan2".
+*)
let ada_supported_funs =
- [("sin", ("Ada.Numerics.Elementary_Functions", "Sin"));
- ("cos", ("Ada.Numerics.Elementary_Functions", "Cos"));
- ("tan", ("Ada.Numerics.Elementary_Functions", "Tan"))]
+ [("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"));]
let is_builtin_fun ident =
List.mem ident Basic_library.internal_funs ||
@@ -82,27 +106,25 @@ let pp_filename extension fmt pp_name =
(* Package pretty print functions *)
+(** Return true if its the arrow machine
+ @param machine the machine to test
+*)
+let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id
+
(** Print the name of the arrow package.
@param fmt the formater to print on
**)
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
-(** Print the name of a package associated to a node.
- @param fmt the formater to print on
- @param machine the machine
-**)
-let pp_package_name_from_node fmt node =
- if String.equal Arrow.arrow_id node.node_id then
- fprintf fmt "%t" pp_arrow_package_name
- else
- fprintf fmt "%a" pp_clean_ada_identifier node.node_id
-
(** Print the name of a package associated to a machine.
@param fmt the formater to print on
@param machine the machine
**)
let pp_package_name fmt machine =
- pp_package_name_from_node fmt machine.mname
+ 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 the ada package introduction sentence it can be used for body and
declaration. Boolean parameter body should be true if it is a body delcaration.
@@ -177,7 +199,7 @@ let get_machine machines instance =
try
List.find (function m -> m.mname.node_id=id) machines
with
- Not_found -> assert false
+ Not_found -> assert false (*TODO*)
(* Type pretty print functions *)
@@ -246,7 +268,7 @@ let pp_type fmt typ =
| 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 fmt typ.tid
+ | Types.Tunivar -> pp_polymorphic_type fmt typ.Types.tid
| Types.Tbasic _ -> eprintf "Tbasic@."; assert false (*TODO*)
| Types.Tconst _ -> eprintf "Tconst@."; assert false (*TODO*)
| Types.Tclock _ -> eprintf "Tclock@."; assert false (*TODO*)
@@ -261,6 +283,22 @@ let pp_type fmt typ =
(*| _ -> 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 (Num.num_of_int 0, 0, "0.0")
+ | Types.Basic.Tbool -> Const_tag tag_false
+ | _ -> assert false
+
+(** Make a default value from a given type.
+ @param typ the type
+**)
+let mk_default_value typ =
+ match (Types.repr typ).Types.tdesc with
+ | Types.Tbasic t -> mk_val (Cst (default_ada_cst t)) typ
+ | _ -> assert false (*TODO*)
(** Test if two types are the same.
@param typ1 the first type
@@ -472,7 +510,7 @@ let pp_step_prototype m fmt =
@param pp_name name function printer
**)
let pp_reset_prototype m fmt =
- let state_mode = if is_machine_statefull m then Some InOut else None in
+ let state_mode = if is_machine_statefull m then Some Out else None in
pp_base_prototype state_mode m.mstatic [] fmt pp_reset_procedure_name
(** Print the prototype of the init procedure of a machine.
@@ -685,7 +723,8 @@ let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals,
let pp_ada_const fmt c =
match c with
| Const_int i -> pp_print_int fmt i
- | Const_real (c, e, s) -> pp_print_string fmt s
+ | Const_real (c, e, s) ->
+ fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
| Const_tag t -> pp_ada_tag fmt t
| Const_string _ | Const_modeid _ ->
(Format.eprintf
@@ -788,3 +827,14 @@ let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals,
| _ ->
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
+**)
+let pp_machine_filename extension fmt machine =
+ pp_filename extension fmt (function fmt -> pp_package_name fmt machine)
+
+let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
diff --git a/src/backends/Ada/ada_backend_wrapper.ml b/src/backends/Ada/ada_backend_wrapper.ml
index 337ca0c8cff40abe20c3aa778a7cd5fe5dc03202..7609c8a3b71f8759bc25751a92fd9e1e68cf8c4e 100644
--- a/src/backends/Ada/ada_backend_wrapper.ml
+++ b/src/backends/Ada/ada_backend_wrapper.ml
@@ -49,7 +49,7 @@ struct
@param machine the main machine
**)
let pp_main_adb fmt machine =
- let pp_str str fmt = fprintf fmt "%s"str in
+ let pp_str str fmt = fprintf fmt "%s" str in
(* Dependances *)
let text_io = "Ada.Text_IO" in
let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in
@@ -119,14 +119,80 @@ struct
pp_with_machine machine
(pp_main_procedure_definition machine) (locals, instrs)
- (** Print the gpr project file.
+ (** Print the name of the ada project configuration file.
+ @param fmt the formater to print on
+ @param main_machine the machine associated to the main node
+ **)
+ let pp_project_configuration_name fmt basename =
+ fprintf fmt "%s.adc" basename
+
+ (** Print the project configuration file.
@param fmt the formater to print on
@param machine the main machine
**)
- let pp_project_file fmt machine =
- fprintf fmt "project %a is@. for Main use (\"%a\");@.end %a;"
- pp_package_name machine
- (pp_filename "adb") pp_main_procedure_name
- pp_package_name machine
+ let pp_project_configuration_file fmt machine =
+ fprintf fmt "pragma SPARK_Mode (On);"
+
+ (** Print the name of the ada project file.
+ @param base_name name of the lustre file
+ @param fmt the formater to print on
+ @param machine_opt the main machine option
+ **)
+ let pp_project_name basename fmt machine_opt =
+ fprintf fmt "%s.gpr" basename
+
+ let pp_for_single name arg fmt =
+ fprintf fmt "for %s use \"%s\"" name arg
+
+ let pp_for name args fmt =
+ fprintf fmt "for %s use (@[%a@])" name
+ (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
+ args
+
+ let pp_content fmt lines =
+ fprintf fmt " @[<v>%a%t@]"
+ (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
+ (Utils.pp_final_char_if_non_empty ";" lines)
+
+ let pp_package name lines fmt =
+ fprintf fmt "package %s is@,%a@,end %s"
+ name
+ pp_content lines
+ name
+
+ (** Print the gpr project file, if there is a machine in machine_opt then
+ an executable project is made else it is a library.
+ @param fmt the formater to print on
+ @param machine_opt the main machine option
+ **)
+ let pp_project_file machines basename fmt machine_opt =
+ let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
+ @(match machine_opt with
+ | None -> []
+ | Some m -> [asprintf "%a" pp_main_filename m]) in
+ let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
+ fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
+ pp_content
+ ((match machine_opt with
+ | None -> [
+ pp_for_single "Library_Name" basename;
+ pp_for_single "Library_Dir" "lib";
+ ]
+ | Some machine -> [
+ pp_for "Main" [asprintf "%t" pp_main_procedure_name];
+ pp_for_single "Exec_Dir" "bin";
+ ])
+ @[
+ pp_for_single "Object_Dir" "obj";
+ pp_for "Source_Files" adbs;
+ pp_package "Builder" [
+ pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
+ ];
+ pp_package "Prove" [
+ pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
+ ]
+ ])
+ project_name
+
end
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index a6748f3835d13016e218e0c61b2bece107eac0f8..dc0525ca88455cca91fc101c843d9f3aa31aaeb9 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -547,7 +547,7 @@ let translate fmt basename prog machines =
fprintf fmt "\"nodes\": @[<v 0>{@ ";
(* Previous alternative: mapping normalized lustre to EMF:
fprintf_list ~sep:",@ " pp_decl fmt prog; *)
- pp_emf_list pp_machine fmt (List.rev machines);
+ pp_emf_list pp_machine fmt machines;
fprintf fmt "}@]@ }";
fprintf fmt "@]@ }"
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index e816f4b69fdb0762231d7c73e4fe5c12a7274e19..2373c589c7b3b351675bf0fd281f198c1f15806a 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -236,22 +236,23 @@ let pp_tag_id fmt t =
fprintf fmt "%i" (get_idx t const_list)
let pp_cst_type c inf fmt (*infered_typ*) =
+ let pp_basic fmt s = fprintf fmt "{ \"kind\": \"%s\" }" s in
match c with
| Const_tag t ->
let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
if typ.tydef_id = "bool" then
- fprintf fmt "\"bool\""
+ pp_basic fmt "bool"
else
pp_tag_type t typ inf fmt
- | Const_int _ -> fprintf fmt "\"int\"" (*!Options.int_type*)
- | Const_real _ -> fprintf fmt "\"real\"" (*!Options.real_type*)
- | Const_string _ -> fprintf fmt "\"string\""
+ | Const_int _ -> pp_basic fmt "int" (*!Options.int_type*)
+ | Const_real _ -> pp_basic fmt "real" (*!Options.real_type*)
+ | Const_string _ -> pp_basic fmt "string"
| _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
let pp_emf_cst c inf fmt =
- let pp_typ fmt =
- fprintf fmt "\"datatype\": { \"kind\": %t } @ "
+ let pp_typ fmt =
+ fprintf fmt "\"datatype\": %t@ "
(pp_cst_type c inf)
in
match c with