Some meaningless rework.

.ocamlformat

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

config/dune

 (install
  (section (site (caisar config)))
- (files provers_autodetection.conf)
+ (files caisar.conf)
 (package caisar))

dune-project

@@ -27,7 +27,10 @@
    (ppx_deriving_yojson (>= 3.6.1))
    (csv (>= 2.4))
   )
-  (sites (share stdlib)(share config))
+  (sites
+   (share stdlib)
+   (share config)
+  )
 )
 
 (package

lib/nnet/dune

 (library
- (name        nnet)
+ (name nnet)
  (public_name nnet)
  (libraries base csv)
  (synopsis "NNet parser"))

lib/nnet/nnet.ml

@@ -42,24 +42,24 @@ let skip_nnet_header filename in_channel =
   try
     while true do
       let line = Stdlib.input_line in_channel in
-      if not (Str.string_match (Str.regexp "//") line 0) then
-        raise End_of_header
+      if not (Str.string_match (Str.regexp "//") line 0)
+      then raise End_of_header
       else pos_in := Stdlib.pos_in in_channel
     done;
     assert false
   with
   | End_of_header ->
-      (* At this point we have read one line past the header part: seek back. *)
-      Stdlib.seek_in in_channel !pos_in;
-      Ok ()
+    (* At this point we have read one line past the header part: seek back. *)
+    Stdlib.seek_in in_channel !pos_in;
+    Ok ()
   | End_of_file ->
-      Error (Format.sprintf "NNet model not found in file `%s'." filename)
+    Error (Format.sprintf "NNet model not found in file `%s'." filename)
 
 (* Retrieve number of layers, inputs, outputs and maximum layer size. *)
 let handle_nnet_basic_info in_channel =
   match handle_nnet_line ~f:Int.of_string in_channel with
   | [ n_layers; n_inputs; n_outputs; max_layer_size ] ->
-      Ok (n_layers, n_inputs, n_outputs, max_layer_size)
+    Ok (n_layers, n_inputs, n_outputs, max_layer_size)
   | _ -> nnet_format_error "second"
   | exception End_of_file -> nnet_format_error "second"
 
@@ -67,7 +67,8 @@ let handle_nnet_basic_info in_channel =
 let handle_nnet_layer_sizes n_layers in_channel =
   try
     let layer_sizes = handle_nnet_line ~f:Int.of_string in_channel in
-    if List.length layer_sizes = n_layers + 1 then Ok layer_sizes
+    if List.length layer_sizes = n_layers + 1
+    then Ok layer_sizes
     else nnet_format_error "third"
   with End_of_file -> nnet_format_error "third"
 
@@ -82,7 +83,8 @@ let handle_nnet_unused_flag in_channel =
 let handle_nnet_min_input_values n_inputs in_channel =
   try
     let min_input_values = handle_nnet_line ~f:Float.of_string in_channel in
-    if List.length min_input_values = n_inputs then Ok min_input_values
+    if List.length min_input_values = n_inputs
+    then Ok min_input_values
     else nnet_format_error "fifth"
   with End_of_file -> nnet_format_error "fifth"
 
@@ -90,7 +92,8 @@ let handle_nnet_min_input_values n_inputs in_channel =
 let handle_nnet_max_input_values n_inputs in_channel =
   try
     let max_input_values = handle_nnet_line ~f:Float.of_string in_channel in
-    if List.length max_input_values = n_inputs then Ok max_input_values
+    if List.length max_input_values = n_inputs
+    then Ok max_input_values
     else nnet_format_error "sixth"
   with End_of_file -> nnet_format_error "sixth"
 
@@ -98,7 +101,8 @@ let handle_nnet_max_input_values n_inputs in_channel =
 let handle_nnet_mean_values n_inputs in_channel =
   try
     let mean_values = handle_nnet_line ~f:Float.of_string in_channel in
-    if List.length mean_values = n_inputs + 1 then
+    if List.length mean_values = n_inputs + 1
+    then
       let mean_input_values, mean_output_value =
         List.split_n mean_values n_inputs
       in
@@ -110,7 +114,8 @@ let handle_nnet_mean_values n_inputs in_channel =
 let handle_nnet_range_values n_inputs in_channel =
   try
     let range_values = handle_nnet_line ~f:Float.of_string in_channel in
-    if List.length range_values = n_inputs + 1 then
+    if List.length range_values = n_inputs + 1
+    then
       let range_input_values, range_output_value =
         List.split_n range_values n_inputs
       in

lib/nnet/nnet.mli

@@ -13,9 +13,9 @@ type t = private {
   min_input_values : float list;  (** Minimum values of inputs. *)
   max_input_values : float list;  (** Maximum values of inputs. *)
   mean_values : float list * float;
-      (** Mean values of inputs and one value for all outputs. *)
+    (** Mean values of inputs and one value for all outputs. *)
   range_values : float list * float;
-      (** Range values of inputs and one value for all outputs. *)
+    (** Range values of inputs and one value for all outputs. *)
   weights_biases : float list list;  (** All weights and biases of NNet model. *)
 }
 (** NNet model metadata. *)

src/detection.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
 open Base
 module Sys = Caml.Sys
 
 let null = if Sys.unix then "/dev/null" else "NUL"
 
-let rec lookup_file l f =
-  match l with
+let rec lookup_file dirs filename =
+  match dirs with
   | [] -> raise Caml.Not_found
-  | a :: l ->
-      let abs = Caml.Filename.concat a f in
-      if Sys.file_exists abs then abs else lookup_file l f
+  | dir :: dirs ->
+    let file = Caml.Filename.concat dir filename in
+    if Sys.file_exists file then file else lookup_file dirs filename
 
 let detect () =
-  Why3.Debug.set_flag Why3.Autodetection.debug;
-  let caisar_autodetection =
-    lookup_file Stdlib_path.Sites.config "provers_autodetection.conf"
-  in
-  let data =
-    Why3.Autodetection.Prover_autodetection_data.from_file caisar_autodetection
-  in
-  let config = Why3.Whyconf.init_config (Some null) in
-  let binaries = Why3.Autodetection.request_binaries_version config data in
-  let provers = Why3.Autodetection.compute_builtin_prover binaries data in
-  Why3.Whyconf.set_provers config provers
+  let open Why3 in
+  Debug.set_flag Why3.Autodetection.debug;
+  let caisar_conf = lookup_file Dirs.Sites.config "caisar.conf" in
+  let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
+  let config = Whyconf.init_config (Some null) in
+  let binaries = Autodetection.request_binaries_version config data in
+  let provers = Autodetection.compute_builtin_prover binaries data in
+  Whyconf.set_provers config provers

src/dune

@@ -6,4 +6,6 @@
   (package caisar)
 )
 
