[interpretation] Remove interpret command and integrate task interpretation into verification.

src/interpretation.ml

@@ -105,6 +105,8 @@ let print_caisar_op fmt caisar_env =
   Pp.print_iter2 Term.Hls.iter Pp.newline Pp.comma Pretty.print_ls pp_caisar_op
     fmt caisar_env.caisar_op_of_ls
 
+let _ = print_caisar_op
+
 let const_real_of_float value =
   let neg = Float.is_negative value in
   let value = Fmt.str "%.64f" (Float.abs value) in
@@ -532,21 +534,7 @@ let interpret_task ~cwd env task =
       caisar_env.caisar_op_of_ls task
   in
   let task = Task.(add_prop_decl task Pgoal g f) in
-  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 file =
-  let cwd =
-    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 file
-  in
-  Wstdlib.Mstr.iter
-    (fun _ theory ->
-      List.iter (Task.split_theory theory None None) ~f:(fun task ->
-        interpret_task ~cwd env task))
-    mstr_theory
+  (* Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task)
+     Pretty.print_term *)
+  (* f print_caisar_op caisar_env; *)
+  task

src/interpretation.mli

@@ -20,11 +20,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Base
+open Why3
 
-val interpret :
-  ?debug:bool ->
-  ?format:string ->
-  loadpath:string list ->
-  Verification.File.t ->
-  unit
+val interpret_task : cwd:string -> Env.env -> Task.task -> Task.task

src/main.ml

@@ -202,10 +202,6 @@ let verify_json ?memlimit ?timelimit ?outfile json =
       ~f:(record_verification_result jin.id verification_result)
   | _ -> failwith "Unexpected more than one theory from a JSON file"
 
-let interpret format loadpath files =
-  let debug = log_level_is_debug () in
-  List.iter ~f:(Interpretation.interpret ~debug ?format ~loadpath) files
-
 let verify_xgboost ?memlimit ?timelimit xgboost dataset prover =
   let memlimit = Option.map memlimit ~f:memlimit_of_string in
   let timelimit = Option.map timelimit ~f:timelimit_of_string in
@@ -362,24 +358,6 @@ let verify_json_cmd =
   in
   Cmd.v info term
 
-let interpret_cmd =
-  let cmdname = "interpret" in
-  let doc =
-    "Interpret the goal and print the strategy that will be executed."
-  in
-  let info =
-    Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
-      ~doc
-      ~man:[ `S Manpage.s_description; `P doc ]
-  in
-  let term =
-    Term.(
-      const (fun format loadpath files _ ->
-        exec_cmd cmdname (fun () -> interpret format loadpath files))
-      $ format $ loadpath $ files $ setup_logs)
-  in
-  Cmd.v info term
-
 let verify_xgboost_cmd =
   let cmdname = "verify-xgboost" in
   let info =
@@ -456,13 +434,7 @@ let () =
 let () =
   try
     Cmd.group ~default:default_cmd default_info
-      [
-        config_cmd;
-        verify_cmd;
-        verify_json_cmd;
-        interpret_cmd;
-        verify_xgboost_cmd;
-      ]
+      [ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ]
     |> Cmd.eval ~catch:false |> Caml.exit
   with exn when not (log_level_is_debug ()) ->
     Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)

src/verification.ml

@@ -247,7 +247,8 @@ let answer_generic limit config prover config_prover driver task =
   let additional_info = Generic None in
   (prover_answer, additional_info)
 
-let call_prover ?dataset ~limit config env prover config_prover driver task =
+let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
+    =
   let prover_answer, additional_info =
     match prover with
     | Prover.Saver -> answer_saver limit config env config_prover dataset task
@@ -256,6 +257,7 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
       let dataset = Unix.realpath (Option.value_exn dataset) in
       answer_dataset limit config env prover config_prover driver dataset task
     | Marabou | Pyrat | Nnenum ->
+      let task = Interpretation.interpret_task ~cwd env task in
       let task = Proof_strategy.apply_native_nn_prover env task in
       answer_generic limit config prover config_prover driver task
     | CVC5 ->
@@ -265,25 +267,22 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
   let id = Task.task_goal task in
   { id; prover_answer; additional_info }
 
-let open_file ?(debug = false) ?format ~loadpath file =
+let open_file ?format env file =
+  match file with
+  | File.Stdin ->
+    ( Unix.getcwd (),
+      Env.(read_channel ?format base_language env "stdin" Caml.stdin) )
+  | File file ->
+    let mlw_files, _ = Env.(read_file ?format base_language env file) in
+    (Caml.Filename.dirname file, mlw_files)
+  | JSON jin ->
+    let th = Json.theory_of_input env jin in
+    (Unix.getcwd () (* TODO *), Wstdlib.Mstr.singleton th.th_name.id_string th)
+
+let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
+  prover ?prover_altern file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env ~debug loadpath in
-  let mstr_theory =
-    match file with
-    | File.Stdin ->
-      Env.(read_channel ?format base_language env "stdin" Caml.stdin)
-    | File file ->
-      let mlw_files, _ = Env.(read_file ?format base_language env file) in
-      mlw_files
-    | JSON jin ->
-      let th = Json.theory_of_input env jin in
-      Wstdlib.Mstr.singleton th.th_name.id_string th
-  in
-  (env, config, mstr_theory)
-
-let verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover
-  ?prover_altern file =
-  let env, config, mstr_theory = open_file ?debug ?format ~loadpath file in
   let main = Whyconf.get_main config in
   let limit =
     let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
@@ -338,10 +337,12 @@ let verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover
       Driver.load_driver_file_and_extras main env file
         config_prover.extra_drivers
   in
+  let cwd, mstr_theory = open_file ?format env file in
   Wstdlib.Mstr.map
     (fun theory ->
       let tasks = Task.split_theory theory None None in
       List.map
-        ~f:(call_prover ?dataset ~limit main env prover config_prover driver)
+        ~f:
+          (call_prover ~cwd ~limit main env prover config_prover driver ?dataset)
         tasks)
     mstr_theory

src/verification.mli

@@ -75,17 +75,5 @@ val verify :
       for each theory, an [answer] for each goal of the theory, respecting the
       order of appearance. *)
 
-val open_file :
-  ?debug:bool ->
-  ?format:string ->
-  loadpath:string list ->
-  File.t ->
-  Env.env * Whyconf.config * Theory.theory Wstdlib.Mstr.t
-(** [open_file ?debug ?format ~loadpath file] just opens the given file.
-
-    @param debug when set, enables debug information.
-    @param format is the [file] format.
-    @param loadpath is the additional loadpath. *)
-
 val create_env :
   ?debug:bool -> string list -> Why3.Env.env * Why3.Whyconf.config