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.

9 files changed, 85 insertions, 74 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 55eb434d38..5bad5f0f52 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -80,22 +80,23 @@ struct
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
-  let raise = fun e -> (); fun () -> raise (Exception e)
+  let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e)
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   let catch = fun s h -> ();
     fun () -> try s ()
       with Exception e as src ->
-        let src = Errors.push src in
-        let e = Backtrace.app_backtrace ~src ~dst:e in
-        h e ()
+        let (src, info) = Errors.push src in
+        h (e, info) ()
 
-  let read_line = fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()
+  let read_line = fun () -> try Pervasives.read_line () with e ->
+    let (e, info) = Errors.push e in raise ~info e ()
 
   let print_char = fun c -> (); fun () -> print_char c
 
   (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()
+  let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e ->
+    let (e, info) = Errors.push e in raise ~info e ()
 
   let timeout = fun n t -> (); fun () ->
     Control.timeout n t (Exception Timeout)
@@ -103,14 +104,13 @@ struct
   let make f = (); fun () ->
     try f ()
     with e when Errors.noncritical e ->
-      let e = Errors.push e in
-      Pervasives.raise (Exception e)
+      let (e, info) = Errors.push e in
+      Util.iraise (Exception e, info)
 
   let run = fun x ->
     try x () with Exception e as src ->
-      let src = Errors.push src in
-      let e = Backtrace.app_backtrace ~src ~dst:e in
-      Pervasives.raise e
+      let (src, info) = Errors.push src in
+      Util.iraise (e, info)
 end
 
 (** {6 Logical layer} *)
@@ -136,7 +136,7 @@ end
 (** A view type for the logical monad, which is a form of list, hence
     we can decompose it with as a list. *)
 type ('a, 'b) list_view =
-  | Nil of exn
+  | Nil of Exninfo.iexn
   | Cons of 'a * 'b
 
 module type Param = sig
@@ -205,9 +205,11 @@ struct
       In that vision, [bind] is simply [concat_map] (though the cps
       version is significantly simpler), [plus] is concatenation, and
       [split] is pattern-matching. *)
+  type rich_exn = Exninfo.iexn
+
   type 'a iolist =
-      { iolist : 'r. (exn -> 'r NonLogical.t) ->
-                     ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+      { iolist : 'r. (rich_exn -> 'r NonLogical.t) ->
+                     ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
                      'r NonLogical.t }
 
   include Monad.Make(struct
@@ -277,7 +279,7 @@ struct
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
 
-  let break (f : exn -> exn option) (m : 'a t) : 'a t = (); fun s ->
+  let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons ->
       m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e))
