reformatting

.ocamlformat

+version=0.18.0
+parens-tuple=multi-line-only
+wrap-comments=true
+cases-exp-indent=2
+break-cases=nested

dune

 ; too bad dune does not support glob in install stanza
 ; (see https://discuss.ocaml.org/t/installing-many-files-with-dune/4143)
 ; TODO: open an issue?
+
 (install
- (section (site (lustrec include_)))
+ (section
+  (site
+   (lustrec include_)))
  (files
-   include/conv.c
-   include/conv.lusi
-   include/conv.lusic
-   include/mpfr_lustre.c
-   include/mpfr_lustre.lusi
-   include/mpfr_lustre.lusic
-   include/mpfr_lustre.h
-   include/simulink_math_fcn.c
-   include/simulink_math_fcn.lusi
-   include/simulink_math_fcn.lusic
-   include/simulink_math_fcn.h
-   include/lustrec_math.lusi
-   include/lustrec_math.lusic
-   include/lustrec_math.h
-   include/arrow.c
-   include/arrow.h
-   include/arrow_spec.h
-   include/arrow_spec.c
-   include/arrow.cpp
-   include/arrow.hpp
-   include/io_frontend.c
-   include/io_frontend.h
-   include/io_frontend.hpp
-   include/lustrec_math.smt2
-   include/StdIn.java))
+  include/conv.c
+  include/conv.lusi
+  include/conv.lusic
+  include/mpfr_lustre.c
+  include/mpfr_lustre.lusi
+  include/mpfr_lustre.lusic
+  include/mpfr_lustre.h
+  include/simulink_math_fcn.c
+  include/simulink_math_fcn.lusi
+  include/simulink_math_fcn.lusic
+  include/simulink_math_fcn.h
+  include/lustrec_math.lusi
+  include/lustrec_math.lusic
+  include/lustrec_math.h
+  include/arrow.c
+  include/arrow.h
+  include/arrow_spec.h
+  include/arrow_spec.c
+  include/arrow.cpp
+  include/arrow.hpp
+  include/io_frontend.c
+  include/io_frontend.h
+  include/io_frontend.hpp
+  include/lustrec_math.smt2
+  include/StdIn.java))
 
 (install
- (section (site (lustrec testgen)))
- (files
-   share/FindLustre.cmake
-   share/helpful_functions.cmake))
+ (section
+  (site
+   (lustrec testgen)))
+ (files share/FindLustre.cmake share/helpful_functions.cmake))
 
 (rule
  (alias runtest)
- (deps (source_tree tests/regression_tests))
- (action (chdir tests/regression_tests
-          (progn
-           (run cmake "-DSUBPROJ=\"unstable\"" "-DLUSTRE_INCLUDE_DIR=%{project_root}/include" .)
-           (run ctest -D Experimental -R "COMPIL_LUS|MAKE|BIN|DIFF" -E LUSTRET --progress)))))
+ (deps
+  (source_tree tests/regression_tests))
+ (action
+  (chdir
+   tests/regression_tests
+   (progn
+    (run
+     cmake
+     "-DSUBPROJ=\"unstable\""
+     "-DLUSTRE_INCLUDE_DIR=%{project_root}/include"
+     .)
+    (run
+     ctest
+     -D
+     Experimental
+     -R
+     "COMPIL_LUS|MAKE|BIN|DIFF"
+     -E
+     LUSTRET
+     --progress)))))

include/dune

@@ -4,20 +4,24 @@
 
 (rule
  (target conv.lusic)
- (action (run lustrec -verbose 0 -I . -d . %{dep:conv.lusi}))
+ (action
+  (run lustrec -verbose 0 -I . -d . %{dep:conv.lusi}))
  (alias install))
 
 (rule
  (targets simulink_math_fcn.lusic simulink_math_fcn.h)
- (action (run lustrec -verbose 0 -I . -d . %{dep:simulink_math_fcn.lusi}))
+ (action
+  (run lustrec -verbose 0 -I . -d . %{dep:simulink_math_fcn.lusi}))
  (alias install))
 
 (rule
  (targets lustrec_math.lusic lustrec_math.h)
- (action (run lustrec -verbose 0 -I . -d . %{dep:lustrec_math.lusi}))
+ (action
+  (run lustrec -verbose 0 -I . -d . %{dep:lustrec_math.lusi}))
  (alias install))
 
 (rule
  (targets mpfr_lustre.lusic mpfr_lustre.h)
- (action (run lustrec -verbose 0 -mpfr 1 -d . %{dep:mpfr_lustre.lusi}))
+ (action
+  (run lustrec -verbose 0 -mpfr 1 -d . %{dep:mpfr_lustre.lusi}))
  (alias install))

src/annotations.ml

@@ -11,12 +11,14 @@
 
 open Lustre_types
 
-
 (* Associate to each annotation key the pair (node, expr tag) *)
-let expr_annotations : (string list, ident * tag) Hashtbl.t=  Hashtbl.create 13
-let node_annotations : (string list, ident) Hashtbl.t=  Hashtbl.create 13
+let expr_annotations : (string list, ident * tag) Hashtbl.t = Hashtbl.create 13
+
+let node_annotations : (string list, ident) Hashtbl.t = Hashtbl.create 13
+
+let add_expr_ann node_id expr_tag key =
+  Hashtbl.add expr_annotations key (node_id, expr_tag)
 
-let add_expr_ann node_id expr_tag key = Hashtbl.add expr_annotations key (node_id, expr_tag)
 let add_node_ann node_id key = Hashtbl.add node_annotations key node_id
 
 let get_expr_annotations key = Hashtbl.find_all expr_annotations key

src/arrow.ml

@@ -9,27 +9,30 @@ let arrow_desc =
     node_id = arrow_id;
     node_type = Type_predef.type_bin_poly_op;
     node_clock = Clock_predef.ck_bin_univ;
-    node_inputs= [Corelang.dummy_var_decl "_in1" arrow_typ; Corelang.dummy_var_decl "_in2" arrow_typ];
-    node_outputs= [Corelang.dummy_var_decl "_out" arrow_typ];
-    node_locals= [];
+    node_inputs =
+      [
+        Corelang.dummy_var_decl "_in1" arrow_typ;
+        Corelang.dummy_var_decl "_in2" arrow_typ;
+      ];
+    node_outputs = [ Corelang.dummy_var_decl "_out" arrow_typ ];
+    node_locals = [];
     node_gencalls = [];
     node_checks = [];
     node_asserts = [];
-    node_stmts= [];
+    node_stmts = [];
     node_dec_stateless = false;
     node_stateless = Some false;
     node_spec = None;
     node_annot = [];
     node_iscontract = false;
-}
+  }
 
 let arrow_top_decl () =
   {
     top_decl_desc = Node arrow_desc;
-    top_decl_owner = (Options_management.core_dependency "arrow");
+    top_decl_owner = Options_management.core_dependency "arrow";
     top_decl_itf = false;
-    top_decl_loc = Location.dummy_loc
+    top_decl_loc = Location.dummy_loc;
   }
 
-let td_is_arrow td =
-  Corelang.node_name td = arrow_id
+let td_is_arrow td = Corelang.node_name td = arrow_id

src/arrow.mli

-val arrow_id: string
-val arrow_top_decl: unit -> Lustre_types.top_decl
-val arrow_desc: Lustre_types.node_desc
-val td_is_arrow: Lustre_types.top_decl -> bool
+val arrow_id : string
+
+val arrow_top_decl : unit -> Lustre_types.top_decl
+
+val arrow_desc : Lustre_types.node_desc
+
+val td_is_arrow : Lustre_types.top_decl -> bool

src/backends/Ada/ada_backend.ml

@@ -11,131 +11,122 @@
 
 open Format
 open Machine_code_types
-
 open Misc_lustre_function
 open Ada_backend_common
 
 let indent_size = 2
 
-(** Log at level 2 a string message with some indentation.
-   @param indent the indentation level
-   @param info the message
-**)
+(** Log at level 2 a string message with some indentation. @param indent the
+    indentation level @param info the message **)
 let log_str_level_two indent info =
-  let str_indent = String.make (indent*indent_size) ' ' in
+  let str_indent = String.make (indent * indent_size) ' ' in
   let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
   Log.report ~level:2 pp_message;
   Format.pp_print_flush Format.err_formatter ()
 
-(** Write a new file with formatter
-   @param destname folder where the file shoudl be created
-   @param pp_filename function printing the filename
-   @param pp_file function wich pretty print the file
-   @param arg will be given to pp_filename and pp_file
-**)
+(** Write a new file with formatter @param destname folder where the file shoudl
+    be created @param pp_filename function printing the filename @param pp_file
+    function wich pretty print the file @param arg will be given to pp_filename
+    and pp_file **)
 let write_file destname pp_filename pp_file arg =
   let path = asprintf "%s%a" destname pp_filename arg in
   let out = open_out path in
   let fmt = formatter_of_out_channel out in
