Replace output channels by regular or diagnostic channels

src/bin/common/parse_command.ml

@@ -533,12 +533,12 @@ let halt_opt version_info where =
                 "\"\nAccepted options are lib, plugins, preludes, data or man")
     in
     match res with
-    | `Ok path -> Printer.print_std "%s@." path
+    | `Ok path -> Printer.print_regular "%s@." path
     | `Error m -> raise (Error (false, m))
   in
   let handle_version_info vi =
     if vi then (
-      Printer.print_std
+      Printer.print_regular
         "@[<v 0>Version          = %s@,\
          Release date     = %s@,\
          Release commit   = %s@]@."
@@ -582,9 +582,9 @@ let mk_opts file () () debug_flags ddebug_flags dddebug_flags rule () halt_opt
     `Ok true
   end
 
-let mk_output_channel_opt std_output err_output =
-  Options.Output.(create_channel std_output |> set_std);
-  Options.Output.(create_channel err_output |> set_err);
+let mk_output_channel_opt regular_output diagnostic_output =
+  Options.Output.(create_channel regular_output |> set_regular);
+  Options.Output.(create_channel diagnostic_output |> set_diagnostic);
   `Ok()
 
 (* Custom sections *)
@@ -1208,52 +1208,29 @@ let parse_fmt_opt =
   let docs = s_fmt in
   let docv = "CHANNEL" in
 
-  let merge_formatters default preferred deprecated =
-    match preferred, deprecated with
-    | Some fmt, _ -> fmt
-    | None, Some fmt -> fmt
-    | None, None -> default
-  in
-
-  let std_output =
+  let regular_output =
     let doc =
       Format.sprintf
-        "Set the standard output used by default to print the results,
+        "Set the regular output used by default to print the results,
           models and unsat cores. Possible values are %s."
         (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
     in
-    let deprecated = "this option is deprecated. Please use --std-output." in
-    let std_output =
-      Arg.(value & opt (some' string) None & info ["std-output"] ~docs
-             ~doc ~docv)
-    in
-    let std_formatter =
-      Arg.(value & opt (some' string) None  & info ["std-formatter"]
-             ~deprecated ~docs ~docv)
-    in
-    Term.(const (merge_formatters "stdout") $ std_output $ std_formatter)
+    Arg.(value & opt string "stdout" & info ["regular-output"] ~docs
+           ~doc ~docv)
   in
 
-  let err_output =
+  let diagnostic_output =
     let doc =
       Format.sprintf
-        "Set the error output used by default to print error, debug and
+        "Set the diagnostic output used by default to print error, debug and
          warning informations. Possible values are %s."
         (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
     in
-    let deprecated = "this option is deprecated. Please use --err-output." in
-    let err_output =
-      Arg.(value & opt (some' string) None & info ["err-output"] ~docs
-             ~doc ~docv)
-    in
-    let err_formatter =
-      Arg.(value & opt (some' string) None & info ["err-formatter"]
-             ~deprecated ~docs ~docv)
-    in
-    Term.(const (merge_formatters "stderr") $ err_output $ err_formatter)
+    Arg.(value & opt string "stderr" & info ["diagnostic-output"] ~docs
+           ~doc ~docv)
   in
 
-  Term.(ret (const mk_output_channel_opt $ std_output $ err_output))
+  Term.(ret (const mk_output_channel_opt $ regular_output $ diagnostic_output))
 
 let main =
 

src/bin/common/signals_profiling.ml

@@ -39,10 +39,10 @@ let init_sigterm_6 () =
   Sys.set_signal Sys.sigint(*-6*)
     (Sys.Signal_handle (fun _ ->
          if Options.get_profiling() then
-           Profiling.switch (Options.Output.get_fmt_err ())
+           Profiling.switch (Options.Output.get_fmt_diagnostic ())
          else begin
-           Printer.print_wrn "User wants me to stop.";
-           Printer.print_std "unknown";
+           Printer.print_diagnostic "User wants me to stop.";
+           Printer.print_regular "unknown";
            exit 1
          end
        )
@@ -58,7 +58,7 @@ let init_sigterm_11_9 () =
            (Sys.Signal_handle
               (fun _ ->
                  Profiling.print true (Steps.get_steps ())
-                   timers (Options.Output.get_fmt_err ());
+                   timers (Options.Output.get_fmt_diagnostic ());
                  exit 1
               )
            )
@@ -72,7 +72,7 @@ let init_sigterm_21 () =
       (Sys.Signal_handle
          (fun _ ->
             Profiling.print false (Steps.get_steps ()) timers
-              (Options.Output.get_fmt_err ());
+              (Options.Output.get_fmt_diagnostic ());
          )
       )
 

src/bin/common/solving_loop.ml

@@ -85,7 +85,7 @@ let main () =
         Profiling.print true
           (Steps.get_steps ())
           (Signals_profiling.get_timers ())
-          (Options.Output.get_fmt_err ());
+          (Options.Output.get_fmt_diagnostic ());
       Some partial_model
     with Util.Timeout ->
       if not (Options.get_timelimit_per_goal()) then exit 142;
@@ -142,11 +142,11 @@ let main () =
         FE.print_status (FE.Timeout None) 0;
         exit 142
       | Parsing.Parse_error ->
-        Printer.print_err "%a" Errors.report
+        Printer.print_diagnostic "%a" Errors.report
           (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),""));
         exit 1
       | Errors.Error e ->
-        Printer.print_err "%a" Errors.report e;
+        Printer.print_diagnostic "%a" Errors.report e;
         exit 1
     in
 
@@ -162,7 +162,7 @@ let main () =
         with
         | Errors.Error e ->
           if e != Warning_as_error then
-            Printer.print_err "%a" Errors.report e;
+            Printer.print_diagnostic "%a" Errors.report e;
           exit 1
       end
     in
@@ -210,7 +210,7 @@ let main () =
   in
   let handle_exn _ bt = function
     | Dolmen.Std.Loc.Syntax_error (_, `Regular msg) ->
