From fa582037fa6e4db96147d1cbefc581ac559a5d94 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 2 Nov 2022 12:14:34 +0100
Subject: [PATCH] Rework and prepare cmdline to accept new command.
---
src/main.ml | 75 ++++++++++++++++++++++++-----------------------------
1 file changed, 34 insertions(+), 41 deletions(-)
diff --git a/src/main.ml b/src/main.ml
index 9afb6b4..6b22ab7 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -158,7 +158,7 @@ let config_cmd =
ret
(const (fun detect _ ->
if not detect
- then `Help (`Pager, Some "config")
+ then `Help (`Pager, Some cmdname)
else
(* TODO: Do not only check for [detect], and enable it by default,
as soon as other options are available. *)
@@ -167,47 +167,43 @@ let config_cmd =
in
Cmd.v info term
+let memlimit =
+ let doc =
+ "Memory limit. $(docv) is intended in megabytes (MB) by default, but \
+ gigabytes (GB) and terabytes (TB) may also be specified instead."
+ in
+ Arg.(
+ value & opt (some string) None & info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
+
+let timelimit =
+ let doc =
+ "Time limit. $(docv) is intended in seconds (s) by default, but minutes \
+ (m) and hours (h) may also be specified instead."
+ in
+ Arg.(
+ value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
+
+let format =
+ let doc = "File format." in
+ Arg.(value & opt (some string) None & info [ "format" ] ~doc)
+
+let loadpath =
+ let doc = "Additional loadpath." in
+ Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
+
let verify_cmd =
let cmdname = "verify" in
- let doc = "Property verification using external provers." in
let info =
+ let doc = "Property verification using external provers." in
Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
~doc
~man:[ `S Manpage.s_description; `P doc ]
in
let term =
let files =
- let doc = "Files to verify." in
+ let doc = "File to verify." in
let file_or_stdin = Verification.File.(of_string, pretty) in
- Arg.(value & pos_all file_or_stdin [] & info [] ~doc)
- in
- let format =
- let doc = "File format." in
- Arg.(value & opt (some string) None & info [ "format" ] ~doc)
- in
- let loadpath =
- let doc = "Additional loadpath." in
- Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
- in
- let memlimit =
- let doc =
- "Memory limit. $(docv) is intended in megabytes (MB) by default, but \
- gigabytes (GB) and terabytes (TB) may also be specified instead."
- in
- Arg.(
- value
- & opt (some string) None
- & info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
- in
- let timelimit =
- let doc =
- "Time limit. $(docv) is intended in seconds (s) by default, but \
- minutes (m) and hours (h) may also be specified instead."
- in
- Arg.(
- value
- & opt (some string) None
- & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
+ Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
in
let prover =
let all_provers = Prover.list_available () in
@@ -227,15 +223,12 @@ let verify_cmd =
Arg.(value & opt (some file) None & info [ "dataset-csv" ] ~doc)
in
Term.(
- ret
- (const
- (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
- `Ok
- (exec_cmd cmdname (fun () ->
- verify format loadpath memlimit timelimit prover dataset_csv
- files)))
- $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv
- $ files $ setup_logs))
+ const
+ (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
+ exec_cmd cmdname (fun () ->
+ verify format loadpath memlimit timelimit prover dataset_csv files))
+ $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv $ files
+ $ setup_logs)
in
Cmd.v info term
--
GitLab