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

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 6b1bf82ab..2db8cc001 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -24,16 +24,19 @@
  *)
 
 open AutoTypes;;
+open AutoCache;;
 
 let debug_print s = () (* prerr_endline s;; *)
 
-let given_clause dbd ?tables maxm ?auto cache subst flags status =
-  prerr_endline ("given_clause " ^ string_of_int maxm);
-  let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout = 
+(* {{{ *********** local given_clause wrapper ***********)
+
+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 true cache
+          Saturation.find_equalities dbd status ?auto smart_flag cache
         in
         let passive = Saturation.make_passive equalities in
         let active = Saturation.make_active [] in
@@ -44,9 +47,11 @@ let given_clause dbd ?tables maxm ?auto cache subst flags status =
         let maxm = max maxm maxmeta in
         active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
     | Some (active,passive,bag,oldcache) -> 
+        (* 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 true ?auto cache
+            Saturation.saturate_more
+              bag active maxm status smart_flag ?auto cache
           else
             bag, [], cache, maxm
         in
@@ -54,17 +59,19 @@ let given_clause dbd ?tables maxm ?auto cache subst flags 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 30 minsteps, minsteps, infinity
+          else max 80 minsteps, minsteps, infinity
         in
         active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
   in
-  let res,a,p, maxmeta = 
+  let res,actives,passives,maxmeta = 
     Saturation.given_clause bag maxmeta status active passive 
       goal_steps saturation_steps timeout
   in
-  res,a,p,bag,cache,maxmeta
+  res,actives,passives,bag,cache,maxmeta
 ;;
 
+(* }}} ****************************************************************)
+
 (* {{{ **************** applyS *******************)
 
 let new_metasenv_and_unify_and_t 
@@ -101,11 +108,11 @@ let new_metasenv_and_unify_and_t
    PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) 
  in
  match 
-   let cache, flags = AutoTypes.cache_empty, AutoTypes.default_flags() in
+   let cache, flags = cache_empty, default_flags() in
    let flags = 
      {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} 
    in
-   given_clause dbd ?tables 0 cache [] flags (proof'''',newmeta) 
+   given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta) 
  with
  | None, active, passive, bag,_,_ -> 
      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
@@ -271,7 +278,7 @@ let equational_case
   prerr_endline (cache_print context cache);
   prerr_endline "</CACHE>";
   match 
-    given_clause dbd ?tables maxm ?auto cache subst flags (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
@@ -307,9 +314,9 @@ let try_candidate
 ;;
 
 let applicative_case 
-  dbd tables maxm depth subst fake_proof goalno goalty metasenv context universe
+  dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
 = 
-  let candidates = get_candidates universe goalty in
+  let candidates = get_candidates cache goalty in
   let tables, elems, maxm = 
     List.fold_left 
       (fun (tables,elems,maxm) cand ->
@@ -322,7 +329,7 @@ let applicative_case
       (tables,[],maxm) candidates
   in
   let elems = sort_new_elems elems in
-  elems, tables, maxm
+  elems, tables, cache, maxm
 ;;
 
 (* Works if there is no dependency over proofs *)
@@ -339,9 +346,11 @@ let calculate_timeout flags =
 let is_equational_case goalty flags =
   let ensure_equational t = 
     if is_an_equational_goal t then true 
-    else 
+    else false
+    (*
       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
       raise (ProofEngineTypes.Fail (lazy msg))
+    *)
   in
   (flags.use_paramod && is_an_equational_goal goalty) || 
   (flags.use_only_paramod && ensure_equational goalty)
@@ -350,14 +359,14 @@ let cache_add_success sort cache k v =
   if sort = P then cache_add_success cache k v else cache
 ;;
 
-let rec auto_main dbd tables maxm context flags elems cache universe =
+let rec auto_main dbd tables maxm context flags elems cache =
   let callback_for_paramod maxm flags proof commonctx cache l = 
-    let flags = {flags with use_paramod = false} in
+    let flags = {flags with use_paramod = false;dont_cache_failures=true} in
     let _,metasenv,_,_ = proof in
     let oldmetasenv = metasenv in
     match
       auto_all_solutions
-        dbd tables maxm universe cache commonctx metasenv l flags
+        dbd tables maxm cache commonctx metasenv l flags
     with
     | [],cache,maxm -> [],cache,maxm
     | solutions,cache,maxm -> 
@@ -396,10 +405,15 @@ let rec auto_main dbd tables maxm context flags elems cache universe =
             aux tables maxm cache tl (* FAILURE (not in prop) *))
           else
           match aux_single tables maxm cache metasenv subst elem goalty cc with
-          | Fail _, tables, cache, maxm' -> 
+          | Fail s, tables, cache, maxm' -> 
               assert(maxm' >= maxm);let maxm = maxm' in
-              debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
-              let cache = cache_add_failure cache goalty depth in
+              debug_print
+                (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
+              let cache = 
+                if flags.dont_cache_failures then 
+                  cache_remove_underinspection cache goalty
+                else cache_add_failure cache goalty depth 
+              in
               aux tables maxm cache tl
           | Success (metasenv,subst,others), tables, cache, maxm' ->
               assert(maxm' >= maxm);let maxm = maxm' in
@@ -439,7 +453,8 @@ let rec auto_main dbd tables maxm context flags elems cache universe =
       (* FAILURE (euristic cut) *)
     match cache_examine cache goalty with
     | Failed_in d when d >= depth -> 
-        Fail "depth",tables,cache,maxm(*FAILURE(depth)*)
+        Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
+        tables,cache,maxm(*FAILURE(depth)*)
     | Succeded t -> 
         assert(List.for_all (fun (i,_) -> i <> goalno) subst);
         let entry = goalno, (cc, t,goalty) in
@@ -463,15 +478,11 @@ let rec auto_main dbd tables maxm context flags elems cache universe =
             | Some elems, tables, cache, maxm -> 
                 elems, tables, cache, maxm (* manca cache *)
             | None, tables,cache,maxm -> 
-                let elems, tables, maxm =
                 applicative_case dbd tables maxm depth subst fake_proof goalno 
-                  goalty metasenv context universe 
-                in elems, tables, cache, maxm
+                  goalty metasenv context cache
           else
-            let elems, tables, maxm =
             applicative_case dbd tables maxm depth subst fake_proof goalno 
-              goalty metasenv context universe
-            in elems, tables, cache, maxm
+              goalty metasenv context cache
         in
         aux tables maxm cache elems
     | _ -> Fail "??",tables,cache,maxm 
@@ -479,13 +490,13 @@ let rec auto_main dbd tables maxm context flags elems cache universe =
     aux tables maxm cache elems
 
 and
-  auto_all_solutions dbd tables maxm universe cache context metasenv gl flags 
+  auto_all_solutions dbd tables maxm cache context metasenv gl flags 
 =
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
   let elems = [metasenv,[],goals] in
   let rec aux tables maxm solutions cache elems flags =
-    match auto_main dbd tables maxm context flags elems cache universe with
+    match auto_main dbd tables maxm context flags elems cache with
     | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
     | Success (metasenv,subst,others),tables,cache,maxm -> 
         if Unix.gettimeofday () > flags.timeout then
@@ -500,25 +511,23 @@ and
 
 (* }}} ****************** AUTO ***************)
 
-let auto_all_solutions dbd universe cache context metasenv gl flags =
+let auto_all_solutions dbd cache context metasenv gl flags =
   let solutions, cache, _ = 
-    auto_all_solutions dbd None 0 universe cache context metasenv gl flags
+    auto_all_solutions dbd None 0 cache context metasenv gl flags
   in
   solutions, cache
 ;;
 
-let auto dbd universe cache context metasenv gl flags =
+let auto dbd cache context metasenv gl flags =
+  let initial_time = Unix.gettimeofday() in
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
   let elems = [metasenv,[],goals] in
-  match auto_main dbd None 0 context flags elems cache universe with
-  | Success (metasenv,subst,_), tables,cache,_ -> Some (subst,metasenv), cache
-  | Fail s,tables,cache,maxm ->
-      let cache = cache_clean cache in
-      match auto_main dbd tables maxm context flags elems cache universe with
-      | Success (metasenv,subst,_), tables,cache,_ -> 
-          Some (subst,metasenv), cache
-      | Fail s,tables,cache,maxm -> prerr_endline s;None,cache
+  match auto_main dbd None 0 context flags elems cache with
+  | 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
 ;;
 
 let applyS_tac ~dbd ~term =