-      Printer.print_err "%t" msg;
+      Printer.print_diagnostic "%t" msg;
       exit 1
     | Util.Timeout ->
       Printer.print_status_timeout None None None None;

src/bin/js/worker_example.ml

@@ -82,7 +82,7 @@ let solve () =
   (Lwt.pick [
       (let%lwt () = Lwt_js.sleep !timeout in
        Lwt.return {(Worker_interface.init_results ()) with
-                   debugs =Some ["Timeout"]});
+                   diagnostic =Some ["Timeout"]});
       (
         let file = String.split_on_char '\n' !file in
         let json_file = Worker_interface.file_to_json None (Some 42) file in
@@ -225,17 +225,17 @@ let onload _ =
              print_error (Some "");
              let%lwt res = solve () in
              (* Update results area *)
-             print_res (process_results res.results);
+             print_res (process_results res.regular);
+             (* Update model *)
+             print_model  (process_results res.regular);
+             (* Update unsat core *)
+             print_unsat_core  (process_results res.regular);
              (* Update errors area if errors occurs at solving *)
-             print_error  (process_results res.errors);
+             print_error  (process_results res.diagnostic);
              (* Update warning area if warning occurs at solving *)
-             print_warning  (process_results res.warnings);
+             print_warning  (process_results res.diagnostic);
              (* Update debug area *)
-             print_debug  (process_results res.debugs);
-             (* Update model *)
-             print_model  (process_results res.results);
-             (* Update unsat core *)
-             print_unsat_core  (process_results res.unsat_core);
+             print_debug  (process_results res.diagnostic);
              (* Update statistics *)
              print_statistics res.statistics;
              Lwt.return_unit);

src/bin/js/worker_interface.ml

@@ -956,44 +956,31 @@ let status_encoding =
 type results = {
   worker_id : int option;
   status : status;
-  results : string list option;
-  errors : string list option;
-  warnings : string list option;
-  debugs : string list option;
+  regular : string list option;
+  diagnostic : string list option;
   statistics : statistics option;
-  unsat_core : string list option;
 }
 
 let init_results () = {
   worker_id = None;
   status = Unknown (-1);
-  results = None;
-  errors = None;
-  warnings = None;
-  debugs = None;
+  regular = None;
+  diagnostic = None;
   statistics = None;
-  unsat_core = None;
 }
 
 let results_encoding =
   conv
-    (fun {worker_id; status; results; errors; warnings;
-          debugs; statistics; unsat_core } ->
-      (worker_id, status, results, errors, warnings,
-       debugs, statistics, unsat_core))
-    (fun (worker_id, status, results, errors, warnings,
-          debugs, statistics, unsat_core) ->
-      {worker_id; status; results; errors; warnings;
-       debugs; statistics; unsat_core })
-    (obj8
+    (fun {worker_id; status; regular; diagnostic; statistics; } ->
+       (worker_id, status, regular, diagnostic, statistics))
+    (fun (worker_id, status, regular, diagnostic, statistics) ->
+       {worker_id; status; regular; diagnostic; statistics })
+    (obj5
        (opt "worker_id" int31)
        (req "status" status_encoding)
-       (opt "results" (list string))
-       (opt "errors" (list string))
-       (opt "warnings" (list string))
-       (opt "debugs" (list string))
-       (opt "statistics" statistics_encoding)
-       (opt "unsat_core" (list string)))
+       (opt "regular" (list string))
+       (opt "diagnostic" (list string))
+       (opt "statistics" statistics_encoding))
 
 let results_to_json res =
   let json_results = Json.construct results_encoding res in

src/bin/js/worker_interface.mli

@@ -195,12 +195,9 @@ type status =
 type results = {
   worker_id : int option;
   status : status;
-  results : string list option;
-  errors : string list option;
-  warnings : string list option;
-  debugs : string list option;
+  regular : string list option;
+  diagnostic : string list option;
   statistics : statistics option;
-  unsat_core : string list option;
 }
 
 (** {2 Functions} *)

