Getting rid of Exninfo hacks.

Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.

To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.

The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.

13 files changed, 62 insertions, 54 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 8c98c813a1..03c9afbf77 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -53,12 +53,12 @@ let _ = Errors.register_handler explain_exn_default
 
 (** Pre-explain a vernac interpretation error *)
 
-let wrap_vernac_error exn strm =
+let wrap_vernac_error (exn, info) strm =
   let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
   let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
-  Exninfo.copy exn e
+  (e, info)
 
-let process_vernac_interp_error exn = match exn with
+let process_vernac_interp_error exn = match fst exn with
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
@@ -99,29 +99,30 @@ let process_vernac_interp_error exn = match exn with
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
       wrap_vernac_error exn (msg ++ str ".")
-  | exc ->
-      exc
+  | _ ->
+      exn
 
 let rec strip_wrapping_exceptions = function
-  | Logic_monad.TacticFailure e as src ->
-    let e = Backtrace.app_backtrace ~src ~dst:e in
+  | Logic_monad.TacticFailure e ->
     strip_wrapping_exceptions e
   | exc -> exc
 
-let process_vernac_interp_error exc =
+let process_vernac_interp_error (exc, info) =
   let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error exc in
-  let ltac_trace = Exninfo.get exc Proof_type.ltac_trace_info in
-  let loc = Option.default Loc.ghost (Loc.get_loc e) in
+  let e = process_vernac_interp_error (exc, info) in
+  let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
+  let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
   | None -> e
   | Some trace ->
+    let (e, info) = e in
     match Himsg.extract_ltac_trace trace loc with
-    | None, loc -> Loc.add_loc e loc
-    | Some msg, loc -> Loc.add_loc (EvaluatedError (msg, Some e)) loc
+    | None, loc -> (e, Loc.add_loc info loc)
+    | Some msg, loc ->
+      (EvaluatedError (msg, Some e), Loc.add_loc info loc)
 
 let _ = Tactic_debug.explain_logic_error :=
-  (fun e -> Errors.print (process_vernac_interp_error e))
+  (fun e -> Errors.print (fst (process_vernac_interp_error (e, Exninfo.null))))
 
 let _ = Tactic_debug.explain_logic_error_no_anomaly :=
-  (fun e -> Errors.print_no_report (process_vernac_interp_error e))
+  (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null))))
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 2079de8b1c..f027f8c751 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : exn -> exn
+val process_vernac_interp_error : Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 0e52fe6ab9..9d4a74b752 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -53,7 +53,7 @@ let load_rcfile() =
     with reraise ->
       let reraise = Errors.push reraise in
       let () = msg_info (str"Load of rcfile failed.") in
-      raise reraise
+      iraise reraise
   else
     Flags.if_verbose msg_info (str"Skipping rcfile loading.")
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index c29b52cec0..05bf3dc98e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -260,16 +260,16 @@ let locate_exn = function
 
 (* Toplevel error explanation. *)
 
-let print_toplevel_error e =
-  let loc = Option.default Loc.ghost (Loc.get_loc e) in
-  let locmsg = match Vernac.get_exn_files e with
+let print_toplevel_error (e, info) =
+  let loc = Option.default Loc.ghost (Loc.get_loc info) in
+  let locmsg = match Vernac.get_exn_files info with
     | Some files -> print_location_in_file files loc
     | None ->
       if locate_exn e && valid_buffer_loc top_buffer loc then
         print_highlight_location top_buffer loc
       else mt ()
   in
-  locmsg ++ Errors.print e
+  locmsg ++ Errors.iprint (e, info)
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =
@@ -297,7 +297,7 @@ let read_sentence () =
   with reraise ->
     let reraise = Errors.push reraise in
     discard_to_dot ();
