calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)

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

2 files changed, 73 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 26b77a82a..e7cf32564 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -487,3 +487,72 @@ let prvect_with_sep sep elem v =
       in
   let n = Array.length v in
   if n = 0 then [< >] else pr (n - 1)
+
+(*s Size of ocaml values. *)
+
+module Size = struct
+  
+  open Obj
+
+  (*s Pointers already visited are stored in a hash-table, where
+      comparisons are done using physical equality. *)
+
+  module H = Hashtbl.Make(
+    struct 
+      type t = Obj.t 
+      let equal = (==) 
+      let hash o = Hashtbl.hash (magic o : int)
+    end)
+	       
+  let node_table = (H.create 257 : unit H.t)
+		     
+  let in_table o = try H.find node_table o; true with Not_found -> false
+      
+  let add_in_table o = H.add node_table o ()
+			 
+  let reset_table () = H.clear node_table
+			 
+  (*s Objects are traversed recursively, as soon as their tags are less than
+      [no_scan_tag]. [count] records the numbers of words already visited. *)
+
+  let size_of_double = size (repr 1.0)
+			 
+  let count = ref 0
+		
+  let rec traverse t =
+    if not (in_table t) then begin
+      add_in_table t;
+      if is_block t then begin
+	let n = size t in
+	let tag = tag t in
+	if tag < no_scan_tag then begin
+	  count := !count + 1 + n;
+	  for i = 0 to n - 1 do
+      	    let f = field t i in 
+	    if is_block f then traverse f
+	  done
+	end else if tag = string_tag then
+	  count := !count + 1 + n 
+	else if tag = double_tag then
+	  count := !count + size_of_double
+	else if tag = double_array_tag then
+	  count := !count + 1 + size_of_double * n 
+	else
+	  incr count
+      end
+    end
+      
+  (*s Sizes of objects in words and in bytes. The size in bytes is computed
+      system-independently according to [Sys.word_size]. *)
+
+  let size_w o =
+    reset_table ();
+    count := 0;
+    traverse (repr o);
+    !count
+
+  let size_b o = (size_w o) * Sys.word_size lsr 3
+
+end
+
+let size_b = Size.size_b
diff --git a/lib/util.mli b/lib/util.mli
index 26d912d15..fc3c980c6 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -158,3 +158,7 @@ val prlist_with_sep :
    (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b list -> 'a Stream.t
 val prvect_with_sep :
    (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b array -> 'a Stream.t
+
+(*s Size of ocaml values. *)
+
+val size_b : 'a -> int