Minor bag fixed, relative to failures.

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 515622d4e02b054ae743c28ba81e27960fc7cf2e..a2a76d4f51075676f331782b79eaae0344b3d642 100644 (file)
--- 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 =