diff options
| -rw-r--r-- | checker/check.mllib | 1 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 1 | ||||
| -rw-r--r-- | lib/clib.mllib | 1 | ||||
| -rw-r--r-- | lib/exninfo.ml | 78 | ||||
| -rw-r--r-- | lib/exninfo.mli | 21 |
6 files changed, 103 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 2d56e163bd..e468f12924 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,4 +1,5 @@ Coq_config +Exninfo Backtrace Int Pp_control diff --git a/dev/printers.mllib b/dev/printers.mllib index fa6d9324c1..0b6ec899e9 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,5 +1,6 @@ Coq_config +Exninfo Backtrace Int Pp_control diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 4e1642a90c..e16f181e6f 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,5 +1,6 @@ Coq_config +Exninfo Backtrace Int Pp_control diff --git a/lib/clib.mllib b/lib/clib.mllib index 55bfdc835e..f412de2f20 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -1,3 +1,4 @@ +Exninfo Backtrace Int Pp_control diff --git a/lib/exninfo.ml b/lib/exninfo.ml new file mode 100644 index 0000000000..b62e83b59c --- /dev/null +++ b/lib/exninfo.ml @@ -0,0 +1,78 @@ +(***********************************************************************) +(* 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. *) + +type 'a t = int +(** Information is retrieved through this identifier. *) + +let token = Obj.repr "HACK" +(** Unique token used to recognize enriched exceptions. *) + +let make = + let cnt = ref 0 in fun () -> + let ans = !cnt in + let () = incr cnt in + ans + +let rec assoc_aux (i : int) = function +| [] -> raise Exit +| (j, v) :: l -> + if i = j then v else assoc_aux i l + +let assoc i l = + try Some (assoc_aux i l) with Exit -> None + +let rec add_assoc (i : int) v = function +| [] -> [i, v] +| (j, w) :: l -> + if i = j then (j, v) :: l + else (j, w) :: add_assoc i v l + +(** Discriminate normal data w.r.t enriched exceptions *) +let is_data obj = + Obj.is_block obj && Obj.size obj = 2 && Obj.field obj 0 == token + +(** Retrieve the optional backtrace set in an exception. *) +let get (e : exn) i = + let obj = Obj.repr e in + let len = Obj.size obj in + let lst = Obj.field obj (len - 1) in + if is_data lst then + let data = Obj.obj (Obj.field lst 1) in + assoc i data + else None + +(** Add data to any exception *) +let add e i v : exn = + let obj = Obj.repr e in + let len = Obj.size obj in + let lst = Obj.field obj (len - 1) in + if is_data lst then + (** The exception was already enriched *) + let data = Obj.obj (Obj.field lst 1) in + (** We retrieve the old information and update it *) + let data = add_assoc i v data in + let ans = Obj.dup obj in + let data = Obj.repr (token, data) in + let () = Obj.set_field ans (len - 1) data in + Obj.obj ans + else + (** This was a plain exception *) + let ans = Obj.new_block 0 (succ len) in + (** We build the new enriched exception from scratch *) + let () = + for i = 0 to len - 1 do + Obj.set_field ans i (Obj.field obj i) + done + in + let data = Obj.repr (token, [i, v]) in + let () = Obj.set_field ans len data in + Obj.obj ans diff --git a/lib/exninfo.mli b/lib/exninfo.mli new file mode 100644 index 0000000000..0c4e6214d7 --- /dev/null +++ b/lib/exninfo.mli @@ -0,0 +1,21 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(** Additional information worn by exceptions. *) + +type +'a t +(** Information containing a given type. *) + +val make : unit -> 'a t +(** Create a new information. *) + +val add : exn -> 'a t -> 'a -> exn +(** Add an information to an exception. *) + +val get : exn -> 'a t -> 'a option +(** Get an information worn by an exception. Returns [None] if undefined. *) |