From 85eb40678ff902571eb3e15f387472dd940d147b Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Sun, 25 Jul 2021 18:23:28 +0200
Subject: [PATCH] Some rework and plug config command in with autodection.
---
src/{detection.ml => autodetection.ml} | 4 ++--
src/language.ml | 12 ++++++----
src/main.ml | 33 +++++++++++++++++++-------
src/{verify.ml => verification.ml} | 4 ++--
tests/autodetect.t | 3 +++
tests/simple.t | 2 +-
6 files changed, 40 insertions(+), 18 deletions(-)
rename src/{detection.ml => autodetection.ml} (93%)
rename src/{verify.ml => verification.ml} (93%)
create mode 100644 tests/autodetect.t
diff --git a/src/detection.ml b/src/autodetection.ml
similarity index 93%
rename from src/detection.ml
rename to src/autodetection.ml
index c4fa222a..2cab84d4 100644
--- a/src/detection.ml
+++ b/src/autodetection.ml
@@ -16,9 +16,9 @@ let rec lookup_file dirs filename =
let file = Caml.Filename.concat dir filename in
if Sys.file_exists file then file else lookup_file dirs filename
-let detect () =
+let autodetect ~debug () =
let open Why3 in
- Debug.set_flag Why3.Autodetection.debug;
+ if debug then Debug.set_flag 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
diff --git a/src/language.ml b/src/language.ml
index d5a06063..12c379e1 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -6,18 +6,20 @@
open Base
-(* Register neural network formats. *)
+(* -- Register neural network format. *)
let nnet_parser env _ filename _ =
let open Why3 in
- let nnet = Pmodule.read_module env [ "caisar" ] "NNet" in
- let nnet_input_type =
- Ty.ty_app Theory.(ns_find_ts nnet.mod_theory.th_export [ "input_type" ]) []
- in
let header = Nnet.parse filename in
match header with
| Error s -> Loc.errorm "%s" s
| Ok header ->
+ let nnet = Pmodule.read_module env [ "caisar" ] "NNet" in
+ let nnet_input_type =
+ Ty.ty_app
+ Theory.(ns_find_ts nnet.mod_theory.th_export [ "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
diff --git a/src/main.ml b/src/main.ml
index 81d0a2b3..fbcfe607 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -10,7 +10,7 @@ module Format = Caml.Format
let caisar = "caisar"
-(* Logs. *)
+(* -- Logs. *)
let pp_header =
let x =
@@ -40,13 +40,30 @@ let setup_logs =
in
Term.(const setup_log $ Logs_cli.level ())
-(* Commands. *)
+(* -- Commands. *)
-let config cmd detect () =
- Logs.debug (fun m -> m "Command `%s'." cmd);
- if detect then Logs.app (fun m -> m "Automatic detection.")
+let config detect () =
+ if detect
+ then begin
+ Logs.debug (fun m -> m "Automatic detection.");
+ let config = Autodetection.autodetect ~debug:false () in
+ let open Why3 in
+ let provers = Whyconf.get_provers config in
+ Logs.app (fun m ->
+ m "@[<v>%a@]"
+ (Pp.print_iter2 Whyconf.Mprover.iter Pp.newline Pp.nothing
+ Whyconf.print_prover Pp.nothing)
+ provers)
+ end
-(* Command line. *)
+let verify format loadpath files =
+ List.iter ~f:(Verification.verify format loadpath) files
+
+let exec_cmd cmdname cmd =
+ Logs.debug (fun m -> m "Command `%s'." cmdname);
+ cmd ()
+
+(* -- Command line. *)
let config_cmd =
let cmdname = "config" in
@@ -83,7 +100,7 @@ let config_cmd =
else
(* TODO: Do not only check for [detect], and enable it by
default, as soon as other options are available. *)
- `Ok (config cmdname true ()))
+ `Ok (exec_cmd cmdname (fun () -> config true ())))
$ const cmdname $ detect $ setup_logs)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man )
@@ -111,7 +128,7 @@ let verify_cmd =
( Term.(
ret
(const (fun format loadpath files ->
- `Ok (List.iter ~f:(Verify.do_verify format loadpath) files))
+ `Ok (exec_cmd cmdname (fun () -> verify format loadpath files)))
$ format $ loadpath $ files)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
diff --git a/src/verify.ml b/src/verification.ml
similarity index 93%
rename from src/verify.ml
rename to src/verification.ml
index 3aa60d7b..f4ba6da9 100644
--- a/src/verify.ml
+++ b/src/verification.ml
@@ -10,7 +10,7 @@ module Format = Caml.Format
let () = Language.register ()
let create_env loadpath =
- let config = Detection.detect () in
+ let config = Autodetection.autodetect ~debug:true () in
let stdlib = Dirs.Sites.stdlib in
let open Why3 in
@@ -20,7 +20,7 @@ let create_env loadpath =
let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
-let do_verify format loadpath file =
+let verify format loadpath file =
let open Why3 in
let env, config = create_env loadpath in
let _, mstr_theory =
diff --git a/tests/autodetect.t b/tests/autodetect.t
new file mode 100644
index 00000000..c391f46e
--- /dev/null
+++ b/tests/autodetect.t
@@ -0,0 +1,3 @@
+Test verify
+ $ caisar config -d
+ [caisar] Alt-Ergo 2.4.0
diff --git a/tests/simple.t b/tests/simple.t
index 2fd8bba5..567c187e 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -1,4 +1,4 @@
-Test help
+Test verify
$ caisar verify -L . --format whyml - <<EOF
> theory T
> use TestNetwork.AsTuple
--
GitLab