Cleaning interface of Util.

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

1 files changed, 0 insertions, 127 deletions

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