added some lines to compile for debugging

[helm.git] / helm / software / components / tactics / auto.ml

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 01749a59cbd66888c9abff969da7a6c28202b9d8..e42c3ba513ed2d9e1e1993616f1336337f2a9f56 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -831,9 +831,13 @@ let pause b = in_pause := b;;
 let cond = Condition.create ();;
 let mutex = Mutex.create ();;
 let hint = ref None;;
+let prune_hint = ref [];;
 
 let step _ = Condition.signal cond;;
 let give_hint n = hint := Some n;;
+let give_prune_hint hint =
+  prune_hint := hint :: !prune_hint
+;;
 
 let check_pause _ =
   if !in_pause then
@@ -1081,7 +1085,7 @@ let equational_case
         assert (maxmeta >= maxm);
         let res' =
           List.map 
-            (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
+            (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
                assert_subst_are_disjoint subst subst';
                let subst = subst@subst' in
                let open_goals = 
@@ -1184,6 +1188,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,12 +1216,63 @@ 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 variant 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 variant tl
+  in
+    aux todo
+
+;;
+let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
+  let s = 
+    HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo 
+  in
+  List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
+;;
+let filter_prune_hint l =
+  let prune = !prune_hint in
+  prune_hint := []; (* possible race... *)
+  if prune = [] then l
+  else List.filter (condition_for_prune_hint prune) l
+;;
 let auto_main tables maxm context flags universe cache elems =
   auto_context := context;
   let rec aux tables maxm flags cache (elems : status) =
 (*     pp_status context elems; *)
+(* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
+    auto_status := elems;
+    check_pause ();
+*)
+    let elems = filter_prune_hint elems in
     match elems with
+    | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
+        (match !hint with
+        | Some i when condition_for_hint i todo ->
+            aux tables maxm flags cache orlist
+        | _ ->
+          hint := None;
+          aux tables maxm flags cache elems)
     | [] ->
         (* complete failure *)
         Gaveup (tables, cache, maxm)
@@ -1244,12 +1318,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
@@ -1269,12 +1346,8 @@ let auto_main tables maxm context flags universe cache elems =
                 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
             | Notfound 
             | Failed_in _ when depth > 0 -> 
-                (match !hint with
-                | Some i when condition_for_hint i todo ->
-                    aux tables maxm flags cache orlist
-                | _ -> hint := None;
-                    (* more depth or is the first time we see the goal *)
-                    if prunable gty todo then
+                ( (* more depth or is the first time we see the goal *)
+                    if prunable m s gty todo then
                       (debug_print (lazy(
                          "FAIL: LOOP: one father is equal"));
                        aux tables maxm flags cache orlist)
@@ -1698,3 +1771,4 @@ let demodulate_tac ~dbd ~universe =
 let pp_proofterm = Equality.pp_proofterm;;
 
 let revision = "$Revision$";;
+let size_and_depth context metasenv t = 100, 100