Little rework.

src/main.ml

@@ -97,32 +97,32 @@ let config_cmd =
   in
   ( Term.(
       ret
-        (const (fun cmdname detect _ ->
+        (const (fun 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 (exec_cmd cmdname (fun () -> config true ())))
-        $ const cmdname $ detect $ setup_logs)),
+        $ detect $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man )
 
 let verify_cmd =
   let cmdname = "verify" in
   let files =
-    let doc = "Files to verify" in
+    let doc = "Files to verify." in
     Arg.(value & pos_all string [] & info [] ~doc)
   in
   let format =
-    let doc = "File format" in
+    let doc = "File format." in
     Arg.(value & opt (some string) None & info [ "format" ] ~doc)
   in
   let loadpath =
-    let doc = "Additional loadpath" in
+    let doc = "Additional loadpath." in
     Arg.(value & opt_all string [] & info [ "L" ] ~doc)
   in
   let prover =
-    let doc = "Prover to use" in
+    let doc = "Prover to use." in
     Arg.(required & opt (some string) None & info [ "p"; "prover" ] ~doc)
   in
   let doc =

src/printer/pyrat.ml

@@ -85,14 +85,12 @@ let rec print_tdecl info fmt task =
     | Use _ | Clone _ -> ()
     | Meta (meta, l) when Theory.meta_equal meta Transformations.meta_input -> (
       match l with
-      | [ MAls ls; MAint i ] ->
-        Why3.Term.Hls.add info.variables ls (Fmt.str "x%i" i)
+      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "x%i" i)
       | _ -> assert false)
     | Meta (meta, l) when Theory.meta_equal meta Transformations.meta_output
       -> (
       match l with
-      | [ MAls ls; MAint i ] ->
-        Why3.Term.Hls.add info.variables ls (Fmt.str "y%i" i)
+      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "y%i" i)
       | _ -> assert false)
     | Meta (_, _) -> ()
     | Decl d -> print_decl info fmt d)
@@ -102,7 +100,7 @@ let print_task args ?old:_ fmt task =
   let info =
     {
       info_syn = Discriminate.get_syntax_map task;
-      variables = Why3.Term.Hls.create 10;
+      variables = Term.Hls.create 10;
     }
   in
   Printer.print_prelude fmt args.Printer.prelude;

src/transformations.ml

@@ -21,62 +21,60 @@ let meta_output =
 let meta_nn_filename =
   Why3.Theory.(
     register_meta_excl "caisar_nnet_or_onnx"
-      ~desc:"Indicates the file containing the network" [ MTstring ])
+      ~desc:"Indicates the filename of the network" [ MTstring ])
 
 (* Retrieve the (input) variables appearing, as arguments, after an 'nnet_apply'
    symbol. *)
 let get_input_variables =
-  let rec aux acc (term : Why3.Term.term) =
+  let open Why3 in
+  let rec aux acc (term : Term.term) =
     match term.t_node with
-    | Why3.Term.Tapp (ls, args) -> (
+    | Term.Tapp (ls, args) -> (
       match Language.lookup_loaded_nnets ls with
       | None -> acc
       | Some _ ->
         let add i acc = function
-          | { Why3.Term.t_node = Tapp (vs, []); _ } ->
-            Why3.Term.Mls.add vs i acc
+          | { Term.t_node = Tapp (vs, []); _ } -> Term.Mls.add vs i acc
           | arg ->
             invalid_arg
-              (Fmt.str "No direct variable in application: %a"
-                 Why3.Pretty.print_term arg)
+              (Fmt.str "No direct variable in application: %a" Pretty.print_term
+                 arg)
         in
         List.foldi ~init:acc ~f:add args)
-    | _ -> Why3.Term.t_fold aux acc term
+    | _ -> Term.t_fold aux acc term
   in
-  Why3.Trans.fold_decl
-    (fun decl acc -> Why3.Decl.decl_fold aux acc decl)
-    Why3.Term.Mls.empty
+  Trans.fold_decl (fun decl acc -> Decl.decl_fold aux acc decl) Term.Mls.empty
 
 (* Create logic symbols for output variables and simplify the formula. *)
 (* TODO: [Reduction_engine] is probably an overkill and should be replaced. *)
 let simplify_goal env input_variables =
-  let rec aux meta hls (term : Why3.Term.term) =
+  let open Why3 in
+  let rec aux meta hls (term : Term.term) =
     match term.t_node with
-    | Why3.Term.Tapp (ls, _) -> (
+    | Term.Tapp (ls, _) -> (
       match Language.lookup_loaded_nnets ls with
-      | None -> Why3.Term.t_map (aux meta hls) term
+      | None -> Term.t_map (aux meta hls) term
       | Some nnet ->
         meta := nnet.filename :: !meta;
         let outputs =
           List.init nnet.nb_outputs ~f:(fun i ->
-            let open Why3 in
             let id = Ident.id_fresh "y" in
             let ls = Term.create_fsymbol id [] nnet.ty_data in
-            hls := (Why3.Decl.create_param_decl ls, ls, i) :: !hls;
+            hls := (Decl.create_param_decl ls, ls, i) :: !hls;
             Term.fs_app ls [] nnet.ty_data)
         in
-        Why3.Term.t_tuple outputs)
-    | _ -> Why3.Term.t_map (aux meta hls) term
+        Term.t_tuple outputs)
+    | _ -> Term.t_map (aux meta hls) term
   in
-  Why3.Trans.fold
+  Trans.fold
     (fun task_hd acc ->
       match task_hd.task_decl.td_node with
-      | Use _ | Clone _ | Meta _ -> Why3.Task.add_tdecl acc task_hd.task_decl
+      | Use _ | Clone _ | Meta _ -> Task.add_tdecl acc task_hd.task_decl
       | Decl { d_node = Dparam ls; _ } -> (
-        let task = Why3.Task.add_tdecl acc task_hd.task_decl in
-        match Why3.Term.Mls.find_opt ls input_variables with
+        let task = Task.add_tdecl acc task_hd.task_decl in
+        match Term.Mls.find_opt ls input_variables with
         | None -> task
-        | Some pos -> Why3.Task.add_meta task meta_input [ MAls ls; MAint pos ])
+        | Some pos -> Task.add_meta task meta_input [ MAls ls; MAint pos ])
       | Decl decl ->
         let meta = ref [] in
         let hls = ref [] in
@@ -87,35 +85,34 @@ let simplify_goal env input_variables =
           else
             let known =
               List.fold !hls ~init:task_hd.task_known ~f:(fun acc (d, _, _) ->
-                Why3.Decl.known_add_decl acc d)
+                Decl.known_add_decl acc d)
             in
             let engine =