-  log_str_level_two 2 ("generating "^path);
+  log_str_level_two 2 ("generating " ^ path);
   pp_file fmt arg;
   pp_print_flush fmt ();
   close_out out
 
-
-(** Exception raised when a machine contains a feature not supported by the
-  Ada backend*)
 exception CheckFailed of string
+(** Exception raised when a machine contains a feature not supported by the Ada
+    backend*)
 
-
-(** Check that a machine match the requirement for an Ada compilation :
-      - No constants.
-   @param machine the machine to test
-**)
+(** Check that a machine match the requirement for an Ada compilation : - No
+    constants. @param machine the machine to test **)
 let check machine =
   match machine.mconst with
-    | [] -> ()
-    | _ -> raise (CheckFailed "machine.mconst should be void")
-
+  | [] ->
+    ()
+  | _ ->
+    raise (CheckFailed "machine.mconst should be void")
 
 let get_typed_submachines machines m =
-  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
+  let instances =
+    List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls
+  in
   let submachines = List.map (get_machine machines) instances in
   List.map2
     (fun instance submachine ->
-      let ident = (fst instance) in
+      let ident = fst instance in
       ident, (get_substitution m ident submachine, submachine))
     instances submachines
 
 let extract_contract machines m =
   let rec find_submachine_from_ident ident = function
-    | [] -> raise Not_found
-    | h::_ when h.mname.node_id = ident -> h
-    | _::t -> find_submachine_from_ident ident t
+    | [] ->
+      raise Not_found
+    | h :: _ when h.mname.node_id = ident ->
+      h
+    | _ :: t ->
+      find_submachine_from_ident ident t
   in
   let extract_ident eexpr =
     match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
-      | Expr_ident ident -> ident
-      | _ -> assert false
-      (*
-      | Expr_const cst -> assert false
-      | Expr_tuple exprs -> assert false
-      | Expr_ite (expr1, expr2, expr3) -> assert false
-      | Expr_arrow (expr1, expr2)  -> assert false
-      | Expr_fby (expr1, expr2) -> assert false
-      | Expr_array exprs -> assert false
-      | Expr_access (expr1, dim) -> assert false
-      | Expr_power (expr1, dim) -> assert false
-      | Expr_pre expr -> assert false
-      | Expr_when (expr,ident,label) -> assert false
-      | Expr_merge (ident, l) -> assert false
-      | Expr_appl call -> assert false
-      *)
+    | Expr_ident ident ->
+      ident
+    | _ ->
+      assert false
+    (* | Expr_const cst -> assert false | Expr_tuple exprs -> assert false |
+       Expr_ite (expr1, expr2, expr3) -> assert false | Expr_arrow (expr1,
+       expr2) -> assert false | Expr_fby (expr1, expr2) -> assert false |
+       Expr_array exprs -> assert false | Expr_access (expr1, dim) -> assert
+       false | Expr_power (expr1, dim) -> assert false | Expr_pre expr -> assert
+       false | Expr_when (expr,ident,label) -> assert false | Expr_merge (ident,
+       l) -> assert false | Expr_appl call -> assert false *)
   in
   match m.mspec.mnode_spec with
-    | Some (NodeSpec ident) ->
-      begin
-        let machine_spec = find_submachine_from_ident ident machines in
-        let guarantees =
-          match machine_spec.mspec.mnode_spec with
-            | Some (Contract contract) ->
-                assert (contract.consts=[]);
-                assert (contract.locals=[]);
-                assert (contract.stmts=[]);
-                assert (contract.assume=[]);
-                List.map extract_ident contract.guarantees
-            | _ -> assert false
-        in
-        let opt_machine_spec =
-          match machine_spec.mstep.step_instrs with
-            | [] -> None
-            | _ -> Some machine_spec
-        in
-        (opt_machine_spec, guarantees)
-      end
-    | _ -> None, []
+  | Some (NodeSpec ident) ->
+    let machine_spec = find_submachine_from_ident ident machines in
+    let guarantees =
+      match machine_spec.mspec.mnode_spec with
+      | Some (Contract contract) ->
+        assert (contract.consts = []);
+        assert (contract.locals = []);
+        assert (contract.stmts = []);
+        assert (contract.assume = []);
+        List.map extract_ident contract.guarantees
+      | _ ->
+        assert false
+    in
+    let opt_machine_spec =
+      match machine_spec.mstep.step_instrs with
+      | [] ->
+        None
+      | _ ->
+        Some machine_spec
+    in
+    opt_machine_spec, guarantees
+  | _ ->
+    None, []
 
 (** 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 name of the lustre file
-   @param prog list of machines to translate
-**)
+    the file and fill them with Ada code representing the machines list given.
+    @param basename name of the lustre file @param prog list of machines to
+    translate **)
 let translate_to_ada basename machines =
   let module Ads = Ada_backend_ads.Main in
   let module Adb = Ada_backend_adb.Main in
   let module Wrapper = Ada_backend_wrapper.Main in
-
   let is_real_machine m =
-    match m.mspec.mnode_spec with
-      | Some (Contract _) -> false
-      | _ -> true
+    match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true
   in
 
   let filtered_machines = List.filter is_real_machine machines in
 
   let typed_submachines =
-    List.map (get_typed_submachines machines) filtered_machines in
-  
+    List.map (get_typed_submachines machines) filtered_machines
+  in
+
   let contracts = List.map (extract_contract machines) filtered_machines in
 
   let _machines = List.combine contracts filtered_machines in
@@ -143,19 +134,23 @@ let translate_to_ada basename machines =
   let _machines = List.combine typed_submachines _machines in
 
   let _pp_filename ext fmt (_, (_, machine)) =
-    pp_machine_filename ext fmt machine in
+    pp_machine_filename ext fmt machine
+  in
 
   (* Extract the main machine if there is one *)
-  let main_machine = (match !Options.main_node with
-  | "" -> None
-  | main_node -> (
-    match Machine_code_common.get_machine_opt filtered_machines main_node with
-    | None -> begin
-      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
-      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
-    end
-    | Some m -> Some m
-  )) in
+  let main_machine =
+    match !Options.main_node with
+    | "" ->
+      None
+    | main_node -> (
+      match Machine_code_common.get_machine_opt filtered_machines main_node with
+      | None ->
+        Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg
+          Error.Main_not_found;
+        raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
+      | Some m ->
+        Some m)
+  in
 
   let destname = !Options.dest_dir ^ "/" in
 
@@ -171,25 +166,23 @@ let translate_to_ada basename machines =
   (* 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 -> ()
-    | Some machine ->
-      write_file destname
-        pp_main_filename
-        (Wrapper.pp_main_adb (*get_typed_submachines filtered_machines machine*))
-        machine;
-      write_file destname
-        (fun fmt _ -> Wrapper.pp_project_name (basename^"_exe") fmt)
-        (Wrapper.pp_project_file filtered_machines basename)
-        main_machine);
-  write_file destname
-    Wrapper.pp_project_configuration_name
+  | None ->
+    ()
+  | Some machine ->
+    write_file destname pp_main_filename Wrapper.pp_main_adb
+      (*get_typed_submachines filtered_machines machine*)
+      machine;
+    write_file destname
+      (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_exe") fmt)
+      (Wrapper.pp_project_file filtered_machines basename)
+      main_machine);
+  write_file destname Wrapper.pp_project_configuration_name
     (fun fmt _ -> Wrapper.pp_project_configuration_file fmt)
     basename;
   write_file destname
-    (fun fmt _ -> Wrapper.pp_project_name (basename^"_lib") fmt)
+    (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_lib") fmt)
     (Wrapper.pp_project_file filtered_machines basename)
-    None;
-
+    None
 
 (* Local Variables: *)
 (* compile-command:"make -C ../../.." *)

src/backends/Ada/ada_backend_adb.ml

@@ -10,42 +10,30 @@
 (********************************************************************)
 
 open Format
-
 open Machine_code_types
 open Lustre_types
 open Corelang
 open Machine_code_common
-
 open Misc_printer
 open Misc_lustre_function
 open Ada_printer
 open Ada_backend_common
 
-(** Main module for generating packages bodies
- **)
-module Main =
-struct
-
+(** Main module for generating packages bodies **)
+module Main = struct
   (** Printing function for basic assignement [var := value].
 
-      @param fmt the formater to print on
-      @param var_name the name of the variable
-      @param value the value to be assigned
-   **)
+      @param fmt the formater to print on @param var_name the name of the
+      variable @param value the value to be assigned **)
   let pp_assign env fmt var value =
-    fprintf fmt "%a := %a"
-      (pp_var env) var
-      (pp_value env) value
+    fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
 
-  (** Printing function for instruction. See
-      {!type:Machine_code_types.instr_t} for more details on
-      machine types.
+  (** Printing function for instruction. See {!type:Machine_code_types.instr_t}
+      for more details on machine types.
 
-      @param typed_submachines list of all typed machine instances of this machine
-      @param machine the current machine
-      @param fmt the formater to print on
-      @param instr the instruction to print
-   **)
+      @param typed_submachines list of all typed machine instances of this
+      machine @param machine the current machine @param fmt the formater to
+      print on @param instr the instruction to print **)
   let rec pp_machine_instr typed_submachines env instr fmt =
     let pp_instr = pp_machine_instr typed_submachines env in
     (* Print args for a step call *)
