X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=117978d8c646c3b06f932fc497b277f3bea8ec50;hb=be292a08ee0c8792b21105952626da05d5f645b9;hp=2db8cc0014ec1d468b60df2872caff898fba9c57;hpb=2eaee49a7ff3ed74598a0db84ce4dbc5bca92380;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 2db8cc001..117978d8c 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,17 +26,17 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug_print s = () (* prerr_endline s;; *)
+let debug_print s = () (*prerr_endline s;;*)
 
 (* {{{ *********** local given_clause wrapper ***********)
 
-let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
+let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
   let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
     match tables with
     | None -> 
         (* first time, do a huge saturation *)
         let bag, equalities, cache, maxmeta = 
-          Saturation.find_equalities dbd status ?auto smart_flag cache
+          Saturation.find_equalities dbd status smart_flag auto cache
         in
         let passive = Saturation.make_passive equalities in
         let active = Saturation.make_active [] in
@@ -50,8 +50,8 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
         (* saturate a bit more if cache cahnged *)
         let bag, equalities, cache, maxm = 
           if cache_size oldcache <> cache_size cache then 
-            Saturation.saturate_more
-              bag active maxm status smart_flag ?auto cache
+            Saturation.close_more
+              bag active maxm status smart_flag auto cache
           else
             bag, [], cache, maxm
         in
@@ -59,7 +59,7 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
         let passive = Saturation.add_to_passive equalities passive in
         let goal_steps, saturation_steps, timeout =
           if flags.use_only_paramod then max_int,max_int,flags.timeout
-          else max 80 minsteps, minsteps, infinity
+          else max 50 minsteps, minsteps, infinity
         in
         active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
   in
@@ -112,7 +112,7 @@ let new_metasenv_and_unify_and_t
    let flags = 
      {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} 
    in
-   given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta) 
+   given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta) 
  with
  | None, active, passive, bag,_,_ -> 
      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
@@ -269,16 +269,18 @@ let is_an_equational_goal = function
 ;;
 
 let equational_case 
-  dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context 
+  dbd tables maxm auto cache depth fake_proof goalno goalty subst context 
     flags
 =
   let ppterm = ppterm context in
   prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
+(*
   prerr_endline "<CACHE>";
   prerr_endline (cache_print context cache);
   prerr_endline "</CACHE>";
+*)
   match 
-    given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) 
+    given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno) 
   with
   | None, active,passive, bag, cache, maxmeta -> 
       let tables = Some (active,passive,bag,cache) in
@@ -356,7 +358,8 @@ let is_equational_case goalty flags =
   (flags.use_only_paramod && ensure_equational goalty)
 ;;
 let cache_add_success sort cache k v =
-  if sort = P then cache_add_success cache k v else cache
+  if sort = P then cache_add_success cache k v else cache_remove_underinspection
+  cache k
 ;;
 
 let rec auto_main dbd tables maxm context flags elems cache =
@@ -472,11 +475,11 @@ let rec auto_main dbd tables maxm context flags elems cache =
           if is_equational_case goalty flags then
             match 
               equational_case dbd tables maxm
-                ~auto:callback_for_paramod cache
+                (Some callback_for_paramod) cache
                 depth fake_proof goalno goalty subst context flags 
             with
             | Some elems, tables, cache, maxm -> 
-                elems, tables, cache, maxm (* manca cache *)
+                elems, tables, cache, maxm 
             | None, tables,cache,maxm -> 
                 applicative_case dbd tables maxm depth subst fake_proof goalno 
                   goalty metasenv context cache
@@ -530,7 +533,7 @@ let auto dbd cache context metasenv gl flags =
   | Fail s,tables,cache,maxm -> None,cache
 ;;
 
-let applyS_tac ~dbd ~term =
+let applyS_tac ~dbd ~term ~params =
  ProofEngineTypes.mk_tactic
   (fun status ->
     try