X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=07d08345c3a7f0f10dc0469466bf0ff2e198baf4;hb=21ee96d317a4f0e7abfe76f697defe78acc10b94;hp=827c1dc46f06a67146cf6d3b1a053971776231bf;hpb=0232b651c37511743ce9e99d517a41adac3a7064;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 827c1dc46..07d08345c 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -14,8 +14,8 @@ open Printf
 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 = 
+(* 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 ()
@@ -25,7 +25,65 @@ open NTacStatus
 module Ast = CicNotationPt
 let app_counter = ref 0
 
-(* =================================== paramod =========================== *)
+(* ======================= utility functions ========================= *)
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+
+let get_sgoalty status g =
+ let _,_,metasenv,subst,_ = status#obj in
+ try
+   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
+   let ty = NCicUntrusted.apply_subst subst ctx ty in
+   let ctx = NCicUntrusted.apply_subst_context 
+     ~fix_projections:true subst ctx
+   in
+     NTacStatus.mk_cic_term ctx ty
+ with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
+;;
+
+let deps status g =
+  let gty = get_sgoalty status g in
+  metas_of_term status gty
+;;
+
+let menv_closure status gl = 
+  let rec closure acc = function
+    | [] -> acc
+    | x::l when IntSet.mem x acc -> closure acc l
+    | x::l -> closure (IntSet.add x acc) (deps status x @ l)
+  in closure IntSet.empty gl
+;;
+
+(* we call a "fact" an object whose hypothesis occur in the goal 
+   or in types of goal-variables *)
+let is_a_fact status ty =   
+  let status, ty, _ = saturate ~delta:max_int status ty in
+  let g_metas = metas_of_term status ty in
+  let clos = menv_closure status g_metas in
+  let _,_,metasenv,_,_ = status#obj in
+  let menv = 
+    List.fold_left
+      (fun acc (i,_) -> IntSet.add i acc)
+      IntSet.empty metasenv
+  in IntSet.equal clos menv;;
+
+let is_a_fact_obj s uri = 
+  let obj = NCicEnvironment.get_checked_obj uri in
+  match obj with
+    | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
+	is_a_fact s (mk_cic_term [] ty)
+(* aggiungere i costruttori *)
+    | _ -> false
+
+let current_goal status = 
+  let open_goals = head_goals status#stack in
+  assert (List.length open_goals  = 1);
+  let open_goal = List.hd open_goals in
+  let gty = get_goalty status open_goal in
+  let ctx = ctx_of gty in
+    open_goal, ctx, gty
+
+
+(* =============================== paramod =========================== *)
 let auto_paramod ~params:(l,_) status goal =
   let gty = get_goalty status goal in
   let n,h,metasenv,subst,o = status#obj in
@@ -44,7 +102,7 @@ let auto_paramod ~params:(l,_) status goal =
     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
   with
   | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
+  | (pt, _, metasenv, subst)::_ -> 
       let status = status#set_obj (n,h,metasenv,subst,o) in
       instantiate status goal (mk_cic_term (ctx_of gty) pt)
 ;;
@@ -53,54 +111,87 @@ let auto_paramod_tac ~params status =
   NTactics.distribute_tac (auto_paramod ~params) status
 ;;
 
-let fast_eq_check ~params status goal =
-  let gty = get_goalty status goal in
+let fast_eq_check_all status eq_cache goal =
   let n,h,metasenv,subst,o = status#obj in
-  let eq_cache = status#eq_cache in
-  let status,t = term_of_cic_term status gty (ctx_of gty) in 
-  match
-    NCicParamod.fast_eq_check status metasenv subst (ctx_of gty) 
-      eq_cache (NCic.Rel ~-1,t) 
-  with
-  | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
+  let gname, ctx, gty = List.assoc goal metasenv in
+  let gty = NCicUntrusted.apply_subst subst ctx gty in
+  let build_status (pt, _, metasenv, subst) =
+    (* let stamp = Unix.gettimeofday () in *)
+    let metasenv, subst, pt, pty = 
+      NCicRefiner.typeof 
+       	(status#set_coerc_db NCicCoercion.empty_db) 
+	metasenv subst ctx pt (Some gty)
+    in
+(* print (lazy (Printf.sprintf "Refined in %fs"
+		     (Unix.gettimeofday() -. stamp))); *)
       let status = status#set_obj (n,h,metasenv,subst,o) in
-      instantiate status goal (mk_cic_term (ctx_of gty) pt)
+      let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
+      let subst = (goal,(gname,ctx,pt,pty)) :: subst in
+	status#set_obj (n,h,metasenv,subst,o)
+  in
+    List.map build_status
+      (NCicParamod.fast_eq_check status metasenv subst ctx 
+	 eq_cache (NCic.Rel ~-1,gty))
 ;;
 
-let fast_eq_check_tac  ~params = 
-  NTactics.distribute_tac (fast_eq_check ~params)
+let fast_eq_check eq_cache status goal =
+  match fast_eq_check_all status eq_cache goal with
+  | [] -> raise (Error (lazy "no proof found",None))
+  | s::_ -> s
 ;;
 
-(*************** subsumption ****************)
-module IntSet = Set.Make(struct type t = int let compare = compare end)
-(* exceptions *)
+let dist_fast_eq_check eq_cache s = 
+  NTactics.distribute_tac (fast_eq_check eq_cache) s
+;;
 
-let get_sgoalty status g =
- let _,_,metasenv,subst,_ = status#obj in
- try
-   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
-   let ty = NCicUntrusted.apply_subst subst ctx ty in
-   let ctx = NCicUntrusted.apply_subst_context 
-     ~fix_projections:true subst ctx
-   in
-     NTacStatus.mk_cic_term ctx ty
- with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
+let auto_eq_check eq_cache status =
+  try 
+    let s = dist_fast_eq_check eq_cache status in
+      [s]
+  with
+    | Error _ -> []
 ;;
 
-let deps status g =
-  let gty = get_sgoalty status g in
-  metas_of_term status gty
+(* warning: ctx is supposed to be already instantiated w.r.t subst *)
+let index_local_equations eq_cache status =
+  let open_goals = head_goals status#stack in
+  let open_goal = List.hd open_goals in
+  let ngty = get_goalty status open_goal in
+  let ctx = ctx_of ngty in
+  let c = ref 0 in
+  List.fold_left 
+    (fun eq_cache _ ->
+       c:= !c+1;
+       let t = NCic.Rel !c in
+	 try
+	   let ty = NCicTypeChecker.typeof [] [] ctx t in
+             debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+	     NCicParamod.forward_infer_step eq_cache t ty
+	 with 
+	   | NCicTypeChecker.TypeCheckerFailure _
+	   | NCicTypeChecker.AssertFailure _ -> eq_cache) 
+    eq_cache ctx
 ;;
 
-let menv_closure status gl = 
-  let rec closure acc = function
-    | [] -> acc
-    | x::l when IntSet.mem x acc -> closure acc l
-    | x::l -> closure (IntSet.add x acc) (deps status x @ l)
-  in closure IntSet.empty gl
+let fast_eq_check_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  dist_fast_eq_check unit_eq s
 ;;
 
+(*
+let fast_eq_check_tac_all  ~params eq_cache status = 
+  let g,_,_ = current_goal status in
+  let allstates = fast_eq_check_all status eq_cache g in
+  let pseudo_low_tac s _ _ = s in
+  let pseudo_low_tactics = 
+    List.map pseudo_low_tac allstates 
+  in
+    List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
+;;
+*)
+
+(*************** subsumption ****************)
+
 let close_wrt_context =
   List.fold_left 
     (fun ty ctx_entry -> 
@@ -1120,7 +1211,50 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
 ;;
 *)
 
+(****************** smart application ********************)
+
+
+let smart_apply t unit_eq status g = 
+  let n,h,metasenv,subst,o = status#obj in
+  let gname, ctx, gty = List.assoc g metasenv in
+  (* let ggty = mk_cic_term context gty in *)
+  let status, t = disambiguate status ctx t None in
+  let status,t = term_of_cic_term status t ctx in
+  let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+  let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in
+  let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
+  let status = status#set_obj (n,h,metasenv,subst,o) in
+  let pterm = if args=[] then t else NCic.Appl(t::args) in
+  let eq_coerc =       
+    let uri = 
+      NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
+    let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
+      NCic.Const ref
+  in
+  let smart = 
+    NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
+  let smart = mk_cic_term ctx smart in 
+    try
+      let status = instantiate status g smart in
+      let _,_,metasenv,subst,_ = status#obj in
+      let _,ctx,jty = List.assoc j metasenv in
+      let jty = NCicUntrusted.apply_subst subst ctx jty in
+        debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
+	fast_eq_check unit_eq status j
+    with
+      | Error _ as e -> debug_print (lazy "error"); raise e
+
+let smart_apply_tac t s =
+  let unit_eq = index_local_equations s#eq_cache s in   
+  NTactics.distribute_tac (smart_apply t unit_eq) s
+
+let smart_apply_auto t eq_cache =
+  NTactics.distribute_tac (smart_apply t eq_cache)
+
+
 (****************** types **************)
+
+
 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
 
 let keys_of_term status t =
@@ -1223,6 +1357,12 @@ type flags = {
         timeout  : float;
 }
 
+type cache =
+    {facts : th_cache; (* positive results *)
+     under_inspection : th_cache; (* to prune looping *)
+     unit_eq : NCicParamod.state
+    }
+
 type sort = T | P
 type goal = int * sort (* goal, depth, sort *)
 type fail = goal * cic_term
@@ -1230,7 +1370,7 @@ type candidate = int * Ast.term (* unique candidate number, candidate *)
 
 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
                                 atoms of the input goals *)
-exception Proved of #NTacStatus.tac_status
+exception Proved of NTacStatus.tac_status
 
 (* let close_failures _ c = c;; *)
 (* let prunable _ _ _ = false;; *)
@@ -1238,28 +1378,36 @@ exception Proved of #NTacStatus.tac_status
 (* let put_in_subst s _ _ _  = s;; *)
 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
 (* let cache_add_underinspection c _ _ = c;; *)
-let equational_case _ _ _ _ _ _ = [];;
+
+let init_cache ?(facts=[]) ?(under_inspection=[]) 
+    ?(unit_eq=NCicParamod.empty_state) _ = 
+    {facts = facts;
+     under_inspection = under_inspection;
+     unit_eq = unit_eq
+    }
+
 let only _ _ _ = true;; 
 
 let candidate_no = ref 0;;
 
-let sort_new_elems l = 
-  List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
-;;
+let openg_no status = List.length (head_goals status#stack)
 
-let try_candidate flags depth status t =
+let sort_new_elems l =
+  List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
+
+let try_candidate flags depth status eq_cache t =
  try
    debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
-   let status = NTactics.apply_tac ("",0,t) status in
-   let open_goals = head_goals status#stack in
-   debug_print ~depth
-     (lazy ("success: "^String.concat " "(List.map string_of_int open_goals)));
-   if List.length open_goals > flags.maxwidth || 
-      (depth = flags.maxdepth && open_goals <> []) then
+  let status = 
+    smart_apply_auto ("",0,t) eq_cache status in 
+ (* let status = NTactics.apply_tac ("",0,t) status in *)
+   let og_no = openg_no status in 
+   if og_no > flags.maxwidth || 
+      (depth = flags.maxdepth && og_no <> 0) then
       (debug_print ~depth (lazy "pruned immediately"); None)
    else
      (incr candidate_no;
-      Some ((!candidate_no,t),status,open_goals))
+      Some ((!candidate_no,t),status))
  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
 ;;
 
@@ -1281,8 +1429,8 @@ let get_candidates status cache signature gty =
   List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
 ;;
 
-let applicative_case depth signature status flags gty cache =
-  let tcache,_ = cache in
+let applicative_case depth signature status flags gty (cache:cache) =
+  let tcache = cache.facts in
   app_counter:= !app_counter+1; 
   let candidates = get_candidates status tcache signature gty in
   debug_print ~depth
@@ -1290,7 +1438,7 @@ let applicative_case depth signature status flags gty cache =
   let elems = 
     List.fold_left 
       (fun elems cand ->
-        match try_candidate flags depth status cand with
+        match try_candidate flags depth status cache.unit_eq cand with
         | None -> elems
         | Some x -> x::elems)
       [] candidates
@@ -1302,7 +1450,7 @@ exception Found
 ;;
 
 (* gty is supposed to be meta-closed *)
-let is_subsumed depth status gty (_,cache) =
+let is_subsumed depth status gty cache =
   if cache=[] then false else (
   debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); 
   let n,h,metasenv,subst,obj = status#obj in
@@ -1343,98 +1491,51 @@ let is_subsumed depth status gty (_,cache) =
     with Found -> debug_print ~depth (lazy "success");true)
 ;;
 
