+++ /dev/null
-(* 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 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 = " <p>\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
projects / helm.git / blobdiff