[interpretation] A pass of code formatting.

bin/dune

@@ -3,5 +3,4 @@
  (section bin)
  (files
   (findmodule.py as findmodule.py)
-  (nnenum.sh as nnenum.sh))
-)
+  (nnenum.sh as nnenum.sh)))

lib/onnx/dune

@@ -5,7 +5,10 @@
  (synopsis "ONNX parser for CAISAR"))
 
 (rule
- (deps onnx_protoc.proto generate_onnx_interface.sh (package ocaml-protoc-plugin))
+ (deps
+  onnx_protoc.proto
+  generate_onnx_interface.sh
+  (package ocaml-protoc-plugin))
  (targets onnx_protoc.ml)
  (action
   (run ./generate_onnx_interface.sh)))

src/interpretation.ml

@@ -118,13 +118,15 @@ let interpret_task ~cwd env task =
   Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
     f print_caisar_op caisar_env
 
-let interpret ?debug ?format ~loadpath (s : Verification.File.t) =
+let interpret ?debug ?format ~loadpath file =
   let cwd =
-    match s with Stdin -> Unix.getcwd () | File s -> Caml.Filename.dirname s
+    match file with
+    | Verification.File.Stdin -> Unix.getcwd ()
+    | File s -> Caml.Filename.dirname s
     | JSON _ -> Unix.getcwd () (*todo *)
   in
   let env, _config, mstr_theory =
-    Verification.open_file ?debug ?format ~loadpath s
+    Verification.open_file ?debug ?format ~loadpath file
   in
   Wstdlib.Mstr.iter
     (fun _ theory ->

src/main.ml

@@ -261,19 +261,18 @@ 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 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 verify_cmd =
   let cmdname = "verify" in

tests/dune

@@ -11,6 +11,5 @@
   bin/cvc5
   bin/nnenum.sh
   filter_tmpdir.sh
-  (glob_files "datasets/a/*")
- )
+  (glob_files "datasets/a/*"))
  (package caisar))