-
-let equational_and_applicative_case
-  signature flags status g depth gty cache 
-=
- let elems = 
-  if false (*is_equational_case gty flags*) then
-    let elems =
-      equational_case
-        signature status flags g gty cache 
-    in
-    let more_elems =
-        applicative_case depth
-          signature status flags gty cache 
-    in
-      elems@more_elems
-  else
-    let elems =
-      (*match LibraryObjects.eq_URI () with
-      | Some _ ->
-         smart_applicative_case dbd tables depth s fake_proof goalno 
-           gty m context signature universe cache flags
-      | None -> *)
-         applicative_case depth
-          signature status flags gty cache 
-    in
-      elems
- in
- let elems = 
-   List.map (fun c,s,gl -> 
-       c,1,1,s,List.map (fun i -> 
-                      let sort = 
-			let gty = get_goalty s i in
-                        let _, sort = typeof s (ctx_of gty) gty in
-                          match term_of_cic_term s sort (ctx_of sort) with
-                            | _, NCic.Sort NCic.Prop -> P
-                            | _ -> T
-                      in
-			i,sort) gl) elems 
- in
- (* let elems = sort_new_elems elems in *)
- elems, cache
-;;
-
-(* warning: ctx is supposed to be already instantiated w.r.t subst *)
-let index_local_equations eq_cache ctx =
-  let c = ref 0 in
-  List.fold_left 
-    (fun cache _ ->
-       c:= !c+1;
-       let t = NCic.Rel 1 in
-	 try
-	   let ty = NCicTypeChecker.typeof [] [] ctx t in
-	     NCicParamod.forward_infer_step eq_cache t ty
-	 with 
-	   | NCicTypeChecker.TypeCheckerFailure _
-	   | NCicTypeChecker.AssertFailure _ -> eq_cache) 
-    eq_cache ctx
-;;
-
 let rec guess_name name ctx = 
   if name = "_" then guess_name "auto" ctx else
   if not (List.mem_assoc name ctx) then name else
   guess_name (name^"'") ctx
 ;;
 
