]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_test/mqgtop.ml
patched
[helm.git] / helm / ocaml / mathql_test / mqgtop.ml
index 6304a65f559bb14d5f35a7fe85d438a5ab85c895..35aca18c48db32f4c715e7b7c1e76e6944bf7aca 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
 let query_num = ref 1
 
 let interp_file = ref "interp.cic" 
 
-let log_file = ref "MQGenLog.htm"
+let log_file = ref ""
 
 let show_queries = ref false
 
@@ -35,9 +38,10 @@ let int_options = ref ""
 
 let nl = " <p>\n"
 
-module MQI = MQueryInterpreter
+module MQX  = MQueryMisc 
+module MQI  = MQueryInterpreter
 module MQIC = MQIConn
-module MQG = MQueryGenerator
+module MQG  = MQueryGenerator
 
 let get_handle () = 
    MQIC.init (MQIC.flags_of_string ! int_options)
@@ -160,7 +164,7 @@ let mpattern n m l =
       | term :: tail -> 
          pattern level tail;
         print_string ("? " ^ CicPp.ppterm term ^ nl);
-        let t0 = Sys.time () in
+        let t = MQX.start_time () in
          let om,rm,sm = C.get_constraints term in
         let oml,rml,sml = List.length om, List.length rm, List.length sm in 
         let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
@@ -170,10 +174,10 @@ let mpattern n m l =
         if not (List.mem q ! queries) then
         begin
            issue handle q;
-           let t1 = Sys.time () -. t0 in
            Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
-           Printf.printf "%i GEN = %i: %.2fs%s"
-              (pred ! query_num) (oml + rml + sml + ool + rol + sol) t1 nl;
+           Printf.printf "%i GEN = %i: %s"
+              (pred ! query_num) (oml + rml + sml + ool + rol + sol) 
+              (MQX.stop_time t ^ nl);
            flush stdout; queries := q :: ! queries
         end
    in 
@@ -227,8 +231,6 @@ let mbackward n m l =
       (List.length ! queries);
    flush stderr
 *)   
-
-let set_options s = int_options := s
  
 let check () =
    let handle = get_handle () in
@@ -245,6 +247,7 @@ let prerr_help () =
    prerr_endline "OPTIONS:\n";
    prerr_endline "-h  -help               shows this help message";
    prerr_endline "-q  -show-queries       outputs generated queries";
+   prerr_endline "-l  -log-file FILE      sets the log file";
    prerr_endline "-o  -options STRING     sets the interpreter options";
    prerr_endline "-c  -check              checks the database connection";
    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
@@ -275,11 +278,11 @@ let rec parse = function
    | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
    | ("-x"|"-execute") :: rem -> execute stdin; parse rem
    | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
-   | ("-o"|"-options") :: arg :: rem -> set_options arg; parse rem
+   | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
    | ("-c"|"-check") :: rem -> check (); parse rem
-(*   | ("-C"|"-compose") :: rem -> compose (); parse rem
-*)   | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
-(*   | ("-M"|"-backward") :: arg :: rem ->
+   | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
+(*   | ("-C"|"-compose") :: rem -> compose (); parse rem   
+   | ("-M"|"-backward") :: arg :: rem ->
       let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
    | ("-MB"|"-multi-backward") :: arg :: rem ->
       let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
@@ -289,10 +292,10 @@ let rec parse = function
    | _ :: rem -> parse rem
 
 let _ =
+   let t = MQX.start_time () in
    Logger.log_callback :=
-      (Logger.log_to_html
-      ~print_and_flush:(function s -> print_string s ; flush stdout)) ; 
+      (Logger.log_to_html 
+       ~print_and_flush:(fun s -> print_string s; flush stdout)) ; 
    parse (List.tl (Array.to_list Sys.argv)); 
-   prerr_endline ("mqgtop: done in " ^ string_of_float (Sys.time ()) ^
-                  " seconds");
+   prerr_endline ("mqgtop: done in " ^ (MQX.stop_time t));
    exit 0