Make settings of cli commands a concrete type

dune-project

@@ -95,11 +95,6 @@
     :with-dev-setup
     (= "dev")))
   (ocamlformat :with-dev-setup)
-  (ppxlib
-   (and
-    (>= "0.35.0")
-    (< "0.36.0")
-    :with-dev-setup))
   (cohttp :with-dev-setup)
   (cohttp-lwt-unix :with-dev-setup)
   (extunix :with-dev-setup)

smtml.opam

@@ -43,7 +43,6 @@ depends: [
   "ounit2" {with-test}
   "benchpress" {with-dev-setup & = "dev"}
   "ocamlformat" {with-dev-setup}
-  "ppxlib" {>= "0.35.0" & < "0.36.0" & with-dev-setup}
   "cohttp" {with-dev-setup}
   "cohttp-lwt-unix" {with-dev-setup}
   "extunix" {with-dev-setup}
@@ -80,5 +79,4 @@ pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#4ba26c9e1d031765e799251480166af720638e6e"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#4ba26c9e1d031765e799251480166af720638e6e"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]
-  ["extunix.0.4.3" "git+https://github.com/filipeom/extunix.git#ff54e8cc7ec9cdc7171861d74d85f326dbcec62e"]
 ]

smtml.opam.template

@@ -3,5 +3,4 @@ pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#4ba26c9e1d031765e799251480166af720638e6e"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#4ba26c9e1d031765e799251480166af720638e6e"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]
-  ["extunix.0.4.3" "git+https://github.com/filipeom/extunix.git#ff54e8cc7ec9cdc7171861d74d85f326dbcec62e"]
 ]

src/bin/cli.ml

@@ -62,62 +62,68 @@ let from_file =
 
 let version = Cmd_version.version
 
-let cmd_run =
-  let info =
-    let doc =
-      "Runs one or more scripts using. Also supports directory inputs"
+let commands =
+  let open Term.Syntax in
+  let cmd_run =
+    let info =
+      let doc =
+        "Runs one or more scripts using. Also supports directory inputs"
+      in
+      Cmd.info ~version "run" ~doc
     in
-    Cmd.info ~version "run" ~doc
-  in
-  let term =
-    let open Term.Syntax in
-    let+ debug
-    and+ dry
-    and+ print_statistics
-    and+ no_strict_status
-    and+ solver_type
-    and+ solver_mode
-    and+ from_file
-    and+ filenames in
-    Cmd_run.run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
-      ~solver_mode ~from_file ~filenames
+    let term =
+      let+ debug
+      and+ dry
+      and+ print_statistics
+      and+ no_strict_status
+      and+ solver_type
+      and+ solver_mode
+      and+ from_file
+      and+ filenames in
+      let settings =
+        Settings.Run.make ~debug ~dry ~print_statistics ~no_strict_status
+          ~solver_type ~solver_mode ?from_file filenames
+      in
+      Cmd_run.run settings
+    in
+    Cmd.v info term
   in
-  Cmd.v info term
 
-let cmd_to_smt2 =
-  let info =
-    let doc = "Convert .smtml into .smt2" in
-    Cmd.info ~version "to-smt2" ~doc
-  in
-  let term =
-    let open Term.Syntax in
-    let+ debug
-    and+ solver_type
-    and+ filename in
-    Cmd_to_smt2.run ~debug ~solver_type ~filename
+  let cmd_to_smt2 =
+    let info =
+      let doc = "Convert .smtml into .smt2" in
+      Cmd.info ~version "to-smt2" ~doc
+    in
+    let term =
+      let+ debug
+      and+ solver_type
+      and+ filename in
+      let settings = Settings.To_smt2.make ~debug ~solver_type filename in
+      Cmd_to_smt2.run settings
+    in
+    Cmd.v info term
   in
-  Cmd.v info term
 
-let cmd_to_smtml =
-  let info =
-    let doc = "Print/Format the content of an .smtml file" in
-    Cmd.info ~version "to-smtml" ~doc
-  in
-  let term =
-    let open Term.Syntax in
-    let+ filename in
-    Cmd_to_smt2.run_to_smtml ~filename
+  let cmd_to_smtml =
+    let info =
+      let doc = "Print/Format the content of an .smtml file" in
+      Cmd.info ~version "to-smtml" ~doc
+    in
+    let term =
+      let+ filename in
+      Cmd_to_smt2.run_to_smtml ~filename
+    in
+    Cmd.v info term
   in
-  Cmd.v info term
 
-let cmd_version =
-  let info =
-    let doc = "Print smtml version and linked libraries" in
-    Cmd.info ~version "version" ~doc
+  let cmd_version =
+    let info =
+      let doc = "Print smtml version and linked libraries" in
+      Cmd.info ~version "version" ~doc
+    in
+    let term = Term.(const Cmd_version.run $ const ()) in
+    Cmd.v info term
   in
