From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 14:20:17 +0000 (+0000) Subject: A bit of profiling functions added here and there. X-Git-Tag: LAST_BEFORE_NEW~95 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2534f543cfce5f39b0445e593df5810ba2cbf5ad;p=helm.git A bit of profiling functions added here and there. --- diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 5a7fe0b9f..4fe206f74 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -120,6 +120,28 @@ let disambiguate_thing ~aliases ~universe CoercDb.use_coercions := saved_use_coercions; raise exn +let disambiguate_thing = + let profiler = CicUtil.profile "disambiguate_thing" in + fun ~aliases ~universe + ~(f:?fresh_instances:bool -> + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + 'a -> 'b) + ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b) + (thing: 'a) + -> profiler.CicUtil.profile + (disambiguate_thing ~aliases ~universe ~f ~set_aliases) thing + +let disambiguate_thing ~aliases ~universe + ~(f:?fresh_instances:bool -> + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + 'a -> 'b) + ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b) + (thing: 'a) += + Obj.magic disambiguate_thing ~aliases ~universe ~f ~set_aliases thing + let set_aliases aliases (choices, user_asked) = (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices), user_asked @@ -137,4 +159,3 @@ let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = assert (fresh_instances = None); let f = Disambiguator.disambiguate_obj ~dbd ~uri in disambiguate_thing ~aliases ~universe ~f ~set_aliases obj - diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 4bb407975..3658b0c20 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -691,6 +691,8 @@ let make_absolute paths path = with Unix.Unix_error _ as exc -> raise (UnableToInclude path) ;; +let profiler_include = CicUtil.profile "include" + let eval_command opts status cmd = let status,cmd = disambiguate_command status cmd in let cmd,notation_ids' = CicNotation.process_notation cmd in @@ -709,7 +711,8 @@ let eval_command opts status cmd = raise (IncludedFileNotCompiled moopath) in let stream = Stream.of_channel ic in let status = ref status in - !eval_from_stream_ref status stream (fun _ _ -> ()); + profiler_include.CicUtil.profile + (!eval_from_stream_ref status stream) (fun _ _ -> ()); close_in ic; !status | GrafiteAst.Set (loc, name, value) -> diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index c4f8f5547..4d549fade 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -176,6 +176,10 @@ let add_obj uri obj status = CicEnvironment.remove_obj uri; (* -1 *) raise exc end + +let add_obj = + let profiler = CicUtil.profile "add_obj" in + fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status module OrderedUri = struct