Some more style reworking.

.ocamlformat

 version=0.19.0
-exp-grouping=preserve
+exp-grouping=parens
 if-then-else=keyword-first
 max-indent=2
 wrap-comments=true

src/language.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
 type nnet = {
   nb_inputs : int;
   nb_outputs : int;
@@ -6,7 +12,7 @@ type nnet = {
 }
 
 val lookup_loaded_nnets : Why3.Term.lsymbol -> nnet option
-(** Return the filename of an nnets Why3 representation *)
+(** @return the filename of an nnets Why3 representation. *)
 
 val register_nnet_support : unit -> unit
-(** register nnet parser *)
+(** Register nnet parser. *)

src/main.ml

@@ -6,7 +6,6 @@
 
 open Base
 open Cmdliner
-module Format = Caml.Format
 
 let caisar = "caisar"
 
@@ -45,7 +44,7 @@ let setup_logs =
 
 let config detect () =
   if detect
-  then begin
+  then (
     Logs.debug (fun m -> m "Automatic detection.");
     let config =
       let debug = match Logs.level () with Some Debug -> true | _ -> false in
@@ -57,8 +56,7 @@ let config detect () =
       m "@[<v>%a@]"
         (Pp.print_iter2 Whyconf.Mprover.iter Pp.newline Pp.nothing
            Whyconf.print_prover Pp.nothing)
-        provers)
-  end
+        provers))
 
 let verify format loadpath prover files =
   List.iter ~f:(Verification.verify format loadpath prover) files
@@ -83,17 +81,16 @@ let config_cmd =
   in
   let detect =
     let doc =
-      Format.sprintf "Detect solvers in \\$PATH (or \\$%s, if specified)."
-        dirvar
+      Fmt.str "Detect solvers in \\$PATH (or \\$%s, if specified)." dirvar
     in
     Arg.(value & flag & info [ "d"; "detect" ] ~doc)
   in
-  let doc = Format.sprintf "%s configuration." caisar in
+  let doc = Fmt.str "%s configuration." caisar in
   let exits = Term.default_exits in
   let man =
     [
       `S Manpage.s_description;
-      `P (Format.sprintf "Handle the configuration of %s." caisar);
+      `P (Fmt.str "Handle the configuration of %s." caisar);
     ]
   in
   ( Term.(

src/transformations.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
 open Base
 
 let meta_input =
   Why3.Theory.(
     register_meta "caisar_input"
-      ~desc:"Indicate the position of the input in the neural network"
+      ~desc:"Indicates the position of the input in the neural network"
       [ MTlsymbol; MTint ])
 
 let meta_output =
   Why3.Theory.(
     register_meta "caisar_output"
-      ~desc:"Indicate the position of the output in the neural network"
+      ~desc:"Indicates the position of the output in the neural network"
       [ MTlsymbol; MTint ])
 
 let get_input_variables =
@@ -96,8 +102,8 @@ let simplify_goal env input_variables =
 let caisar_native_prover env =
   Why3.Trans.seq
     [
-      Why3.Trans.bind get_input_variables (simplify_goal env);
-      (* Why3.Simplify_formula.simplify_; *)
+      Why3.Trans.bind get_input_variables (simplify_goal env)
+      (* Why3.Simplify_formula.simplify_; *);
     ]
 
 let init () =

src/transformations.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
 val init : unit -> unit
-(** register the transformations *)
+(** Register the transformations. *)

src/verification.ml

@@ -5,7 +5,6 @@
 (**************************************************************************)
 
 open Base
-module Format = Caml.Format
 module Filename = Caml.Filename
 
 let () = Language.register_nnet_support ()
@@ -46,5 +45,5 @@ let verify format loadpath prover file =
           in
           Driver.load_driver_absolute env file prover.extra_drivers
       in
-      List.iter tasks ~f:(Format.printf "%a" (Driver.print_task driver)))
+      List.iter tasks ~f:(Fmt.pr "%a" (Driver.print_task driver)))
     mstr_theory