From 91332d82ed5c852a36eb2da15f977bb43aa78c72 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 30 Apr 2009 13:02:14 +0000
Subject: [PATCH] Calling paramodulation instead of demod_all

---
 helm/software/components/tactics/auto.ml | 45 +++++++++++++++++++++---
 1 file changed, 40 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 61ae8bd79..73a96d23b 100644
--- 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
-- 
2.39.2