Remove get file (OCamlPro#1286)

* Remove the option get_file
One step after another, we get rid of the global state!

* Create a new type for parse_command result

Author: Halbaroth

src/bin/common/parse_command.ml

@@ -568,7 +568,12 @@ let mk_opts file () () debug_flags ddebug_flags dddebug_flags backtrace
   Debug.mk ~verbosity:3 dddebug_flags;
   if backtrace then Printexc.record_backtrace true;
   Rule.mk rule;
-  if halt_opt then `Ok false
+  let path =
+    match file with
+    | Some f -> `File f
+    | None -> `Stdin
+  in
+  if halt_opt then `Ok None
   (* If save_used_context was invoked as an option it should
        automatically set unsat_core to true *)
   else begin
@@ -579,14 +584,13 @@ let mk_opts file () () debug_flags ddebug_flags dddebug_flags backtrace
            Filename.chop_extension f
          with Invalid_argument _ -> f
        in
-       set_file f;
        set_session_file (base_file^".agr");
        set_used_context_file base_file;
      | _ -> ()
     );
 
     Gc.set { (Gc.get()) with Gc.allocation_policy = gc };
-    `Ok true
+    `Ok (Some path)
   end
 
 let mk_output_channel_opt regular_output diagnostic_output =
@@ -1500,7 +1504,8 @@ let main =
        ($(i,.mlw) and $(i,.why) are deprecated), \
        $(i,.smt2) or $(i,.psmt2)." in
     let i = Arg.(info [] ~docv:"FILE" ~doc) in
-    Arg.(value & pos ~rev:true 0 (some file) None & i) in
+    Arg.(value & pos ~rev:true 0 (some file) None & i)
+  in
 
   let doc = "Execute Alt-Ergo on the given file." in
   let exits = Cmd.Exit.defaults in
@@ -1576,8 +1581,8 @@ let parse_cmdline_arguments () =
   at_exit Options.Output.close_all;
   let r = Cmd.eval_value main in
   match r with
-  | Ok `Ok true -> ()
-  | Ok `Ok false -> raise (Exit_parse_command 0)
+  | Ok `Ok Some path -> Solving_loop.{ path }
+  | Ok `Ok None -> raise (Exit_parse_command 0)
   | Ok `Version | Ok `Help -> exit 0
   | Error `Parse -> exit Cmd.Exit.cli_error
   | Error `Term -> exit Cmd.Exit.internal_error

src/bin/common/parse_command.mli

@@ -28,9 +28,8 @@
 (** {1 Parse_command module used at start-up to parse the command line} *)
 
 (** Only exported function. Calling it will parse the command line options
-    and set them accordingly for the rest of the execution *)
-val parse_cmdline_arguments : unit -> unit
-
+    and set them accordingly for the rest of the execution. *)
+val parse_cmdline_arguments : unit -> Solving_loop.parse_result
 
 (** Exception used to exit with corresponding retcode *)
 exception Exit_parse_command of int

src/bin/common/solving_loop.ml

@@ -32,6 +32,10 @@ module DO = D_state_option
 module Sy = Symbols
 module O = Options
 
+type parse_result = {
+  path : [`Stdin | `File of string];
+}
+
 exception Exit_with_code of int
 
 type solver_ctx = {
@@ -937,11 +941,9 @@ let process_source ?selector_inst ~print_status src =
   in
   d_fe src
 
-let main () =
-  let path = Options.get_file () in
+let main { path } =
   try
-    if String.equal path "" then
-      process_source ~print_status:Frontend.print_status `Stdin
-    else
-      process_source ~print_status:Frontend.print_status @@ (`File path)
+    process_source
+      ~print_status:Frontend.print_status
+      (path :> D_loop.State.source)
   with Exit_with_code code -> exit code

src/bin/common/solving_loop.mli

@@ -29,9 +29,13 @@ exception Exit_with_code of int
 (** Exception raised to notify that [process_source] cannot continue.
     The integer corresponds to an error code. *)
 
