[lib] Split auxiliary libraries into Coq-specific and general.

Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.

We know split the directory in two, as to make the distinction clear:

- `clib`: contains libraries that are not Coq specific and implement
  common data structures and programming patterns. These libraries
  could be eventually replace with external dependencies and the rest
  of the code base wouldn't notice much.

- `lib`: contains Coq-specific common libraries in widespread use
  along the codebase, but that are not considered part of other
  components. Examples are printing, error handling, or flags.

In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.

Also note that `Deque` is not used ATM.

1 files changed, 104 insertions, 0 deletions

diff --git a/clib/exninfo.ml b/clib/exninfo.ml
new file mode 100644
index 000000000..167d3d6dc
--- /dev/null
+++ b/clib/exninfo.ml
@@ -0,0 +1,104 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** Enriched exceptions have an additional field at the end of their usual data
+    containing a pair composed of the distinguishing [token] and the backtrace
+    information. We discriminate the token by pointer equality. *)
+
+module Store = Store.Make ()
+
+type 'a t = 'a Store.field
+
+type info = Store.t
+
+type iexn = exn * info
+
+let make = Store.field
+let add = Store.set
+let get = Store.get
+let null = Store.empty
+
+exception Unique
+
+let dummy = (Unique, Store.empty)
+
+let current : (int * iexn) list ref = ref []
+(** List associating to each thread id the latest exception raised by an
+    instrumented raise (i.e. {!raise} from this module). It is shared between
+    threads, so we must take care of this when modifying it.
+
+    Invariants: all index keys are unique in the list.
+*)
+
+let lock = Mutex.create ()
+
+let rec remove_assoc (i : int) = function
+| [] -> []
+| (j, v) :: rem as l ->
+  if i = j then rem
+  else
+    let ans = remove_assoc i rem in
+    if rem == ans then l
+    else (j, v) :: ans
+
+let rec find_and_remove_assoc (i : int) = function
+| [] -> dummy, []
+| (j, v) :: rem as l ->
+  if i = j then (v, rem)
+  else
+    let (r, ans) = find_and_remove_assoc i rem in
+    if rem == ans then (r, l)
+    else (r, (j, v) :: ans)
+
+let iraise e =
+  let () = Mutex.lock lock in
+  let id = Thread.id (Thread.self ()) in
+  let () = current := (id, e) :: remove_assoc id !current in
+  let () = Mutex.unlock lock in
+  raise (fst e)
+
+let raise ?info e = match info with
+| None ->
+  let () = Mutex.lock lock in
+  let id = Thread.id (Thread.self ()) in
+  let () = current := remove_assoc id !current in
+  let () = Mutex.unlock lock in
+  raise e
+| Some i ->
+  let () = Mutex.lock lock in
+  let id = Thread.id (Thread.self ()) in
+  let () = current := (id, (e, i)) :: remove_assoc id !current in
+  let () = Mutex.unlock lock in
+  raise e
+
+let find_and_remove () =
+  let () = Mutex.lock lock in
+  let id = Thread.id (Thread.self ()) in
+  let (v, l) = find_and_remove_assoc id !current in
+  let () = current := l in
+  let () = Mutex.unlock lock in
+  v
+
+let info e =
+  let (src, data) = find_and_remove () in
+  if src == e then
+    (** Slightly unsound, some exceptions may not be unique up to pointer
+        equality. Though, it should be quite exceptional to be in a situation
+        where the following holds:
+
+        1. An argument-free exception is raised through the enriched {!raise};
+        2. It is not captured by any enriched with-clause (which would reset
+            the current data);
+        3. The same exception is raised through the standard raise, accessing
+            the wrong data.
+    . *)
+    data
+  else
+    (** Mismatch: the raised exception is not the one stored, either because the
+        previous raise was not instrumented, or because something went wrong. *)
+    Store.empty