-    raise reraise
+    iraise reraise
 
 (** [do_vernac] reads and executes a toplevel phrase, and print error
     messages when an exception is raised, except for the following:
@@ -322,6 +322,7 @@ let do_vernac () =
         if Mltop.is_ocaml_top() then raise Errors.Drop
         else ppnl (str"Error: There is no ML toplevel." ++ fnl ())
     | any ->
+        let any = Errors.push any in
         Format.set_formatter_out_channel stdout;
         let msg = print_toplevel_error any ++ fnl () in
         pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 4aedaa0352..3011471f2a 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -30,7 +30,7 @@ val set_prompt : (unit -> string) -> unit
   May raise only the following exceptions: [Drop] and [End_of_input],
   meaning we get out of the Coq loop. *)
 
-val print_toplevel_error : exn -> std_ppcmds
+val print_toplevel_error : Exninfo.iexn -> std_ppcmds
 
 (** Parse and execute one vernac command. *)
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5bf8cfb3ba..83d6936447 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -581,12 +581,13 @@ let init arglist =
       check_vi_tasks ();
       outputstate ()
     with any ->
+      let any = Errors.push any in
       flush_all();
       let msg =
         if !batch_mode then mt ()
         else str "Error during initialization:" ++ fnl ()
       in
-      fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly any)
+      fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any))
   end;
   if !batch_mode then begin
     flush_all();
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6e63c4e13f..85f8f61a84 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -310,8 +310,9 @@ let parse_format ((loc, str) : lstring) =
     else
       error "Empty format."
   with reraise ->
-    let e = Errors.push reraise in
-    Loc.raise loc e
+    let (e, info) = Errors.push reraise in
+    let info = Loc.add_loc info loc in
+    iraise (e, info)
 
 (***********************)
 (* Analyzing notations *)
@@ -1136,7 +1137,7 @@ let with_lib_stk_protection f x =
   with reraise ->
     let reraise = Errors.push reraise in
     let () = Lib.unfreeze fs in
-    raise reraise
+    iraise reraise
 
 let with_syntax_protection f x =
   with_lib_stk_protection
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index d9b739354e..9b040d70bd 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -120,8 +120,8 @@ let ml_load s =
        with
        | e when Errors.noncritical e ->
         let e = Errors.push e in
-        match e with
-        | (UserError _ | Failure _ | Not_found as u) -> raise u
+        match fst e with
+        | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
         | exc ->
             let msg = report_on_load_obj_error exc in
             errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d5073802de..aa0685861a 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -839,7 +839,8 @@ let rec solve_obligation prg num tac =
 			  
 			obls (pred rem)
 		  with e when Errors.noncritical e ->
-                    pperror (Errors.print (Cerrors.process_vernac_interp_error e))
+                    let e = Errors.push e in
+                    pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
 		in
 		  match res with
 		  | Remain n when n > 0 ->
@@ -892,7 +893,7 @@ and solve_obligation_by_tac prg obls i tac =
 	      true
 	  else false
 	with e when Errors.noncritical e ->
-          let e = Errors.push e in
+          let (e, _) = Errors.push e in
           match e with
 	  | Refiner.FailError (_, s) ->
 	      user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 98a3d7496d..e5c9849a91 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -78,9 +78,9 @@ let get_exn_files e = Exninfo.get e files_of_exn
 
 let add_exn_files e f = Exninfo.add e files_of_exn f
 
-let raise_with_file f e =
-  let inner_f = match get_exn_files e with None -> f | Some ff -> ff.inner in
-  raise (add_exn_files e { outer = f; inner = inner_f })
+let raise_with_file f (e, info) =
+  let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in
+  iraise (e, add_exn_files info { outer = f; inner = inner_f })
 
 let disable_drop = function
   | Drop -> Errors.error "Drop is forbidden."
@@ -232,7 +232,7 @@ let rec vernac_com verbosely checknav (loc,com) =
 	  with reraise ->
             let reraise = Errors.push reraise in
 	    restore_translator_coqdoc st;
-	    raise reraise
+	    iraise reraise
 	end
 
     | v when !just_parsing -> ()
@@ -246,11 +246,11 @@ let rec vernac_com verbosely checknav (loc,com) =
       let com = if !Flags.time then VernacTime [loc,com] else com in
       interp com
     with reraise ->