-let intro ~depth status (tcache,fcache) name =
+let is_prod status = 
+  let _, ctx, gty = current_goal status in
+  let _, raw_gty = term_of_cic_term status gty ctx in
+  match raw_gty with
+    | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
+    | _ -> None
+
+let intro ~depth status facts name =
   let status = NTactics.intro_tac name status in
-  let open_goals = head_goals status#stack in
-  assert (List.length open_goals  = 1);
-  let open_goal = List.hd open_goals in
-  let ngty = get_goalty status open_goal in
-  let ctx = ctx_of ngty in
+  let _, ctx, ngty = current_goal status in
   let t = mk_cic_term ctx (NCic.Rel 1) in
   let status, keys = keys_of_term status t in
-  let tcache = List.fold_left (add_to_th t) tcache keys in
-    debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
+  let facts = List.fold_left (add_to_th t) facts keys in
+    debug_print ~depth (lazy ("intro: "^ name));
   (* unprovability is not stable w.r.t introduction *)
-  status, (tcache,[])
+  status, facts
 ;;
 
-let rec intros ~depth status cache =
-  let open_goals = head_goals status#stack in
-  assert (List.length open_goals  = 1);
-  let open_goal = List.hd open_goals in
-  let gty = get_goalty status open_goal in
-  let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in
-  match raw_gty with
-    | NCic.Prod (name,_,_) ->
-	let status,cache =
-	  intro ~depth status cache (guess_name name (ctx_of gty))
-	in intros ~depth status cache 
-    | _ -> status, cache, open_goal
+let rec intros_facts ~depth status facts =
+  match is_prod status with
+    | Some(name) ->
+	let status,facts =
+	  intro ~depth status facts name
+	in intros_facts ~depth status facts 
+    | _ -> status, facts
+;; 
+
+let rec intros ~depth status (cache:cache) =
+    match is_prod status with
+      | Some _ ->
+	  let status,facts =
+	    intros_facts ~depth status cache.facts 
+	  in 
+	    (* we reindex the equation from scratch *)
+	  let unit_eq = 
+	    index_local_equations status#eq_cache status in
+	    (* under_inspection must be set to empty *)
+	  status, init_cache ~facts ~unit_eq () 
+      | _ -> status, cache
 ;;
 
 let reduce ~depth status g = 
