X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=e85b89b95fe4ddbe76fa3b5dd6340bdf893fae38;hb=b19dc7f6536f70b2dc911e8b78538dfcc64b6d4a;hp=59e90e6daec19d7aaa6c9e2b4c27f7f61c86feda;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 59e90e6da..e85b89b95 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,9 +26,9 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug = false;;
+let debug = true;;
 let debug_print s = 
-  if debug then () else prerr_endline (Lazy.force s);;
+  if debug then prerr_endline (Lazy.force s);;
 
 (* functions for retrieving theorems *)
 
@@ -708,8 +708,8 @@ let try_candidate
     in
     debug_print (lazy ("   OK: " ^ ppterm cand));
     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
-    assert_subst_are_disjoint subst subst';
-    let subst = subst@subst' in
+    (* assert_subst_are_disjoint subst subst'; *)
+    let subst = subst' in
     let open_goals = order_new_goals metasenv subst open_goals ppterm in
     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
     Some (metasenv,subst,open_goals), tables , maxmeta
@@ -745,7 +745,8 @@ let is_a_green_cut goalty =
   CicUtil.is_meta_closed goalty
 ;;
 
-let prop = function (_,_,P) -> true | _ -> false;;
+let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
+
 let calculate_timeout flags = 
     if flags.timeout = 0. then 
       (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
@@ -790,12 +791,16 @@ let rec auto_main tables maxm context flags elems universe cache =
         try
           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
           debug_print 
-	    (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
+	    (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^
+                   "with depth"^string_of_int depth));
           debug_print (lazy (AutoCache.cache_print context cache));
-          if sort = T && tl <> [] then (* FIXME!!!! *)
+          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 tl (* FAILURE (not in prop) *)) *)
           else
           match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
           | Fail s, tables, cache, maxm' -> 
@@ -818,12 +823,12 @@ let rec auto_main tables maxm context flags elems universe cache =
                 debug_print 
 		  (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
                 if is_a_green_cut goalty then
-                  (assert_proof_is_valid proof metasenv context goalty;
+                  (* assert_proof_is_valid proof metasenv context goalty; *)
                   let cache = cache_add_success sort cache goalty proof in
-                  aux flags tables maxm cache ((metasenv,subst,gl)::tl))
+                  aux flags tables maxm cache ((metasenv,subst,gl)::tl)
                 else
                   (let goalty = CicMetaSubst.apply_subst subst goalty in
-                  assert_proof_is_valid proof metasenv context goalty;
+                 (* assert_proof_is_valid proof metasenv context goalty; *)
                   let cache = 
                     if is_a_green_cut goalty then
                       cache_add_success sort cache goalty proof
@@ -845,9 +850,14 @@ let rec auto_main tables maxm context flags elems universe cache =
           aux flags tables maxm cache ((metasenv,subst,gl)::tl)
 
   and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
+    (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
     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),
@@ -859,7 +869,9 @@ let rec auto_main tables maxm context flags elems universe cache =
         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
         debug_print (lazy ("  CACHE HIT!"));
         Success (metasenv, subst, []), tables, cache, maxm
-    | UnderInspection -> Fail "looping",tables,cache, maxm
+    | UnderInspection -> 
+	(* assert (not (is_a_green_cut goalty)); *)
+	Fail "looping",tables,cache, maxm
     | Notfound 
     | Failed_in _ when depth > 0 -> (* we have more depth now *)
         let cache = cache_add_underinspection cache goalty depth in