From 6c3a5a7adc3f37ddfb99a69b050fbf324e95e583 Mon Sep 17 00:00:00 2001
From: Matteo Selmi <matteo.selmi@mail.polimi.it>
Date: Tue, 13 Jul 2004 08:35:28 +0000
Subject: [PATCH] Modified filtering function

---
 helm/ocaml/tactics/filter_auto.ml     | 25 ++++++++++++++++++-------
 helm/ocaml/tactics/filter_auto.mli    |  1 +
 helm/ocaml/tactics/newConstraints.ml  |  8 ++++++++
 helm/ocaml/tactics/newConstraints.mli |  1 +
 helm/ocaml/tactics/tacticChaser.ml    |  4 ++--
 5 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml
index a87be6c49..b5fa2e2d7 100644
--- a/helm/ocaml/tactics/filter_auto.ml
+++ b/helm/ocaml/tactics/filter_auto.ml
@@ -67,7 +67,7 @@ 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 =
@@ -83,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 distinct(refObj0.source) from " ^ from ^ " where " ^ where in
-    (* prerr_endline query;*)
+     (*prerr_endline query;*)
     Mysql.exec conn query
 ;;
 
@@ -127,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
diff --git a/helm/ocaml/tactics/filter_auto.mli b/helm/ocaml/tactics/filter_auto.mli
index 06909a836..699eacf62 100644
--- a/helm/ocaml/tactics/filter_auto.mli
+++ b/helm/ocaml/tactics/filter_auto.mli
@@ -36,4 +36,5 @@ val filter_uris:
 	Mysql.dbd ->
 	NewConstraints.StringSet.t ->
 	(int * string) list ->
+	string ->
 	(int * string) list
diff --git a/helm/ocaml/tactics/newConstraints.ml b/helm/ocaml/tactics/newConstraints.ml
index 00cf27956..f384e6f4d 100644
--- a/helm/ocaml/tactics/newConstraints.ml
+++ b/helm/ocaml/tactics/newConstraints.ml
@@ -310,3 +310,11 @@ let prefixes n t =
     | None, set when (SetSet.is_empty set) -> None, []
     | _, _ -> assert false
 ;;
+
+let mainandcons t =
+  let const = constants_concl t in
+  match prefixes 1 t with 
+    Some main, _ -> main, const
+  | _,_ ->  assert false
+;;
+
diff --git a/helm/ocaml/tactics/newConstraints.mli b/helm/ocaml/tactics/newConstraints.mli
index d81c66fb0..52c2d7169 100644
--- a/helm/ocaml/tactics/newConstraints.mli
+++ b/helm/ocaml/tactics/newConstraints.mli
@@ -58,3 +58,4 @@ val constants_concl : Cic.term -> StringSet.t
 
 val pp_prefixes : ((int * (StringSet.elt list)) list) -> string
 
+val mainandcons : Cic.term -> (string *  StringSet.t)
diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index e4e20f640..831ccc6f4 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -145,7 +145,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
   *)
   (* concl_cost are the costants in the conclusion of the proof 
      while hyp_const are the constants in the hypothesis *)
-  let concl_const = NewConstraints.constants_concl ty in
+  let (main_concl,concl_const) = NewConstraints.mainandcons ty in
   prerr_endline ("Ne sono rimasti 1 " ^ string_of_int (List.length uris));
   let hyp t set =
     match t with
@@ -161,7 +161,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
     if (List.length uris < (Filter_auto.power 2 (List.length (NewConstraints.StringSet.elements all_const))))
      then 
      (prerr_endline("metodo vecchio");List.filter (Filter_auto.filter_new_constants conn all_const) uris)
-    else Filter_auto.filter_uris conn all_const uris in 
+    else Filter_auto.filter_uris conn all_const uris main_concl in 
 (*
   let uris =
     (* ristretto all cache *)
-- 
2.39.2