@@ -56,158 +44,175 @@ struct
     in
     (* Print a case *)
     let pp_case fmt (g, hl) =
-      fprintf fmt "case %a is@,%aend case"
-        (pp_value env) g
-        pp_block (List.map pp_when hl)
+      fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block
+        (List.map pp_when hl)
     in
     (* Print a if *)
     (* If neg is true the we must test for the negation of the condition. It
        first check that we don't have a negation and a else case, if so it
-       inverses the two branch and remove the negation doing a recursive
-       call. *)
+       inverses the two branch and remove the negation doing a recursive call. *)
     let pp_if fmt (neg, g, instrs1, instrs2) =
       let pp_cond =
-        if neg then
-          fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
-        else
-          pp_value env
+        if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
+        else pp_value env
       in
-      let pp_else = match instrs2 with
-        | None -> fun fmt -> fprintf fmt ""
-        | Some i2 -> fun fmt ->
-            fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
+      let pp_else =
+        match instrs2 with
+        | None ->
+          fun fmt -> fprintf fmt ""
+        | Some i2 ->
+          fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
       in
-      fprintf fmt "if %a then@,%a%tend if"
-        pp_cond g
-        pp_block (List.map pp_instr instrs1)
+      fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block
+        (List.map pp_instr instrs1)
         pp_else
     in
     match get_instr_desc instr with
-      (* no reset *)
-      | MNoReset _ -> ()
-      (* TODO: handle clear_reset *)
-      | MClearReset -> ()
-      (* reset  *)
-      | MSetReset i when List.mem_assoc i typed_submachines ->
-          let (substitution, submachine) = get_instance i typed_submachines in
-          let pp_package = pp_package_name_with_polymorphic substitution submachine in
-          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
-          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
-      | MLocalAssign (ident, value) ->
-          pp_assign env fmt ident value
-      | MStateAssign (ident, value) ->
-          pp_assign env fmt ident value
-      | MStep ([i0], i, vl) when is_builtin_fun i ->
-          let value = mk_val (Fun (i, vl)) i0.var_type in
-            pp_assign env fmt i0 value
-      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
-          let (substitution, submachine) = get_instance i typed_submachines in
-          let pp_package = pp_package_name_with_polymorphic substitution submachine in
-          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
-          let output = List.map pp_var_name il in
-          let args =
-            (if is_machine_statefull submachine then [[pp_state i]] else [])
-              @(if input!=[] then [input] else [])
-              @(if output!=[] then [output] else [])
-          in
-          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
-      | MBranch (_, []) -> assert false
-      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
-          pp_if fmt (build_if g c1 i1 tl)
-      | MBranch (g, hl) -> pp_case fmt (g, hl)
-      | MComment s  ->
-          let lines = String.split_on_char '\n' s in
-          fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
-      | _ -> assert false
+    (* no reset *)
+    | MNoReset _ ->
+      ()
+    (* TODO: handle clear_reset *)
+    | MClearReset ->
+      ()
+    (* reset *)
+    | MSetReset i when List.mem_assoc i typed_submachines ->
+      let substitution, submachine = get_instance i typed_submachines in
+      let pp_package =
+        pp_package_name_with_polymorphic substitution submachine
+      in
+      let args =
+        if is_machine_statefull submachine then [ [ pp_state i ] ] else []
+      in
+      pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
+    | MLocalAssign (ident, value) ->
+      pp_assign env fmt ident value
+    | MStateAssign (ident, value) ->
+      pp_assign env fmt ident value
+    | MStep ([ i0 ], i, vl) when is_builtin_fun i ->
+      let value = mk_val (Fun (i, vl)) i0.var_type in
+      pp_assign env fmt i0 value
+    | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
+      let substitution, submachine = get_instance i typed_submachines in
+      let pp_package =
+        pp_package_name_with_polymorphic substitution submachine
+      in
+      let input = List.map (fun x fmt -> pp_value env fmt x) vl in
+      let output = List.map pp_var_name il in
+      let args =
+        (if is_machine_statefull submachine then [ [ pp_state i ] ] else [])
+        @ (if input != [] then [ input ] else [])
+        @ if output != [] then [ output ] else []
+      in
+      pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
+    | MBranch (_, []) ->
+      assert false
+    | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
+      pp_if fmt (build_if g c1 i1 tl)
+    | MBranch (g, hl) ->
+      pp_case fmt (g, hl)
+    | MComment s ->
+      let lines = String.split_on_char '\n' s in
+      fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
+    | _ ->
+      assert false
 
   (** Print the definition of the step procedure from a machine.
 
-     @param typed_submachines list of all typed machine instances of this machine
-     @param fmt the formater to print on
-     @param machine the machine
-  **)
+      @param typed_submachines list of all typed machine instances of this
+      machine @param fmt the formater to print on @param machine the machine **)
   let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
-    let transform_local_to_state_assign instr = match instr.instr_desc with
-      | MLocalAssign (ident, value) -> 
+    let transform_local_to_state_assign instr =
+      match instr.instr_desc with
+      | MLocalAssign (ident, value) ->
         { instr with instr_desc = MStateAssign (ident, value) }
-      | _ -> instr
+      | _ ->
+        instr
     in
-    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
-      | None -> [], []
+    let pp_local_ghost_list, spec_instrs =
+      match m_spec_opt with
+      | None ->
+        [], []
       | Some m_spec ->
-          List.map (build_pp_var_decl_local (Some (true, false, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
-          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
+        ( List.map
+            (build_pp_var_decl_local (Some (true, false, [], [])))
+            (List.filter
+               (fun x -> not (List.mem x.var_id guarantees))
+               m_spec.mstep.step_locals),
+          List.map transform_local_to_state_assign m_spec.mstep.step_instrs )
+    in
+    let pp_local_list =
+      List.map (build_pp_var_decl_local None) m.mstep.step_locals
+    in
+    let pp_instr_list =
+      List.map
+        (pp_machine_instr typed_submachines env)
+        (m.mstep.step_instrs @ spec_instrs)
+    in
+    let content =
+      AdaProcedureContent
+        ( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])
+          @ if pp_local_list = [] then [] else [ pp_local_list ]),
+          pp_instr_list )
     in
-    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
-    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
-    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
     pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
 
   (** Print the definition of the reset procedure from a machine.
 
-     @param typed_submachines list of all typed machine instances of this machine
-     @param fmt the formater to print on
-     @param machine the machine
-  **)
+      @param typed_submachines list of all typed machine instances of this
+      machine @param fmt the formater to print on @param machine the machine **)
   let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
-    let build_assign = function var ->
-      mkinstr (MStateAssign (var, mk_default_value var.var_type))
+    let build_assign = function
+      | var ->
+        mkinstr (MStateAssign (var, mk_default_value var.var_type))
     in
-    let env, memory = match m_spec_opt with
-      | None -> env, m.mmemory
-      | Some _ ->
-          env,
-          (m.mmemory)
+    let env, memory =
+      match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory
     in
     let assigns = List.map build_assign memory in
-    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
-    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
+    let pp_instr_list =
+      List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)
+    in
+    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt
+      (AdaProcedureContent ([], pp_instr_list))
 
-  (** Print the package definition(ads) of a machine.
-    It requires the list of all typed instance.
-    A typed submachine instance is (ident, type_machine) with ident
-    the instance name and typed_machine is (substitution, machine) with machine
-    the machine associated to the instance and substitution the instanciation of
-    all its polymorphic types.
-     @param fmt the formater to print on
-     @param typed_submachines list of all typed machine instances of this machine
-     @param m the machine
-  **)
-  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
+  (** Print the package definition(ads) of a machine. It requires the list of
+      all typed instance. A typed submachine instance is (ident, type_machine)
+      with ident the instance name and typed_machine is (substitution, machine)
+      with machine the machine associated to the instance and substitution the
+      instanciation of all its polymorphic types. @param fmt the formater to
+      print on @param typed_submachines list of all typed machine instances of
+      this machine @param m the machine **)
+  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))
+      =
     let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
     let pp_reset fmt =
       if is_machine_statefull machine then
-        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
-      else
-        fprintf fmt ""
+        fprintf fmt "%a;@,@,"
+          (pp_reset_definition env typed_submachines)
+          (machine, opt_spec_machine)
+      else fprintf fmt ""
     in
     let aux pkgs (id, _) =
       try
-        let (pkg, _) = List.assoc id ada_supported_funs in
-        if List.mem pkg pkgs then
-          pkgs
-        else
-          pkg::pkgs
+        let pkg, _ = List.assoc id ada_supported_funs in
+        if List.mem pkg pkgs then pkgs else pkg :: pkgs
       with Not_found -> pkgs
     in
     let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
     let pp_content fmt =
