Adding more primitives to Exninfo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16214 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 61 insertions, 8 deletions

diff --git a/lib/exninfo.ml b/lib/exninfo.ml
index b62e83b59..21d4eb208 100644
--- a/lib/exninfo.ml
+++ b/lib/exninfo.ml
@@ -36,10 +36,21 @@ let rec add_assoc (i : int) v = function
   if i = j then (j, v) :: l
   else (j, w) :: add_assoc i v l
 
+let rec merge_assoc l1 l2 = match l1 with
+| [] -> l2
+| (i, v) :: l1 -> add_assoc i v (merge_assoc l1 l2)
+
 (** 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
 
+(** As [Array.blit] *)
+let blit obj1 off1 obj2 off2 len =
+  for i = 0 to len - 1 do
+    let data = Obj.field obj1 (off1 + i) in
+    Obj.set_field obj2 (off2 + i) data
+  done
+
 (** Retrieve the optional backtrace set in an exception. *)
 let get (e : exn) i =
   let obj = Obj.repr e in
@@ -68,11 +79,44 @@ let add e i v : exn =
     (** 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 () = blit obj 0 ans 0 len in
     let data = Obj.repr (token, [i, v]) in
     let () = Obj.set_field ans len data in
     Obj.obj ans
+
+let clear e =
+  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 ans = Obj.new_block 0 (pred len) in
+    let () = blit obj 0 ans 0 (pred len) in
+    Obj.obj ans
+  else e
+
+let copy (src : exn) (dst : exn) =
+  let obj = Obj.repr src in
+  let len = Obj.size obj in
+  let lst = Obj.field obj (len - 1) in
+  if is_data lst then
+    (** First object has data *)
+    let src_data = Obj.obj (Obj.field lst 1) in
+    let obj = Obj.repr dst in
+    let len = Obj.size obj in
+    let lst = Obj.field obj (len - 1) in
+    if is_data lst then
+      (** second object has data *)
+      let dst_data = Obj.obj (Obj.field lst 1) in
+      let ans = Obj.dup obj in
+      let data = Obj.repr (token, merge_assoc dst_data src_data) in
+      let () = Obj.set_field ans len data in
+      Obj.obj ans
+    else
+      (** second object has no data *)
+      let ans = Obj.new_block 0 (succ len) in
+      (** We build the new enriched exception from scratch *)
+      let () = blit obj 0 ans 0 len in
+      let data = Obj.repr (token, src_data) in
+      let () = Obj.set_field ans len data in
+      Obj.obj ans
+  else dst
diff --git a/lib/exninfo.mli b/lib/exninfo.mli
index 0c4e6214d..dca8ff7de 100644
--- a/lib/exninfo.mli
+++ b/lib/exninfo.mli
@@ -12,10 +12,19 @@ type +'a t
 (** Information containing a given type. *)
 
 val make : unit -> 'a t
-(** Create a new information. *)
+(** Create a new piece of information. *)
 
 val add : exn -> 'a t -> 'a -> exn
-(** Add an information to an exception. *)
+(** Add information to an exception. *)
 
 val get : exn -> 'a t -> 'a option
-(** Get an information worn by an exception. Returns [None] if undefined. *)
+(** Get information worn by an exception. Returns [None] if undefined. *)
+
+(* val remove : exn -> 'a t -> exn *)
+(** TODO: Remove a given piece of information. *)
+
+val clear : exn -> exn
+(** Remove any information. *)
+
+val copy : exn -> exn -> exn
+(** [copy src dst] adds the additional info from [src] to [dst]. *)