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 _ = MQueryStandard.init
  30 let _ = MQueryHELM.init
  31
  32 let query_num = ref 1
  33
  34 let interp_file = ref "interp.cic"
  35
  36 let log_file = ref ""
  37
  38 let show_queries = ref false
  39
  40 let int_options = ref ""
  41
  42 let nl = " <p>\n"
  43
  44 module IO = MQueryIO
  45 module U  = MQueryUtil
  46 module I  = MQueryInterpreter
  47 module C  = MQIConn
  48 module G  = MQueryGenerator
  49 module L  = MQGTopLexer
  50 module P  = MQGTopParser
  51 module TL = CicTextualLexer
  52 module TP = CicTextualParser
  53 module C3 = CGLocateInductive
  54 module C2 = CGSearchPattern
  55 module C1 = CGMatchConclusion
  56 module GU = MQGUtil
  57 module M  = MQueryMisc
  58
  59 let get_handle () =
  60    C.init (C.flags_of_string ! int_options)
  61           (fun s -> print_string s; flush stdout)
  62
  63 let issue handle q =
  64    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
  65    let perm = 64 * 6 + 8 * 6 + 4 in
  66    let time () =
  67       let lt = Unix.localtime (Unix.time ()) in
  68       "NEW LOG: " ^
  69       string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
  70       string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
  71       string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
  72       string_of_int (lt.Unix.tm_hour) ^ ":" ^
  73       string_of_int (lt.Unix.tm_min) ^ ":" ^
  74       string_of_int (lt.Unix.tm_sec)
  75    in
  76    let log q r =
  77       let och = open_out_gen mode perm ! log_file in
  78       let out = output_string och in
  79       if ! query_num = 1 then out (time () ^ nl);
  80       out ("Query: " ^ string_of_int ! query_num ^ nl);
  81       IO.text_of_query out nl q;
  82       out ("Result: " ^ nl);
  83       IO.text_of_result out nl r;
  84       close_out och
  85    in
  86    if ! show_queries then IO.text_of_query (output_string stdout) nl q;
  87    let r = I.execute handle q in
  88    IO.text_of_result (output_string stdout) nl r;
  89    if ! log_file <> "" then log q r;
  90    incr query_num;
  91    flush stdout
  92
  93 let get_interp () =
  94    let lexer = function
  95       | TP.ID s                -> P.ID s
  96       | TP.CONURI u            -> P.CONURI u
  97       | TP.VARURI u            -> P.VARURI u
  98       | TP.INDTYURI (u, p)     -> P.INDTYURI (u, p)
  99       | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
 100       | TP.LETIN               -> P.ALIAS
 101       | TP.EOF                 -> P.EOF
 102       | _                     -> assert false
 103    in
 104    let ich = open_in ! interp_file in
 105    let lexbuf = Lexing.from_channel ich in
 106    let f = P.interp (fun x -> lexer (TL.token x)) lexbuf in
 107    close_in ich; f
 108
 109 let get_terms interp =
 110    let interp = get_interp () in
 111    let lexbuf = Lexing.from_channel stdin in
 112    let rec aux () =
 113       try
 114          let dom, mk_term =
 115             CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
 116          in
 117          (snd (mk_term interp)) :: aux ()
 118       with
 119       CicTextualParser0.Eof -> []
 120    in
 121    aux ()
 122
 123 let rec join f v1 v2 =
 124    match v1, v2 with
 125       | [], v                          -> f v
 126       | v, []                          -> f v
 127       | h1 :: t1, h2 :: _ when h1 < h2 ->
 128          let g h = f (h1 :: h) in join g t1 v2
 129       | h1 :: _, h2 :: t2 when h1 > h2 ->
 130          let g h = f (h2 :: h) in join g v1 t2
 131       | h1 :: t1, _ :: t2              ->
 132          let g h = f (h1 :: h) in join g t1 t2
 133
 134 let rec diff f v1 v2 =
 135    match v1, v2 with
 136       | [], _                          -> f []
 137       | _, []                          -> f v1
 138       | h1 :: t1, h2 :: _ when h1 < h2 ->
 139          let g h = f (h1 :: h) in diff g t1 v2
 140       | h1 :: _, h2 :: t2 when h1 > h2 -> diff f v1 t2
 141       | _ :: t1, _ :: t2               -> diff f t1 t2
 142
 143 let add f r k l = join f r [M.string_of_uriref (k, l)]
 144
 145 let rec add_cons f r k i j = function
 146    | []      -> f r
 147    | _ :: tl ->
 148       let g s = add f s k [i; j] in
 149       add_cons g r k i (succ j) tl
 150
 151 let rec refobj_l refobj_t map f r = function
 152    | []        -> f r
 153    | h :: tail ->
 154       let f r = refobj_l refobj_t map f r tail in
 155       refobj_t f r (map h)
 156
 157 let rec refobj_t f r = function
 158    | Cic.Implicit _
 159    | Cic.Meta _
 160    | Cic.Sort _
 161    | Cic.Rel _                      -> f r
 162    | Cic.Cast (t, u)
 163    | Cic.Prod (_, t, u)
 164    | Cic.Lambda (_, t, u)
 165    | Cic.LetIn (_, t, u)            ->
 166       let f r = refobj_t f r u in refobj_t f r t
 167    | Cic.Appl tl                    ->
 168       refobj_l refobj_t (fun x -> x) f r tl
 169    | Cic.Fix (_, tl)                ->
 170       let f r = refobj_l refobj_t (fun (_, _, _, u) -> u) f r tl in
 171       refobj_l refobj_t (fun (_, _, t, _) -> t) f r tl
 172    | Cic.CoFix (_, tl)              ->
 173       let f r = refobj_l refobj_t (fun (_, _, u) -> u) f r tl in
 174       refobj_l refobj_t (fun (_, t, _) -> t) f r tl
 175    | Cic.Var (k, tl)                ->
 176       let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
 177       add f r k []
 178    | Cic.Const (k, tl)              ->
 179       let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
 180       add f r k []
 181    | Cic.MutInd (k, i, tl)          ->
 182       let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
 183       add f r k [i]
 184    | Cic.MutConstruct (k, i, j, tl) ->
 185       let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
 186       add f r k [i; j]
 187    | Cic.MutCase (k, i, t, u, tl)   ->
 188       let f r = refobj_l refobj_t (fun u -> u) f r tl in
 189       let f r = refobj_t f r u in
 190       let f r = refobj_t f r t in
 191       let f r = add f r k [i] in
 192       add_cons f r k i 1 tl
 193
 194 let get_refobj f r uri =
 195    let body, ty = M.get_object (M.uriref_of_string uri) in
 196    let f r = diff f r [uri] in
 197    let f r = refobj_t f r body in
 198    refobj_t f r ty
 199
 200 let rec get_refobj_l f r = function
 201    | []       -> f r
 202    | uri :: l ->
 203       let f r = get_refobj_l f r l in
 204       get_refobj f r uri
 205
 206 let show_refobj uri =
 207    let f = List.iter print_endline in
 208    get_refobj f [] uri
 209
 210 let compute_shells uri =
 211    let rec aux r d n =
 212       let f p r =
 213          let l = List.length r in
 214          Printf.printf "found %i objects\n" l; flush stdout;
 215          let f d = if l > 0 then aux r d (succ n) in
 216          join f d p
 217       in
 218       Printf.printf "shells: computing level %i ... " n; flush stdout;
 219       let f r = get_refobj_l (f r) [] r in
 220       diff f r d
 221    in
 222    aux [uri] [] 0
 223
 224 let pp_term_of b uri =
 225    let s = try
 226       let body, ty = M.get_object (M.uriref_of_string uri) in
 227       if b then CicPp.ppterm body else CicPp.ppterm ty
 228    with
 229       | M.CurrentProof        -> "proof in progress"
 230       | M.InductiveDefinition -> "inductive definition"
 231       | M.IllFormedFragment   -> "ill formed fragment identifier"
 232    in print_endline s; flush stdout
 233
 234 let rec display = function
 235    | []           -> ()
 236    | term :: tail ->
 237       display tail;
 238       print_string ("? " ^ CicPp.ppterm term ^ nl);
 239       flush stdout
 240
 241 let execute ich =
 242    let lexbuf = Lexing.from_channel ich in
 243    let handle = get_handle () in
 244    let rec execute_aux () =
 245       try
 246          let q = IO.query_of_text lexbuf in
 247          issue handle q; execute_aux ()
 248       with End_of_file -> ()
 249    in
 250    execute_aux ();
 251    C.close handle
 252
 253 let compose () =
 254    let handle = get_handle () in
 255    let cl = P.specs L.spec_token (Lexing.from_channel stdin) in
 256    issue handle (G.compose cl);
 257    C.close handle
 258
 259 let locate name =
 260    let handle = get_handle () in
 261    issue handle (G.locate name);
 262    C.close handle
 263
 264 let unreferred target source =
 265    let handle = get_handle () in
 266    issue handle (G.unreferred target source);
 267    C.close handle
 268
 269 let mpattern n m l =
 270    let queries = ref [] in
 271    let univ = Some C2.universe in
 272    let handle = get_handle () in
 273    let rec pattern level = function
 274       | []           -> ()
 275       | term :: tail ->
 276          pattern level tail;
 277          print_string ("? " ^ CicPp.ppterm term ^ nl);
 278          let t = U.start_time () in
 279          let om,rm,sm = C2.get_constraints term in
 280          let oml,rml,sml = List.length om, List.length rm, List.length sm in
 281          let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
 282          let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
 283          let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
 284          let q = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in
 285          if not (List.mem q ! queries) then
 286          begin
 287             issue handle q;
 288             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 289             Printf.printf "%i GEN = %i: %s"
 290                (pred ! query_num) (oml + rml + sml + ool + rol + sol)
 291                (U.stop_time t ^ nl);
 292             flush stdout; queries := q :: ! queries
 293          end
 294    in
 295    for level = max m n downto min m n do
 296       Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level;
 297       flush stderr; pattern level l
 298    done;
 299    Printf.eprintf "\nmqgtop: pattern: %i queries issued\n"
 300       (List.length ! queries);
 301    flush stderr;
 302    C.close handle
 303
 304 let mbackward n m l =
 305    let queries = ref [] in
 306    let univ = Some C1.universe in
 307    let handle = get_handle () in
 308    let rec backward level = function
 309       | []           -> ()
 310       | term :: tail ->
 311          backward level tail;
 312          print_string ("? " ^ CicPp.ppterm term ^ nl);
 313          let t = U.start_time () in
 314          let list_of_must, only = C1.get_constraints [] [] term in
 315          let max_level = pred (List.length list_of_must) in
 316          let must = List.nth list_of_must (min level max_level) in
 317          let q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in
 318          if not (List.mem q ! queries) then
 319          begin
 320             issue handle q;
 321             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 322             Printf.printf "%i GEN = %i: %s"
 323                (pred ! query_num) (List.length must)
 324                (U.stop_time t ^ nl);
 325             flush stdout; queries := q :: ! queries
 326          end
 327    in
 328    for level = max m n downto min m n do
 329       Printf.eprintf "\nmqgtop: backward: trying level %i\n" level;
 330       flush stderr; backward level l
 331    done;
 332    Printf.eprintf "\nmqgtop: backward: %i queries issued\n"
 333       (List.length ! queries);
 334    flush stderr;
 335    C.close handle
 336
 337 let inductive l =
 338    let queries = ref [] in
 339    let univ = None in
 340    let handle = get_handle () in
 341    let rec aux = function
 342       | []           -> ()
 343       | term :: tail ->
 344          aux tail;
 345          print_string ("? " ^ CicPp.ppterm term ^ nl);
 346          let t = U.start_time () in
 347          let m = C3.get_constraints term in
 348          let q = G.query_of_constraints univ m (None, None, None) in
 349          if not (List.mem q ! queries) then
 350          begin
 351             issue handle q;
 352             Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
 353             Printf.printf "%i GEN: %s"
 354                (pred ! query_num) (U.stop_time t ^ nl);
 355             flush stdout; queries := q :: ! queries
 356          end
 357    in
 358    aux l;
 359    Printf.eprintf "\nmqgtop: inductive: %i queries issued\n"
 360       (List.length ! queries);
 361    flush stderr;
 362    C.close handle
 363
 364 let check () =
 365    let handle = get_handle () in
 366    Printf.eprintf
 367       "mqgtop: current options: %s, connection: %s\n"
 368       ! int_options (if C.connected handle then "on" else "off");
 369    C.close handle
 370
 371 let prerr_help () =
 372    prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n";
 373    prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
 374    prerr_endline "testing purposes. mqgtop reads its input from stdin and produces ith output";
 375    prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
 376    prerr_endline "OPTIONS:\n";
 377    prerr_endline "-h  -help               shows this help message";
 378    prerr_endline "-q  -show-queries       outputs generated queries";
 379    prerr_endline "-l  -log-file FILE      sets the log file";
 380    prerr_endline "-o  -options STRING     sets the interpreter options";
 381    prerr_endline "-c  -check              checks the database connection";
 382    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
 383    prerr_endline "-b  -bodyof URI         outputs the CIC body of the given HELM object";
 384    prerr_endline "-r  -refobj URI         outputs the references in the given HELM object";
 385    prerr_endline "-s  -shells URI         computes the reference shells of the given HELM object";
 386    prerr_endline "-x  -execute            issues a query given in the input file";
 387    prerr_endline "-i  -interp FILE        sets the CIC short names interpretation file";
 388    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
 389    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
 390    prerr_endline "-U  T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns";
 391    prerr_endline "-C  -compose            issues the \"Compose\" query reading its specifications";
 392    prerr_endline "                        from the input file";
 393    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all";
 394    prerr_endline "                        CIC terms in the input file";
 395    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
 396    prerr_endline "                        on all CIC terms in the input file";
 397    prerr_endline "-P  -pattern LEVEL      issues the \"Pattern\" query for the given level on all";
 398    prerr_endline "                        CIC terms in the input file";
 399    prerr_endline "-MP -multi-pattern      issues the \"Pattern\" query for each level from 7 to 0";
 400    prerr_endline "                        on all CIC terms in the input file";
 401    prerr_endline "-I                      issues the \"Inductive\" query on all CIC terms in the";
 402    prerr_endline "                        input file\n";
 403    prerr_endline "NOTES: * current interpreter options are:";
 404    prerr_endline "         P (postgres), G (Galax), S (show statistics), Q (quiet)";
 405    prerr_endline "       * CIC terms are read with the HELM CIC Textual Parser";
 406    prerr_endline "       * -typeof / -bodyof do not work with proofs in progress\n"
 407
 408 let rec parse = function
 409    | [] -> ()
 410    | ("-h"|"-help") :: rem -> prerr_help (); parse rem
 411    | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
 412    | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
 413    | ("-t"|"-typeof") :: arg :: rem -> pp_term_of false arg; parse rem
 414    | ("-b"|"-bodyof") :: arg :: rem -> pp_term_of true arg; parse rem
 415    | ("-r"|"-refobj") :: arg :: rem -> show_refobj arg; parse rem
 416    | ("-s"|"-shells") :: arg :: rem -> compute_shells arg; parse rem
 417    | ("-x"|"-execute") :: rem -> execute stdin; parse rem
 418    | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
 419    | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
 420    | ("-c"|"-check") :: rem -> check (); parse rem
 421    | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
 422    | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
 423    | ("-C"|"-compose") :: rem -> compose (); parse rem
 424    | ("-B"|"-backward") :: arg :: rem ->
 425       let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
 426    | ("-MB"|"-multi-backward") :: arg :: rem ->
 427       let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
 428    | ("-P"|"-pattern") :: arg :: rem ->
 429       let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
 430    | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
 431    | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem ->
 432       unreferred arg1 arg2; parse rem
 433    | ("-I"|"-inductive") :: rem -> inductive (get_terms ()); parse rem
 434    | _ :: rem -> parse rem
 435
 436 let _ =
 437    Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml";
 438    let t = U.start_time () in
 439 (*   Logger.log_callback :=
 440       (Logger.log_to_html
 441        ~print_and_flush:(fun s -> print_string s; flush stdout)) ;
 442 *)   parse (List.tl (Array.to_list Sys.argv));
 443    prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
 444    exit 0