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