-(generate_sites_module (module stdlib_path) (sites caisar))
+(generate_sites_module
+  (module dirs)
+  (sites caisar))

src/language.ml

@@ -6,7 +6,7 @@
 
 open Base
 
-(* Register neural network languages *)
+(* Register neural network formats. *)
 
 let nnet_parser env _ filename _ =
   let open Why3 in
@@ -18,24 +18,24 @@ let nnet_parser env _ filename _ =
   match header with
   | Error s -> Loc.errorm "%s" s
   | Ok header ->
-      let id_as_tuple = Ident.id_fresh "As_tuple" in
-      let th_uc = Pmodule.create_module env id_as_tuple in
-      let th_uc = Pmodule.use_export th_uc nnet in
-      let ls_out =
-        Term.create_fsymbol
-          (Ident.id_fresh "nnet_apply")
-          (List.init header.n_inputs ~f:(fun _ -> nnet_input_type))
-          (Ty.ty_tuple
-             (List.init header.n_outputs ~f:(fun _ -> nnet_input_type)))
-      in
+    let id_as_tuple = Ident.id_fresh "AsTuple" in
+    let th_uc = Pmodule.create_module env id_as_tuple in
+    let th_uc = Pmodule.use_export th_uc nnet in
+    let ls_nnet_apply =
+      let f _ = nnet_input_type in
+      Term.create_fsymbol
+        (Ident.id_fresh "nnet_apply")
+        (List.init header.n_inputs ~f)
+        (Ty.ty_tuple (List.init header.n_outputs ~f))
+    in
 
-      let th_uc =
-        Pmodule.add_pdecl ~vc:false th_uc
-          (Pdecl.create_pure_decl @@ Decl.create_param_decl ls_out)
-      in
-      Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
+    let th_uc =
+      Pmodule.add_pdecl ~vc:false th_uc
+        (Pdecl.create_pure_decl @@ Decl.create_param_decl ls_nnet_apply)
+    in
+    Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
 
 let register () =
