/ - Diff - LustreC

       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
-...
         | [] -> ()
         | _ -> 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
-...
     (** 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
-...
       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 *)
-...
       (* 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: *)

          @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.
-...
          @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.

       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)
-...
          @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

     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 ||
-...
     (* 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.
-...
         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 *)
-...
         | 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*)
-...
         (*| _ -> 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
     (** 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
-...
        @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.
-...
       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
-...
         | _                 ->
           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

          @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
-...
           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

Project

General

Profile

CristalCaveGem » LustreC

Revision 61e0c3c4

Added by Guillaume DAVY about 4 years ago