Skip to content

Commit 5c91aa2

Browse files
filipeomfilipeom
committed
Make settings of cli commands a concrete type
Making cli command settings a concrete type makes it easier to then derive serializers to yaml/toml as well as the cmdliner parsers.
1 parent 723ece2 commit 5c91aa2

File tree

5 files changed

+98
-64
lines changed

5 files changed

+98
-64
lines changed

‎src/bin/cli.ml‎

Lines changed: 54 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -62,62 +62,68 @@ let from_file =
6262

6363
let version = Cmd_version.version
6464

65-
let cmd_run =
66-
let info =
67-
let doc =
68-
"Runs one or more scripts using. Also supports directory inputs"
65+
let commands =
66+
let open Term.Syntax in
67+
let cmd_run =
68+
let info =
69+
let doc =
70+
"Runs one or more scripts using. Also supports directory inputs"
71+
in
72+
Cmd.info ~version "run" ~doc
6973
in
70-
Cmd.info ~version "run" ~doc
71-
in
72-
let term =
73-
let open Term.Syntax in
74-
let+ debug
75-
and+ dry
76-
and+ print_statistics
77-
and+ no_strict_status
78-
and+ solver_type
79-
and+ solver_mode
80-
and+ from_file
81-
and+ filenames in
82-
Cmd_run.run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
83-
~solver_mode ~from_file ~filenames
74+
let term =
75+
let+ debug
76+
and+ dry
77+
and+ print_statistics
78+
and+ no_strict_status
79+
and+ solver_type
80+
and+ solver_mode
81+
and+ from_file
82+
and+ filenames in
83+
let settings =
84+
Settings.Run.make ~debug ~dry ~print_statistics ~no_strict_status
85+
~solver_type ~solver_mode ?from_file filenames
86+
in
87+
Cmd_run.run settings
88+
in
89+
Cmd.v info term
8490
in
85-
Cmd.v info term
8691

87-
let cmd_to_smt2 =
88-
let info =
89-
let doc = "Convert .smtml into .smt2" in
90-
Cmd.info ~version "to-smt2" ~doc
91-
in
92-
let term =
93-
let open Term.Syntax in
94-
let+ debug
95-
and+ solver_type
96-
and+ filename in
97-
Cmd_to_smt2.run ~debug ~solver_type ~filename
92+
let cmd_to_smt2 =
93+
let info =
94+
let doc = "Convert .smtml into .smt2" in
95+
Cmd.info ~version "to-smt2" ~doc
96+
in
97+
let term =
98+
let+ debug
99+
and+ solver_type
100+
and+ filename in
101+
let settings = Settings.To_smt2.make ~debug ~solver_type filename in
102+
Cmd_to_smt2.run settings
103+
in
104+
Cmd.v info term
98105
in
99-
Cmd.v info term
100106

101-
let cmd_to_smtml =
102-
let info =
103-
let doc = "Print/Format the content of an .smtml file" in
104-
Cmd.info ~version "to-smtml" ~doc
105-
in
106-
let term =
107-
let open Term.Syntax in
108-
let+ filename in
109-
Cmd_to_smt2.run_to_smtml ~filename
107+
let cmd_to_smtml =
108+
let info =
109+
let doc = "Print/Format the content of an .smtml file" in
110+
Cmd.info ~version "to-smtml" ~doc
111+
in
112+
let term =
113+
let+ filename in
114+
Cmd_to_smt2.run_to_smtml ~filename
115+
in
116+
Cmd.v info term
110117
in
111-
Cmd.v info term
112118

113-
let cmd_version =
114-
let info =
115-
let doc = "Print smtml version and linked libraries" in
116-
Cmd.info ~version "version" ~doc
119+
let cmd_version =
120+
let info =
121+
let doc = "Print smtml version and linked libraries" in
122+
Cmd.info ~version "version" ~doc
123+
in
124+
let term = Term.(const Cmd_version.run $ const ()) in
125+
Cmd.v info term
117126
in
118-
let term = Term.(const Cmd_version.run $ const ()) in
119-
Cmd.v info term
120127

121-
let commands =
122128
let info = Cmd.info ~version "smtml" in
123129
Cmd.group info [ cmd_run; cmd_to_smt2; cmd_to_smtml; cmd_version ]

‎src/bin/cmd_run.ml‎

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,12 @@ let parse_file filename =
2525
in
2626
List.rev files
2727

