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

diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml
index 9a7c8d9db..2bf4e5f82 100644
--- a/helm/mathql_test/mqgtop.ml
+++ b/helm/mathql_test/mqgtop.ml
@@ -46,8 +46,8 @@ module L  = MQGTopLexer
 module P  = MQGTopParser
 module TL = CicTextualLexer
 module TP = CicTextualParser
-module C2 = MQueryLevels2
-module C1 = MQueryLevels
+module C2 = CGSearchPattern
+module C1 = CGMatchConclusion
 module GU = MQGUtil
 
 let get_handle () = 
@@ -156,6 +156,11 @@ let locate name =
    issue handle (G.locate name); 
    C.close handle
 
+let unreferred target source =
+   let handle = get_handle () in  
+   issue handle (G.unreferred target source); 
+   C.close handle
+
 let mpattern n m l =
    let queries = ref [] in
    let univ = Some GU.universe_for_search_pattern in 
@@ -193,9 +198,6 @@ let mpattern n m l =
 
 let mbackward n m l =
    let queries = ref [] in
-   let torigth_restriction (u, b) =
-      let p = if b then `MainConclusion None else `InConclusion in (p, u)
-   in
    let univ = Some GU.universe_for_match_conclusion in
    let handle = get_handle () in
    let rec backward level = function
@@ -204,12 +206,10 @@ let mbackward n m l =
          backward level tail;
 	 print_string ("? " ^ CicPp.ppterm term ^ nl);
 	 let t = U.start_time () in
-	 let list_of_must, only = C1.out_restr [] [] term in
+	 let list_of_must, only = C1.get_constraints [] [] term in
          let max_level = pred (List.length list_of_must) in 
 	 let must = List.nth list_of_must (min level max_level) in 
-	 let rigth_must = List.map torigth_restriction must in
-	 let rigth_only = Some (List.map torigth_restriction only) in
-	 let q = G.query_of_constraints univ (rigth_must, [], []) (rigth_only , None, None) in 
+	 let q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in 
 	 if not (List.mem q ! queries) then
 	 begin
 	    issue handle q;
@@ -261,7 +261,8 @@ let prerr_help () =
    prerr_endline "-P  -pattern LEVEL      issues the \"Pattern\" query for the given level on all";
    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\n";
+   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 "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";
@@ -280,13 +281,15 @@ let rec parse = function
    | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
    | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
    | ("-C"|"-compose") :: rem -> compose (); parse rem   
-   | ("-M"|"-backward") :: arg :: rem ->
+   | ("-B"|"-backward") :: arg :: rem ->
       let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
    | ("-MB"|"-multi-backward") :: arg :: rem ->
       let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
    | ("-P"|"-pattern") :: arg :: rem ->
       let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
    | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
+   | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem ->
+      unreferred arg1 arg2; parse rem
    | _ :: rem -> parse rem
 
 let _ =