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 aca89bd4a609a8b427aaa71fc4f8200786fc81b5..c2d933b0a091750b5205587faddbf872984f7216 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -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,13 @@ 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 
             (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' -> 
@@ -818,12 +820,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 +847,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 +862,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 +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
 
@@ -939,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 =
@@ -1177,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"))
 ;;