Fix error handling of dolmen (#842)

When dolmen fails, its default behavior is to call exit with a custom exit code. This MR overrides the error function of the dolmen loop so that alt-ergo keeps control over the exit code.

src/lib/frontend/d_loop.ml

@@ -31,7 +31,29 @@
 module DStd = Dolmen.Std
 module Dl = Dolmen_loop
 
-module State = Dl.State
+module State = struct
+  include Dl.State
+
+  (* Overriding error function so that error does not savagely exit. *)
+  let error ?file ?loc st error payload =
+    let st = flush st () in
+    let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
+    let aux _ =
+      let code, descr = Dl.(Code.descr Dl.Report.Error.(code error)) in
+      raise (Errors.(error (Dolmen_error (code, descr))))
+    in
+    match get report_style st with
+    | Minimal ->
+      Format.kfprintf aux Format.err_formatter
+        "E:%s@." (Dl.Report.Error.mnemonic error)
+    | Regular | Contextual ->
+      Format.kfprintf aux Format.err_formatter
+        ("@[<v>%a%a @[<hov>%a@]%a@]@.")
+        (pp_loc ?file st) loc
+        Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Error"
+        Dl.Report.Error.print (error, payload)
+        Dl.Report.Error.print_hints (error, payload)
+end
 module Pipeline = Dl.Pipeline.Make(State)
 
 module Parser = Dolmen_loop.Parser.Make(State)

src/lib/structures/errors.ml

@@ -92,6 +92,7 @@ type error =
   | Typing_error of Loc.t * typing_error
   | Run_error of run_error
   | Warning_as_error
+  | Dolmen_error of (int * string)
 
 exception Error of error
 
@@ -256,4 +257,7 @@ let report fmt = function
   | Run_error e ->
     Options.pp_comment fmt "Fatal Error: ";
     report_run_error fmt e
+  | Dolmen_error (code, descr) ->
+    Options.pp_comment fmt
+      (Format.sprintf "Error %s (code %i)" descr code);
   | Warning_as_error -> ()

src/lib/structures/errors.mli

@@ -100,6 +100,8 @@ type error =
   | Typing_error of Loc.t * typing_error (** Error used at typing *)
   | Run_error of run_error (** Error used during solving *)
   | Warning_as_error
+  | Dolmen_error of (int * string)
+  (** Error code + description raised by dolmen. *)
 
 (** {2 Exceptions } *)