-      fprintf fmt "%t%a"
-        (*Define the reset procedure*)
-        pp_reset
-        
+      fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset
         (*Define the step procedure*)
-        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
+        (pp_step_definition env typed_submachines)
+        (machine, opt_spec_machine, guarantees)
     in
     fprintf fmt "%a%t%a;@."
-      
       (* Include all the required packages*)
-      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
+      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate))
+      packages
       (Utils.pp_final_char_if_non_empty ";@,@," packages)
-      
       (*Print package*)
-      (pp_package (pp_package_name machine) [] true ) pp_content
-
+      (pp_package (pp_package_name machine) [] true)
+      pp_content
 end
 
 (* Local Variables: *)

src/backends/Ada/ada_backend_ads.ml

@@ -10,216 +10,248 @@
 (********************************************************************)
 
 open Format
-
 open Machine_code_types
 open Lustre_types
-
 open Misc_lustre_function
 open Ada_printer
 open Ada_backend_common
 
-
-
 (** Functions printing the .ads file **)
-module Main =
-struct
-
-  let rec init f = function i when i < 0 -> [] | i -> (f i)::(init f (i-1)) (*should be replaced by the init of list from ocaml std lib*)
+module Main = struct
+  let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)
+  (*should be replaced by the init of list from ocaml std lib*)
 
   let suffixOld = "_old"
+
   let suffixNew = "_new"
+
   let pp_invariant_name fmt = fprintf fmt "inv"
+
   let pp_transition_name fmt = fprintf fmt "transition"
+
   let pp_init_name fmt = fprintf fmt "init"
-  let pp_state_name_predicate suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
-  let pp_axiomatize_package_name fmt = fprintf  fmt "axiomatize"
+
+  let pp_state_name_predicate suffix fmt =
+    fprintf fmt "%t%s" pp_state_name suffix
+
+  let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"
 
   (** Print the expression function representing the transition predicate.
-     @param fmt the formater to print on
-  **)
+      @param fmt the formater to print on **)
   let pp_init_predicate fmt () =
-    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
-    pp_predicate pp_init_name [[new_state]] true fmt None
+    let new_state =
+      AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
+    in
+    pp_predicate pp_init_name [ [ new_state ] ] true fmt None
 
   (** Print the expression function representing the transition predicate.
-     @param fmt the formater to print on
-     @param machine the machine
-  **)
+      @param fmt the formater to print on @param machine the machine **)
   let pp_transition_predicate fmt (_, m) =
-    let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in
-    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
+    let old_state =
+      AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None
+    in
+    let new_state =
+      AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
+    in
     let inputs = build_pp_var_decl_step_input AdaIn None m in
     let outputs = build_pp_var_decl_step_output AdaIn None m in
-    pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) true fmt None
+    pp_predicate pp_transition_name
+      ([ [ old_state; new_state ] ] @ inputs @ outputs)
+      true fmt None
 
   let pp_invariant_predicate fmt () =
-    pp_predicate pp_invariant_name [[build_pp_state_decl AdaIn None]] true fmt None
+    pp_predicate pp_invariant_name
+      [ [ build_pp_state_decl AdaIn None ] ]
+      true fmt None
 
-  (** Print a new statement instantiating a generic package.
-     @param fmt the formater to print on
-     @param substitutions the instanciation substitution
-     @param machine the machine to instanciate
-  **)
+  (** Print a new statement instantiating a generic package. @param fmt the
+      formater to print on @param substitutions the instanciation substitution
+      @param machine the machine to instanciate **)
   let pp_new_package fmt (substitutions, machine) =
     let pp_name = pp_package_name machine in
     let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
-    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
+    let instanciations =
+      List.map
+        (fun (id, typ) -> pp_polymorphic_type id, fun fmt -> pp_type fmt typ)
+        substitutions
+    in
     pp_package_instanciation pp_new_name pp_name fmt instanciations
 
-  (** Remove duplicates from a list according to a given predicate.
-     @param eq the predicate defining equality
-     @param l the list to parse
-  **)
+  (** Remove duplicates from a list according to a given predicate. @param eq
+      the predicate defining equality @param l the list to parse **)
   let remove_duplicates eq l =
-    let aux l x = if List.exists (eq x) l then l else x::l in
+    let aux l x = if List.exists (eq x) l then l else x :: l in
     List.fold_left aux [] l
 
-
-  (** Compare two typed machines.
-  **)
+  (** Compare two typed machines. **)
   let eq_typed_machine (subst1, machine1) (subst2, machine2) =
-    (String.equal machine1.mname.node_id machine2.mname.node_id) &&
-    (List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
-
-
-  (** Print the package declaration(ads) of a machine.
-    It requires the list of all typed instance.
-    A typed submachine is a (ident, typed_machine) with
-      - ident: the name 
-      - typed_machine: a (substitution, machine) with
-        - machine: the submachine struct
-        - substitution the instanciation of all its polymorphic types.
-     @param fmt the formater to print on
-     @param typed_submachines list of all typed submachines of this machine
-     @param m the machine
-  **)
+    String.equal machine1.mname.node_id machine2.mname.node_id
+    && List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2
+
+  (** Print the package declaration(ads) of a machine. It requires the list of
+      all typed instance. A typed submachine is a (ident, typed_machine) with -
+      ident: the name - typed_machine: a (substitution, machine) with - machine:
+      the submachine struct - substitution the instanciation of all its
+      polymorphic types. @param fmt the formater to print on @param
+      typed_submachines list of all typed submachines of this machine @param m
+      the machine **)
   let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
     let typed_machines = snd (List.split typed_submachines) in
-    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
-    
-    let machines_to_import = List.map pp_package_name (snd (List.split typed_machines_set)) in
+    let typed_machines_set =
+      remove_duplicates eq_typed_machine typed_machines
+    in
+
+    let machines_to_import =
+      List.map pp_package_name (snd (List.split typed_machines_set))
+    in
 
     let polymorphic_types = find_all_polymorphic_type m in
-    
+
     let typed_machines_to_instanciate =
-      List.filter (fun (l, _) -> l != []) typed_machines_set in
+      List.filter (fun (l, _) -> l != []) typed_machines_set
+    in
 
-    let typed_instances = List.filter is_submachine_statefull typed_submachines in
+    let typed_instances =
+      List.filter is_submachine_statefull typed_submachines
+    in
 
-    let memories = match m_spec_opt with
-      | None -> []
-      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x)) m.mmemory
+    let memories =
+      match m_spec_opt with
+      | None ->
+        []
+      | Some m ->
+        List.map
+          (fun x ->
+            pp_var_decl
+              (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
+          m.mmemory
     in
     let ghost_private = memories in
-    (* Commented since not used. Could be reinjected in the code 
-    let vars_spec = match m_spec_opt with
-      | None -> []
-      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, false, [], []))) (m_spec.mmemory)
-    in *)
+    (* Commented since not used. Could be reinjected in the code let vars_spec =
+       match m_spec_opt with | None -> [] | Some m_spec -> List.map
+       (build_pp_var_decl AdaNoMode (Some (true, false, [], [])))
+       (m_spec.mmemory) in *)
     let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
-    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
+    let states =
+      List.map
+        (build_pp_state_decl_from_subinstance AdaNoMode None)
+        typed_instances
+    in
     let var_lists =
-      (if states = [] then [] else [states]) @
-      (if vars = [] then [] else [vars]) in
-    
+      (if states = [] then [] else [ states ])
+      @ if vars = [] then [] else [ vars ]
+    in
+
     let pp_ifstatefull fmt pp =
-      if is_machine_statefull m then
-        fprintf fmt "%t" pp
-      else
-        fprintf fmt ""
+      if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""
     in
 
     let pp_state_decl_and_reset fmt =
-      let init fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_init_name, [[pp_state_name]]) in
-      let contract = Some (false, false, [], [init]) in
+      let init fmt =
+        pp_call fmt
+          ( pp_access pp_axiomatize_package_name pp_init_name,
+            [ [ pp_state_name ] ] )
+      in
+      let contract = Some (false, false, [], [ init ]) in
       fprintf fmt "%t;@,@,%a;@,@,"
         (*Declare the state type*)
         (pp_type_decl pp_state_type AdaPrivate)
-        
         (*Declare the reset procedure*)
-        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract) AdaNoContent
+        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)
+        AdaNoContent
     in
 
     let pp_private_section fmt =
       fprintf fmt "@,private@,@,%a%t%a%t%a"