-  Why3.Env.(
-    register_format ~desc:"NNet format (ReLU only)" Why3.Pmodule.mlw_language
+  Why3.(
+    Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
       "NNet" [ "nnet" ] nnet_parser)

src/main.ml

@@ -24,13 +24,13 @@ let pp_header =
     match l with
     | Logs.App -> Fmt.pf ppf "[%a] " Fmt.(styled app_style string) x
     | Logs.Error ->
-        pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h)
+      pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h)
     | Logs.Warning ->
-        pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h)
+      pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h)
     | Logs.Info ->
-        pp_h ppf info_style (match h with None -> "INFO" | Some h -> h)
+      pp_h ppf info_style (match h with None -> "INFO" | Some h -> h)
     | Logs.Debug ->
-        pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h)
+      pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h)
 
 let setup_logs =
   let setup_log level =
@@ -78,11 +78,12 @@ let config_cmd =
   ( Term.(
       ret
         (const (fun cmdname detect _ ->
-             if not detect then `Help (`Pager, Some "config")
-             else
-               (* TODO: Do not only check for [detect], and enable it by
-                  default, as soon as other options are available. *)
-               `Ok (config cmdname true ()))
+           if not detect
+           then `Help (`Pager, Some "config")
+           else
+             (* TODO: Do not only check for [detect], and enable it by
+                default, as soon as other options are available. *)
+             `Ok (config cmdname true ()))
         $ const cmdname $ detect $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man )
 
@@ -110,7 +111,7 @@ let verify_cmd =
   ( Term.(
       ret
         (const (fun format loadpath files ->
-             `Ok (List.iter ~f:(Prove.prove format loadpath) files))
+           `Ok (List.iter ~f:(Verify.do_verify format loadpath) files))
         $ format $ loadpath $ files)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 

src/prove.ml

-open Base
-
-let () = Language.register ()
-
-let create_env loadpath =
-  let conf = Detection.detect () in
-  let stdlib = Stdlib_path.Sites.stdlib in
-  ( Why3.Env.create_env
-      (loadpath @ stdlib @ Why3.Whyconf.loadpath (Why3.Whyconf.get_main conf)),
-    conf )
-
-let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
-
-let prove format loadpath file =
-  let env, config = create_env loadpath in
-  let _, m =
-    match file with
-    | "-" ->
-        ( "stdin",
-          Why3.Env.read_channel ?format Why3.Env.base_language env "stdin"
-            Caml.stdin )
-    | fname ->
-        let mlw_files, _ =
-          Why3.Env.read_file ?format Why3.Env.base_language env fname
-        in
-        (fname, mlw_files)
-  in
-  Why3.Wstdlib.Mstr.iter
-    (fun _ th ->
-      let l = Why3.Task.split_theory th None None in
-      let prover = Why3.Whyconf.filter_one_prover config altergo in
-      let driver =
-        Why3.Whyconf.load_driver (Why3.Whyconf.get_main config) env prover
-      in
-      List.iter l ~f:(Fmt.pr "%a" (Why3.Driver.print_task driver)))
-    m

src/verify.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Base
+module Format = Caml.Format
+
+let () = Language.register ()
+
+let create_env loadpath =
+  let config = Detection.detect () in
+  let stdlib = Dirs.Sites.stdlib in
+
+  let open Why3 in
+  ( Env.create_env
+      (loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
+    config )
+
+let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
+
+let do_verify format loadpath file =
+  let open Why3 in
+  let env, config = create_env loadpath in
+  let _, mstr_theory =
+    match file with
+    | "-" ->
+      ("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
+    | filename ->
+      let mlw_files, _ = Env.(read_file ?format base_language env filename) in
+      (filename, mlw_files)
+  in
+  Wstdlib.Mstr.iter
+    (fun _ theory ->
+      let tasks = Task.split_theory theory None None in
+      let prover = Whyconf.filter_one_prover config altergo in
+      let driver = Whyconf.(load_driver (get_main config) env prover) in
+      List.iter tasks ~f:(Format.printf "%a" (Driver.print_task driver)))
+    mstr_theory

stdlib/caisar.mlw

 theory NNet
-       use ieee_float.Float64
-       type input_type = t
+  use ieee_float.Float64
+  type input_type = t
 end