Cleaning interface of Util.

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

9 files changed, 163 insertions, 246 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index 3e4c0a4b3..3a4a2f566 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -66,6 +66,7 @@ sig
 
   (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
   val tabulate : (int -> 'a) -> int -> 'a list
+  val interval : int -> int -> int list
   val make : int -> 'a -> 'a list
   val assign : 'a list -> int -> 'a -> 'a list
   val distinct : 'a list -> bool
@@ -369,6 +370,12 @@ let tabulate f len =
   loop dummy 0;
   dummy.tail
 
+let interval n m =
+  let rec interval_n (l,m) =
+    if n > m then l else interval_n (m::l, pred m)
+  in
+  interval_n ([], m)
+
 let addn n v =
   let rec aux n l =
     if n = 0 then l
diff --git a/lib/cList.mli b/lib/cList.mli
index ef4406150..20b63dcd6 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -79,6 +79,10 @@ sig
   val tabulate : (int -> 'a) -> int -> 'a list
   (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 
+  val interval : int -> int -> int list
+  (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when 
+      [j <= i]. *)
+
   val make : int -> 'a -> 'a list
   (** [make n x] returns a list made of [n] times [x]. Raise
       [Invalid_argument "List.make"] if [n] is negative. *)
diff --git a/lib/cObj.ml b/lib/cObj.ml
new file mode 100644
index 000000000..ed14563df
--- /dev/null
+++ b/lib/cObj.ml
@@ -0,0 +1,111 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(*s Logical and physical size of ocaml values. *)
+
+(** {6 Logical sizes} *)
+
+let c = ref 0
+let s = ref 0
+let b = ref 0
+let m = ref 0
+
+let rec obj_stats d t =
+  if Obj.is_int t then m := max d !m
+  else if Obj.tag t >= Obj.no_scan_tag then
+    if Obj.tag t = Obj.string_tag then
+      (c := !c + Obj.size t; b := !b + 1; m := max d !m)
+    else if Obj.tag t = Obj.double_tag then
+      (s := !s + 2; b := !b + 1; m := max d !m)
+    else if Obj.tag t = Obj.double_array_tag then
+      (s := !s + 2 * Obj.size t; b := !b + 1; m := max d !m)
+    else (b := !b + 1; m := max d !m)
+  else
+    let n = Obj.size t in
+    s := !s + n; b := !b + 1;
+    block_stats (d + 1) (n - 1) t
+
+and block_stats d i t =
+  if i >= 0 then (obj_stats d (Obj.field t i); block_stats d (i-1) t)
+
+let obj_stats a =
+  c := 0; s:= 0; b:= 0; m:= 0;
+  obj_stats 0 (Obj.repr a);
+  (!c, !s + !b, !m)
+
+(** {6 Physical sizes} *)
+
+(*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 (Obj.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 = Obj.size (Obj.repr 1.0)
+
+let count = ref 0
+
+let rec traverse t =
+  if not (in_table t) then begin
+    if Obj.is_block t then begin
+      add_in_table t;
+      let n = Obj.size t in
+      let tag = Obj.tag t in
+      if tag < Obj.no_scan_tag then begin
+        count := !count + 1 + n;
+        for i = 0 to n - 1 do
+          let f = Obj.field t i in traverse f
+        done
+      end else if tag = Obj.string_tag then
+        count := !count + 1 + n
+      else if tag = Obj.double_tag then
+        count := !count + size_of_double
+      else if tag = Obj.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 o =
+  reset_table ();
+  count := 0;
+  traverse (Obj.repr o);
+  !count
+
+let size_b o = (size o) * (Sys.word_size / 8)
+
+let size_kb o = (size o) / (8192 / Sys.word_size)
+
+(*s Total size of the allocated ocaml heap. *)
+
+let heap_size () =
+  let stat = Gc.stat ()
+  and control = Gc.get () in
+  let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
+  (max_words_total * (Sys.word_size / 8))
+
+let heap_size_kb () = (heap_size () + 1023) / 1024
diff --git a/lib/cObj.mli b/lib/cObj.mli
new file mode 100644
index 000000000..61c778f1f
--- /dev/null
+++ b/lib/cObj.mli
@@ -0,0 +1,34 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(** {6 Physical size of an ocaml value.}
+
+  These functions explore objects recursively and may allocate a lot. *)
+
+val size : 'a -> int
+(** Physical size of an object in words. *)
+
+val size_b : 'a -> int
+(** Same as [size] in bytes. *)
+
+val size_kb : 'a -> int
+(** Same as [size] in kilobytes. *)
+
+(** {6 Logical size of an OCaml value *)
+
+val obj_stats : 'a -> int * int * int
+(** Return the (logical) value size, the string size, and the maximum depth of
+    the object. This loops on cyclic structures. *)
+
+(** {6 Total size of the allocated ocaml heap. } *)
+
+val heap_size : unit -> int
+(** Heap size, in words. *)
+
+val heap_size_kb : unit -> int
+(** Heap size, in kilobytes. *)
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 3716a1021..0dd24d74c 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -4,6 +4,7 @@ Coq_config
 Segmenttree
 Unicodetable
 Deque
+CObj
 CList
 CArray
 Util
diff --git a/lib/profile.ml b/lib/profile.ml
index 9002972d9..b49a66e2f 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -657,80 +657,15 @@ let profile7 e f a b c d g h i =
     last_alloc := get_alloc ();
     raise exn
 
-(* Some utilities to compute the logical and physical sizes and depth
-   of ML objects *)
-
-let c = ref 0
-let s = ref 0
-let b = ref 0
-let m = ref 0
-
-let rec obj_stats d t =
-  if Obj.is_int t then m := max d !m
-  else if Obj.tag t >= Obj.no_scan_tag then
-    if Obj.tag t = Obj.string_tag then
-      (c := !c + Obj.size t; b := !b + 1; m := max d !m)
-    else if Obj.tag t = Obj.double_tag then
-      (s := !s + 2; b := !b + 1; m := max d !m)
-    else if Obj.tag t = Obj.double_array_tag then
-      (s := !s + 2 * Obj.size t; b := !b + 1; m := max d !m)
-    else (b := !b + 1; m := max d !m)
-  else
-    let n = Obj.size t in
-    s := !s + n; b := !b + 1;
-    block_stats (d + 1) (n - 1) t
-
-and block_stats d i t =
-  if i >= 0 then (obj_stats d (Obj.field t i); block_stats d (i-1) t)
-
-let obj_stats a =
-  c := 0; s:= 0; b:= 0; m:= 0;
-  obj_stats 0 (Obj.repr a);
-  (!c, !s + !b, !m)
-
-module H = Hashtbl.Make(
-  struct
-    type t = Obj.t
-    let equal = (==)
-    let hash o = Hashtbl.hash (Obj.magic o : int)
-  end)
-
-let tbl = H.create 13
-
-let rec obj_shared_size s t =
-  if Obj.is_int t then s
-  else if H.mem tbl t then s
-  else begin
-    H.add tbl t ();
-    let n = Obj.size t in
-    if Obj.tag t >= Obj.no_scan_tag then
-      if Obj.tag t = Obj.string_tag then (c := !c + n; s + 1)
-      else if Obj.tag t = Obj.double_tag then s + 3
-      else if Obj.tag t = Obj.double_array_tag then s + 2 * n + 1
-      else s + 1
-    else
-      block_shared_size (s + n + 1) (n - 1) t
-  end
-
-and block_shared_size s i t =
-  if i < 0 then s
-  else block_shared_size (obj_shared_size s (Obj.field t i)) (i-1) t
-
-let obj_shared_size a =
-  H.clear tbl;
-  c := 0;
-  let s = obj_shared_size 0 (Obj.repr a) in
-  (!c, s)
-
 let print_logical_stats a =
-  let (c, s, d) = obj_stats a in
+  let (c, s, d) = CObj.obj_stats a in
   Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d
 
 let print_stats a =
-  let (c1, s, d) = obj_stats a in
-  let (c2, o) = obj_shared_size a in
-  Printf.printf "Size: %8d (str: %8d) (exp: %10d)  Depth: %6d\n"
-    (o + c2) c2 (s + c1) d
+  let (c1, s, d) = CObj.obj_stats a in
+  let c2 = CObj.size a in
+  Printf.printf "Size: %8d (exp: %10d)  Depth: %6d\n"
+    c2 (s + c1) d
 (*
 let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 }
 *)
diff --git a/lib/profile.mli b/lib/profile.mli
index a67622fd2..812fd8b1e 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -113,12 +113,3 @@ val print_logical_stats : 'a -> unit
    This function allocates itself a lot (the same order of magnitude
    as the physical size of its argument) *)
 val print_stats : 'a -> unit
-
-(** Return logical size (first for strings, then for not strings),
-   (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 (string part and rest) 
-   This function allocates itself a lot *)
-val obj_shared_size : 'a -> int * int
diff --git a/lib/util.ml b/lib/util.ml
index 6f9f9bd83..6c1fc39b5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -428,133 +428,6 @@ module Intset = Set.Make(struct type t = int let compare (x:t) (y:t) = compare x
 
 module Intmap = Map.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
 
-let intmap_in_dom x m =
-  try let _ = Intmap.find x m in true with Not_found -> false
-
-let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m []
-
-let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m []
-
-let interval n m =
-  let rec interval_n (l,m) =
-    if n > m then l else interval_n (m::l,pred m)
-  in
-  interval_n ([],m)
-
-(*s Memoization *)
-
-let memo1_eq eq f =
-  let m = ref None in
-  fun x ->
-    match !m with
-        Some(x',y') when eq x x' -> y'
-      | _ -> let y = f x in m := Some(x,y); y
-
-let memo1_1 f = memo1_eq (==) f
-let memo1_2 f =
-  let f' =
-    memo1_eq (fun (x,y) (x',y') -> x==x' && y==y') (fun (x,y) -> f x y) in
-  (fun x y -> f'(x,y))
-
-(* Memorizes the last n distinct calls to f. Since there is no hash,
-   Efficient only for small n. *)
-let memon_eq eq n f =
-  let cache = ref [] in (* the cache: a stack *)
-  let m = ref 0 in      (* usage of the cache *)
-  let rec find x = function
-    | (x',y')::l when eq x x' -> y', l (* cell is moved to the top *)
-    | [] -> (* we assume n>0, so creating one memo cell is OK *)
-        incr m; (f x, [])
-    | [_] when !m>=n -> f x,[] (* cache is full: dispose of last cell *)
-    | p::l (* not(eq x (fst p)) *) -> let (y,l') = find x l in (y, p::l')
-  in
-  (fun x ->
-    let (y,l) = find x !cache in
-    cache := (x,y)::l;
-    y)
-
-
-(*s Size of ocaml values. *)
-
-module Size = struct
-
-  (*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 (Obj.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 = Obj.size (Obj.repr 1.0)
-
-  let count = ref 0
-
-  let rec traverse t =
-    if not (in_table t) then begin
-      add_in_table t;
-      if Obj.is_block t then begin
-	let n = Obj.size t in
-	let tag = Obj.tag t in
-	if tag < Obj.no_scan_tag then begin
-	  count := !count + 1 + n;
-	  for i = 0 to n - 1 do
-      	    let f = Obj.field t i in
-	    if Obj.is_block f then traverse f
-	  done
-	end else if tag = Obj.string_tag then
-	  count := !count + 1 + n
-	else if tag = Obj.double_tag then
-	  count := !count + size_of_double
-	else if tag = Obj.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 (Obj.repr o);
-    !count
-
-  let size_b o = (size_w o) * (Sys.word_size / 8)
-
-  let size_kb o = (size_w o) / (8192 / Sys.word_size)
-
-end
-
-let size_w = Size.size_w
-let size_b = Size.size_b
-let size_kb = Size.size_kb
-
-(*s Total size of the allocated ocaml heap. *)
-
-let heap_size () =
-  let stat = Gc.stat ()
-  and control = Gc.get () in
-  let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
-  (max_words_total * (Sys.word_size / 8))
-
-let heap_size_kb () = (heap_size () + 1023) / 1024
-
 (*s interruption *)
 
 let interrupt = ref false
diff --git a/lib/util.mli b/lib/util.mli
index a7586547e..1333d1854 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -15,11 +15,6 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
 
-(** Going down pairs *)
-
-val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
-val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
-
 (** Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
@@ -106,46 +101,12 @@ val delayed_force : 'a delayed -> 'a
 
 (** {6 Misc. } *)
 
-type ('a,'b) union = Inl of 'a | Inr of 'b
+type ('a, 'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
 
 module Intmap : Map.S with type key = int
 
-val intmap_in_dom : int -> 'a Intmap.t -> bool
-val intmap_to_list : 'a Intmap.t -> (int * 'a) list
-val intmap_inv : 'a Intmap.t -> 'a -> int list
-
-val interval : int -> int -> int list
-
-(** {6 Memoization. } *)
-
-(** General comments on memoization:
-   - cache is created whenever the function is supplied (because of
-      ML's polymorphic value restriction).
-   - cache is never flushed (unless the memoized fun is GC'd)
- 
-   One cell memory: memorizes only the last call *)
-val memo1_1 : ('a -> 'b) -> ('a -> 'b)
-val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
-
-(** with custom equality (used to deal with various arities) *)
-val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
-
-(** Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
-val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
-
-(** {6 Size of an ocaml value (in words, bytes and kilobytes). } *)
-
-val size_w : 'a -> int
-val size_b : 'a -> int
-val size_kb : 'a -> int
-
-(** {6 Total size of the allocated ocaml heap. } *)
-
-val heap_size : unit -> int
-val heap_size_kb : unit -> int
-
 (** {6 ... } *)
 (** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)