-      (*Instantiate the polymorphic type that need to be instantiated*)
-      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
-      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
-      
-      (*Define the state type*)
-      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
-        
-      (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
-      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private
+        (*Instantiate the polymorphic type that need to be instantiated*)
+        (Utils.fprintf_list ~sep:";@," pp_new_package)
+        typed_machines_to_instanciate
+        (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
+        (*Define the state type*)
+        pp_ifstatefull
+        (fun fmt -> pp_record pp_state_type fmt var_lists)
+        (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
+        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
+        ghost_private
     in
 
     let pp_content fmt =
       let pp_contract_opt =
-        let pp_var x fmt =
-            pp_clean_ada_identifier fmt x
-        in
+        let pp_var x fmt = pp_clean_ada_identifier fmt x in
         let guarantee_post_conditions = List.map pp_var guarantees in
         let state_pre_conditions, state_post_conditions =
           if is_machine_statefull m then
-          begin
             let input = List.map pp_var_name m.mstep.step_inputs in
             let output = List.map pp_var_name m.mstep.step_outputs in
             let args =
-              [[pp_old pp_state_name;pp_state_name]]
-                @(if input!=[] then [input] else [])
-                @(if output!=[] then [output] else [])
+              [ [ pp_old pp_state_name; pp_state_name ] ]
+              @ (if input != [] then [ input ] else [])
+              @ if output != [] then [ output ] else []
+            in
+            let transition fmt =
+              pp_call fmt
+                (pp_access pp_axiomatize_package_name pp_transition_name, args)
             in
-            let transition fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_transition_name, args) in
-            let invariant fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_invariant_name, [[pp_state_name]]) in
-            [invariant], [transition;invariant]
-          end
-          else
-            [], []
+            let invariant fmt =
+              pp_call fmt
+                ( pp_access pp_axiomatize_package_name pp_invariant_name,
+                  [ [ pp_state_name ] ] )
+            in
+            [ invariant ], [ transition; invariant ]
+          else [], []
+        in
+        let post_conditions =
+          state_post_conditions @ guarantee_post_conditions
         in
-        let post_conditions = state_post_conditions@guarantee_post_conditions in
         let pre_conditions = state_pre_conditions in
-        if post_conditions = [] && pre_conditions = [] then
-          None
-        else
-          Some (false, false, pre_conditions, post_conditions)
+        if post_conditions = [] && pre_conditions = [] then None
+        else Some (false, false, pre_conditions, post_conditions)
+      in
+      let pp_guarantee name =
+        pp_var_decl
+          ( AdaNoMode,
+            (fun fmt -> pp_clean_ada_identifier fmt name),
+            pp_boolean_type,
+            Some (true, false, [], []) )
       in
-      let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, false, [], []))) in
       let ghost_public = List.map pp_guarantee guarantees in
       fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%t"
-        
-        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_public
+        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
+        ghost_public
         (Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
-        
         pp_ifstatefull pp_state_decl_and_reset
-        
         (*Declare the step procedure*)
-        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
-        
-        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
-        
-        (pp_package (pp_axiomatize_package_name) [] false)
-          (fun fmt -> fprintf fmt "pragma Annotate (GNATProve, External_Axiomatization);@,@,%a;@,%a;@,%a"
+        (pp_procedure pp_step_procedure_name (build_pp_arg_step m)
+           pp_contract_opt)
+        AdaNoContent pp_ifstatefull
+        (fun fmt -> fprintf fmt ";@,")
+        (pp_package pp_axiomatize_package_name [] false)
+        (fun fmt ->
+          fprintf fmt
+            "pragma Annotate (GNATProve, External_Axiomatization);@,\
+             @,\
+             %a;@,\
+             %a;@,\
+             %a"
             (*Declare the init predicate*)
             pp_init_predicate ()
             (*Declare the transition predicate*)
             pp_transition_predicate (m_spec_opt, m)
             (*Declare the invariant predicate*)
             pp_invariant_predicate ())
-        
         (*Print the private section*)
         pp_private_section
     in
-    
+
     let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
     let pp_generics = List.map pp_poly_type polymorphic_types in
-    
+
     fprintf fmt "@[<v>%a%t%a;@]@."
-      
       (* Include all the subinstance package*)
-      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
+      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility))
+      machines_to_import
       (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
-      
       (*Begin the package*)
-      (pp_package (pp_package_name m) pp_generics false) pp_content
-
+      (pp_package (pp_package_name m) pp_generics false)
+      pp_content
 end

src/backends/Ada/ada_backend_common.mli

 open Format
-
 open Machine_code_types
 open Lustre_types
 open Types
-
 open Ada_printer
 open Misc_printer
 
 val pp_state_name : printer
+
 val pp_state_type : printer
+
 val pp_reset_procedure_name : printer
+
 val pp_step_procedure_name : printer
+
 val pp_main_procedure_name : printer
+
 val pp_polymorphic_type : int -> printer
+
 val pp_past_name : int -> printer
 
 val is_builtin_fun : string -> bool
-val ada_supported_funs : (string*(string*string)) list
+
+val ada_supported_funs : (string * (string * string)) list
 
 val pp_var_name : var_decl -> formatter -> unit
-val pp_var : ((string*printer) list) -> formatter -> var_decl -> unit
-val pp_value : ((string*printer) list) -> formatter -> value_t -> unit
+
+val pp_var : (string * printer) list -> formatter -> var_decl -> unit
+
+val pp_value : (string * printer) list -> formatter -> value_t -> unit
+
 val pp_type : formatter -> type_expr -> unit
+
 val pp_var_type : formatter -> var_decl -> unit
 
 val pp_package_name : machine_t -> printer
-val pp_package_name_with_polymorphic : (int * Types.type_expr) list -> machine_t -> printer
+
+val pp_package_name_with_polymorphic :
+  (int * Types.type_expr) list -> machine_t -> printer
 
 val mk_default_value : type_expr -> value_t
 
 val build_pp_var_decl : parameter_mode -> ada_with -> var_decl -> ada_var_decl
+
 val build_pp_var_decl_local : ada_with -> var_decl -> ada_local_decl
-val build_pp_var_decl_step_input : parameter_mode -> ada_with -> machine_t -> (ada_var_decl list list)
-val build_pp_var_decl_step_output : parameter_mode -> ada_with -> machine_t -> (ada_var_decl list list)
-val build_pp_arg_step : machine_t -> (ada_var_decl list list)
-val build_pp_arg_reset : machine_t -> (ada_var_decl list list)
-val build_pp_state_decl_from_subinstance : parameter_mode -> ada_with -> (string * ((int * Types.type_expr) list * Machine_code_types.machine_t)) -> ada_var_decl
+
+val build_pp_var_decl_step_input :
+  parameter_mode -> ada_with -> machine_t -> ada_var_decl list list
+
+val build_pp_var_decl_step_output :
+  parameter_mode -> ada_with -> machine_t -> ada_var_decl list list
+
+val build_pp_arg_step : machine_t -> ada_var_decl list list
+
+val build_pp_arg_reset : machine_t -> ada_var_decl list list
+
+val build_pp_state_decl_from_subinstance :
+  parameter_mode ->
+  ada_with ->
+  string * ((int * Types.type_expr) list * Machine_code_types.machine_t) ->
+  ada_var_decl
+
 val build_pp_state_decl : parameter_mode -> ada_with -> ada_var_decl
 
 val pp_machine_filename : string -> formatter -> machine_t -> unit
+
 val pp_main_filename : formatter -> machine_t -> unit

src/backends/Ada/ada_backend_wrapper.ml

@@ -10,111 +10,148 @@
 (********************************************************************)
 
 open Format
-
 open Machine_code_types
 open Lustre_types
-
 open Misc_printer
 open Misc_lustre_function
 open Ada_printer
 open Ada_backend_common
 
-module Main =
-struct
-
+module Main = struct
   let build_text_io_package_local typ =
-    AdaLocalPackage (
-      (fun fmt -> fprintf fmt "%s_IO" typ),
-      (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
-      [((fun fmt -> fprintf fmt "Num"), (fun fmt -> fprintf fmt "%s" typ))])
-
-  (** Print the main file calling in a loop the step function of the main machine.
-     @param fmt the formater to print on
-     @param machine the main machine
-  **)
+    AdaLocalPackage
+      ( (fun fmt -> fprintf fmt "%s_IO" typ),
+        (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
+        [ ((fun fmt -> fprintf fmt "Num"), fun fmt -> fprintf fmt "%s" typ) ] )
+
+  (** Print the main file calling in a loop the step function of the main
+      machine. @param fmt the formater to print on @param machine the main
+      machine **)
   let pp_main_adb fmt machine =
     let statefull = is_machine_statefull machine in
-    
+
     let pp_package = pp_package_name_with_polymorphic [] machine in
-    
+
     (* Dependances *)
     let text_io = "Ada.Text_IO" in
-    
+
     (* Locals *)
     let locals =
-      [[build_text_io_package_local "Integer";build_text_io_package_local "Float"]]
-      @(if statefull then [[AdaLocalVar (build_pp_state_decl_from_subinstance AdaNoMode None (asprintf "%t" pp_state_name, ([], machine)))]] else [])
-      @(if machine.mstep.step_inputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_inputs] else [])
-      @(if machine.mstep.step_outputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_outputs] else [])
+      [
+        [
+          build_text_io_package_local "Integer";
+          build_text_io_package_local "Float";
+        ];
+      ]
+      @ (if statefull then
+         [
+           [
+             AdaLocalVar
+               (build_pp_state_decl_from_subinstance AdaNoMode None
+                  (asprintf "%t" pp_state_name, ([], machine)));
+           ];
+         ]
+        else [])
+      @ (if machine.mstep.step_inputs != [] then
+         [ List.map (build_pp_var_decl_local None) machine.mstep.step_inputs ]
+        else [])
+      @
+      if machine.mstep.step_outputs != [] then
+        [ List.map (build_pp_var_decl_local None) machine.mstep.step_outputs ]
+      else []
     in
 
     (* Stream instructions *)
-    let get_basic var = match (Types.repr var.var_type ).Types.tdesc with
-        Types.Tbasic x -> x | _ -> assert false in
+    let get_basic var =
+      match (Types.repr var.var_type).Types.tdesc with
+      | Types.Tbasic x ->
+        x
+      | _ ->
+        assert false
+    in
     let pp_read fmt var =
       match get_basic var with
-        | Types.Basic.Tbool ->
-            fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
-              (pp_var_name var)
-        | _ ->
-            fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)"
-              (pp_var_name var)
-              pp_var_type var
+      | Types.Basic.Tbool ->
+        fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
+          (pp_var_name var)
+      | _ ->
+        fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var)
+          pp_var_type var
     in
     let pp_write fmt var =
       match get_basic var with
