From f2771b346a41445df23adb6acccd7ee6b1578666 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 10 Dec 2009 12:22:41 +0000
Subject: [PATCH] Minor bag fixed, relative to failures.

---
 helm/software/components/ng_tactics/nnAuto.ml | 22 +++++++++----------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 515622d4e..a2a76d4f5 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -11,12 +11,12 @@
 
 open Printf
 
-let debug = ref true
+let debug = ref false
 let debug_print ?(depth=0) s = 
   if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
-(* let print= debug_print *)
- let print ?(depth=0) s = 
-  prerr_endline (String.make depth '\t'^Lazy.force s) 
+let print= debug_print 
+(* let print ?(depth=0) s = 
+  prerr_endline (String.make depth '\t'^Lazy.force s) *)
 
 let debug_do f = if !debug then f () else ()
 
@@ -1430,7 +1430,7 @@ let index_local_equations eq_cache status =
        let t = NCic.Rel !c in
 	 try
 	   let ty = NCicTypeChecker.typeof [] [] ctx t in
-             prerr_endline ("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty));
+             debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
 	     NCicParamod.forward_infer_step eq_cache t ty
 	 with 
 	   | NCicTypeChecker.TypeCheckerFailure _
@@ -1474,7 +1474,6 @@ let rec intros_facts ~depth status facts =
 let rec intros ~depth status (cache:cache) =
     match is_prod status with
       | Some _ ->
-          prerr_endline "is prod";
 	  let status,facts =
 	    intros_facts ~depth status cache.facts 
 	  in 
@@ -1509,15 +1508,13 @@ let do_something signature flags status g depth gty cache =
   (* backward aplications *)
   let l1 = applicative_case depth signature status flags gty cache in
   (* fast paramodulation *) 
-  let l2 = [] in
-(*
+  let l2 = 
     List.map 
       (fun s ->
 	 incr candidate_no;
 	 ((!candidate_no,Ast.Ident("__paramod",None)),s))
       (auto_eq_check cache.unit_eq status)
   in
-*)
   (* states in l2 have have an set of subgoals: no point to sort them *)
     l2 @ (sort_new_elems (l@l1)), cache
 ;;
@@ -1637,7 +1634,8 @@ let rec auto_clusters
 
 and
 
-(* let rec auto_main flags signature cache status k depth = *)
+(* the goals returned upon failure are an unsatisfiable subset 
+   of the initial head goals in the stack *)
 
 auto_main flags signature (cache:cache) depth status: unit =
   debug_print ~depth (lazy "entering auto main");
@@ -1646,7 +1644,7 @@ auto_main flags signature (cache:cache) depth status: unit =
   let goals = head_goals status#stack in
   match goals with
     | [] -> raise (Proved status)
-    | _ ->
+    | orig::_ ->
         let branch = List.length(goals)>1 in
 	if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
         else
@@ -1707,7 +1705,7 @@ auto_main flags signature (cache:cache) depth status: unit =
 		     unsat)
 	    IntSet.empty alternatives
 	in
-	  raise (Gaveup IntSet.add g unsat)
+	  raise (Gaveup IntSet.add orig unsat)
 ;;
 		 
 let int name l def = 
-- 
2.39.2