Procedural: clear tactics added

[helm.git] / helm / software / components / tactics / auto.ml

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index e85b89b95fe4ddbe76fa3b5dd6340bdf893fae38..c2d933b0a091750b5205587faddbf872984f7216 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,7 +26,7 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug = true;;
+let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
@@ -795,12 +795,9 @@ let rec auto_main tables maxm context flags elems universe cache =
                    "with depth"^string_of_int depth));
           debug_print (lazy (AutoCache.cache_print context cache));
           if sort = T (* && tl <> []*)  then 
-          aux flags tables maxm cache ((metasenv,subst,gl)::tl)
-         (* Success (metasenv,subst,tl), tables, cache,maxm *)
-          (*
             (debug_print 
               (lazy (" FAILURE(not in prop)"));
-            aux flags tables maxm cache tl (* FAILURE (not in prop) *)) *)
+            aux flags tables maxm cache ((metasenv,subst,gl)::tl))
           else
           match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
           | Fail s, tables, cache, maxm' -> 
@@ -854,10 +851,6 @@ let rec auto_main tables maxm context flags elems universe cache =
     let goalty = CicMetaSubst.apply_subst subst goalty in
 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
       (* FAILURE (euristic cut) *)
-    if depth <= 0 then
-       Fail (string_of_int goalno ^ "as depth <=0"),
-          tables,cache,maxm (*FAILURE(depth)*)
-      else
     match cache_examine cache goalty with
     | Failed_in d when d >= depth -> 
         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
@@ -898,7 +891,7 @@ let rec auto_main tables maxm context flags elems universe cache =
            elems, tables, cache, maxm, flags  
         in
         aux flags tables maxm cache elems
-    | _ -> Fail "??",tables,cache,maxm 
+    | _ -> Fail "depth = 0",tables,cache,maxm 
   in
     aux flags tables maxm cache elems
 
@@ -951,7 +944,9 @@ let auto flags metasenv tables universe cache context metasenv gl =
   | Success (metasenv,subst,_), tables,cache,_ -> 
       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
       Some (subst,metasenv), cache
-  | Fail s,tables,cache,maxm -> None,cache
+  | Fail s,tables,cache,maxm -> 
+      prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+      None,cache
 ;;
 
 let bool params name default =
@@ -1189,6 +1184,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
             in
               proof,opened
        | Fail s,tables,cache,maxm -> 
+           prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
            raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 ;;