28-
let run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
29-
~solver_mode ~from_file ~filenames =
30-
if debug then Logs.Src.set_level Log.src (Some Logs.Debug);
28+
let run (s : Settings.Run.t) =
29+
(* ~debug ~dry ~print_statistics ~no_strict_status ~solver_type *)
30+
(* ~solver_mode ~from_file ~filenames = *)
31+
if s.debug then Logs.Src.set_level Log.src (Some Logs.Debug);
3132
Logs.set_reporter @@ Logs.format_reporter ();
32-
let module Solver = (val get_solver debug solver_type solver_mode) in
33+
let module Solver = (val get_solver s.debug s.solver_type s.solver_mode) in
3334
let module Interpret = Interpret.Make (Solver) in
3435
let total_tests = ref 0 in
3536
let total_t = ref 0. in
@@ -40,7 +41,7 @@ let run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
4041
incr total_tests;
4142
let start_t = Unix.gettimeofday () in
4243
Fun.protect ~finally:(fun () ->
43-
if print_statistics then (
44+
if s.print_statistics then (
4445
let exec_t = Unix.gettimeofday () -. start_t in
4546
total_t := !total_t +. exec_t;
4647
Log.app (fun m -> m "Run %a in %.06f" Fpath.pp file exec_t) ) )
@@ -50,8 +51,9 @@ let run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
5051
with Parse.Syntax_error err -> Error (`Parsing_error (file, err))
5152
in
5253
match ast with
53-
| Ok _ when dry -> state
54-
| Ok ast -> Some (Interpret.start ?state ast ~no_strict_status)
54+
| Ok _ when s.dry -> state
55+
| Ok ast ->
56+
Some (Interpret.start ?state ast ~no_strict_status:s.no_strict_status)
5557
| Error (`Parsing_error ((fpath, err_msg) as err)) ->
5658
Log.err (fun k -> k "%a: %s" Fpath.pp fpath err_msg);
5759
incr exception_count;
@@ -83,16 +85,16 @@ let run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
8385
prev_state )
8486
in
8587
let _ =
86-
match from_file with
87-
| None -> List.fold_left run_path None filenames
88+
match s.from_file with
89+
| None -> List.fold_left run_path None s.filenames
8890
| Some file -> (
8991
match parse_file file with
9092
| Error (`Msg err) ->
9193
Log.err (fun k -> k "%s" err);
9294
None
9395
| Ok files -> List.fold_left run_file None files )
9496
in
95-
if print_statistics then Log.app (fun k -> k "total time: %.06f" !total_t);
97+
if s.print_statistics then Log.app (fun k -> k "total time: %.06f" !total_t);
9698
let write_exception_log =
9799
let open Smtml_prelude.Result in
98100
function

‎src/bin/cmd_to_smt2.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
open Smtml
22

3-
let run ~debug ~solver_type ~filename =
3+
let run (settings : Settings.To_smt2.t) =
44
let module Mappings : Mappings_intf.S_with_fresh =
5-
(val Solver_type.to_mappings solver_type)
5+
(val Solver_type.to_mappings settings.solver_type)
66
in
7-
Mappings.set_debug debug;
8-
let ast = Parse.from_file filename in
7+
Mappings.set_debug settings.debug;
8+
let ast = Parse.from_file settings.filename in
99
let assertions =
1010
List.filter_map (function Ast.Assert e -> Some e | _ -> None) ast
1111
in
12-
let name = Fpath.to_string @@ Fpath.base filename in
12+
let name = Fpath.to_string @@ Fpath.base settings.filename in
1313
Fmt.pr "%a" (Mappings.Smtlib.pp ~name ?logic:None ?status:None) assertions
1414

1515
let run_to_smtml ~filename =

‎src/bin/dune‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
(package smtml)
33
(name main)
44
(public_name smtml)
5-
(libraries cmdliner dune-build-info smtml)
5+
(libraries cmdliner dune-build-info ppx_deriving smtml)
6+
(preprocess
7+
(pps ppx_deriving.make))
68
(instrumentation
79
(backend bisect_ppx)))

‎src/bin/settings.ml‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
(* We want these types for settings so that we can derive serializers for yaml/toml as well as cmdliner in the future *)
2+
3+
module Run = struct
4+
type t =
5+
{ debug : bool
6+
; dry : bool
7+
; print_statistics : bool
8+
; no_strict_status : bool
9+
; solver_type : Smtml.Solver_type.t
10+
; solver_mode : Smtml.Solver_mode.t
11+
; from_file : Fpath.t option
12+
; filenames : Fpath.t list [@main]
13+
}
14+
[@@deriving make]
15+
end
16+
17+
module To_smt2 = struct
18+
type t =
19+
{ debug : bool
20+
; solver_type : Smtml.Solver_type.t
21+
; filename : Fpath.t [@main]
22+
}
23+
[@@deriving make]
24+
end

0 commit comments

Comments
 (0)