@@ -1451,16 +1552,24 @@ let reduce ~depth status g =
     in
     let status = status#set_obj (n,h,metasenv,subst,o) in
     incr candidate_no;
-    [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]])
+    [(!candidate_no,Ast.Ident("__whd",None)),status])
 ;;
 
 let do_something signature flags status g depth gty cache =
+  (* whd *)
   let l = reduce ~depth status g in
-  let l1,cache =
-      (equational_and_applicative_case 
-	 signature flags status g depth gty cache)
+  (* backward aplications *)
+  let l1 = applicative_case depth signature status flags gty cache in
+  (* fast paramodulation *) 
+  let l2 = 
+    List.map 
+      (fun s ->
+	 incr candidate_no;
+	 ((!candidate_no,Ast.Ident("__paramod",None)),s))
+      (auto_eq_check cache.unit_eq status)
   in
-    sort_new_elems (l@l1), cache
+  (* states in l2 have have an set of subgoals: no point to sort them *)
+    l2 @ (sort_new_elems (l@l1)), cache
 ;;
 
 let pp_goal = function
@@ -1578,43 +1687,46 @@ 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 depth status: unit =
+auto_main flags signature (cache:cache) depth status: unit =
   debug_print ~depth (lazy "entering auto main");
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = sort_tac (clean_up_tac status) in
   let goals = head_goals status#stack in
   match goals with
     | [] -> raise (Proved status)
