X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=42df90768263b2749c30f9ff81c1c0dcf4f9b12c;hb=a7063fc0997a9d9eae6c329443e67ab92c4b6a0f;hp=9b716637a9ed8c0c1c4ba2736034595365b461b3;hpb=9547c888a55a5372ff2f6a2d2a9eab7d5d7c01fb;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 9b716637a..42df90768 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
  let debug = false
  let debug_print s = if debug then prerr_endline (Lazy.force s)
 
@@ -120,13 +122,6 @@ let new_search_theorems f dbd proof goal depth sign =
 
 exception NoOtherChoices;;
 
-let is_in_metasenv goal metasenv =
-  try
-    let (_, ey ,ty) =
-      CicUtil.lookup_meta goal metasenv in
-      true
-  with CicUtil.Meta_not_found _ -> false 
-
 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
  universe
   =
@@ -137,7 +132,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
   let _,metasenv,p,_ = proof in
     (* first of all we check if the goal has been already
        inspected *)
-  assert (is_in_metasenv goal metasenv);
+  assert (CicUtil.exists_meta goal metasenv);
   let exitus =
     try Hashtbl.find inspected_goals ty
     with Not_found -> NotYetInspected in
@@ -234,13 +229,9 @@ and auto_new dbd width already_seen_goals universe = function
   | [] -> []
   | (subst,(proof, goals, sign))::tl ->
       let _,metasenv,_,_ = proof in
-      let is_in_metasenv (goal, _) =
-        try
-          let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
-          true
-        with CicUtil.Meta_not_found _ -> false 
+      let goals'=
+        List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
-      let goals'= List.filter is_in_metasenv goals in
     	auto_new_aux dbd 
         width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
 
@@ -304,13 +295,14 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
 ;;
 *)
 
+(*
 let paramodulation_tactic = ref
   (fun dbd ?full ?depth ?width status ->
-     raise (ProofEngineTypes.Fail "Not Ready yet..."));;
+     raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
 
 let term_is_equality = ref
   (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-
+*)
 
 let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
     ?full ~(dbd:HMysql.dbd) () =
@@ -325,7 +317,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
         auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)]
       with
         [] ->  debug_print(lazy "Auto failed");
-	  raise (ProofEngineTypes.Fail "No Applicable theorem")
+	  raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
       | (_,(proof,[],_))::_ ->
           let t2 = Unix.gettimeofday () in
 	  debug_print (lazy "AUTO_TAC HA FINITO");
@@ -342,12 +334,12 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
       | Some _ ->
           let _, metasenv, _, _ = proof in
           let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-          full || (!term_is_equality meta_goal)
+          full || (Inference.term_is_equality meta_goal)
     in
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
-      !paramodulation_tactic dbd ~depth ~width ~full (proof, goal)
+      Saturation.saturate dbd ~depth ~width ~full (proof, goal)
 (*       with ProofEngineTypes.Fail _ -> *)
 (*         normal_auto () *)
     ) else