]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/syntax_extensions/profiling_macros.ml
parameter sintax added to axiom statement
[helm.git] / helm / software / components / syntax_extensions / profiling_macros.ml
index 7febf92440b9c02e1af8ee37e4c05b52315fe712..9f5034a589dede7f45b7ec7ecbde5041882f01a8 100644 (file)
@@ -5,8 +5,8 @@ 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 ensure_label_in_table label =
@@ -29,13 +29,12 @@ let start label =
 let stop label extra =
   ensure_label_in_table label;
   let id = Hashtbl.find profiler_label2int label in
-  "(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 __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_start_stop _ label = 
@@ -73,8 +72,11 @@ let profile_stop _ label =
   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);;
+*)
+