-              Why3.Reduction_engine.create
+              Reduction_engine.create
                 {
                   compute_defs = false;
                   compute_builtin = true;
-                  compute_def_set = Why3.Term.Sls.empty;
+                  compute_def_set = Term.Sls.empty;
                 }
                 env known
             in
-            Why3.Reduction_engine.normalize ~limit:100 engine
-              Why3.Term.Mvs.empty term
+            Reduction_engine.normalize ~limit:100 engine Term.Mvs.empty term
         in
-        let decl = Why3.Decl.decl_map map decl in
+        let decl = Decl.decl_map map decl in
         let acc =
           List.fold !hls ~init:acc ~f:(fun acc (d, ls, i) ->
-            let task = Why3.Task.add_decl acc d in
-            Why3.Task.add_meta task meta_output [ MAls ls; MAint i ])
+            let task = Task.add_decl acc d in
+            Task.add_meta task meta_output [ MAls ls; MAint i ])
         in
         let acc =
           List.fold !meta ~init:acc ~f:(fun acc s ->
-            Why3.Task.add_meta acc meta_nn_filename [ MAstr s ])
+            Task.add_meta acc meta_nn_filename [ MAstr s ])
         in
-        Why3.Task.add_decl acc decl)
+        Task.add_decl acc decl)
     None
 
 let caisar_native_prover env =
-  Why3.Trans.seq [ Why3.Trans.bind get_input_variables (simplify_goal env) ]
+  Why3.(Trans.seq [ Trans.bind get_input_variables (simplify_goal env) ])
 
 let init () =
   Why3.Trans.register_env_transform

src/transformations.mli

@@ -14,4 +14,4 @@ val meta_output : Why3.Theory.meta
 (** Indicate the output position. *)
 
 val meta_nn_filename : Why3.Theory.meta
-(** The filename of the nnet or onnx *)
+(** The filename of the nnet or onnx model. *)

src/verification.ml

@@ -26,8 +26,8 @@ let call_prover ~limit prover driver task =
   let nn_file =
     match Task.on_meta_excl Transformations.meta_nn_filename task_prepared with
     | Some [ MAstr nn_file ] -> nn_file
-    | Some _ -> assert false
-    | None -> invalid_arg (Fmt.str "No neural network in the goal")
+    | Some _ -> assert false (* By construction of the meta. *)
+    | None -> invalid_arg (Fmt.str "No neural network model found in task")
   in
   let command = Re.replace_string nnet_or_onnx ~by:nn_file command in
   let prover_call =
@@ -45,12 +45,12 @@ let verify format loadpath prover file =
   let timeout = None in
   let steps = match steplimit with Some 0 -> None | _ -> steplimit in
   let limit =
-    let memlimit = Why3.Whyconf.memlimit (Why3.Whyconf.get_main config) in
-    let def = Why3.Call_provers.empty_limit in
+    let memlimit = Whyconf.(memlimit (get_main config)) in
+    let def = Call_provers.empty_limit in
     {
-      Why3.Call_provers.limit_time = Why3.Opt.get_def def.limit_time timeout;
-      Why3.Call_provers.limit_steps = Why3.Opt.get_def def.limit_time steps;
-      Why3.Call_provers.limit_mem = memlimit;
+      Call_provers.limit_time = Opt.get_def def.limit_time timeout;
+      Call_provers.limit_steps = Opt.get_def def.limit_time steps;
+      Call_provers.limit_mem = memlimit;
     }
   in
   let _, mstr_theory =