Nouveau profiler compatible avec ocaml >= 3.01

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

1 files changed, 20 insertions, 0 deletions

diff --git a/lib/profile.mli b/lib/profile.mli
index 8d4105cf6a..13c75cc8c0 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -106,3 +106,23 @@ val profile7 :
   ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) 
     -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
 
+
+(* Some utilities to compute the logical and physical sizes and depth
+   of ML objects *)
+
+(* Print logical size (in words) and depth of its argument *)
+(* This function does not disturb the heap *)
+val print_logical_stats : 'a -> unit
+
+(* Print physical size, logical size (in words) and depth of its argument *)
+(* This function allocates itself a lot (the same order of magnitude
+   as the physical size of its argument) *)
+val print_stats : 'a -> unit
+
+(* Return physical size, logical size (in words) and depth of its argument *)
+(* This function allocates itself a lot *)
+val obj_stats : 'a -> int * int * int
+
+(* Return physical size of its argument *)
+(* This function allocates itself a lot *)
+val obj_shared_size : 'a -> int