X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fsyntax_extensions%2Fprofiling_macros.ml;h=9f5034a589dede7f45b7ec7ecbde5041882f01a8;hb=6ad533c972e6c9e9db53f38f972e7c0792160f2e;hp=fe5926a432c9312e5ef88e9ebadf778027def622;hpb=4cdf45f08cd95641a094312ddc558320b874fa16;p=helm.git

diff --git a/components/syntax_extensions/profiling_macros.ml b/components/syntax_extensions/profiling_macros.ml
index fe5926a43..9f5034a58 100644
--- a/components/syntax_extensions/profiling_macros.ml
+++ b/components/syntax_extensions/profiling_macros.ml
@@ -3,48 +3,80 @@ let profiler_no = ref 0;;
 let profiler_label2int = Hashtbl.create 3;;
 let name = ref "";;
 
-
 let banner _ pname = 
   name := pname; 
- "(Array.make "^string_of_int max_profilers^" (0,0.)),
-  (Array.make "^string_of_int max_profilers^" (0.))"
+ "(Array.make "^string_of_int max_profilers^" (0,0.)), "^
+ "(Array.make "^string_of_int max_profilers^" (0.))"
 ;;
 
-let profile_start _ label =
-  if !profiler_no > max_profilers then
-    raise (Invalid_argument "Too many profilers.");
+let ensure_label_in_table label =
   if not (Hashtbl.mem profiler_label2int label) then
     begin
+      if !profiler_no > max_profilers then
+        raise (Invalid_argument "Too many profilers.");
       Hashtbl.add profiler_label2int label !profiler_no;
       incr profiler_no;
-    end;
+    end
+;;
+  
+
+let start label =
+  ensure_label_in_table label;
   let id = Hashtbl.find profiler_label2int label in
   " ((snd "^ !name^").("^string_of_int id^") <- Unix.gettimeofday()) "
 ;;
       
-let profile_stop _ label =
-  if not (Hashtbl.mem profiler_label2int label) then
-    raise (Invalid_argument "Profiler 'stop' before 'begin'.");
+let stop label extra =
+  ensure_label_in_table label;
   let id = Hashtbl.find profiler_label2int label in
-  " (
-    let interval = 
-      Unix.gettimeofday () -. (snd "^ !name^").("^string_of_int id^") 
-    in
-    let oldcount,oldval = (fst "^ !name^").("^string_of_int id^") in
-    (fst "^ !name^").("^string_of_int id^") <- (oldcount+1,interval +. oldval)
-   ) "
+  "(let __res = " ^ extra ^ "  in ( "^
+  "let interval = Unix.gettimeofday () -. "^
+    "(snd "^ !name^").("^string_of_int id^") in "^
+  "let oldcount,oldval = (fst "^ !name^").("^string_of_int id^") in "^
+  "(fst "^ !name^").("^string_of_int id^") <- "^
+    "(oldcount+1,interval +. oldval)); __res )"
 ;;
 
-let profile_show _ _ =
+let profile_start_stop _ label = 
+  let label,extra =
+    match Str.bounded_split (Str.regexp "\n") label 2 with
+    | [label;extra] -> label,extra
+    | _ -> 
+        raise (Invalid_argument ("Profiler 'stop' with a bad label:" ^ label))
+  in
+  let start = start label in
+  let stop = stop label extra in
+  "let _ = " ^ start ^ " in " ^ stop
+;; 
+
+let profile_show _ prefix =
   (Hashtbl.fold 
     (fun k v acc -> 
       acc ^ 
       "let t = (fst "^ !name^").("^string_of_int v^") in "^
-      "let acc = acc ^ Printf.sprintf \"%20s: %5d %8.4f\" \""^k^"\" (fst t) (snd t) in")
+      "let acc = acc ^ Printf.sprintf \"%-15s %25s: %8d %8.4f\\n\" \"" ^ 
+      prefix ^ "\" \"" ^  k ^
+      "\" (fst t) (snd t) in ")
     profiler_label2int "let acc = \"\" in ") ^ " acc "
 ;;
 
+let profile_start _ label = start label ;;
+let profile_stop _ label = 
+  let label,extra =
+    match Str.bounded_split (Str.regexp "\n") label 2 with
+    | [label;extra] -> label,extra
+    | [label] -> label,"()"
+    | _ -> 
+        raise (Invalid_argument ("Profiler 'stop' with a bad label:" ^ label))
+  in
+  stop label extra
+;;
+
+(*
 Quotation.add "profiler" (Quotation.ExStr banner);;
+Quotation.add "profile" (Quotation.ExStr profile_start_stop);;
 Quotation.add "start" (Quotation.ExStr profile_start);;
 Quotation.add "stop" (Quotation.ExStr profile_stop);;
 Quotation.add "show" (Quotation.ExStr profile_show);;
+*)
+