@@ -285,7 +287,7 @@ struct
 
   (** For [reflect] and [split] see the "Backtracking, Interleaving,
       and Terminating Monad Transformers" paper.  *)
-  type 'a reified = ('a, exn -> 'a reified) list_view NonLogical.t
+  type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t
 
   let rec reflect (m : 'a reified) : 'a iolist =
     { iolist = fun nil cons ->
@@ -296,7 +298,7 @@ struct
       NonLogical.(m >>= next)
     }
 
-  let split (m : 'a t) : ('a, exn -> 'a t) list_view t = (); fun s ->
+  let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s ->
     let m = m s in
     let rnil e = NonLogical.return (Nil e) in
     let rcons p l = NonLogical.return (Cons (p, l)) in
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index 46cab18d25..0d05a2181e 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -60,9 +60,9 @@ module NonLogical : sig
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
-  val raise : exn -> 'a t
+  val raise : ?info:Exninfo.info -> exn -> 'a t
   (** [try ... with ...] but restricted to {!Exception}. *)
-  val catch : 'a t -> (exn -> 'a t) -> 'a t
+  val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
   val timeout : int -> 'a t -> 'a t
 
   (** Construct a monadified side-effect. Exceptions raised by the argument are
@@ -98,7 +98,7 @@ end
 (** A view type for the logical monad, which is a form of list, hence
     we can decompose it with as a list. *)
 type ('a, 'b) list_view =
-| Nil of exn
+| Nil of Exninfo.iexn
 | Cons of 'a * 'b
 
 (** The monad is parametrised in the types of state, environment and
@@ -140,17 +140,17 @@ module Logical (P:Param) : sig
   val local : P.e -> 'a t -> 'a t
   val update : (P.u -> P.u) -> unit t
 
-  val zero : exn -> 'a t
-  val plus : 'a t -> (exn -> 'a t) -> 'a t
-  val split : 'a t -> (('a,(exn->'a t)) list_view) t
+  val zero : Exninfo.iexn -> 'a t
+  val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
+  val split : 'a t -> (('a,(Exninfo.iexn->'a t)) list_view) t
   val once : 'a t -> 'a t
-  val break : (exn -> exn option) -> 'a t -> 'a t
+  val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t
 
   val lift : 'a NonLogical.t -> 'a t
 
   type 'a reified
 
-  val repr : 'a reified -> ('a, exn -> 'a reified) list_view NonLogical.t
+  val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t
 
   val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8e0f3accb2..f4747c0d01 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -142,7 +142,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   with reraise ->
     let reraise = Errors.push reraise in
     delete_current_proof ();
-    raise reraise
+    iraise reraise
 
 let build_by_tactic env ctx ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 8dd7396868..1a13edf17e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -91,7 +91,7 @@ val start_dependent_proof :
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : (exn -> exn) -> closed_proof
+val close_proof : Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 01bb41ad35..f1d10bbe55 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -230,7 +230,7 @@ let apply env t sp =
   let ans = Proof.repr (Proof.run t false (sp,env)) in
   let ans = Logic_monad.NonLogical.run ans in
   match ans with
-  | Nil e -> raise (TacticFailure e)
+  | Nil (e, info) -> iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
     r, state, status, Trace.to_tree info
 
@@ -260,7 +260,12 @@ module Monad = Proof
 
 
 (** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO = Proof.zero
+let tclZERO ?info e =
+  let info = match info with
+  | None -> Exninfo.null
+  | Some info -> info
+  in
+  Proof.zero (e, info)
 
 (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
     the successes of [t1] have been depleted and it failed with [e],
@@ -312,17 +317,17 @@ let tclEXACTLY_ONCE e t =
   let open Logic_monad in
   let open Proof in
   split t >>= function
-    | Nil e -> tclZERO e
+    | Nil (e, info) -> tclZERO ~info e
     | Cons (x,k) ->
-        Proof.split (k e) >>= function
+        Proof.split (k (e, Exninfo.null)) >>= function
           | Nil _ -> tclUNIT x
           | _ -> tclZERO MoreThanOneSuccess
 
 
 (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
 type 'a case =
-| Fail of exn
-| Next of 'a * (exn -> 'a tactic)
+| Fail of iexn
+| Next of 'a * (iexn -> 'a tactic)
 let tclCASE t =
   let open Logic_monad in
   let map = function
@@ -745,12 +750,12 @@ let tclTIMEOUT n t =
         | Logic_monad.Nil e -> return (Util.Inr e)
         | Logic_monad.Cons (r, _) -> return (Util.Inl r)
       end
-      begin let open Logic_monad.NonLogical in function
-        | Logic_monad.Timeout -> return (Util.Inr Timeout)
-        | Logic_monad.TacticFailure e as src ->
-          let e = Backtrace.app_backtrace ~src ~dst:e in
-          return (Util.Inr e)
-        | e -> Logic_monad.NonLogical.raise e
+      begin let open Logic_monad.NonLogical in function (e, info) ->
+        match e with
+        | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
+        | Logic_monad.TacticFailure e ->
+          return (Util.Inr (e, info))
+        | e -> Logic_monad.NonLogical.raise ~info e
       end
   end >>= function
     | Util.Inl (res,s,m,i) ->
@@ -758,7 +763,7 @@ let tclTIMEOUT n t =
         Proof.put m >>
         Proof.update (fun _ -> i) >>
         return res
-    | Util.Inr e -> tclZERO e
+    | Util.Inr (e, info) -> tclZERO ~info e
 
 let tclTIME s t =
   let pr_time t1 t2 n msg =
@@ -775,11 +780,11 @@ let tclTIME s t =
     tclUNIT () >>= fun () ->
     let tstart = System.get_time() in
     Proof.split t >>= let open Logic_monad in function
-    | Nil e ->
+    | Nil (e, info) ->
       begin
         let tend = System.get_time() in
         pr_time tstart tend n "failure";
-        tclZERO e
+        tclZERO ~info e
       end
     | Cons (x,k) ->
         let tend = System.get_time() in
@@ -894,8 +899,8 @@ module Goal = struct
         let (gl, sigma) = nf_gmake env sigma goal in
         tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
       with e when catchable_exception e ->
-        let e = Errors.push e in
-        tclZERO e
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
     end
     end
 
@@ -917,8 +922,8 @@ module Goal = struct
       tclEVARMAP >>= fun sigma ->
       try f (gmake env sigma goal)
       with e when catchable_exception e ->
-        let e = Errors.push e in
-        tclZERO e
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
     end
     end
 
@@ -1082,8 +1087,8 @@ module V82 = struct
       InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
       Pv.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
-      let e = Errors.push e in
-      tclZERO e
+      let (e, info) = Errors.push e in
+      tclZERO ~info e
 
 
   (* normalises the evars in the goals, and stores the result in
@@ -1141,9 +1146,8 @@ module V82 = struct
       let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
     with Logic_monad.TacticFailure e as src ->
-      let src = Errors.push src in
-      let e = Backtrace.app_backtrace ~src ~dst:e in
-      raise e
+      let (_, info) = Errors.push src in
+      iraise (e, info)
 
   let put_status = Status.put
 
@@ -1151,6 +1155,7 @@ module V82 = struct
 
   let wrap_exceptions f =
     try f ()
-    with e when catchable_exception e -> let e = Errors.push e in tclZERO e
+    with e when catchable_exception e ->
+      let (e, info) = Errors.push e in tclZERO ~info e
 
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index eb54ba3ae5..25f4547a91 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -12,6 +12,7 @@
     ['a tactic] is the (abstract) type of tactics modifying the proof
     state and returning a value of type ['a]. *)
 
+open Util
 open Term
 
 (** Main state of tactics *)
@@ -172,24 +173,24 @@ module Monad : Monad.S with type +'a t = 'a tactic
 (** {7 Failure and backtracking} *)
 
 (** [tclZERO e] fails with exception [e]. It has no success. *)
-val tclZERO : exn -> 'a tactic
+val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
 
 (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
     the successes of [t1] have been depleted and it failed with [e],
     then it behaves as [t2 e]. In other words, [tclOR] inserts a
     backtracking point. *)
-val tclOR : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
+val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
 
 (** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
     success or [t2 e] if [t1] fails with [e]. It is analogous to
     [try/with] handler of exception in that it is not a backtracking
     point. *)
-val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
+val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
 
 (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
     succeeds at least once then it behaves as [tclBIND a s] otherwise,
     if [a] fails with [e], then it behaves as [f e]. *)
-val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tactic
+val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic
 
 (** [tclONCE t] behave like [t] except it has at most one success:
     [tclONCE t] stops after the first success of [t]. If [t] fails
@@ -211,8 +212,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
     continuation. It is the most general primitive to control
     backtracking. *)
 type 'a case =
-  | Fail of exn
-  | Next of 'a * (exn -> 'a tactic)
+  | Fail of iexn
+  | Next of 'a * (iexn -> 'a tactic)
 val tclCASE : 'a tactic -> 'a case tactic
 
 (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
@@ -220,7 +221,7 @@ val tclCASE : 'a tactic -> 'a case tactic
     failure with an exception [e] such that [p e = Some e'] is raised. At
     which point it drops the remaining successes, failing with [e'].
     [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *)
-val tclBREAK : (exn -> exn option) -> 'a tactic -> 'a tactic
+val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
 
 
 (** {7 Focusing tactics} *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 391a78b34a..e443ce0772 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -218,14 +218,14 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   rslt;;
 
 
-let catch_failerror e =
+let catch_failerror (e, info) =
   if catchable_exception e then Control.check_for_interrupt ()
   else match e with
   | FailError (0,_) ->
       Control.check_for_interrupt ()
   | FailError (lvl,s) ->
-    raise (Exninfo.copy e (FailError (lvl - 1, s)))
-  | e -> raise e
+    iraise (FailError (lvl - 1, s), info)
+  | e -> iraise (e, info)
   (** FIXME: do we need to add a [Errors.push] here? *)
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
@@ -233,7 +233,8 @@ let tclORELSE0 t1 t2 g =
   try
     t1 g
   with (* Breakpoint *)
-    | e when Errors.noncritical e -> catch_failerror e; t2 g
+    | e when Errors.noncritical e ->
+      let e = Errors.push e in catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
@@ -245,7 +246,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
-    with e when Errors.noncritical e -> catch_failerror e; None
+    with e when Errors.noncritical e ->
+      let e = Errors.push e in catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
@@ -270,16 +272,17 @@ let ite_gen tcal tac_if continue tac_else gl=
       success:=true;result in
   let tac_else0 e gl=
     if !success then
-      raise e
+      iraise e
     else
       try
         tac_else gl
       with
-        e' when Errors.noncritical e' -> raise e in
+        e' when Errors.noncritical e' -> iraise e in
   try
     tcal tac_if0 continue gl
   with (* Breakpoint *)
-  | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl
+  | e when Errors.noncritical e ->
+    let e = Errors.push e in catch_failerror e; tac_else0 e gl
 
 (* Try the first tactic and, if it succeeds, continue with
    the second one, and if it fails, use the third one *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index ea1677f069..744843fc94 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -102,7 +102,7 @@ exception FailError of int * Pp.std_ppcmds Lazy.t
 
 (** Takes an exception and either raise it at the next
    level or do nothing. *)
-val catch_failerror  : exn -> unit
+val catch_failerror  : Exninfo.iexn -> unit
 
 val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 80aaf9f2a9..b25f37b369 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -138,9 +138,9 @@ let rec prompt level =
     Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
-      begin function
+      begin function (e, info) -> match e with
         | End_of_file -> exit
-        | e -> raise e
+        | e -> raise ~info e
       end
     >>= fun inst ->
     match inst with
@@ -154,9 +154,9 @@ let rec prompt level =
       end
     | _ ->
         Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1)))
-          begin function
+          begin function (e, info) -> match e with
             | Failure _ | Invalid_argument _ -> prompt level
-            | e -> raise e
+            | e -> raise ~info e
           end
   end
 
@@ -189,7 +189,7 @@ let debug_prompt lev tac f =
   (* What to execute *)
   Proofview.tclOR
     (f newlevel)
-    begin fun reraise ->
+    begin fun (reraise, info) ->
       Proofview.tclTHEN
         (Proofview.tclLIFT begin
           (skip:=0) >> (skipped:=0) >>
@@ -197,7 +197,7 @@ let debug_prompt lev tac f =
               msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise)
             else return ()
         end)
-        (Proofview.tclZERO reraise)
+        (Proofview.tclZERO ~info reraise)
     end
 
 let is_debug db =