-  let term = Term.(const Cmd_version.run $ const ()) in
-  Cmd.v info term
 
-let commands =
   let info = Cmd.info ~version "smtml" in
   Cmd.group info [ cmd_run; cmd_to_smt2; cmd_to_smtml; cmd_version ]

src/bin/cmd_run.ml

@@ -25,11 +25,12 @@ let parse_file filename =
   in
   List.rev files
 
-let run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
-  ~solver_mode ~from_file ~filenames =
-  if debug then Logs.Src.set_level Log.src (Some Logs.Debug);
+let run (s : Settings.Run.t) =
+  (* ~debug ~dry ~print_statistics ~no_strict_status ~solver_type *)
+  (*   ~solver_mode ~from_file ~filenames = *)
+  if s.debug then Logs.Src.set_level Log.src (Some Logs.Debug);
   Logs.set_reporter @@ Logs.format_reporter ();
-  let module Solver = (val get_solver debug solver_type solver_mode) in
+  let module Solver = (val get_solver s.debug s.solver_type s.solver_mode) in
   let module Interpret = Interpret.Make (Solver) in
   let total_tests = ref 0 in
   let total_t = ref 0. in
@@ -40,7 +41,7 @@ let run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
     incr total_tests;
     let start_t = Unix.gettimeofday () in
     Fun.protect ~finally:(fun () ->
-      if print_statistics then (
+      if s.print_statistics then (
         let exec_t = Unix.gettimeofday () -. start_t in
         total_t := !total_t +. exec_t;
         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
       with Parse.Syntax_error err -> Error (`Parsing_error (file, err))
     in
     match ast with
-    | Ok _ when dry -> state
-    | Ok ast -> Some (Interpret.start ?state ast ~no_strict_status)
+    | Ok _ when s.dry -> state
+    | Ok ast ->
+      Some (Interpret.start ?state ast ~no_strict_status:s.no_strict_status)
     | Error (`Parsing_error ((fpath, err_msg) as err)) ->
       Log.err (fun k -> k "%a: %s" Fpath.pp fpath err_msg);
       incr exception_count;
@@ -83,16 +85,16 @@ let run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
         prev_state )
   in
   let _ =
-    match from_file with
-    | None -> List.fold_left run_path None filenames
+    match s.from_file with
+    | None -> List.fold_left run_path None s.filenames
     | Some file -> (
       match parse_file file with
       | Error (`Msg err) ->
         Log.err (fun k -> k "%s" err);
         None
       | Ok files -> List.fold_left run_file None files )
   in
-  if print_statistics then Log.app (fun k -> k "total time: %.06f" !total_t);
+  if s.print_statistics then Log.app (fun k -> k "total time: %.06f" !total_t);
   let write_exception_log =
     let open Smtml_prelude.Result in
     function

src/bin/cmd_to_smt2.ml

@@ -1,15 +1,15 @@
 open Smtml
 
-let run ~debug ~solver_type ~filename =
+let run (settings : Settings.To_smt2.t) =
   let module Mappings : Mappings_intf.S_with_fresh =
-    (val Solver_type.to_mappings solver_type)
+    (val Solver_type.to_mappings settings.solver_type)
   in
-  Mappings.set_debug debug;
-  let ast = Parse.from_file filename in
+  Mappings.set_debug settings.debug;
+  let ast = Parse.from_file settings.filename in
   let assertions =
     List.filter_map (function Ast.Assert e -> Some e | _ -> None) ast
   in
-  let name = Fpath.to_string @@ Fpath.base filename in
+  let name = Fpath.to_string @@ Fpath.base settings.filename in
   Fmt.pr "%a" (Mappings.Smtlib.pp ~name ?logic:None ?status:None) assertions
 
 let run_to_smtml ~filename =

src/bin/dune

@@ -2,6 +2,8 @@
  (package smtml)
  (name main)
  (public_name smtml)
- (libraries cmdliner dune-build-info smtml)
+ (libraries cmdliner dune-build-info ppx_deriving smtml)
+ (preprocess
+  (pps ppx_deriving.make))
  (instrumentation
   (backend bisect_ppx)))

src/bin/settings.ml

@@ -0,0 +1,24 @@
+(* We want these types for settings so that we can derive serializers for yaml/toml as well as cmdliner in the future *)
+
+module Run = struct
+  type t =
+    { debug : bool
+    ; dry : bool
+    ; print_statistics : bool
+    ; no_strict_status : bool
+    ; solver_type : Smtml.Solver_type.t
+    ; solver_mode : Smtml.Solver_mode.t
+    ; from_file : Fpath.t option
+    ; filenames : Fpath.t list [@main]
+    }
+  [@@deriving make]
+end
+
+module To_smt2 = struct
+  type t =
+    { debug : bool
+    ; solver_type : Smtml.Solver_type.t
+    ; filename : Fpath.t [@main]
+    }
+  [@@deriving make]
+end