From 5b68d2eb20b98e9c7630961391c6862b0df7fa83 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 1 Oct 2021 10:19:10 +0200
Subject: [PATCH] Some more style reworking.
---
.ocamlformat | 2 +-
src/language.mli | 10 ++++++++--
src/main.ml | 13 +++++--------
src/transformations.ml | 14 ++++++++++----
src/transformations.mli | 8 +++++++-
src/verification.ml | 3 +--
6 files changed, 32 insertions(+), 18 deletions(-)
diff --git a/.ocamlformat b/.ocamlformat
index a2874612..7523471a 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,5 +1,5 @@
version=0.19.0
-exp-grouping=preserve
+exp-grouping=parens
if-then-else=keyword-first
max-indent=2
wrap-comments=true
diff --git a/src/language.mli b/src/language.mli
index 23ef26ce..f1812f1d 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -1,3 +1,9 @@
+(**************************************************************************)
+(* *)
+(* 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. *)
diff --git a/src/main.ml b/src/main.ml
index 5e07bf7e..8d5bdaf6 100644
--- a/src/main.ml
+++ b/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.(
diff --git a/src/transformations.ml b/src/transformations.ml
index e8ceeb81..762bd9d6 100644
--- a/src/transformations.ml
+++ b/src/transformations.ml
@@ -1,15 +1,21 @@
+(**************************************************************************)
+(* *)
+(* 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 () =
diff --git a/src/transformations.mli b/src/transformations.mli
index 1d3779c2..0df41287 100644
--- a/src/transformations.mli
+++ b/src/transformations.mli
@@ -1,2 +1,8 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(**************************************************************************)
+
val init : unit -> unit
-(** register the transformations *)
+(** Register the transformations. *)
diff --git a/src/verification.ml b/src/verification.ml
index 624acb45..02f14d60 100644
--- a/src/verification.ml
+++ b/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
--
GitLab