From: Matteo Selmi <matteo.selmi@mail.polimi.it>
Date: Fri, 18 Jun 2004 13:50:11 +0000 (+0000)
Subject: Corrections to "auto" tactic
X-Git-Tag: pre_subst_in_kernel~19
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a1bb9ea2a09b4b64ae8b61144da4c1035d1c1f1;p=helm.git

Corrections to "auto" tactic
---

diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml
index f4964f575..a87be6c49 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 = 
@@ -71,10 +72,7 @@ let rec exec_query (conn:Mysql.dbd) uris k =
     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 
@@ -91,8 +89,8 @@ let rec exec_query (conn:Mysql.dbd) uris k =
   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
 ;;
 
diff --git a/helm/ocaml/tactics/match_concl.ml b/helm/ocaml/tactics/match_concl.ml
index 078cb931a..c2266cd10 100644
--- a/helm/ocaml/tactics/match_concl.ml
+++ b/helm/ocaml/tactics/match_concl.ml
@@ -136,8 +136,9 @@ let rec exec_must (conn:Mysql.dbd) (l:MQGTypes.r_obj list) (cc:count_condition)
 	     ("no_inconcl_aux.source = refObj0.source")::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 refObj0.source from " ^ from ^ " where " ^ where in
+   (* prerr_endline query;*)
     Mysql.exec conn query
 ;;
 
diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index c8217e786..b0148224c 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -136,7 +136,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
     let len = String.length s in
     let suffix = String.sub s (len-4) 4 in
       not (suffix  = ".var") in
-  let uris = List.filter isvar uris in
+  let uris = List.filter isvar uris in 
   (* delete all not "cic:/Coq" uris *)
   (*
   let uris =
@@ -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_of ty in
+  let concl_const = NewConstraints.constants_concl ty in
   prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
   let hyp t set =
     match t with