aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cList.ml7
-rw-r--r--lib/cList.mli4
-rw-r--r--lib/cObj.ml111
-rw-r--r--lib/cObj.mli34
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/profile.ml75
-rw-r--r--lib/profile.mli9
-rw-r--r--lib/util.ml127
-rw-r--r--lib/util.mli41
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) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 05:00:53 +0000