From bff51607cfdda137d7bc55d802895d7f794d5768 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Dec 2014 20:34:09 +0100
Subject: 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.
---
 proofs/proofview.mli | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'proofs/proofview.mli')

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} *)
-- 
cgit v1.2.3