-      let reraise = Errors.push reraise in
+      let (reraise, info) = Errors.push reraise in
       Format.set_formatter_out_channel stdout;
-      let loc' = Option.default Loc.ghost (Loc.get_loc reraise) in
-      if Loc.is_ghost loc' then Loc.raise loc reraise
-      else raise reraise
+      let loc' = Option.default Loc.ghost (Loc.get_loc info) in
+      if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
+      else iraise (reraise, info)
 
 and read_vernac_file verbosely s =
   Flags.make_warn verbosely;
@@ -269,14 +269,14 @@ and read_vernac_file verbosely s =
       pp_flush ()
     done
   with any ->   (* whatever the exception *)
-    let e = Errors.push any in
+    let (e, info) = Errors.push any in
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
           if do_beautify () then
             pr_new_syntax (Loc.make_loc (max_int,max_int)) None
-      | _ -> raise_with_file fname (disable_drop e)
+      | _ -> raise_with_file fname (disable_drop e, info)
 
 (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
    It executes one vernacular command. By default the command is
@@ -299,9 +299,9 @@ let load_vernac verb file =
     read_vernac_file verb file;
     if !Flags.beautify_file then close_out !chan_beautify;
   with any ->
-    let e = Errors.push any in
+    let (e, info) = Errors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
-    raise_with_file file (disable_drop e)
+    raise_with_file file (disable_drop e, info)
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d46622a027..42353c31aa 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -39,4 +39,4 @@ val is_navigation_vernac : Vernacexpr.vernac_expr -> bool
 
 type location_files = { outer : string; inner : string }
 
-val get_exn_files : exn -> location_files option
+val get_exn_files : Exninfo.info -> location_files option
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 287bf2304d..4a4c5a4339 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -355,7 +355,7 @@ let dump_universes_gen g s =
   with reraise ->
     let reraise = Errors.push reraise in
     close ();
-    raise reraise
+    iraise reraise
 
 let dump_universes sorted s =
   let g = Global.universes () in
@@ -2037,10 +2037,10 @@ let vernac_timeout f =
 
 let restore_timeout () = current_timeout := None
 
-let locate_if_not_already loc exn =
-  match Loc.get_loc exn with
-  | None -> Loc.add_loc exn loc
-  | Some l -> if Loc.is_ghost l then Loc.add_loc exn loc else exn
+let locate_if_not_already loc (e, info) =
+  match Loc.get_loc info with
+  | None -> (e, Loc.add_loc info loc)
+  | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info)
 
 exception HasNotFailed
 exception HasFailed of string
@@ -2056,11 +2056,13 @@ let with_fail b f =
            try f v; raise HasNotFailed
            with
            | HasNotFailed as e -> raise e
-           | e -> raise (HasFailed (Pp.string_of_ppcmds
-              (Errors.print (Cerrors.process_vernac_interp_error e)))))
+           | e ->
+              let e = Errors.push e in
+              raise (HasFailed (Pp.string_of_ppcmds
+              (Errors.iprint (Cerrors.process_vernac_interp_error e)))))
         ()
     with e when Errors.noncritical e -> 
-      let e = Errors.push e in
+      let (e, _) = Errors.push e in
       match e with
       | HasNotFailed ->
           errorlabstrm "Fail" (str "The command has not failed!")
@@ -2116,7 +2118,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             let e = locate_if_not_already loc e in
             let () = restore_timeout () in
             Flags.program_mode := orig_program_mode;
-            raise e
+            iraise e
   and aux_list ?locality ?polymorphism isprogcmd l =
     List.iter (aux false) (List.map snd l)
   in
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 31d1c641cd..863a923dad 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open Errors
 
@@ -56,4 +57,4 @@ let call ?locality (opn,converted_args) =
         let reraise = Errors.push reraise in
         if !Flags.debug then
 	  msg_debug (str"Vernac Interpreter " ++ str !loc);
-        raise reraise
+        iraise reraise