X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_test%2Fmqgtop.ml;fp=helm%2Focaml%2Fmathql_test%2Fmqgtop.ml;h=6304a65f559bb14d5f35a7fe85d438a5ab85c895;hb=48b9bb5e9504aba97cff28a9d7e2797feb42972e;hp=0000000000000000000000000000000000000000;hpb=39c8c5c53680cd374a3eb76993a592cf29bb92ba;p=helm.git diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml new file mode 100644 index 000000000..6304a65f5 --- /dev/null +++ b/helm/ocaml/mathql_test/mqgtop.ml @@ -0,0 +1,298 @@ +(* 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/. + *) + +let query_num = ref 1 + +let interp_file = ref "interp.cic" + +let log_file = ref "MQGenLog.htm" + +let show_queries = ref false + +let int_options = ref "" + +let nl = "

\n" + +module MQI = MQueryInterpreter +module MQIC = MQIConn +module MQG = MQueryGenerator + +let get_handle () = + MQIC.init (MQIC.flags_of_string ! int_options) + (fun s -> print_string s; flush stdout) + +let issue handle q = + let module U = MQueryUtil in + let mode = [Open_wronly; Open_append; Open_creat; Open_text] in + let perm = 64 * 6 + 8 * 6 + 4 in + let time () = + let lt = Unix.localtime (Unix.time ()) in + "NEW LOG: " ^ + string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_year + 1900) ^ " " ^ + string_of_int (lt.Unix.tm_hour) ^ ":" ^ + string_of_int (lt.Unix.tm_min) ^ ":" ^ + string_of_int (lt.Unix.tm_sec) + in + let log q r = + let och = open_out_gen mode perm ! log_file in + let out = output_string och in + if ! query_num = 1 then out (time () ^ nl); + out ("Query: " ^ string_of_int ! query_num ^ nl); + U.text_of_query out q nl; + out ("Result: " ^ nl); + U.text_of_result out r nl; + close_out och + in + if ! show_queries then U.text_of_query (output_string stdout) q nl; + let r = MQI.execute handle q in + U.text_of_result (output_string stdout) r nl; + if ! log_file <> "" then log q r; + incr query_num; + flush stdout + +let get_interp () = + let module L = CicTextualLexer in + let module T = CicTextualParser in + let module P = MQGTopParser in + let lexer = function + | T.ID s -> P.ID s + | T.CONURI u -> P.CONURI u + | T.VARURI u -> P.VARURI u + | T.INDTYURI (u, p) -> P.INDTYURI (u, p) + | T.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s) + | T.LETIN -> P.ALIAS + | T.EOF -> P.EOF + | _ -> assert false + in + let ich = open_in ! interp_file in + let lexbuf = Lexing.from_channel ich in + let f = P.interp (fun x -> lexer (L.token x)) lexbuf in + close_in ich; f + +let get_terms interp = + let interp = get_interp () in + let lexbuf = Lexing.from_channel stdin in + let rec aux () = + try + let dom, mk_term = + CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf + in + (snd (mk_term interp)) :: aux () + with + CicTextualParser0.Eof -> [] + in + aux () + +let pp_type_of uri = + let u = UriManager.uri_of_string uri in + let s = match (CicEnvironment.get_obj u) with + | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty + | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty + | _ -> "Current proof or inductive definition." +(* + | Cic.CurrentProof (_,conjs,te,ty) -> + | C.InductiveDefinition _ -> +*) + in print_endline s; flush stdout + +let rec display = function + | [] -> () + | term :: tail -> + display tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + flush stdout + +let execute ich = + let module U = MQueryUtil in + let lexbuf = Lexing.from_channel ich in + let handle = get_handle () in + let rec execute_aux () = + try + let q = U.query_of_text lexbuf in + issue handle q; execute_aux () + with End_of_file -> () + in + execute_aux (); + MQIC.close handle +(* +let compose () = + let module P = MQGTopParser in + let module L = MQGTopLexer in + let module G = MQueryGeneratorNew in + let cl = P.specs L.spec_token (Lexing.from_channel stdin) in + issue (G.compose cl) +*) +let locate name = + let handle = get_handle () in + issue handle (MQG.locate name); + MQIC.close handle + +let mpattern n m l = + let module C = MQueryLevels2 in + let queries = ref [] in + let handle = get_handle () in + let rec pattern level = function + | [] -> () + | term :: tail -> + pattern level tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t0 = Sys.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 + 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; + flush stdout; queries := q :: ! queries + end + in + for level = max m n downto min m n do + Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level; + flush stderr; pattern level l + done; + Printf.eprintf "\nmqgtop: pattern: %i queries issued\n" + (List.length ! queries); + flush stderr; + MQIC.close handle +(* +let mbackward n m l = + let module C = MQueryLevels in + let module G = MQueryGenerator in + let queries = ref [] in + let torigth_restriction (u, b) = + let p = if b + then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" + in + (u, p, None) + in + let rec backward level = function + | [] -> () + | term :: tail -> + backward level tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t0 = Sys.time () in + let list_of_must, only = C.out_restr [] [] term in + let max_level = pred (List.length list_of_must) in + let must = List.nth list_of_must (min level max_level) in + let rigth_must = List.map torigth_restriction must in + let rigth_only = Some (List.map torigth_restriction only) in + let q = G.searchPattern (rigth_must, [], []) (rigth_only , None, None) in + if not (List.mem q ! queries) then + begin + issue 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) (List.length must) t1 nl; + flush stdout; queries := q :: ! queries + end + in + for level = max m n downto min m n do + Printf.eprintf "\nmqgtop: backward: trying level %i\n" level; + flush stderr; backward level l + done; + Printf.eprintf "\nmqgtop: backward: %i queries issued\n" + (List.length ! queries); + flush stderr +*) + +let set_options s = int_options := s + +let check () = + let handle = get_handle () in + Printf.eprintf + "mqgtop: current options: %s, connection: %s\n" + ! int_options (if MQIC.connected handle then "on" else "off"); + MQIC.close handle + +let prerr_help () = + prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n"; + prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for"; + prerr_endline "testing purposes. mqgtop reads its input from stdin and produces ith output"; + prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n"; + prerr_endline "OPTIONS:\n"; + prerr_endline "-h -help shows this help message"; + prerr_endline "-q -show-queries outputs generated queries"; + 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 "-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 " 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"; + prerr_endline "NOTES: * current interpreter options are:"; + prerr_endline " P (postgres), G (Galax), S (show statistics), Q (quiet)"; + prerr_endline " * CIC terms are read with the HELM CIC Textual Parser"; + prerr_endline " * -typeof does not work with inductive types and proofs in progress\n" + +let rec parse = function + | [] -> () + | ("-h"|"-help") :: rem -> prerr_help (); parse rem + | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem + | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem + | ("-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 + | ("-c"|"-check") :: rem -> check (); parse rem +(* | ("-C"|"-compose") :: rem -> compose (); parse rem +*) | ("-L"|"-locate") :: arg :: rem -> locate arg; 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 +*) | ("-P"|"-pattern") :: arg :: rem -> + let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem + | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem + | _ :: rem -> parse rem + +let _ = + Logger.log_callback := + (Logger.log_to_html + ~print_and_flush:(function 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"); + exit 0