-        | Types.Basic.Tbool ->
-            fprintf fmt "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \"' \")"
-              (pp_var_name var)
-              (pp_var_name var)
-        | Types.Basic.Tint ->
-            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Integer_IO.Put(%t);@,Ada.Text_IO.Put_Line(\"' \")"
-              (pp_var_name var)
-              (pp_var_name var)
-        | Types.Basic.Treal ->
-            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
-              (pp_var_name var)
-              (pp_var_name var)
-        | Types.Basic.Tstring | Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
+      | Types.Basic.Tbool ->
+        fprintf fmt
+          "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \
+           \"' \")"
+          (pp_var_name var) (pp_var_name var)
+      | Types.Basic.Tint ->
+        fprintf fmt
+          "Ada.Text_IO.Put(\"'%t': '\");@,\
+           Integer_IO.Put(%t);@,\
+           Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
+      | Types.Basic.Treal ->
+        fprintf fmt
+          "Ada.Text_IO.Put(\"'%t': '\");@,\
+           Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\
+           Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
+      | Types.Basic.Tstring | Types.Basic.Trat ->
+        assert false
+      (* Could not be the top level inputs *)
     in
 
     (* Loop instructions *)
     let pp_loop fmt =
-      let args = pp_state_name::(List.map pp_var_name (machine.mstep.step_inputs@machine.mstep.step_outputs)) in
-      fprintf fmt "while not Ada.Text_IO.End_Of_File loop@,  @[<v>%a;@,%a;@,%a;@]@,end loop"
-        (Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
-        pp_call (pp_package_access (pp_package, pp_step_procedure_name), [args])
-        (Utils.fprintf_list ~sep:";@," pp_write) machine.mstep.step_outputs in
-    
+      let args =
+        pp_state_name
+        ::
+        List.map pp_var_name
+          (machine.mstep.step_inputs @ machine.mstep.step_outputs)
+      in
+      fprintf fmt
+        "while not Ada.Text_IO.End_Of_File loop@,\
+        \  @[<v>%a;@,\
+         %a;@,\
+         %a;@]@,\
+         end loop"
+        (Utils.fprintf_list ~sep:";@," pp_read)
+        machine.mstep.step_inputs pp_call
+        (pp_package_access (pp_package, pp_step_procedure_name), [ args ])
+        (Utils.fprintf_list ~sep:";@," pp_write)
+        machine.mstep.step_outputs
+    in
+
     (* Print the file *)
-    let instrs = (if statefull then [fun fmt -> pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), [[pp_state_name]])] else [])@[pp_loop] in
-    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]"
-      (pp_with AdaPrivate) (pp_str text_io)
+    let instrs =
+      (if statefull then
+       [
+         (fun fmt ->
+           pp_call fmt
+             ( pp_package_access (pp_package, pp_reset_procedure_name),
+               [ [ pp_state_name ] ] ));
+       ]
+      else [])
+      @ [ pp_loop ]
+    in
+    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)
       (pp_with AdaPrivate) (pp_package_name machine)
-      (pp_procedure pp_main_procedure_name [] None) (AdaProcedureContent (locals, instrs))
-
-  (** 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
-  **)
-  let pp_project_configuration_file fmt =
-    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
-  **)
-  let pp_project_name basename fmt =
-    fprintf fmt "%s.gpr" basename
-
-  let pp_for_single name arg fmt =
-    fprintf fmt "for %s use \"%s\"" name arg
+      (pp_procedure pp_main_procedure_name [] None)
+      (AdaProcedureContent (locals, instrs))
+
+  (** 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
+      **)
+  let pp_project_configuration_file fmt = 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 **)
+  let pp_project_name basename fmt = 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
@@ -123,49 +160,62 @@ struct
 
   let pp_content fmt lines =
     fprintf fmt "  @[<v>%a%t@]"
-      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
+      (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
-  **)
+    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 _ -> [
-          pp_for "Main" [asprintf "%t" pp_main_procedure_name];
-          pp_for_single "Exec_Dir" "bin";
+    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 _ ->
+         [
+           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";
+                ];
+              pp_for_single "Proof_Dir" (asprintf "proof");
+            ];
         ])
-    @[
-      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"];
-        pp_for_single "Proof_Dir" (asprintf "proof");
-      ]
-    ])
-    project_name
-
-
-  end
+      project_name
+end

src/backends/Ada/ada_printer.mli

@@ -3,58 +3,92 @@ open Misc_printer
 
 type parameter_mode = AdaNoMode | AdaIn | AdaOut | AdaInOut
 
-type kind_def = AdaType | AdaProcedure | AdaFunction | AdaPackageDecl | AdaPackageBody
+type kind_def =
+  | AdaType
+  | AdaProcedure
+  | AdaFunction
+  | AdaPackageDecl
+  | AdaPackageBody
 
 type visibility = AdaNoVisibility | AdaPrivate | AdaLimitedPrivate
 
-type ada_with = (bool * bool * (printer list) * (printer list)) option
+type ada_with = (bool * bool * printer list * printer list) option
 
 type ada_var_decl = parameter_mode * printer * printer * ada_with
 
 type ada_local_decl =
   | AdaLocalVar of ada_var_decl
-  | AdaLocalPackage of (printer * printer * ((printer*printer) list))
+  | AdaLocalPackage of (printer * printer * (printer * printer) list)
 
 type def_content =
   | AdaNoContent
   | AdaPackageContent of printer
   | AdaSimpleContent of printer
   | AdaVisibilityDefinition of visibility
-  | AdaProcedureContent of ((ada_local_decl list list) * (printer list))
-  | AdaRecord of (ada_var_decl list list)
-  | AdaPackageInstanciation of (printer * ((printer*printer) list))
+  | AdaProcedureContent of (ada_local_decl list list * printer list)
+  | AdaRecord of ada_var_decl list list
+  | AdaPackageInstanciation of (printer * (printer * printer) list)
 
 val pp_integer_type : printer
+
 val pp_float_type : printer
+
 val pp_boolean_type : printer
 
 val pp_clean_ada_identifier : formatter -> string -> unit
-val pp_package_access : (printer*printer) -> printer
+
+val pp_package_access : printer * printer -> printer
+
 val pp_block : formatter -> printer list -> unit
+
 val pp_oneline_comment : formatter -> string -> unit
+
 val pp_with : visibility -> formatter -> printer -> unit
+
 val pp_var_decl : ada_var_decl -> printer
-val pp_access :  printer -> printer -> formatter -> unit
-val pp_call : formatter -> (printer*(printer list list)) -> unit
+
+val pp_access : printer -> printer -> formatter -> unit
+
+val pp_call : formatter -> printer * printer list list -> unit
+
 val pp_old : printer -> printer
+
 val pp_adastring : printer -> printer
 
-val pp_or : (printer list) -> printer
-val pp_and : (printer list) -> printer
+val pp_or : printer list -> printer
+
+val pp_and : printer list -> printer
 
 (* declaration printer *)
 val pp_package : printer -> printer list -> bool -> formatter -> printer -> unit
-val pp_package_instanciation : printer -> printer -> formatter -> (printer*printer) list -> unit
+
+val pp_package_instanciation :
+  printer -> printer -> formatter -> (printer * printer) list -> unit
+
 val pp_type_decl : printer -> visibility -> printer
+
 val pp_record : printer -> formatter -> ada_var_decl list list -> unit