-    | g::tlg ->
+    | orig::_ ->
+        let branch = List.length(goals)>1 in
 	if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
         else
 	let status = 
-	  if tlg=[] then status 
-	  else NTactics.branch_tac status in
-        let status, cache, g = intros ~depth status cache in
-        let gty = get_goalty status g in
+	  if branch then NTactics.branch_tac status 
+	  else status in
+        let status, cache = intros ~depth status cache in
+        let g,gctx, gty = current_goal status in
 	let ctx,ty = close status g in
 	let closegty = mk_cic_term ctx ty in
-        let status, gty = apply_subst status (ctx_of gty) gty in
+        let status, gty = apply_subst status gctx gty in
 	debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); 
-        if is_subsumed depth status closegty cache then 
+        if is_subsumed depth status closegty cache.under_inspection then 
 	  (debug_print (lazy "SUBSUMED");
 	   raise (Gaveup IntSet.add g IntSet.empty))
 	else 
 	let alternatives, cache = 
           do_something signature flags status g depth gty cache in
-	let loop_cache =         
-	  let tcache,fcache = cache in
-	    tcache,add_to_th closegty fcache closegty in
+	let loop_cache =
+	  let under_inspection = 
+	    add_to_th closegty cache.under_inspection closegty in
+          {cache with under_inspection = under_inspection} in
 	let unsat =
 	  List.fold_left
             (* the underscore information does not need to be returned
                by do_something *)
