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

diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml
index 6fae7b737..b5fa2e2d7 100644
--- a/helm/ocaml/tactics/filter_auto.ml
+++ b/helm/ocaml/tactics/filter_auto.ml
@@ -32,14 +32,17 @@ 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 =
-  (*query to obtain all the constants in the hypothesis of the theorem*)
+  let uri = escape uri in
+  (*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 = 
@@ -57,9 +60,106 @@ let hyp_const (conn:Mysql.dbd) uri =
    const, the set of the costants of the proof *)
 let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
    let hyp = hyp_const conn uri in
-   prerr_endline (NewConstraints.pp_StringSet hyp);
+ (*  prerr_endline (NewConstraints.pp_StringSet hyp);*)
     NewConstraints.StringSet.subset hyp const
 ;;
 
+
+
+
+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 ^ "'";
+        "(not ("^refObjn^".h_position ="^in_body^"))"] in
+    let where' = 
+      if n = 0 then new_must@where
+      else 
+       (refObjn^".source = refObj" ^ (string_of_int (n-1)) 
+       ^ ".source")::new_must@where in
+  (n+1,("refObj as "^refObjn)::from,where')
+  in
+  let (_,from,where) = 
+    List.fold_left add_must (0,[],[]) uris in
+  let from,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;*)
+    Mysql.exec conn query
+;;
+
+let powerset set =
+  let rec powerset_r set sub =
+    if (NewConstraints.StringSet.is_empty set) then sub
+    else 
+      let a = NewConstraints.StringSet.min_elt set in
+      let newset = NewConstraints.StringSet.remove a set in
+      let newsub = NewConstraints.SetSet.union (NewConstraints.SetSet.add (NewConstraints.StringSet.singleton a)
+                   (NewConstraints.SetSet.fold 
+		       (fun s t -> (NewConstraints.SetSet.add (NewConstraints.StringSet.add a s) t)) 
+		            sub NewConstraints.SetSet.empty)) sub in
+      powerset_r newset newsub in
+powerset_r set NewConstraints.SetSet.empty
+;;
+
+let setset_to_listlist setset =
+  let listset = NewConstraints.SetSet.elements setset in
+  let res = 
+    List.map 
+      (fun set -> 
+	 let el = NewConstraints.StringSet.elements set in
+	 (List.length el, el)) listset in
+    (* ordered by descending cardinality *)
+List.sort (fun (n,_) (m,_) -> m - n) res
+
+let exist_element list_of_uris (_,uri) =
+  let ex u =
+    if u = uri then true
+    else false
+  in
+List.exists ex list_of_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,main) m in
+		  let f a = 
+		    match (Array.to_list a) with
+			[Some uri] -> uri
+		        | _ -> assert false in
+		    Mysql.map ~f:f res))
+	      subsets_of_consts)
+      in
+List.filter (exist_element uris_of_const) uris
+;;  
+   
+let rec power n m =
+  if (m = 1) then n
+  else n*(power n (m-1))
+;;