X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql_test%2Fmqgtop.ml;h=bb776474761377a2fca8451524889a9e09b4398f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2bf4e5f82c55926abc033123ea228fc48c566495;hpb=96134b9ec1030ed15cea00d751dd4d744463f62c;p=helm.git

diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml
index 2bf4e5f82..bb7764747 100644
--- a/helm/mathql_test/mqgtop.ml
+++ b/helm/mathql_test/mqgtop.ml
@@ -46,13 +46,14 @@ module L  = MQGTopLexer
 module P  = MQGTopParser
 module TL = CicTextualLexer
 module TP = CicTextualParser
+module C3 = CGLocateInductive
 module C2 = CGSearchPattern
 module C1 = CGMatchConclusion
 module GU = MQGUtil
 
 let get_handle () = 
-   C.init (C.flags_of_string ! int_options)
-          (fun s -> print_string s; flush stdout) 
+   C.init ~flags:(C.flags_of_string ! int_options)
+          ~log:(fun s -> print_string s; flush stdout) () 
              
 let issue handle q =
    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
@@ -72,14 +73,14 @@ let issue handle q =
       let out = output_string och in 
       if ! query_num = 1 then out (time () ^ nl);
       out ("Query: " ^ string_of_int ! query_num ^ nl);
-      U.text_of_query out q nl;
+      U.text_of_query out nl q;
       out ("Result: " ^ nl);
-      U.text_of_result out r nl;
+      U.text_of_result out nl r;
       close_out och
    in
-   if ! show_queries then U.text_of_query (output_string stdout) q nl;
+   if ! show_queries then U.text_of_query (output_string stdout) nl q;
    let r = I.execute handle q in    
-   U.text_of_result (output_string stdout) r nl;
+   U.text_of_result (output_string stdout) nl r;
    if ! log_file <> "" then log q r; 
    incr query_num;
    flush stdout
@@ -163,7 +164,7 @@ let unreferred target source =
 
 let mpattern n m l =
    let queries = ref [] in
-   let univ = Some GU.universe_for_search_pattern in 
+   let univ = Some C2.universe in 
    let handle = get_handle () in
    let rec pattern level = function
       | []           -> ()
@@ -198,7 +199,7 @@ let mpattern n m l =
 
 let mbackward n m l =
    let queries = ref [] in
-   let univ = Some GU.universe_for_match_conclusion in
+   let univ = Some C1.universe in
    let handle = get_handle () in
    let rec backward level = function
       | []           -> ()
@@ -229,6 +230,33 @@ let mbackward n m l =
    flush stderr;
    C.close handle
 
+let inductive l = 
+   let queries = ref [] in
+   let univ = None in 
+   let handle = get_handle () in
+   let rec aux = function
+      | []           -> ()
+      | term :: tail -> 
+         aux tail;
+	 print_string ("? " ^ CicPp.ppterm term ^ nl);
+	 let t = U.start_time () in
+         let m = C3.get_constraints term in
+	 let q = G.query_of_constraints univ m (None, None, None) in 
+	 if not (List.mem q ! queries) then
+	 begin
+	    issue handle q;
+	    Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
+	    Printf.printf "%i GEN: %s"
+	       (pred ! query_num) (U.stop_time t ^ nl);
+	    flush stdout; queries := q :: ! queries
+	 end
+   in 
+   aux l;
+   Printf.eprintf "\nmqgtop: inductive: %i queries issued\n" 
+      (List.length ! queries);
+   flush stderr;
+   C.close handle
+
 let check () =
    let handle = get_handle () in
    Printf.eprintf 
@@ -252,6 +280,7 @@ let prerr_help () =
    prerr_endline "-i  -interp FILE        sets the CIC short names interpretation file";
    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
+   prerr_endline "-U  T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns";
    prerr_endline "-C  -compose            issues the \"Compose\" query reading its specifications";
    prerr_endline "                        from the input file"; 
    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all";
@@ -262,7 +291,8 @@ let prerr_help () =
    prerr_endline "                        CIC terms in the input file";
    prerr_endline "-MP -multi-pattern      issues the \"Pattern\" query for each level from 7 to 0";
    prerr_endline "                        on all CIC terms in the input file";
-   prerr_endline "-U  T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns\n";
+   prerr_endline "-I                      issues the \"Inductive\" query on all CIC terms in the";
+   prerr_endline "                        input file\n";
    prerr_endline "NOTES: * current interpreter options are:";
    prerr_endline "         P (postgres), G (Galax), S (show statistics), Q (quiet)";
    prerr_endline "       * CIC terms are read with the HELM CIC Textual Parser";
@@ -290,13 +320,17 @@ let rec parse = function
    | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
    | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem ->
       unreferred arg1 arg2; parse rem
+   | ("-I"|"-inductive") :: rem -> inductive (get_terms ()); parse rem
    | _ :: rem -> parse rem
 
 let _ =
+   Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml";
    let t = U.start_time () in
-   Logger.log_callback :=
-      (Logger.log_to_html 
+(*
+   CicLogger.log_callback :=
+      (CicLogger.log_to_html 
        ~print_and_flush:(fun s -> print_string s; flush stdout)) ; 
+*)
    parse (List.tl (Array.to_list Sys.argv)); 
    prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
    exit 0