1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
29 let _ = MQueryStandard.init
30 let _ = MQueryHELM.init
34 let interp_file = ref "interp.cic"
38 let show_queries = ref false
40 let int_options = ref ""
46 module I = MQueryInterpreter
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
60 C.init (C.flags_of_string ! int_options)
61 (fun s -> print_string s; flush stdout)
64 let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
65 let perm = 64 * 6 + 8 * 6 + 4 in
67 let lt = Unix.localtime (Unix.time ()) in
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)
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;
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;
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
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
109 let get_terms interp =
110 let interp = get_interp () in
111 let lexbuf = Lexing.from_channel stdin in
115 CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
117 (snd (mk_term interp)) :: aux ()
119 CicTextualParser0.Eof -> []
123 let rec join f v1 v2 =
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
134 let rec diff f v1 v2 =
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
143 let add f r k l = join f r [M.string_of_uriref (k, l)]
145 let rec add_cons f r k i j = function
148 let g s = add f s k [i; j] in
149 add_cons g r k i (succ j) tl
151 let rec refobj_l refobj_t map f r = function
154 let f r = refobj_l refobj_t map f r tail in
157 let rec refobj_t f r = function
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
168 refobj_l refobj_t (fun x -> x) f r 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
176 let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
178 | Cic.Const (k, tl) ->
179 let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
181 | Cic.MutInd (k, i, tl) ->
182 let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
184 | Cic.MutConstruct (k, i, j, tl) ->
185 let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
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
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
200 let rec get_refobj_l f r = function
203 let f r = get_refobj_l f r l in
206 let show_refobj uri =
207 let f = List.iter print_endline in
210 let compute_shells uri =
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
218 Printf.printf "shells: computing level %i ... " n; flush stdout;
219 let f r = get_refobj_l (f r) [] r in
224 let pp_term_of b uri =
226 let body, ty = M.get_object (M.uriref_of_string uri) in
227 if b then CicPp.ppterm body else CicPp.ppterm ty
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
234 let rec display = function
238 print_string ("? " ^ CicPp.ppterm term ^ nl);
242 let lexbuf = Lexing.from_channel ich in
243 let handle = get_handle () in
244 let rec execute_aux () =
246 let q = IO.query_of_text lexbuf in
247 issue handle q; execute_aux ()
248 with End_of_file -> ()
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);
260 let handle = get_handle () in
261 issue handle (G.locate name);
264 let unreferred target source =
265 let handle = get_handle () in
266 issue handle (G.unreferred target source);
270 let queries = ref [] in
271 let univ = Some C2.universe in
272 let handle = get_handle () in
273 let rec pattern level = function
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
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
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
299 Printf.eprintf "\nmqgtop: pattern: %i queries issued\n"
300 (List.length ! queries);
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
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
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
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
332 Printf.eprintf "\nmqgtop: backward: %i queries issued\n"
333 (List.length ! queries);
338 let queries = ref [] in
340 let handle = get_handle () in
341 let rec aux = function
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
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
359 Printf.eprintf "\nmqgtop: inductive: %i queries issued\n"
360 (List.length ! queries);
365 let handle = get_handle () in
367 "mqgtop: current options: %s, connection: %s\n"
368 ! int_options (if C.connected handle then "on" else "off");
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"
408 let rec parse = function
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
437 Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml";
438 let t = U.start_time () in
439 (* Logger.log_callback :=
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));