diff --git a/src/main.ml b/src/main.ml
index 3183ba7d2d2ff88b3fdb0823671b7bf93daabb30..f41eb638ac6f26798c86f819785dacc5ef045a9b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -202,44 +202,6 @@ let exec_cmd cmdname cmd =
(* -- Command line. *)
-let config_cmd =
- let cmdname = "config" in
- let info =
- let doc = Fmt.str "%s configuration." caisar in
- let exits = Cmd.Exit.defaults in
- let man =
- [
- `S Manpage.s_description;
- `P (Fmt.str "Handle the configuration of %s." caisar);
- ]
- in
- Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man
- in
- let term =
- let detect =
- let doc = "Detect solvers in \\$PATH." in
- Arg.(value & flag & info [ "d"; "detect" ] ~doc)
- in
- Term.(
- ret
- (const (fun detect _ ->
- if not detect
- 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. *)
- `Ok (exec_cmd cmdname (fun () -> config true ())))
- $ detect $ setup_logs))
- in
- Cmd.v info term
-
-let define_constants =
- let doc = "Define a declared constant with the given value." in
- Arg.(
- value
- & opt_all (Arg.pair ~sep:':' string string) []
- & info [ "define"; "def" ] ~doc ~docv:"name:value")
-
let memlimit =
let doc =
"Memory limit. $(docv) is intended in megabytes (MB) by default, but \
@@ -256,18 +218,20 @@ let timelimit =
Arg.(
value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
-let loadpath =
- let doc = "Additional loadpath." in
- Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
-
-let format =
- let doc = "File format." in
- Arg.(value & opt (some string) None & info [ "format" ] ~doc)
-
-let files =
- let doc = "File to verify." in
- let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
- Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
+let prover =
+ let all_provers = Prover.list_available () in
+ let doc =
+ Fmt.str "Prover to use. Support is provided for the following $(docv)s: %a."
+ (Fmt.list ~sep:Fmt.comma Fmt.string)
+ (List.map ~f:Prover.to_string all_provers)
+ in
+ let provers =
+ Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
+ in
+ Arg.(
+ required
+ & opt (some provers) None
+ & info [ "p"; "prover" ] ~doc ~docv:"PROVER")
let verify_cmd =
let cmdname = "verify" in
@@ -277,21 +241,13 @@ let verify_cmd =
~doc
~man:[ `S Manpage.s_description; `P doc ]
in
- let prover =
- let all_provers = Prover.list_available () in
- let doc =
- Fmt.str
- "Prover to use. Support is provided for the following $(docv)s: %a."
- (Fmt.list ~sep:Fmt.comma Fmt.string)
- (List.map ~f:Prover.to_string all_provers)
- in
- let provers =
- Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
- in
- Arg.(
- required
- & opt (some provers) None
- & info [ "p"; "prover" ] ~doc ~docv:"PROVER")
+ let loadpath =
+ let doc = "Additional loadpath." in
+ Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
+ in
+ let format =
+ let doc = "File format." in
+ Arg.(value & opt (some string) None & info [ "format" ] ~doc)
in
let prover_altern =
let doc = "Alternative prover configuration." in
@@ -301,29 +257,32 @@ let verify_cmd =
let doc = "Dataset $(docv) (CSV format only)." in
Arg.(value & opt (some file) None & info [ "dataset" ] ~doc ~docv:"FILE")
in
- let term =
+ let define_constants =
+ let doc = "Define a declared constant with the given value." in
+ Arg.(
+ value
+ & opt_all (Arg.pair ~sep:':' string string) []
+ & info [ "define"; "def" ] ~doc ~docv:"name:value")
+ in
+ let files =
+ let doc = "File(s) to verify." in
+ let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
+ Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
+ in
+ let verify_term =
+ let verify format loadpath memlimit timelimit prover prover_altern dataset
+ def_constants files () =
+ ignore
+ (verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover
+ ?prover_altern ~def_constants files)
+ in
Term.(
- const
- (fun
- format
- loadpath
- memlimit
- timelimit
- prover
- prover_altern
- dataset
- def_constants
- files
- _
- ->
- exec_cmd cmdname (fun () ->
- ignore
- (verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover
- ?prover_altern ~def_constants files)))
- $ format $ loadpath $ memlimit $ timelimit $ prover $ prover_altern
- $ dataset $ define_constants $ files $ setup_logs)
- in
- Cmd.v info term
+ const (fun _ -> exec_cmd cmdname)
+ $ setup_logs
+ $ (const verify $ format $ loadpath $ memlimit $ timelimit $ prover
+ $ prover_altern $ dataset $ define_constants $ files))
+ in
+ Cmd.v info verify_term
let verify_json_cmd =
let cmdname = "verify-json" in
@@ -346,55 +305,77 @@ let verify_json_cmd =
Arg.(
required & pos ~rev:true 0 (some file) None & info [] ~doc ~docv:"FILE")
in
- let term =
+ let verify_json_term =
+ let verify_json memlimit timelimit outfile json () =
+ verify_json ?memlimit ?timelimit ?outfile json
+ in
Term.(
- const (fun memlimit timelimit json outfile _ ->
- exec_cmd cmdname (fun () ->
- verify_json ?memlimit ?timelimit ?outfile json))
- $ memlimit $ timelimit $ json $ outfile $ setup_logs)
+ const (fun _ -> exec_cmd cmdname)
+ $ setup_logs
+ $ (const verify_json $ memlimit $ timelimit $ outfile $ json))
in
- Cmd.v info term
+ Cmd.v info verify_json_term
let verify_xgboost_cmd =
let cmdname = "verify-xgboost" in
let info =
- let doc = "EXPERIMENTAL: Property verification of xgboost file." in
+ let doc = "EXPERIMENTAL: Property verification of XGBoost file." in
Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
~doc
~man:[ `S Manpage.s_description; `P doc ]
in
- let prover =
- let all_provers = Prover.list_available () in
- let doc =
- Fmt.str
- "Prover to use. Support is provided for the following $(docv)s: %a."
- (Fmt.list ~sep:Fmt.comma Fmt.string)
- (List.map ~f:Prover.to_string all_provers)
- in
- let provers =
- Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
+ let xgboost =
+ let doc = "XGBoost model file in JSON format." in
+ Arg.(required & pos 0 (some file) None & info [] ~doc ~docv:"FILE")
+ in
+ let dataset =
+ let doc = "Dataset file (CSV, or SVM)." in
+ Arg.(required & pos 1 (some file) None & info [] ~doc ~docv:"FILE")
+ in
+ let verify_xgboost_term =
+ let verify_xgboost memlimit timelimit xgboost dataset prover () =
+ verify_xgboost ?memlimit ?timelimit xgboost dataset prover
in
- Arg.(
- required
- & opt (some provers) None
- & info [ "p"; "prover" ] ~doc ~docv:"PROVER")
- in
- let term =
- let xgboost =
- let doc = "xgboost json model file." in
- Arg.(required & pos 0 (some file) None & info [] ~doc ~docv:"FILE")
+ Term.(
+ const (fun _ -> exec_cmd cmdname)
+ $ setup_logs
+ $ (const verify_xgboost $ memlimit $ timelimit $ xgboost $ dataset
+ $ prover))
+ in
+ Cmd.v info verify_xgboost_term
+
+let config_cmd =
+ let cmdname = "config" in
+ let info =
+ let doc = Fmt.str "%s configuration." caisar in
+ let exits = Cmd.Exit.defaults in
+ let man =
+ [
+ `S Manpage.s_description;
+ `P (Fmt.str "Handle the configuration of %s." caisar);
+ ]
in
- let dataset =
- let doc = "dataset file (csv, or svm)." in
- Arg.(required & pos 1 (some file) None & info [] ~doc ~docv:"FILE")
+ Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man
+ in
+ let config_term =
+ let detect =
+ let doc = "Detect solvers in \\$PATH." in
+ Arg.(value & flag & info [ "d"; "detect" ] ~doc)
in
Term.(
- const (fun memlimit timelimit xgboost dataset prover _ ->
- exec_cmd cmdname (fun () ->
- verify_xgboost ?memlimit ?timelimit xgboost dataset prover))
- $ memlimit $ timelimit $ xgboost $ dataset $ prover $ setup_logs)
+ ret
+ (const (fun detect _ ->
+ if not detect
+ 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. *)
+ `Ok (exec_cmd cmdname (fun () -> config true ())))
+ $ detect $ setup_logs))
in
- Cmd.v info term
+ Cmd.v info config_term
+
+let default = Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ()))
let default_info =
let doc =
@@ -416,10 +397,8 @@ let default_info =
let exits = Cmd.Exit.defaults in
Cmd.info caisar ~version ~doc ~sdocs ~exits ~man
-let default_cmd = Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ()))
-
let () =
Logging.protect_main (fun () ->
- Cmd.group ~default:default_cmd default_info
+ Cmd.group ~default default_info
[ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ]
|> Cmd.eval ~catch:false |> Stdlib.exit)