-val pp_procedure : printer -> (ada_var_decl list list) -> ada_with -> formatter -> def_content -> unit
-val pp_predicate : printer -> (ada_var_decl list list) -> bool -> formatter -> (printer option) -> unit
+
+val pp_procedure :
+  printer ->
+  ada_var_decl list list ->
+  ada_with ->
+  formatter ->
+  def_content ->
+  unit
+
+val pp_predicate :
+  printer ->
+  ada_var_decl list list ->
+  bool ->
+  formatter ->
+  printer option ->
+  unit
 (* Local function :
 
-val pp_parameter_mode : formatter -> parameter_mode -> unit
-val pp_kind_def : formatter -> kind_def -> unit
-val pp_visibility : formatter -> visibility -> unit
-val pp_var_decl_lists : formatter -> ada_var_decl list list -> unit
-val pp_def_args : formatter -> ada_var_decl list list -> unit
-val pp_def : formatter -> (kind_def*printer*(ada_var_decl list list)*(printer option)*def_content*(printer option)) -> unit
-*)
+   val pp_parameter_mode : formatter -> parameter_mode -> unit val pp_kind_def :
+   formatter -> kind_def -> unit val pp_visibility : formatter -> visibility ->
+   unit val pp_var_decl_lists : formatter -> ada_var_decl list list -> unit val
+   pp_def_args : formatter -> ada_var_decl list list -> unit val pp_def :
+   formatter -> (kind_def*printer*(ada_var_decl list list)*(printer
+   option)*def_content*(printer option)) -> unit *)

src/backends/Ada/misc_printer.ml

@@ -3,22 +3,16 @@ open Format
 type printer = formatter -> unit
 
 (** Encapsulate a pretty print function to lower case its result when applied
-   @param pp the pretty print function
-   @param fmt the formatter
-   @param arg the argument of the pp function
-**)
+    @param pp the pretty print function @param fmt the formatter @param arg the
+    argument of the pp function **)
 let pp_lowercase pp fmt =
   let str = asprintf "%t" pp in
-  fprintf fmt "%s" (String. lowercase_ascii str)
+  fprintf fmt "%s" (String.lowercase_ascii str)
 
-(** Print a filename by lowercasing the base and appending an extension.
-   @param extension the extension to append to the package name
-   @param fmt the formatter
-   @param pp_name the file base name printer
-**)
+(** Print a filename by lowercasing the base and appending an extension. @param
+    extension the extension to append to the package name @param fmt the
+    formatter @param pp_name the file base name printer **)
 let pp_filename extension fmt pp_name =
-  fprintf fmt "%t.%s"
-    (pp_lowercase pp_name)
-    extension
+  fprintf fmt "%t.%s" (pp_lowercase pp_name) extension
 
 let pp_str str fmt = fprintf fmt "%s" str

src/backends/C/c_backend.ml

@@ -11,23 +11,19 @@
 
 open Utils.Format
 open C_backend_mauve
+
 (******************************************************************************)
 (*                        Translation function                                *)
 (******************************************************************************)
-(* USELESS
-let makefile_opt print basename dependencies makefile_fmt machines =
-  (* If a main node is identified, generate a main target for it *)
-  match !Options.main_node with
-  | "" ->  ()
-  | main_node -> (
-    match Machine_code.get_machine_opt main_node machines with
-    | None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; ()
-    | Some _ -> print basename !Options.main_node dependencies makefile_fmt
-  )
-*)
-
-let c_or_cpp f =
-  if !Options.cpp then f ^ ".cpp" else f ^ ".c" (* Could be changed *)
+(* USELESS let makefile_opt print basename dependencies makefile_fmt machines =
+   (* If a main node is identified, generate a main target for it *) match
+   !Options.main_node with | "" -> () | main_node -> ( match
+   Machine_code.get_machine_opt main_node machines with | None -> Format.eprintf
+   "Unable to find a main node named %s@.@?" main_node; () | Some _ -> print
+   basename !Options.main_node dependencies makefile_fmt ) *)
+
+let c_or_cpp f = if !Options.cpp then f ^ ".cpp" else f ^ ".c"
+(* Could be changed *)
 
 let with_main_node machines node f =
   if node <> "" then
@@ -42,14 +38,19 @@ let with_main_node machines node f =
       f m
 
 let gen_files
-    (print_alloc_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *))
-    basename prog machines dependencies =
+    ( print_alloc_header,
+      print_lib_c,
+      print_main_c,
+      print_makefile,
+      preprocess
+    (* , print_cmake *) ) basename prog machines dependencies =
   let destname = !Options.dest_dir ^ "/" ^ basename in
-  
+
   let machines, spec = preprocess machines in
 
   (* Generating H alloc file *)
-  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
+  let alloc_header_file = destname ^ "_alloc.h" in
+  (* Could be changed *)
   with_out_file alloc_header_file (fun header_fmt ->
       print_alloc_header header_fmt basename prog machines dependencies spec);
 
@@ -79,44 +80,41 @@ let gen_files
           print_mauve_fsm source_mauve_fmt m));
 
   (* Generating Makefile *)
-  (* Makefiles:
-     - for the moment two cases
-     1. Classical Makefile, only when provided with a main node
-     May contain additional framac eacsl targets
-     2. Cmake : 2 files
-         - lustrec-basename.cmake describing all variables
-         - the main CMakeLists.txt activating the first file
-     - Later option 1 should be removed
-  *)
+  (* Makefiles: - for the moment two cases 1. Classical Makefile, only when
+     provided with a main node May contain additional framac eacsl targets 2.
+     Cmake : 2 files - lustrec-basename.cmake describing all variables - the
+     main CMakeLists.txt activating the first file - Later option 1 should be
+     removed *)
   (* Case 1 *)
   if main_node <> "" then
-    let makefile_file = destname ^ ".makefile" in (* Could be changed *)
+    let makefile_file = destname ^ ".makefile" in
+    (* Could be changed *)
     with_out_file makefile_file (fun makefile_fmt ->
         print_makefile basename main_node dependencies makefile_fmt)
 
-  (* (\* Case 2 *\) *)
-  (* let cmake_file = "lustrec-" ^ basename ^ ".cmake" in *)
-  (* let cmake_file_full_path = !Options.dest_dir ^ "/" ^ cmake_file in *)
-  (* let cmake_out = open_out cmake_file_full_path in *)
-  (* let cmake_fmt = formatter_of_out_channel cmake_out in *)
-  (* (\* Generating Makefile *\) *)
-  (* print_cmake basename main_node dependencies makefile_fmt; *)
-    
-  (*   close_out makefile_out *)
-  
+(* (\* Case 2 *\) *)
+(* let cmake_file = "lustrec-" ^ basename ^ ".cmake" in *)
+(* let cmake_file_full_path = !Options.dest_dir ^ "/" ^ cmake_file in *)
+(* let cmake_out = open_out cmake_file_full_path in *)
+(* let cmake_fmt = formatter_of_out_channel cmake_out in *)
+(* (\* Generating Makefile *\) *)
+(* print_cmake basename main_node dependencies makefile_fmt; *)
+
+(* close_out makefile_out *)
+
 let print_c_header basename =
-  let header_m = match !Options.spec with
+  let header_m =
+    match !Options.spec with
     | "no" ->
-      C_backend_header.(module EmptyMod : MODIFIERS_HDR)
-
+      C_backend_header.((module EmptyMod : MODIFIERS_HDR))
     | "acsl" ->
-      C_backend_header.(module C_backend_spec.HdrMod : MODIFIERS_HDR)
-
-    | "c" -> assert false        (* not implemented yet *)
-
-    | _ -> assert false
+      C_backend_header.((module C_backend_spec.HdrMod : MODIFIERS_HDR))
+    | "c" ->
+      assert false (* not implemented yet *)
+    | _ ->
+      assert false
   in
-  let module Header = C_backend_header.Main (val header_m) in
+  let module Header = C_backend_header.Main ((val header_m)) in
   let destname = !Options.dest_dir ^ "/" ^ basename in
   (* Generating H file *)
   let lusic = Lusic.read_lusic destname ".lusic" in
@@ -129,41 +127,39 @@ let translate_to_c generate_c_header basename prog machines dependencies =
   let header_m, source_m, source_main_m, makefile_m, preprocess =
     match !Options.spec with
     | "no" ->
-      C_backend_header.(module EmptyMod : MODIFIERS_HDR),
-      C_backend_src.(module EmptyMod : MODIFIERS_SRC),
-      C_backend_main.(module EmptyMod : MODIFIERS_MAINSRC),
-      C_backend_makefile.(module EmptyMod : MODIFIERS_MKF),
-      fun m -> m, []
-
+      ( C_backend_header.((module EmptyMod : MODIFIERS_HDR)),
+        C_backend_src.((module EmptyMod : MODIFIERS_SRC)),
+        C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
+        C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)),
+        fun m -> m, [] )
     | "acsl" ->
       let open C_backend_spec in
