From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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