-val main : unit -> unit
-(** Main function solve the input problem. The processed source is given
-    by the file located at [Options.get_file ()]. *)
+type parse_result = {
+  path : [`Stdin | `File of string];
+  (** Path to the input file. *)
+}
+
+val main : parse_result -> unit
+(** [main path] solves the input problem [path]. *)
 
 val process_source :
   ?selector_inst:(AltErgoLib.Expr.t -> bool) ->

src/bin/js/main_text_js.ml

@@ -34,9 +34,9 @@ let parse_cmdline () =
   with Parse_command.Exit_parse_command i -> exit i
 
 let () =
-  parse_cmdline ();
+  let path = parse_cmdline () in
   AltErgoLib.Printer.init_colors ();
   AltErgoLib.Printer.init_output_format ();
   Signals_profiling.init_signals ();
   Logs.set_reporter (AltErgoLib.Printer.reporter);
-  Solving_loop.main ()
+  Solving_loop.main path

src/bin/js/options_interface.ml

@@ -193,5 +193,3 @@ let set_options r =
   set_options_opt Options.set_restricted r.restricted;
   set_options_opt Options.set_tighten_vars r.tighten_vars;
   set_options_opt Options.set_timers r.timers;
-
-  set_options_opt Options.set_file r.file;

src/bin/js/worker_example.ml

@@ -65,7 +65,6 @@ let solve () =
   let options =
     {(Worker_interface.init_options ()) with
      input_format = None;
-     file = Some "try-alt-ergo";
      debug = Some true;
      verbose = Some true;
      answers_with_loc = Some false;

src/bin/js/worker_interface.ml

@@ -252,8 +252,6 @@ type options = {
   restricted : bool option;
   tighten_vars : bool option;
   timers : bool option;
-
-  file : string option;
 }
 
 let init_options () = {
@@ -351,8 +349,6 @@ let init_options () = {
   restricted = None;
   tighten_vars = None;
   timers = None;
-
-  file = None;
 }
 
 
@@ -496,7 +492,7 @@ let opt7_encoding =
   conv
     (fun opt7 -> opt7)
     (fun opt7 -> opt7)
-    (obj9
+    (obj8
        (opt "no_contracongru" bool)
        (opt "no_fm" bool)
        (opt "no_nla" bool)
@@ -505,7 +501,6 @@ let opt7_encoding =
        (opt "restricted" bool)
        (opt "tighten_vars" bool)
        (opt "timers" bool)
-       (opt "file" string)
     )
 
 let options_encoding =
@@ -620,8 +615,7 @@ let options_to_json opt =
      opt.no_theory,
      opt.restricted,
      opt.tighten_vars,
-     opt.timers,
-     opt.file)
+     opt.timers)
   in
   let json_all_options = Json.construct options_encoding
       (dbg_opt1,
@@ -731,8 +725,7 @@ let options_from_json options =
          no_theory,
          restricted,
          tighten_vars,
-         timers,
-         file) = all_opt7 in
+         timers) = all_opt7 in
     {
       debug;
       debug_ac;
@@ -813,8 +806,7 @@ let options_from_json options =
       no_theory;
       restricted;
       tighten_vars;
-      timers;
-      file
+      timers
     }
   | Error _e -> assert false
 

src/bin/js/worker_interface.mli

@@ -149,8 +149,6 @@ type options = {
   restricted : bool option;
   tighten_vars : bool option;
   timers : bool option;
-
-  file : string option;
 }
 
 type used_axiom =

src/bin/text/main_text.ml

@@ -34,9 +34,9 @@ let parse_cmdline () =
   with Parse_command.Exit_parse_command i -> exit i
 
 let () =
-  parse_cmdline ();
+  let path = parse_cmdline () in
   AltErgoLib.Printer.init_colors ();
   AltErgoLib.Printer.init_output_format ();
   Signals_profiling.init_signals ();
   Logs.set_reporter (AltErgoLib.Printer.reporter);
-  Solving_loop.main ()
+  Solving_loop.main path