* 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
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)
| 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
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
(List.length ! queries);
flush stderr
*)
-
-let set_options s = int_options := s
let check () =
let handle = get_handle () in
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";
| ("-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
| _ :: 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
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
module U = MQueryUtil
module X = MQueryMisc
module I = MQueryInterpreter
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
let _ =
let module U = MQueryUtil in
let module X = MQueryMisc in
projects / helm.git / commitdiff