src/bin/js/worker_js.ml

@@ -68,16 +68,10 @@ let main worker_id content =
   try
     (* Create buffer for each formatter
        The content of this buffers are then retrieved and send as results *)
-    let buf_std = create_buffer () in
-    Options.Output.set_std (snd buf_std);
-    let buf_err = create_buffer () in
-    Options.Output.set_err (snd buf_err);
-    let buf_wrn = create_buffer () in
-    Options.Output.set_wrn (snd buf_wrn);
-    let buf_dbg = create_buffer () in
-    Options.Output.set_dbg (snd buf_dbg);
-    let buf_usc = create_buffer () in
-    Options.Output.set_usc (snd buf_usc);
+    let buf_regular = create_buffer () in
+    Options.Output.set_regular (snd buf_regular);
+    let buf_diagnostic = create_buffer () in
+    Options.Output.set_diagnostic (snd buf_diagnostic);
 
     (* Status updated regarding if AE succed or failed
        (error or steplimit reached) *)
@@ -170,7 +164,7 @@ let main worker_id content =
         I.parse_file ~content ~format:None
       with
       | Parsing.Parse_error ->
-        Printer.print_err "%a" Errors.report
+        Printer.print_diagnostic "%a" Errors.report
           (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),""));
         raise Exit
       | Errors.Error e ->
@@ -184,7 +178,7 @@ let main worker_id content =
             end
           | _ -> returned_status := Worker_interface.Error "Error"
         end;
-        Printer.print_err "%a" Errors.report e;
+        Printer.print_diagnostic "%a" Errors.report e;
         raise Exit
     in
     let all_used_context = FE.init_all_used_context () in
@@ -194,7 +188,7 @@ let main worker_id content =
         let l, env = I.type_parsed state.env assertion_stack p in
         List.fold_left (typed_loop all_used_context) { state with env; } l
       with Errors.Error e ->
-        Printer.print_err "%a" Errors.report e;
+        Printer.print_diagnostic "%a" Errors.report e;
         raise Exit
     in
 
@@ -240,13 +234,10 @@ let main worker_id content =
     {
       Worker_interface.worker_id = worker_id;
       Worker_interface.status = !returned_status;
-      Worker_interface.results = check_buffer_content buf_std;
-      Worker_interface.errors = check_buffer_content buf_err;
-      Worker_interface.warnings = check_buffer_content buf_wrn;
-      Worker_interface.debugs = check_buffer_content buf_dbg;
+      Worker_interface.regular = check_buffer_content buf_regular;
+      Worker_interface.diagnostic = check_buffer_content buf_diagnostic;
       Worker_interface.statistics =
         check_context_content (compute_statistics ());
-      Worker_interface.unsat_core = check_buffer_content buf_usc;
     }
 
   with
@@ -255,15 +246,15 @@ let main worker_id content =
     { res with
       Worker_interface.worker_id = worker_id;
       Worker_interface.status = Error "Assertion failure";
-      Worker_interface.errors =
+      Worker_interface.diagnostic =
         Some [Format.sprintf "assertion failed: %s line %d char %d" s l p];
     }
   | Errors.Error e ->
     let res = Worker_interface.init_results () in
     { res with
       Worker_interface.worker_id = worker_id;
       Worker_interface.status = Error "";
-      Worker_interface.errors =
+      Worker_interface.diagnostic =
         Some [Format.asprintf "%a" Errors.report e]
     }
   | _ ->

src/bin/text/main_text.ml

@@ -44,6 +44,6 @@ let () =
   register_input ();
   parse_cmdline ();
   AltErgoLib.Printer.init_colors ();
-  AltErgoLib.Printer.init_output_format ();
+  (*   AltErgoLib.Printer.init_output_format (); *)
   Signals_profiling.init_signals ();
   Solving_loop.main ()

src/lib/frontend/frontend.ml

@@ -291,7 +291,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
          not (get_debug_unsat_core()) &&
          not (get_save_used_context())
       then
-        Printer.print_fmt (Options.Output.get_fmt_usc ())
+        Printer.print_regular
           "unsat-core:@,%a@."
           (Ex.print_unsat_core ~tab:true) dep;
       check_status_consistency status;

src/lib/reasoners/ac.ml

@@ -117,7 +117,7 @@ module Make (X : Sig.X) = struct
         if not (c1 = 0 && c2 = 0 ||
                 c1 < 0 && c2 > 0 ||
                 c1 > 0 && c2 < 0) then begin
-          print_err
+          print_diagnostic
             "Ac.compare:@ %a vs %a@  = %d@ \
              But@ \
              Ac.compare:@ %a vs %a@  = %d"
@@ -192,7 +192,7 @@ module Make (X : Sig.X) = struct
                     distribute = true},
         ctx
       | {xs; _} ->
-        Printer.print_err
+        Printer.print_diagnostic
           "AC theory expects only terms with 2 arguments; \
            got %i (%a)." (List.length xs) Expr.print_list xs;
         assert false