From: Ferruccio Guidi Date: Wed, 21 May 2003 11:00:31 +0000 (+0000) Subject: patched X-Git-Tag: submitted~41 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=02f8929bd58c6408545b550bcad0edb8702ca933;p=helm.git patched --- diff --git a/helm/ocaml/mathql_test/.depend b/helm/ocaml/mathql_test/.depend index 6974b7052..6c5f0ca1b 100644 --- a/helm/ocaml/mathql_test/.depend +++ b/helm/ocaml/mathql_test/.depend @@ -1,2 +1,2 @@ -mqgtop.cmo: mQGTopParser.cmi +mqgtop.cmo: mQGTopParser.cmo mqgtop.cmx: mQGTopParser.cmx diff --git a/helm/ocaml/mathql_test/mQGTopLexer.mll b/helm/ocaml/mathql_test/mQGTopLexer.mll index cf116641b..476460646 100644 --- a/helm/ocaml/mathql_test/mQGTopLexer.mll +++ b/helm/ocaml/mathql_test/mQGTopLexer.mll @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* AUTOR: Ferruccio Guidi + *) + { open MQGTopParser diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly index 9fd70a033..8aa01b6c4 100644 --- a/helm/ocaml/mathql_test/mQGTopParser.mly +++ b/helm/ocaml/mathql_test/mQGTopParser.mly @@ -23,6 +23,10 @@ * http://cs.unibo.it/helm/. */ +/* AUTOR: Ferruccio Guidi + */ + + %{ let f (x, y, z) = x let s (x, y, z) = y diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml index 6304a65f5..35aca18c4 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 + *) + 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 = "

\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 diff --git a/helm/ocaml/mathql_test/mqitop.ml b/helm/ocaml/mathql_test/mqitop.ml index a9673205f..8a8053718 100644 --- a/helm/ocaml/mathql_test/mqitop.ml +++ b/helm/ocaml/mathql_test/mqitop.ml @@ -1,3 +1,31 @@ +(* 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 + *) + module U = MQueryUtil module X = MQueryMisc module I = MQueryInterpreter diff --git a/helm/ocaml/mathql_test/mqtop.ml b/helm/ocaml/mathql_test/mqtop.ml index d601d65f9..4b8da7f49 100644 --- a/helm/ocaml/mathql_test/mqtop.ml +++ b/helm/ocaml/mathql_test/mqtop.ml @@ -1,3 +1,31 @@ +(* 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 + *) + let _ = let module U = MQueryUtil in let module X = MQueryMisc in