helm/ocaml/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 let query_num = ref 1
  27
  28 let interp_file = ref "interp.cic"
  29
  30 let log_file = ref "MQGenLog.htm"
  31
  32 let show_queries = ref false
  33
  34 let int_options = ref ""
  35
  36 let nl = " <p>\n"
  37
  38 module MQI = MQueryInterpreter
  39 module MQIC = MQIConn
  40 module MQG = MQueryGenerator
  41
  42 let get_handle () =
  43    MQIC.init (MQIC.flags_of_string ! int_options)
  44              (fun s -> print_string s; flush stdout)
  45
  46 let issue handle q =
  47    let module U = MQueryUtil in
  48    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
  49    let perm = 64 * 6 + 8 * 6 + 4 in
  50    let time () =
  51       let lt = Unix.localtime (Unix.time ()) in
  52       "NEW LOG: " ^
  53       string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
  54       string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
  55       string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
  56       string_of_int (lt.Unix.tm_hour) ^ ":" ^
  57       string_of_int (lt.Unix.tm_min) ^ ":" ^
  58       string_of_int (lt.Unix.tm_sec)
  59    in
  60    let log q r =
  61       let och = open_out_gen mode perm ! log_file in
  62       let out = output_string och in
  63       if ! query_num = 1 then out (time () ^ nl);
  64       out ("Query: " ^ string_of_int ! query_num ^ nl);
  65       U.text_of_query out q nl;
  66       out ("Result: " ^ nl);
  67       U.text_of_result out r nl;
  68       close_out och
  69    in
  70    if ! show_queries then U.text_of_query (output_string stdout) q nl;
  71    let r = MQI.execute handle q in
  72    U.text_of_result (output_string stdout) r nl;
  73    if ! log_file <> "" then log q r;
  74    incr query_num;
  75    flush stdout
  76
  77 let get_interp () =
  78    let module L = CicTextualLexer in
  79    let module T = CicTextualParser in
  80    let module P = MQGTopParser in
  81    let lexer = function
  82       | T.ID s                -> P.ID s
  83       | T.CONURI u            -> P.CONURI u
  84       | T.VARURI u            -> P.VARURI u
  85       | T.INDTYURI (u, p)     -> P.INDTYURI (u, p)
  86       | T.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
  87       | T.LETIN               -> P.ALIAS
  88       | T.EOF                 -> P.EOF
  89       | _                     -> assert false
  90    in
  91    let ich = open_in ! interp_file in
  92    let lexbuf = Lexing.from_channel ich in
  93    let f = P.interp (fun x -> lexer (L.token x)) lexbuf in
  94    close_in ich; f
  95
  96 let get_terms interp =
  97    let interp = get_interp () in
  98    let lexbuf = Lexing.from_channel stdin in
  99    let rec aux () =
 100       try
 101          let dom, mk_term =
 102             CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
 103          in
 104          (snd (mk_term interp)) :: aux ()
 105       with
 106       CicTextualParser0.Eof -> []
 107    in
 108    aux ()
 109
 110 let pp_type_of uri =
 111    let u = UriManager.uri_of_string uri in
 112    let s = match (CicEnvironment.get_obj u) with
 113       | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
 114       | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
 115       | _                          -> "Current proof or inductive definition."
 116 (*
 117       | Cic.CurrentProof (_,conjs,te,ty) ->
 118       | C.InductiveDefinition _ ->
 119 *)
 120    in print_endline s; flush stdout
 121
 122 let rec display = function
 123    | []           -> ()
 124    | term :: tail ->
 125       display tail;
 126       print_string ("? " ^ CicPp.ppterm term ^ nl);
 127       flush stdout
 128
 129 let execute ich =
 130    let module U = MQueryUtil in
 131    let lexbuf = Lexing.from_channel ich in
 132    let handle = get_handle () in
 133    let rec execute_aux () =
 134       try
 135          let q = U.query_of_text lexbuf in
 136          issue handle q; execute_aux ()
 137       with End_of_file -> ()
 138    in
 139    execute_aux ();
 140    MQIC.close handle
 141 (*
 142 let compose () =
 143    let module P = MQGTopParser in
 144    let module L = MQGTopLexer in
 145    let module G = MQueryGeneratorNew in
 146    let cl = P.specs L.spec_token (Lexing.from_channel stdin) in
 147    issue (G.compose cl)
 148 *)
 149 let locate name =
 150    let handle = get_handle () in
 151    issue handle (MQG.locate name);
 152    MQIC.close handle
 153
 154 let mpattern n m l =
 155    let module C = MQueryLevels2 in
 156    let queries = ref [] in
 157    let handle = get_handle () in
 158    let rec pattern level = function
 159       | []           -> ()
 160       | term :: tail ->
 161          pattern level tail;
 162          print_string ("? " ^ CicPp.ppterm term ^ nl);
 163          let t0 = Sys.time () in
 164          let om,rm,sm = C.get_constraints term in
 165          let oml,rml,sml = List.length om, List.length rm, List.length sm in
 166          let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
 167          let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
 168          let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
 169          let q = MQG.searchPattern (om,rm,sm) (oo,ro,so) in
 170          if not (List.mem q ! queries) then
 171          begin
 172             issue handle q;
 173             let t1 = Sys.time () -. t0 in
 174             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 175             Printf.printf "%i GEN = %i: %.2fs%s"
 176                (pred ! query_num) (oml + rml + sml + ool + rol + sol) t1 nl;
 177             flush stdout; queries := q :: ! queries
 178          end
 179    in
 180    for level = max m n downto min m n do
 181       Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level;
 182       flush stderr; pattern level l
 183    done;
 184    Printf.eprintf "\nmqgtop: pattern: %i queries issued\n"
 185       (List.length ! queries);
 186    flush stderr;
 187    MQIC.close handle
 188 (*
 189 let mbackward n m l =
 190    let module C = MQueryLevels in
 191    let module G = MQueryGenerator in
 192    let queries = ref [] in
 193    let torigth_restriction (u, b) =
 194       let p = if b
 195          then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
 196          else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
 197       in
 198       (u, p, None)
 199    in
 200    let rec backward level = function
 201       | []           -> ()
 202       | term :: tail ->
 203          backward level tail;
 204          print_string ("? " ^ CicPp.ppterm term ^ nl);
 205          let t0 = Sys.time () in
 206          let list_of_must, only = C.out_restr [] [] term in
 207          let max_level = pred (List.length list_of_must) in
 208          let must = List.nth list_of_must (min level max_level) in
 209          let rigth_must = List.map torigth_restriction must in
 210          let rigth_only = Some (List.map torigth_restriction only) in
 211          let q = G.searchPattern (rigth_must, [], []) (rigth_only , None, None) in
 212          if not (List.mem q ! queries) then
 213          begin
 214             issue q;
 215             let t1 = Sys.time () -. t0 in
 216             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 217             Printf.printf "%i GEN = %i: %.2fs%s"
 218                (pred ! query_num) (List.length must) t1 nl;
 219             flush stdout; queries := q :: ! queries
 220          end
 221    in
 222    for level = max m n downto min m n do
 223       Printf.eprintf "\nmqgtop: backward: trying level %i\n" level;
 224       flush stderr; backward level l
 225    done;
 226    Printf.eprintf "\nmqgtop: backward: %i queries issued\n"
 227       (List.length ! queries);
 228    flush stderr
 229 *)
 230
 231 let set_options s = int_options := s
 232
 233 let check () =
 234    let handle = get_handle () in
 235    Printf.eprintf
 236       "mqgtop: current options: %s, connection: %s\n"
 237       ! int_options (if MQIC.connected handle then "on" else "off");
 238    MQIC.close handle
 239
 240 let prerr_help () =
 241    prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n";
 242    prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
 243    prerr_endline "testing purposes. mqgtop reads its input from stdin and produces ith output";
 244    prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
 245    prerr_endline "OPTIONS:\n";
 246    prerr_endline "-h  -help               shows this help message";
 247    prerr_endline "-q  -show-queries       outputs generated queries";
 248    prerr_endline "-o  -options STRING     sets the interpreter options";
 249    prerr_endline "-c  -check              checks the database connection";
 250    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
 251    prerr_endline "-x  -execute            issues a query given in the input file";
 252    prerr_endline "-i  -interp FILE        sets the CIC short names interpretation file";
 253    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
 254    prerr_endline "-C  -compose            issues the \"Compose\" query reading its specifications";
 255    prerr_endline "                        from the input file";
 256    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
 257    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all";
 258    prerr_endline "                        CIC terms in the input file";
 259    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
 260    prerr_endline "                        on all CIC terms in the input file";
 261    prerr_endline "-P  -pattern LEVEL      issues the \"Pattern\" query for the given level on all";
 262    prerr_endline "                        CIC terms in the input file";
 263    prerr_endline "-MP -multi-pattern      issues the \"Pattern\" query for each level from 7 to 0";
 264    prerr_endline "                        on all CIC terms in the input file\n";
 265    prerr_endline "NOTES: * current interpreter options are:";
 266    prerr_endline "         P (postgres), G (Galax), S (show statistics), Q (quiet)";
 267    prerr_endline "       * CIC terms are read with the HELM CIC Textual Parser";
 268    prerr_endline "       * -typeof does not work with inductive types and proofs in progress\n"
 269
 270 let rec parse = function
 271    | [] -> ()
 272    | ("-h"|"-help") :: rem -> prerr_help (); parse rem
 273    | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
 274    | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
 275    | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
 276    | ("-x"|"-execute") :: rem -> execute stdin; parse rem
 277    | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
 278    | ("-o"|"-options") :: arg :: rem -> set_options arg; parse rem
 279    | ("-c"|"-check") :: rem -> check (); parse rem
 280 (*   | ("-C"|"-compose") :: rem -> compose (); parse rem
 281 *)   | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
 282 (*   | ("-M"|"-backward") :: arg :: rem ->
 283       let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
 284    | ("-MB"|"-multi-backward") :: arg :: rem ->
 285       let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
 286 *)   | ("-P"|"-pattern") :: arg :: rem ->
 287       let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
 288    | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
 289    | _ :: rem -> parse rem
 290
 291 let _ =
 292    Logger.log_callback :=
 293       (Logger.log_to_html
 294       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
 295    parse (List.tl (Array.to_list Sys.argv));
 296    prerr_endline ("mqgtop: done in " ^ string_of_float (Sys.time ()) ^
 297                   " seconds");
 298    exit 0