From 5e029a748c53fde142de1b0ee08a0fd100c01f06 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 May 2007 13:20:33 +0000
Subject: [PATCH] Improved pruning (no propress).

---
 components/tactics/auto.ml | 57 +++++++++++++++++++++++++++++++++++---
 1 file changed, 53 insertions(+), 4 deletions(-)

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 01749a59c..ae2ecd21b 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -1184,6 +1184,25 @@ let remove_s_from_fl (id,_,_) (fl : fail list) =
   in 
     aux fl
 ;;
+
+let prunable_for_size flags s m todo =
+  let rec aux b = function
+    | (S _)::tl -> aux b tl
+    | (D (_,_,T))::tl -> aux b tl
+    | (D g)::tl -> 
+	(match calculate_goal_ty g s m with
+          | None -> aux b tl
+          | Some (canonical_ctx, gty) -> 
+            let gsize, _ = 
+              Utils.weight_of_term 
+		~consider_metas:false ~count_metas_occurrences:true gty in
+	    let newb = b || gsize > flags.maxgoalsizefactor in
+	    aux newb tl)
+    | [] -> b
+  in
+    aux false todo
+
+(*
 let prunable ty todo =
   let rec aux b = function
     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
@@ -1193,6 +1212,33 @@ let prunable ty todo =
   in
     aux false todo
 ;;
+*)
+
+let prunable menv subst ty todo =
+  let rec aux = function
+    | (S(_,k,_,_))::tl ->
+	(match Equality.meta_convertibility_subst k ty menv with
+	  | None -> aux tl
+	  | Some variant -> no_progress variant tl (* || aux tl)*) )
+    | (D (_,_,T))::tl -> aux tl
+    | _ -> false
+  and no_progress variant = function
+    | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
+    | D ((n,_,P) as g)::tl -> 
+	(match calculate_goal_ty g subst menv with
+           | None -> no_progress subst tl
+           | Some (_, gty) -> 
+	       (match calculate_goal_ty g variant menv with
+		  | None -> assert false
+		  | Some (_, gty') ->  
+		      if gty = gty' then
+			no_progress variant tl
+		      else false))
+    | _::tl -> no_progress subst tl
+  in
+    aux todo
+
+;;
 
 let auto_main tables maxm context flags universe cache elems =
   auto_context := context;
@@ -1244,12 +1290,15 @@ let auto_main tables maxm context flags universe cache elems =
             aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
         | Some (canonical_ctx, gty) -> 
             let gsize, _ = 
-              Utils.weight_of_term ~count_metas_occurrences:true gty 
+              Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty 
             in
             if gsize > flags.maxgoalsizefactor then
-              (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int size));
+	      (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
                aux tables maxm flags cache orlist)
-            else
+            else if prunable_for_size flags s m todo then
+		(prerr_endline ("POTO at depth: "^(string_of_int depth));
+	         aux tables maxm flags cache orlist)
+	    else
             (* still to be proved *)
             (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
             match cache_examine cache gty with
@@ -1274,7 +1323,7 @@ let auto_main tables maxm context flags universe cache elems =
                     aux tables maxm flags cache orlist
                 | _ -> hint := None;
                     (* more depth or is the first time we see the goal *)
-                    if prunable gty todo then
+                    if prunable m s gty todo then
                       (debug_print (lazy(
                          "FAIL: LOOP: one father is equal"));
                        aux tables maxm flags cache orlist)
-- 
2.39.2