-	    (fun unsat ((_,t),_,_,status,_) ->
+	    (fun unsat ((_,t),status) ->
 	       let depth',looping_cache = 
-		 if t=(Ast.Implicit `JustOne) then depth,cache 
+		 if t=Ast.Ident("__whd",None) then depth,cache 
 		 else depth+1, loop_cache in
                debug_print (~depth:depth') 
 		 (lazy ("Case: " ^ CicNotationPp.pp_term t));
@@ -1623,20 +1735,20 @@ auto_main flags signature cache depth status: unit =
                with 
 		 | Proved status ->
                      debug_print (~depth:depth') (lazy "proved");
-		     if tlg=[] then raise (Proved status) 
-		     else 
+		     if branch then 
 		       let status = NTactics.merge_tac status
-		     in
-		     ( (* old cache, here *)
-		       try auto_clusters flags signature cache 
-			depth status; assert false
-		      with Gaveup f ->
-			debug_print ~depth 
-			  (lazy ("Unsat1 at depth " ^ (string_of_int depth)
+		       in
+			 (* old cache, here *)
+			 try auto_clusters flags signature cache 
+			   depth status; assert false
+			 with Gaveup f ->
+			   debug_print ~depth 
+			     (lazy ("Unsat1 at depth " ^ (string_of_int depth)
 				   ^ ": " ^ 
 				   (pp_goals status (IntSet.elements f))));
                         (* TODO: cache failures *)
-			IntSet.union f unsat)
+			   IntSet.union f unsat
+		     else raise (Proved status) 
 		 | Gaveup f -> 
 		     debug_print (~depth:depth')
 		       (lazy ("Unsat2 at depth " ^ (string_of_int depth')
@@ -1646,7 +1758,7 @@ auto_main flags signature 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 = 
@@ -1655,9 +1767,13 @@ let int name l def =
 ;;
 
 let auto_tac ~params:(_univ,flags) status =
+  let oldstatus = status in
+  let status = (status:> NTacStatus.tac_status) in
   let goals = head_goals status#stack in
-  let status, cache = mk_th_cache status goals in
-(*   pp_th status cache; *)
+  let status, facts = mk_th_cache status goals in
+  let unit_eq = index_local_equations status#eq_cache status in 
+  let cache = init_cache ~facts ~unit_eq  () in 
+(*   pp_th status facts; *)
 (*
   NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> 
     debug_print (lazy(
@@ -1693,7 +1809,7 @@ let auto_tac ~params:(_univ,flags) status =
       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
       let flags = { flags with maxdepth = x } 
       in 
-	try auto_clusters flags signature (cache,[]) 0 status;status 
+	try auto_clusters flags signature cache 0 status;assert false
 	with
 	  | Gaveup _ -> up_to (x+1) y
 	  | Proved s -> 
@@ -1703,7 +1819,8 @@ let auto_tac ~params:(_univ,flags) status =
 		  | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
 		  | _ -> assert false
               in
-		s#set_stack stack
+	      let s = s#set_stack stack in
+		oldstatus#set_status s 
   in
   let s = up_to depth depth in
     print(lazy