X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql_test%2Fmqgtop.ml;fp=helm%2Fmathql_test%2Fmqgtop.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=bb776474761377a2fca8451524889a9e09b4398f;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml deleted file mode 100644 index bb7764747..000000000 --- a/helm/mathql_test/mqgtop.ml +++ /dev/null @@ -1,336 +0,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 - *) - -let query_num = ref 1 - -let interp_file = ref "interp.cic" - -let log_file = ref "" - -let show_queries = ref false - -let int_options = ref "" - -let nl = "

\n" - -module U = MQueryUtil -module I = MQueryInterpreter -module C = MQIConn -module G = MQueryGenerator -module L = MQGTopLexer -module P = MQGTopParser -module TL = CicTextualLexer -module TP = CicTextualParser -module C3 = CGLocateInductive -module C2 = CGSearchPattern -module C1 = CGMatchConclusion -module GU = MQGUtil - -let get_handle () = - C.init ~flags:(C.flags_of_string ! int_options) - ~log:(fun s -> print_string s; flush stdout) () - -let issue handle q = - 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 nl q; - out ("Result: " ^ nl); - U.text_of_result out nl r; - close_out och - in - if ! show_queries then U.text_of_query (output_string stdout) nl q; - let r = I.execute handle q in - U.text_of_result (output_string stdout) nl r; - if ! log_file <> "" then log q r; - incr query_num; - flush stdout - -let get_interp () = - let lexer = function - | TP.ID s -> P.ID s - | TP.CONURI u -> P.CONURI u - | TP.VARURI u -> P.VARURI u - | TP.INDTYURI (u, p) -> P.INDTYURI (u, p) - | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s) - | TP.LETIN -> P.ALIAS - | TP.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 (TL.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 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 (); - C.close handle - -let compose () = - let handle = get_handle () in - let cl = P.specs L.spec_token (Lexing.from_channel stdin) in - issue handle (G.compose cl); - C.close handle - -let locate name = - let handle = get_handle () in - issue handle (G.locate name); - C.close handle - -let unreferred target source = - let handle = get_handle () in - issue handle (G.unreferred target source); - C.close handle - -let mpattern n m l = - let queries = ref [] in - let univ = Some C2.universe in - let handle = get_handle () in - let rec pattern level = function - | [] -> () - | term :: tail -> - pattern level tail; - print_string ("? " ^ CicPp.ppterm term ^ nl); - let t = U.start_time () in - let om,rm,sm = C2.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 = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in - if not (List.mem q ! queries) then - begin - issue handle q; - Printf.eprintf "[%i] " (pred ! query_num); flush stderr; - Printf.printf "%i GEN = %i: %s" - (pred ! query_num) (oml + rml + sml + ool + rol + sol) - (U.stop_time t ^ 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; - C.close handle - -let mbackward n m l = - let queries = ref [] in - let univ = Some C1.universe in - let handle = get_handle () in - let rec backward level = function - | [] -> () - | term :: tail -> - backward level tail; - print_string ("? " ^ CicPp.ppterm term ^ nl); - let t = U.start_time () in - let list_of_must, only = C1.get_constraints [] [] 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 q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in - if not (List.mem q ! queries) then - begin - issue handle q; - Printf.eprintf "[%i] " (pred ! query_num); flush stderr; - Printf.printf "%i GEN = %i: %s" - (pred ! query_num) (List.length must) - (U.stop_time t ^ 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; - C.close handle - -let inductive l = - let queries = ref [] in - let univ = None in - let handle = get_handle () in - let rec aux = function - | [] -> () - | term :: tail -> - aux tail; - print_string ("? " ^ CicPp.ppterm term ^ nl); - let t = U.start_time () in - let m = C3.get_constraints term in - let q = G.query_of_constraints univ m (None, None, None) in - if not (List.mem q ! queries) then - begin - issue handle q; - Printf.eprintf "[%i] " (pred ! query_num); flush stderr; - Printf.printf "%i GEN: %s" - (pred ! query_num) (U.stop_time t ^ nl); - flush stdout; queries := q :: ! queries - end - in - aux l; - Printf.eprintf "\nmqgtop: inductive: %i queries issued\n" - (List.length ! queries); - flush stderr; - C.close handle - -let check () = - let handle = get_handle () in - Printf.eprintf - "mqgtop: current options: %s, connection: %s\n" - ! int_options (if C.connected handle then "on" else "off"); - C.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 "-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 "-L -locate ALIAS issues the \"Locate\" query for the given alias"; - prerr_endline "-U T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns"; - 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 " 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"; - prerr_endline "-I issues the \"Inductive\" query on all CIC terms in the"; - prerr_endline " 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 -> int_options := arg; parse rem - | ("-c"|"-check") :: rem -> check (); parse 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 - | ("-B"|"-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 - | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem -> - unreferred arg1 arg2; parse rem - | ("-I"|"-inductive") :: rem -> inductive (get_terms ()); parse rem - | _ :: rem -> parse rem - -let _ = - Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml"; - let t = U.start_time () in -(* - CicLogger.log_callback := - (CicLogger.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 " ^ (U.stop_time t)); - exit 0