X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fmathql_test%2Fmqgtop.ml;h=be35ac6c874586a74d165989c8722599cf85b265;hb=cab4eba3c7da115ecc1973d989b321b46835e1eb;hp=6304a65f559bb14d5f35a7fe85d438a5ab85c895;hpb=48b9bb5e9504aba97cff28a9d7e2797feb42972e;p=helm.git

diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml
index 6304a65f5..be35ac6c8 100644
--- a/helm/ocaml/mathql_test/mqgtop.ml
+++ b/helm/ocaml/mathql_test/mqgtop.ml
@@ -23,11 +23,14 @@
  * 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,20 +164,20 @@ 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
 	 let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
          let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
-	 let q = MQG.searchPattern (om,rm,sm) (oo,ro,so) in 
+	 let q = MQG.query_of_constraints None (om,rm,sm) (oo,ro,so) in 
 	 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,20 +247,21 @@ 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";
    prerr_endline "-x  -execute            issues a query given in the input file";
    prerr_endline "-i  -interp FILE        sets the CIC short names interpretation file";
    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
-   prerr_endline "-C  -compose            issues the \"Compose\" query reading its specifications";
-   prerr_endline "                        from the input file";
    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
+(*   prerr_endline "-C  -compose            issues the \"Compose\" query reading its specifications";
+   prerr_endline "                        from the input file"; 
    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all";
    prerr_endline "                        CIC terms in the input file";
    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
    prerr_endline "                        on all CIC terms in the input file";
-   prerr_endline "-P  -pattern LEVEL      issues the \"Pattern\" query for the given level on all";
+*)   prerr_endline "-P  -pattern LEVEL      issues the \"Pattern\" query for the given level on all";
    prerr_endline "                        CIC terms in the input file";
    prerr_endline "-MP -multi-pattern      issues the \"Pattern\" query for each level from 7 to 0";
    prerr_endline "                        on all CIC terms in the input file\n";
@@ -275,11 +278,12 @@ 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
+   | ("-L"|"-Locate") :: arg :: rem -> locate 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 +293,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