--- /dev/null
+requires=""
+version="0.0.1"
+archive(byte)="extlib.cma"
+archive(native)="extlib.cmxa"
+linkopts=""
-requires="zip expat"
+requires="zip expat helm-extlib"
version="0.0.1"
archive(byte)="xml.cma"
archive(native)="xml.cmxa"
# Warning: the modules must be in compilation order
NULL =
MODULES = \
+ extlib \
xml \
registry \
utf8_macros \
| 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,_,_,_)
(** 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
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
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
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)
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
--- /dev/null
+*.cm[iaox]
+*.cmxa
--- /dev/null
+hExtlib.cmo: hExtlib.cmi
+hExtlib.cmx: hExtlib.cmi
--- /dev/null
+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
--- /dev/null
+(* 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 }
+
--- /dev/null
+(* 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
PACKAGE = xml
-REQUIRES = zip expat
+REQUIRES = zip expat helm-extlib
PREDICATES =
INTERFACE_FILES = \
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
projects / helm.git / commitdiff