From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jun 2002 13:04:53 +0000 (+0000)
Subject: Benchmarcking informations output.
X-Git-Tag: V_0_3_0_debian_8~36
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9a5fcfd85222669ba70aae8c73433afc047f8f8a;p=helm.git

Benchmarcking informations output.
---

diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml
index ad27d1959..611fdf388 100644
--- a/helm/ocaml/mathql_interpreter/mqint.ml
+++ b/helm/ocaml/mathql_interpreter/mqint.ml
@@ -86,8 +86,17 @@ let rec execute_ex env =
      intersect_ex (execute_ex env l1) (execute_ex env l2)
  |  MQLRVar rvar -> [List.assoc rvar env]
  |  MQLetIn (lvar, l1, l2) ->
-     let _ = letin_ex lvar (execute_ex env l1) in
-      execute_ex env l2
+     let t = Unix.time () in
+      let res =
+       (*CSC: The interesting code *)
+       let _ = letin_ex lvar (execute_ex env l1) in
+        execute_ex env l2
+       (*CSC: end of the interesting code *)
+      in
+       print_string ("LETIN = " ^ string_of_int (List.length res) ^ ": ") ;
+       print_endline (string_of_float (Unix.time () -. t) ^ "s") ;
+       flush stdout ;
+       res
  |  MQLetRef rvar ->
      letref_ex rvar
 ;;