helm/mathql_test/mqgtop.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  27  *)
  28
  29 let query_num = ref 1
  30
  31 let interp_file = ref "interp.cic"
  32
  33 let log_file = ref ""
  34
  35 let show_queries = ref false
  36
  37 let int_options = ref ""
  38
  39 let nl = " <p>\n"
  40
  41 module IO = MQueryIO
  42 module U  = MQueryUtil
  43 module I  = MQueryInterpreter
  44 module C  = MQIConn
  45 module G  = MQueryGenerator
  46 module L  = MQGTopLexer
  47 module P  = MQGTopParser
  48 module TL = CicTextualLexer
  49 module TP = CicTextualParser
  50 module C3 = CGLocateInductive
  51 module C2 = CGSearchPattern
  52 module C1 = CGMatchConclusion
  53 module GU = MQGUtil
  54
  55 let get_handle () =
  56    C.init (C.flags_of_string ! int_options)
  57           (fun s -> print_string s; flush stdout)
  58
  59 let issue handle q =
  60    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
  61    let perm = 64 * 6 + 8 * 6 + 4 in
  62    let time () =
  63       let lt = Unix.localtime (Unix.time ()) in
  64       "NEW LOG: " ^
  65       string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
  66       string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
  67       string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
  68       string_of_int (lt.Unix.tm_hour) ^ ":" ^
  69       string_of_int (lt.Unix.tm_min) ^ ":" ^
  70       string_of_int (lt.Unix.tm_sec)
  71    in
  72    let log q r =
  73       let och = open_out_gen mode perm ! log_file in
  74       let out = output_string och in
  75       if ! query_num = 1 then out (time () ^ nl);
  76       out ("Query: " ^ string_of_int ! query_num ^ nl);
  77       IO.text_of_query out nl q;
  78       out ("Result: " ^ nl);
  79       IO.text_of_result out nl r;
  80       close_out och
  81    in
  82    if ! show_queries then IO.text_of_query (output_string stdout) nl q;
  83    let r = I.execute handle q in
  84    IO.text_of_result (output_string stdout) nl r;
  85    if ! log_file <> "" then log q r;
  86    incr query_num;
  87    flush stdout
  88
  89 let get_interp () =
  90    let lexer = function
  91       | TP.ID s                -> P.ID s
  92       | TP.CONURI u            -> P.CONURI u
  93       | TP.VARURI u            -> P.VARURI u
  94       | TP.INDTYURI (u, p)     -> P.INDTYURI (u, p)
  95       | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
  96       | TP.LETIN               -> P.ALIAS
  97       | TP.EOF                 -> P.EOF
  98       | _                     -> assert false
  99    in
 100    let ich = open_in ! interp_file in
 101    let lexbuf = Lexing.from_channel ich in
 102    let f = P.interp (fun x -> lexer (TL.token x)) lexbuf in
 103    close_in ich; f
 104
 105 let get_terms interp =
 106    let interp = get_interp () in
 107    let lexbuf = Lexing.from_channel stdin in
 108    let rec aux () =
 109       try
 110          let dom, mk_term =
 111             CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
 112          in
 113          (snd (mk_term interp)) :: aux ()
 114       with
 115       CicTextualParser0.Eof -> []
 116    in
 117    aux ()
 118
 119 let pp_type_of uri =
 120    let u = UriManager.uri_of_string uri in
 121    let s = match (CicEnvironment.get_obj u) with
 122       | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
 123       | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
 124       | _                          -> "Current proof or inductive definition."
 125 (*
 126       | Cic.CurrentProof (_,conjs,te,ty) ->
 127       | C.InductiveDefinition _ ->
 128 *)
 129    in print_endline s; flush stdout
 130
 131 let rec display = function
 132    | []           -> ()
 133    | term :: tail ->
 134       display tail;
 135       print_string ("? " ^ CicPp.ppterm term ^ nl);
 136       flush stdout
 137
 138 let execute ich =
 139    let lexbuf = Lexing.from_channel ich in
 140    let handle = get_handle () in
 141    let rec execute_aux () =
 142       try
 143          let q = IO.query_of_text lexbuf in
 144          issue handle q; execute_aux ()
 145       with End_of_file -> ()
 146    in
 147    execute_aux ();
 148    C.close handle
 149
 150 let compose () =
 151    let handle = get_handle () in
 152    let cl = P.specs L.spec_token (Lexing.from_channel stdin) in
 153    issue handle (G.compose cl);
 154    C.close handle
 155
 156 let locate name =
 157    let handle = get_handle () in
 158    issue handle (G.locate name);
 159    C.close handle
 160
 161 let unreferred target source =
 162    let handle = get_handle () in
 163    issue handle (G.unreferred target source);
 164    C.close handle
 165
 166 let mpattern n m l =
 167    let queries = ref [] in
 168    let univ = Some C2.universe in
 169    let handle = get_handle () in
 170    let rec pattern level = function
 171       | []           -> ()
 172       | term :: tail ->
 173          pattern level tail;
 174          print_string ("? " ^ CicPp.ppterm term ^ nl);
 175          let t = U.start_time () in
 176          let om,rm,sm = C2.get_constraints term in
 177          let oml,rml,sml = List.length om, List.length rm, List.length sm in
 178          let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
 179          let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
 180          let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
 181          let q = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in
 182          if not (List.mem q ! queries) then
 183          begin
 184             issue handle q;
 185             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 186             Printf.printf "%i GEN = %i: %s"
 187                (pred ! query_num) (oml + rml + sml + ool + rol + sol)
 188                (U.stop_time t ^ nl);
 189             flush stdout; queries := q :: ! queries
 190          end
 191    in
 192    for level = max m n downto min m n do
 193       Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level;
 194       flush stderr; pattern level l
 195    done;
 196    Printf.eprintf "\nmqgtop: pattern: %i queries issued\n"
 197       (List.length ! queries);
 198    flush stderr;
 199    C.close handle
 200
 201 let mbackward n m l =
 202    let queries = ref [] in
 203    let univ = Some C1.universe in
 204    let handle = get_handle () in
 205    let rec backward level = function
 206       | []           -> ()
 207       | term :: tail ->
 208          backward level tail;
 209          print_string ("? " ^ CicPp.ppterm term ^ nl);
 210          let t = U.start_time () in
 211          let list_of_must, only = C1.get_constraints [] [] term in
 212          let max_level = pred (List.length list_of_must) in
 213          let must = List.nth list_of_must (min level max_level) in
 214          let q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in
 215          if not (List.mem q ! queries) then
 216          begin
 217             issue handle q;
 218             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 219             Printf.printf "%i GEN = %i: %s"
 220                (pred ! query_num) (List.length must)
 221                (U.stop_time t ^ nl);
 222             flush stdout; queries := q :: ! queries
 223          end
 224    in
 225    for level = max m n downto min m n do
 226       Printf.eprintf "\nmqgtop: backward: trying level %i\n" level;
 227       flush stderr; backward level l
 228    done;
 229    Printf.eprintf "\nmqgtop: backward: %i queries issued\n"
 230       (List.length ! queries);
 231    flush stderr;
 232    C.close handle
 233
 234 let inductive l =
 235    let queries = ref [] in
 236    let univ = None in
 237    let handle = get_handle () in
 238    let rec aux = function
 239       | []           -> ()
 240       | term :: tail ->
 241          aux tail;
 242          print_string ("? " ^ CicPp.ppterm term ^ nl);
 243          let t = U.start_time () in
 244          let m = C3.get_constraints term in
 245          let q = G.query_of_constraints univ m (None, None, None) in
 246          if not (List.mem q ! queries) then
 247          begin
 248             issue handle q;
 249             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 250             Printf.printf "%i GEN: %s"
 251                (pred ! query_num) (U.stop_time t ^ nl);
 252             flush stdout; queries := q :: ! queries
 253          end
 254    in
 255    aux l;
 256    Printf.eprintf "\nmqgtop: inductive: %i queries issued\n"
 257       (List.length ! queries);
 258    flush stderr;
 259    C.close handle
 260
 261 let check () =
 262    let handle = get_handle () in
 263    Printf.eprintf
 264       "mqgtop: current options: %s, connection: %s\n"
 265       ! int_options (if C.connected handle then "on" else "off");
 266    C.close handle
 267
 268 let prerr_help () =
 269    prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n";
 270    prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
 271    prerr_endline "testing purposes. mqgtop reads its input from stdin and produces ith output";
 272    prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
 273    prerr_endline "OPTIONS:\n";
 274    prerr_endline "-h  -help               shows this help message";
 275    prerr_endline "-q  -show-queries       outputs generated queries";
 276    prerr_endline "-l  -log-file FILE      sets the log file";
 277    prerr_endline "-o  -options STRING     sets the interpreter options";
 278    prerr_endline "-c  -check              checks the database connection";
 279    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
 280    prerr_endline "-x  -execute            issues a query given in the input file";
 281    prerr_endline "-i  -interp FILE        sets the CIC short names interpretation file";
 282    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
 283    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
 284    prerr_endline "-U  T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns";
 285    prerr_endline "-C  -compose            issues the \"Compose\" query reading its specifications";
 286    prerr_endline "                        from the input file";
 287    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all";
 288    prerr_endline "                        CIC terms in the input file";
 289    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
 290    prerr_endline "                        on all CIC terms in the input file";
 291    prerr_endline "-P  -pattern LEVEL      issues the \"Pattern\" query for the given level on all";
 292    prerr_endline "                        CIC terms in the input file";
 293    prerr_endline "-MP -multi-pattern      issues the \"Pattern\" query for each level from 7 to 0";
 294    prerr_endline "                        on all CIC terms in the input file";
 295    prerr_endline "-I                      issues the \"Inductive\" query on all CIC terms in the";
 296    prerr_endline "                        input file\n";
 297    prerr_endline "NOTES: * current interpreter options are:";
 298    prerr_endline "         P (postgres), G (Galax), S (show statistics), Q (quiet)";
 299    prerr_endline "       * CIC terms are read with the HELM CIC Textual Parser";
 300    prerr_endline "       * -typeof does not work with inductive types and proofs in progress\n"
 301
 302 let rec parse = function
 303    | [] -> ()
 304    | ("-h"|"-help") :: rem -> prerr_help (); parse rem
 305    | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
 306    | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
 307    | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
 308    | ("-x"|"-execute") :: rem -> execute stdin; parse rem
 309    | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
 310    | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
 311    | ("-c"|"-check") :: rem -> check (); parse rem
 312    | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
 313    | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
 314    | ("-C"|"-compose") :: rem -> compose (); parse rem
 315    | ("-B"|"-backward") :: arg :: rem ->
 316       let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
 317    | ("-MB"|"-multi-backward") :: arg :: rem ->
 318       let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
 319    | ("-P"|"-pattern") :: arg :: rem ->
 320       let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
 321    | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
 322    | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem ->
 323       unreferred arg1 arg2; parse rem
 324    | ("-I"|"-inductive") :: rem -> inductive (get_terms ()); parse rem
 325    | _ :: rem -> parse rem
 326
 327 let _ =
 328    let t = U.start_time () in
 329    Logger.log_callback :=
 330       (Logger.log_to_html
 331        ~print_and_flush:(fun s -> print_string s; flush stdout)) ;
 332    parse (List.tl (Array.to_list Sys.argv));
 333    prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
 334    exit 0