[SAVer] Lint wrt ocamlformat rules.

lib/ovo/ovo.ml

@@ -67,8 +67,8 @@ let parse_in_channel filename in_channel =
     skip_ovo_header filename in_channel >>= fun () ->
     let in_channel = Csv.of_channel in_channel in
     handle_ovo_unused_flag in_channel >>= fun () ->
-    handle_ovo_basic_info in_channel >>= fun (n_is) ->
-    handle_ovo_basic_info in_channel >>= fun (n_os) ->
+    handle_ovo_basic_info in_channel >>= fun n_is ->
+    handle_ovo_basic_info in_channel >>= fun n_os ->
     Csv.close_in in_channel;
     Ok { n_inputs = n_is; n_outputs = n_os }
   with

src/language.ml

@@ -7,8 +7,9 @@
 open Why3
 open Base
 
-(* Support for several model formats: - NNet and ONNX for neural networks, - OVO
-   for for SVM *)
+(* Support for several model formats: *)
+(* - NNet and ONNX for neural networks *)
+(* - OVO for for SVM *)
 
 type nnshape = {
   nb_inputs : int;
@@ -17,16 +18,12 @@ type nnshape = {
   filename : string;
 }
 
-type svmshape = {
-  nb_inputs : int;
-  nb_classes : int;
-  filename : string;
-}
+type svmshape = { nb_inputs : int; nb_classes : int; filename : string }
 
-let loaded_nets = Why3.Term.Hls.create 10
-let loaded_svms  = Why3.Term.Hls.create 10
-let lookup_loaded_nets = Why3.Term.Hls.find_opt loaded_nets
-let lookup_loaded_svms = Why3.Term.Hls.find_opt loaded_svms
+let loaded_nets = Term.Hls.create 10
+let loaded_svms = Term.Hls.create 10
+let lookup_loaded_nets = Term.Hls.find_opt loaded_nets
+let lookup_loaded_svms = Term.Hls.find_opt loaded_svms
 
 let register_nn_as_tuple nb_inputs nb_outputs filename env =
 let net = Pmodule.read_module env [ "caisar" ] "NN" in
@@ -60,13 +57,9 @@ let register_svm_as_array nb_inputs nb_classes filename env =
   let th_uc = Pmodule.create_module env id_as_array in
   let th_uc = Pmodule.use_export th_uc svm in
   let ls_svm_apply =
-    Term.create_fsymbol
-      (Ident.id_fresh "svm_apply")
-      []
-      svm_type
+    Term.create_fsymbol (Ident.id_fresh "svm_apply") [] svm_type
   in
-  Why3.Term.Hls.add loaded_svms ls_svm_apply
-    { filename; nb_inputs; nb_classes };
+  Term.Hls.add loaded_svms ls_svm_apply { filename; nb_inputs; nb_classes };
   let th_uc =
     Pmodule.add_pdecl ~vc:false th_uc
       (Pdecl.create_pure_decl (Decl.create_param_decl ls_svm_apply))
@@ -89,7 +82,8 @@ let ovo_parser env _ filename _ =
   let model = Ovo.parse filename in
   match model with
   | Error s -> Loc.errorm "%s" s
-  | Ok model -> register_svm_as_array model.n_inputs model.n_outputs filename env
+  | Ok model ->
+    register_svm_as_array model.n_inputs model.n_outputs filename env
 
 let register_nnet_support () =
   Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
@@ -100,5 +94,5 @@ let register_onnx_support () =
     onnx_parser
 
 let register_ovo_support () =
-    Env.register_format ~desc:"OVO format" Pmodule.mlw_language "OVO" [ "ovo" ]
-      ovo_parser
+  Env.register_format ~desc:"OVO format" Pmodule.mlw_language "OVO" [ "ovo" ]
+    ovo_parser

src/main.ml

@@ -157,10 +157,7 @@ let verify_cmd =
     Arg.(required & opt (some provers) None & info [ "p"; "prover" ] ~doc)
   in
   let dataset_csv =
-    let doc =
-      "Dataset under .csv format to use for analyse.\n\
-      \    Currently only supported by SAVer."
-    in
+    let doc = "Dataset under CSV format. Currently only supported by SAVer." in
     Arg.(value & opt (some string) None & info [ "dataset-csv" ] ~doc)
   in
   let doc =

src/verification.ml

@@ -145,8 +145,7 @@ let answer_saver limit config task env prover dataset_csv =
   in
   answer
 
-let answer_generic limit config task driver
-  (prover : Why3.Whyconf.config_prover) =
+let answer_generic limit config task driver (prover : Whyconf.config_prover) =
   let task_prepared = Driver.prepare_task driver task in
   let tasks =
     (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
@@ -175,7 +174,7 @@ let answer_generic limit config task driver
   let answer = combine_prover_answers answers in
   answer
 
-let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
+let call_prover ~limit config (prover : Whyconf.config_prover) driver env
   dataset_csv task =
   let prover_answer =
     if String.equal prover.prover.prover_name "SAVer"