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.

1 files changed, 11 insertions, 8 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 391a78b34..e443ce077 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 *)