-      C_backend_header.(module HdrMod : MODIFIERS_HDR),
-      C_backend_src.(module SrcMod : MODIFIERS_SRC),
-      C_backend_main.(module EmptyMod : MODIFIERS_MAINSRC),
-      C_backend_makefile.(module MakefileMod : MODIFIERS_MKF),
-      preprocess_acsl
-
-    | "c" -> assert false        (* not implemented yet *)
-
-    | _ -> assert false
+      ( C_backend_header.((module HdrMod : MODIFIERS_HDR)),
+        C_backend_src.((module SrcMod : MODIFIERS_SRC)),
+        C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
+        C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)),
+        preprocess_acsl )
+    | "c" ->
+      assert false (* not implemented yet *)
+    | _ ->
+      assert false
   in
-  let module Header = C_backend_header.Main (val header_m) in
-  let module Source = C_backend_src.Main (val source_m) in
-  let module SourceMain = C_backend_main.Main (val source_main_m) in
-  let module Makefile = C_backend_makefile.Main (val makefile_m) in
+  let module Header = C_backend_header.Main ((val header_m)) in
+  let module Source = C_backend_src.Main ((val source_m)) in
+  let module SourceMain = C_backend_main.Main ((val source_main_m)) in
+  let module Makefile = C_backend_makefile.Main ((val makefile_m)) in
   (* let module CMakefile = C_backend_cmake.Main (MakefileMod) in *)
   let funs =
-    Header.print_alloc_header,
-    Source.print_lib_c,
-    SourceMain.print_main_c,
-    Makefile.print_makefile,
-    preprocess
+    ( Header.print_alloc_header,
+      Source.print_lib_c,
+      SourceMain.print_main_c,
+      Makefile.print_makefile,
+      preprocess )
     (* CMakefile.print_makefile *)
   in
   if generate_c_header then print_c_header basename;
   gen_files funs basename prog machines dependencies
 
-
 (* Local Variables: *)
 (* compile-command:"make -C ../../.." *)
 (* End: *)

src/backends/C/c_backend_cmake.ml

@@ -14,93 +14,106 @@ open LustreSpec
 open Corelang
 
 let header_has_code header =
-  List.exists 
-    (fun top -> 
+  List.exists
+    (fun top ->
       match top.top_decl_desc with
-      | Const _ -> true 
-      | ImportedNode nd -> nd.nodei_in_lib = []
-      | _ -> false
-    )
+      | Const _ ->
+        true
+      | ImportedNode nd ->
+        nd.nodei_in_lib = []
+      | _ ->
+        false)
     header
 
 let header_libs header =
-  List.fold_left (fun accu top ->
-    match top.top_decl_desc with
-      | ImportedNode nd -> Utils.list_union nd.nodei_in_lib accu
-      | _ -> accu 
-  ) [] header 
-    
+  List.fold_left
+    (fun accu top ->
+      match top.top_decl_desc with
+      | ImportedNode nd ->
+        Utils.list_union nd.nodei_in_lib accu
+      | _ ->
+        accu)
+    [] header
 
-let compiled_dependencies dep = 
+let compiled_dependencies dep =
   List.filter (fun (Dep (_, _, header, _)) -> header_has_code header) dep
 
-let lib_dependencies dep = 
-  List.fold_left 
-    (fun accu (Dep (_, _, header, _)) -> Utils.list_union (header_libs header) accu) [] dep
-    
-let fprintf_dependencies fmt (dep: dep_t list) =
+let lib_dependencies dep =
+  List.fold_left
+    (fun accu (Dep (_, _, header, _)) ->
+      Utils.list_union (header_libs header) accu)
+    [] dep
+
+let fprintf_dependencies fmt (dep : dep_t list) =
   let compiled_dep = compiled_dependencies dep in
-  List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s;  *)
-    fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
-    (("${INC}/io_frontend.c"):: (* IO functions when a main function is computed *)
-	(List.map 
-	   (fun (Dep (local, s, _, _)) -> 
-	     (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")
-	   compiled_dep))
+  List.iter
+    (fun s ->
+      (* Format.eprintf "Adding dependency: %s@." s; *)
+      fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
+    ("${INC}/io_frontend.c"
+     ::
+     (* IO functions when a main function is computed *)
+     List.map
+       (fun (Dep (local, s, _, _)) ->
+         (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")
+       compiled_dep)
 
-module type MODIFIERS_MKF =
-sig (* dep was (bool * ident * top_decl list) *)
-  val other_targets: Format.formatter -> string -> string -> dep_t list -> unit
+module type MODIFIERS_MKF = sig
+  (* dep was (bool * ident * top_decl list) *)
+  val other_targets : Format.formatter -> string -> string -> dep_t list -> unit
 end
 
-module EmptyMod =
-(struct
+module EmptyMod : MODIFIERS_MKF = struct
   let other_targets _ _ _ _ = ()
-end: MODIFIERS_MKF)
-
-module Main = functor (Mod: MODIFIERS_MKF) -> 
-struct
-
-
-  let print_cmake basename nodename (dependencies:  dep_t list) fmt =
-
-    (* Printing the basic file CMakeLists.txt *)
-    let fmt_CMakeLists_txt = formatter_of_out_channel (open_out (!Options.dest_dir ^ "/CMakeLists.txt")) in
-    fprintf fmt_CMakeLists_txt "cmake_minimum_required(VERSION 3.0)@.";
-    fprintf fmt_CMakeLists_txt "project(%s C)@." basename;
-    fprintf mt_CMakeLists_txt "@.";
-    fprintf mt_CMakeLists_txt "set(LUSTREC_DEFINE_TARGETS ON)@.";
-    fprintf mt_CMakeLists_txt "include(lustrec-%s.cmake)" basename;
+end
 
-    
-    fprintf fmt "GCC=gcc@.";
-    fprintf fmt "LUSTREC=%s@." Sys.executable_name;
-    fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
-    fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
-    fprintf fmt "@.";
+module Main =
+functor
+  (Mod : MODIFIERS_MKF)
+  ->
+  struct
+    let print_cmake basename nodename (dependencies : dep_t list) fmt =
+      (* Printing the basic file CMakeLists.txt *)
+      let fmt_CMakeLists_txt =
+        formatter_of_out_channel
+          (open_out (!Options.dest_dir ^ "/CMakeLists.txt"))
+      in
+      fprintf fmt_CMakeLists_txt "cmake_minimum_required(VERSION 3.0)@.";
+      fprintf fmt_CMakeLists_txt "project(%s C)@." basename;
+      fprintf mt_CMakeLists_txt "@.";
+      fprintf mt_CMakeLists_txt "set(LUSTREC_DEFINE_TARGETS ON)@.";
+      fprintf mt_CMakeLists_txt "include(lustrec-%s.cmake)" basename;
 
-    (* Main binary *)
-    fprintf fmt "%s_%s: %s.c %s_main.c@." basename nodename basename basename;
-    fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s.c@." basename;  
-    fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s_main.c@." basename;   
-    fprintf_dependencies fmt dependencies;    
-    fprintf fmt "\t${GCC} -O0 -o %s_%s io_frontend.o %a %s.o %s_main.o %a@." basename nodename 
-      (Utils.fprintf_list ~sep:" " (fun fmt (Dep (_, s, _, _)) -> Format.fprintf fmt "%s.o" s)) 
-      (compiled_dependencies dependencies)
-      basename (* library .o *)
-      basename (* main function . o *) 
-      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) (lib_dependencies dependencies)
-    ;
-    fprintf fmt "@.";
-    fprintf fmt "clean:@.";
-    fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename;
-    fprintf fmt "@.";
-    fprintf fmt ".PHONY: %s_%s@." basename nodename;
-    fprintf fmt "@.";
-    Mod.other_targets fmt basename nodename dependencies;
-    fprintf fmt "@.";
+      fprintf fmt "GCC=gcc@.";
+      fprintf fmt "LUSTREC=%s@." Sys.executable_name;
+      fprintf fmt "LUSTREC_BASE=%s@."
+        (Filename.dirname (Filename.dirname Sys.executable_name));
+      fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
+      fprintf fmt "@.";
 
-end
+      (* Main binary *)
+      fprintf fmt "%s_%s: %s.c %s_main.c@." basename nodename basename basename;
+      fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s.c@." basename;
+      fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s_main.c@." basename;
+      fprintf_dependencies fmt dependencies;
+      fprintf fmt "\t${GCC} -O0 -o %s_%s io_frontend.o %a %s.o %s_main.o %a@."
+        basename nodename
+        (Utils.fprintf_list ~sep:" " (fun fmt (Dep (_, s, _, _)) ->
+             Format.fprintf fmt "%s.o" s))
+        (compiled_dependencies dependencies)
+        basename (* library .o *) basename
+        (* main function . o *)
+        (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
+        (lib_dependencies dependencies);
+      fprintf fmt "@.";
+      fprintf fmt "clean:@.";
+      fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename;
+      fprintf fmt "@.";
+      fprintf fmt ".PHONY: %s_%s@." basename nodename;
+      fprintf fmt "@.";
+      Mod.other_targets fmt basename nodename dependencies;
+      fprintf fmt "@."
+  end
 
 (* Local Variables: *)
 (* compile-command:"make -C ../../.." *)