X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ffilter_auto.ml;h=b5fa2e2d79df12e44f5c398e699518a88de97620;hb=f55b5800229c0819448abf38dfeb1527b4ec08e2;hp=f4964f575327f8695eb08dfcfc8dda19e9ebf0fc;hpb=cb54cf0485d2df551ad674ee3beb087ef6f90a3c;p=helm.git

diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml
index f4964f575..b5fa2e2d7 100644
--- a/helm/ocaml/tactics/filter_auto.ml
+++ b/helm/ocaml/tactics/filter_auto.ml
@@ -32,6 +32,8 @@ let main_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConc
 
 let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;;
 
+let in_body = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InBody'";;
+
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
 
 let hyp_const (conn:Mysql.dbd) uri =
@@ -39,9 +41,8 @@ let hyp_const (conn:Mysql.dbd) uri =
   (*query to obtain all the constants in the hypothesis and conclusion of the theorem*)
   let query =
      "select h_occurrence from refObj where source='"^uri^
-    "' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^
-    "or h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
-(*  prerr_endline ("$$$$$$$$$$$$$$$"^query);*)
+    "' and (not (h_position ="^in_body^"))" in
+  (*prerr_endline ("$$$$$$$$$$$$$$$"^query);*)
   let result = Mysql.exec conn query in 
   (* now we transform the result in a set *)
   let f a = 
@@ -66,15 +67,12 @@ let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
 
 
 
-let rec exec_query (conn:Mysql.dbd) uris k = 
+let rec exec_query (conn:Mysql.dbd) (uris,main) k  = 
   let add_must (n,from,where) uri =
     let refObjn = "refObj" ^ (string_of_int n) in
     let new_must =
       [ refObjn^".h_occurrence = '" ^ uri ^ "'";
-        "("^refObjn^".h_position = " ^ main_conclusion^ " or "
-	^refObjn^".h_position = " ^ in_conclusion^ " or "
-	^refObjn^".h_position = " ^ main_hypothesis^ " or "
-	^refObjn^".h_position = " ^ in_hypothesis^ ")"] in
+        "(not ("^refObjn^".h_position ="^in_body^"))"] in
     let where' = 
       if n = 0 then new_must@where
       else 
@@ -85,14 +83,17 @@ let rec exec_query (conn:Mysql.dbd) uris k =
   let (_,from,where) = 
     List.fold_left add_must (0,[],[]) uris in
   let from,where = 
-    "no_concl_hyp"::from, 
-    ("no=" ^ (string_of_int k))::
-    ("no_concl_hyp.source = refObj0.source")::where
+    ["no_concl_hyp";"refObj as main"]@from, 
+    ["no=" ^ (string_of_int k);
+     "no_concl_hyp.source = refObj0.source";
+     "main.source = refObj0.source";
+     "main.h_occurrence = '" ^ main ^ "'";
+     "main.h_position = " ^ main_conclusion]@where
   in
   let from = String.concat "," from in
   let where = String.concat " and " where in
-  let query = "select refObj0.source from " ^ from ^ " where " ^ where in
-   (* prerr_endline query;*)
+  let query = "select distinct(refObj0.source) from " ^ from ^ " where " ^ where in
+     (*prerr_endline query;*)
     Mysql.exec conn query
 ;;
 
@@ -129,15 +130,23 @@ List.exists ex list_of_uris
 ;;
     
 
-let filter_uris (conn:Mysql.dbd) const uris =
+let filter_uris (conn:Mysql.dbd) const uris main =
   let subsets_of_consts = 
     setset_to_listlist (powerset const) in
+  let ex u =
+    if u = main then true
+    else false
+  in
+  let subsets_of_consts =
+  List.filter 
+  	(fun (_,b) -> (List.exists ex b)) 
+		subsets_of_consts in
   let uris_of_const =
     List.concat
      (List.map 
 	      (fun (m,s) -> 
 		 (let res = 
-		    exec_query conn s m in
+		    exec_query conn (s,main) m in
 		  let f a = 
 		    match (Array.to_list a) with
 			[Some uri] -> uri