From: Claudio Sacerdoti Coen Date: Fri, 23 Sep 2005 16:03:12 +0000 (+0000) Subject: CicUtil.profile ==> HExtlib.profile X-Git-Tag: LAST_BEFORE_NEW~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=108f7ef287b08d4d7228790d7c6d956434f16c6c;p=helm.git CicUtil.profile ==> HExtlib.profile --- diff --git a/helm/ocaml/METAS/meta.helm-extlib.src b/helm/ocaml/METAS/meta.helm-extlib.src new file mode 100644 index 000000000..849658fc4 --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-extlib.src @@ -0,0 +1,5 @@ +requires="" +version="0.0.1" +archive(byte)="extlib.cma" +archive(native)="extlib.cmxa" +linkopts="" diff --git a/helm/ocaml/METAS/meta.helm-xml.src b/helm/ocaml/METAS/meta.helm-xml.src index 933038f79..626e644fc 100644 --- a/helm/ocaml/METAS/meta.helm-xml.src +++ b/helm/ocaml/METAS/meta.helm-xml.src @@ -1,4 +1,4 @@ -requires="zip expat" +requires="zip expat helm-extlib" version="0.0.1" archive(byte)="xml.cma" archive(native)="xml.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 0fd0bd934..a59228b34 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,6 +1,7 @@ # Warning: the modules must be in compilation order NULL = MODULES = \ + extlib \ xml \ registry \ utf8_macros \ diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 8bb137f20..818342515 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -209,34 +209,6 @@ let rec mk_rels howmany from = | 0 -> [] | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) -let profiling_enabled = true - -type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } -let profile = - if profiling_enabled then - function s -> - let total = ref 0.0 in - let profile f x = - let before = Unix.gettimeofday () in - try - let res = f x in - let after = Unix.gettimeofday () in - total := !total +. (after -. before); - res - with - exc -> - let after = Unix.gettimeofday () in - total := !total +. (after -. before); - raise exc - in - at_exit - (fun () -> - print_endline - ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); - { profile = profile } - else - function _ -> { profile = fun f x -> f x } - let id_of_annterm = function | Cic.ARel (id,_,_,_) diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 744ac3211..3243faec8 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -60,9 +60,3 @@ val attributes_of_obj: Cic.obj -> Cic.attribute list (** mk_rels [howmany] [from] * creates a list of [howmany] rels starting from [from] in decreasing order *) val mk_rels : int -> int -> Cic.term list - -(** profile s - * returns a profiling function; [s] is used for labelling the total time at - the end of the execution *) -type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } -val profile : string -> profiler diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index d267b52b1..0679b9aee 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -690,7 +690,7 @@ module Make (C: Callbacks) = fun _ _ _ -> term)) uris -let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing" +let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe @@ -784,7 +784,7 @@ let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing" let foo () = let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in (k , ugraph1 ) -in refine_profiler.CicUtil.profile foo () +in refine_profiler.HExtlib.profile foo () with | Try_again -> Uncertain, ugraph | Invalid_choice -> Ko, ugraph diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 0b63f6a8c..b450d2502 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -40,13 +40,13 @@ exception AssertFailure of string;; let debug_print = fun _ -> () -let profiler = CicUtil.profile "CicRefine.fo_unif" +let profiler = HExtlib.profile "CicRefine.fo_unif" let fo_unif_subst subst context metasenv t1 t2 ugraph = try let foo () = CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph -in profiler.CicUtil.profile foo () +in profiler.HExtlib.profile foo () with (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg)) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) @@ -1088,10 +1088,10 @@ let type_of_aux' metasenv context term = raise e ;; *) -let profiler2 = CicUtil.profile "CicRefine" +let profiler2 = HExtlib.profile "CicRefine" let type_of_aux' metasenv context term ugraph = - profiler2.CicUtil.profile (type_of_aux' metasenv context term) ugraph + profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph let typecheck metasenv uri obj = - profiler2.CicUtil.profile (typecheck metasenv uri) obj + profiler2.HExtlib.profile (typecheck metasenv uri) obj diff --git a/helm/ocaml/extlib/.cvsignore b/helm/ocaml/extlib/.cvsignore new file mode 100644 index 000000000..8d64a5378 --- /dev/null +++ b/helm/ocaml/extlib/.cvsignore @@ -0,0 +1,2 @@ +*.cm[iaox] +*.cmxa diff --git a/helm/ocaml/extlib/.depend b/helm/ocaml/extlib/.depend new file mode 100644 index 000000000..cbb3fcdfe --- /dev/null +++ b/helm/ocaml/extlib/.depend @@ -0,0 +1,2 @@ +hExtlib.cmo: hExtlib.cmi +hExtlib.cmx: hExtlib.cmi diff --git a/helm/ocaml/extlib/Makefile b/helm/ocaml/extlib/Makefile new file mode 100644 index 000000000..6dccb5a90 --- /dev/null +++ b/helm/ocaml/extlib/Makefile @@ -0,0 +1,12 @@ +PACKAGE = extlib +REQUIRES = +PREDICATES = + +INTERFACE_FILES = \ + hExtlib.mli +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = + +include ../Makefile.common diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml new file mode 100644 index 000000000..6e1f3564a --- /dev/null +++ b/helm/ocaml/extlib/hExtlib.ml @@ -0,0 +1,56 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +(** PROFILING *) + +let profiling_enabled = true + +type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } +let profile = + if profiling_enabled then + function s -> + let total = ref 0.0 in + let profile f x = + let before = Unix.gettimeofday () in + try + let res = f x in + let after = Unix.gettimeofday () in + total := !total +. (after -. before); + res + with + exc -> + let after = Unix.gettimeofday () in + total := !total +. (after -. before); + raise exc + in + at_exit + (fun () -> + print_endline + ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); + { profile = profile } + else + function _ -> { profile = fun f x -> f x } + diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli new file mode 100644 index 000000000..05a8b7d29 --- /dev/null +++ b/helm/ocaml/extlib/hExtlib.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(** profile s + * returns a profiling function; [s] is used for labelling the total time at + the end of the execution *) +type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } +val profile : string -> profiler diff --git a/helm/ocaml/xml/Makefile b/helm/ocaml/xml/Makefile index 7ecb75457..fabd2dfce 100644 --- a/helm/ocaml/xml/Makefile +++ b/helm/ocaml/xml/Makefile @@ -1,5 +1,5 @@ PACKAGE = xml -REQUIRES = zip expat +REQUIRES = zip expat helm-extlib PREDICATES = INTERFACE_FILES = \ diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml index 6d6775c6d..4439fad1d 100644 --- a/helm/ocaml/xml/xml.ml +++ b/helm/ocaml/xml/xml.ml @@ -101,6 +101,10 @@ let pp_to_outchan strm oc = flush oc ;; +let pp_to_outchan = + let profiler = HExtlib.profile "Xml.pp_to_outchan" in + fun strm oc -> profiler.HExtlib.profile (pp_to_outchan strm) oc + let pp_to_gzipchan strm oc = pp_gen (fun s -> Gzip.output oc s 0 (String.length s)) strm