Calling paramodulation instead of demod_all

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 61ae8bd791fbbe173f62fe1f5f60c7150521e302..73a96d23b50c76f7a4f65b51cd9a627b943af209 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,7 +26,7 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug = true;;
+let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
@@ -404,7 +404,7 @@ let init_cache_and_tables
              c metasenv [] context st (Some head), maxmeta)
        (automation_cache,CicMkImplicit.new_meta metasenv subst) ct
     in
-    AutomationCache.pp_cache automation_cache;
+    (* AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
     cache
@@ -440,7 +440,7 @@ let init_cache_and_tables
          AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
        automation_cache s_t_ty
     in
-    AutomationCache.pp_cache automation_cache;
+    (* AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
     cache_add_list cache_empty context t_ty
@@ -1105,7 +1105,7 @@ let apply_smart_aux
         in
         match
           Saturation.given_clause bag (proof'''',newmeta) active passive 
-            20 2 infinity
+            1 0 infinity
         with 
           | None, active, passive, bag -> 
               raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
@@ -1601,6 +1601,33 @@ let equational_case
                 (active,passive,bag), cache, flags
       end
     else
+      begin
+        debug_print (lazy ("NARROWING DEL GOAL: " ^ 
+                         string_of_int goalno ^ " " ^ ppterm goalty ));
+        let goal_steps, saturation_steps, timeout =
+          1,0,flags.timeout 
+        in
+        match
+          Saturation.given_clause bag status active passive 
+            goal_steps saturation_steps timeout
+        with 
+          | None, active, passive, bag -> 
+              [], (active,passive,bag), cache, flags
+          | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
+            passive,bag ->
+              assert_subst_are_disjoint subst subst';
+              let subst = 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
+              incr candidate_no;
+              [(!candidate_no,proof),metasenv,subst,open_goals], 
+                (active,passive,bag), cache, flags
+      end
+(*
       begin
         let params = ([],["use_context","false"]) in
         let automation_cache = { 
@@ -1609,6 +1636,7 @@ let equational_case
         in
         try 
           let ((_,metasenv,subst,_,_,_),open_goals) =
+
             solve_rewrite ~params ~automation_cache
               (fake_proof, goalno)
           in
@@ -1635,6 +1663,7 @@ let equational_case
           res', (active,passive,bag), cache, flags 
 *)
       end
+*)
 ;;
 
 let sort_new_elems = 
@@ -1768,7 +1797,13 @@ let smart_applicative_case dbd
           try_candidate dbd goalty
             tables subst fake_proof goalno depth context cand
         with
-        | None, tables -> tables, elems
+        | None, tables ->
+            (* if normal application fails we try to be smart *)
+           (match try_smart_candidate dbd goalty
+               tables subst fake_proof goalno depth context cand
+            with
+              | None, tables -> tables, elems
+               | Some x, tables -> tables, x::elems)
         | Some x, tables -> tables, x::elems)
       (tables,[]) candidates
   in