Skip to content
Browse files

Cleaning interface of Util.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 7208928 commit 4422e16f529359bb96c7eee214b2b6648958ef48 @ppedrot ppedrot committed
View
2 checker/check.ml
@@ -370,4 +370,4 @@ open Printf
let mem s =
let m = try_find_library s in
- h 0 (str (sprintf "%dk" (size_kb m)))
+ h 0 (str (sprintf "%dk" (CObj.size_kb m)))
View
1 checker/check.mllib
@@ -7,6 +7,7 @@ Loc
Segmenttree
Unicodetable
Errors
+CObj
CList
CArray
Util
View
2 checker/check_stat.ml
@@ -20,7 +20,7 @@ let memory_stat = ref false
let print_memory_stat () =
if !memory_stat then begin
- Format.printf "total heap size = %d kbytes\n" (heap_size_kb ());
+ Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ());
Format.print_newline();
flush_all()
end
View
1 dev/printers.mllib
@@ -8,6 +8,7 @@ Loc
Segmenttree
Unicodetable
Errors
+CObj
CList
CArray
Util
View
7 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
View
4 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. *)
View
111 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
View
34 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. *)
View
1 lib/clib.mllib
@@ -4,6 +4,7 @@ Coq_config
Segmenttree
Unicodetable
Deque
+CObj
CList
CArray
Util
View
75 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 }
*)
View
9 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
View
127 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
View
41 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) *)
View
4 library/library.ml
@@ -665,5 +665,5 @@ open Printf
let mem s =
let m = try_find_library s in
h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
- (size_kb m) (size_kb m.library_compiled)
- (size_kb m.library_objects)))
+ (CObj.size_kb m) (CObj.size_kb m.library_compiled)
+ (CObj.size_kb m.library_objects)))
View
6 plugins/extraction/extraction.ml
@@ -333,7 +333,7 @@ and extract_type_scheme env db c p =
| _ ->
let rels = fst (splay_prod env none (type_of env c)) in
let env = push_rels_assum rels env in
- let eta_args = List.rev_map mkRel (interval 1 p) in
+ let eta_args = List.rev_map mkRel (List.interval 1 p) in
extract_type env db 0 (lift p c) eta_args
@@ -719,7 +719,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let oi = mi.ind_packets.(i) in
let nb_tvars = List.length oi.ip_vars
and types = List.map (expand env) oi.ip_types.(j-1) in
- let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
+ let list_tvar = List.map (fun i -> Tvar i) (List.interval 1 nb_tvars) in
let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
let type_cons = instantiation (nb_tvars, type_cons) in
(* Then, the usual variables [s], [ls], [la], ... *)
@@ -848,7 +848,7 @@ let decomp_lams_eta_n n m env c t =
let d = n - m in
(* we'd better keep rels' as long as possible. *)
let rels = (List.firstn d rels) @ rels' in
- let eta_args = List.rev_map mkRel (interval 1 d) in
+ let eta_args = List.rev_map mkRel (List.interval 1 d) in
rels, applist (lift d c,eta_args)
(* Let's try to identify some situation where extracted code
View
9 pretyping/evarutil.ml
@@ -100,9 +100,16 @@ let is_ground_env evd env =
| _ -> true in
List.for_all is_ground_decl (rel_context env) &&
List.for_all is_ground_decl (named_context env)
+
(* Memoization is safe since evar_map and environ are applicative
structures *)
-let is_ground_env = memo1_2 is_ground_env
+let memo f =
+ let m = ref None in
+ fun x y -> match !m with
+ | Some (x', y', r) when x == x' && y == y' -> r
+ | _ -> let r = f x y in m := Some (x, y, r); r
+
+let is_ground_env = memo is_ground_env
(* Return the head evar if any *)
View
2 pretyping/inductiveops.ml
@@ -82,7 +82,7 @@ let mis_is_recursive_subset listind rarg =
Array.exists one_is_rec (dest_subterms rarg)
let mis_is_recursive (ind,mib,mip) =
- mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1))
+ mis_is_recursive_subset (List.interval 0 (mib.mind_ntypes - 1))
mip.mind_recargs
let mis_nf_constructor_type (ind,mib,mip) j =
View
4 tactics/equality.ml
@@ -656,7 +656,7 @@ let descend_then sigma env head dirn =
it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
let brl =
List.map build_branch
- (interval 1 (Array.length mip.mind_consnames)) in
+ (List.interval 1 (Array.length mip.mind_consnames)) in
let ci = make_case_info env ind RegularStyle in
mkCase (ci, p, head, Array.of_list brl)))
@@ -699,7 +699,7 @@ let construct_discriminator sigma env dirn c sort =
let endpt = if i = dirn then true_0 else false_0 in
it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
let brl =
- List.map build_branch(interval 1 (Array.length mip.mind_consnames)) in
+ List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
let ci = make_case_info env ind RegularStyle in
mkCase (ci, p, c, Array.of_list brl)
View
2 tactics/tactics.ml
@@ -1247,7 +1247,7 @@ let any_constructor with_evars tacopt gl =
tclFIRST
(List.map
(fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t)
- (interval 1 nconstr)) gl
+ (List.interval 1 nconstr)) gl
let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1
let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2
View
2 toplevel/command.ml
@@ -534,7 +534,7 @@ let compute_possible_guardness_evidences (ids,_,na) =
but doing it properly involves delta-reduction, and it finally
doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
- interval 0 (List.length ids - 1)
+ List.interval 0 (List.length ids - 1)
type recursive_preentry =
identifier list * constr option list * types list
View
2 toplevel/coqtop.ml
@@ -41,7 +41,7 @@ let memory_stat = ref false
let print_memory_stat () =
if !memory_stat then
- pp (str "total heap size = " ++ int (heap_size_kb ()) ++ str " kbytes" ++ fnl ())
+ pp (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ())
let _ = at_exit print_memory_stat
View
2 toplevel/lemmas.ml
@@ -51,7 +51,7 @@ let adjust_guardness_conditions const = function
| Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
(* let possible_indexes =
List.map2 (fun i c -> match i with Some i -> i | None ->
- interval 0 (List.length ((lam_assum c))))
+ List.interval 0 (List.length ((lam_assum c))))
lemma_guard (Array.to_list fixdefs) in
*)
let indexes =
View
2 toplevel/metasyntax.ml
@@ -831,7 +831,7 @@ let internalization_type_of_entry_type = function
| ETBinderList _ | ETConstrList _ -> assert false
let set_internalization_type typs =
- List.map (down_snd internalization_type_of_entry_type) typs
+ List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
let make_internalization_vars recvars mainvars typs =
let maintyps = List.combine mainvars typs in

0 comments on commit 4422e16

Please sign in to comment.
Something went wrong with that request. Please try again.