diff options
author | 2013-04-15 16:05:23 +0000 | |
---|---|---|
committer | 2013-04-15 16:05:23 +0000 | |
commit | 589c0c07eb3f9554f6d0949c07f475be53b1bb2b (patch) | |
tree | 678f2eb6b62d89696875e177e6232359586fcf64 /lib/cObj.mli | |
parent | 6bcf420febbce8092db54eb23ed17fa3963c0c99 (diff) |
votour: a small tool for guided tours of .vo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/cObj.mli')
-rw-r--r-- | lib/cObj.mli | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/lib/cObj.mli b/lib/cObj.mli index 3264ca61f..16933a4aa 100644 --- a/lib/cObj.mli +++ b/lib/cObj.mli @@ -19,6 +19,31 @@ val size_b : 'a -> int val size_kb : 'a -> int (** Same as [size] in kilobytes. *) +(** {6 Physical size of an ocaml value with sharing.} *) + +(** This time, all the size of objects are computed with respect + to a larger object containing them all, and we only count + the new blocks not already seen earlier in the left-to-right + visit of the englobing object. *) + +(** Provides the global object in which we'll search shared sizes *) + +val register_shared_size : 'a -> unit + +(** Shared size (in word) of an object with respect to the global object + given by the last [register_shared_size]. *) + +val shared_size_of_obj : 'a -> int + +(** Same, with an object indicated by its occurrence in the global + object. The very same object could have a zero size or not, depending + of the occurrence we're considering in the englobing object. + For speaking of occurrences, we use an [int list] for a path + of field indexes (leftmost = deepest block, rightmost = top block of the + global object). *) + +val shared_size_of_pos : int list -> int + (** {6 Logical size of an OCaml value.} *) val obj_stats : 'a -> int * int * int |