Even if we are at depth 0, we first check in the cache for a solution,

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

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 59e90e6daec19d7aaa6c9e2b4c27f7f61c86feda..c7cffc8af6403383a60a18510dafabf1dd65930a 100644 (file)
--- a/components/tactics/auto.ml
+++ b/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,6 +850,7 @@ 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) *)
@@ -859,7 +865,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
@@ -886,7 +894,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