Removed debug printings.

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index c9f641cb3ae72ef01a32c204311698dbdfa31208..ce0a1b00ee2c2e45b20ef04ea6473c96a156dae1 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -55,17 +55,21 @@ let menv_closure status 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:0 status ty in
-  debug_print (lazy (ppterm status ty));
+let is_a_fact status ty =  
+  let status, ty, metas = saturate ~delta:0 status ty in
+  debug_print (lazy ("saturated ty :" ^ (ppterm status ty)));
   let g_metas = metas_of_term status ty in
   let clos = menv_closure status g_metas in
-  let _,_,metasenv,_,_ = status#obj 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;;
+      (fun acc m ->
+         let _, m = term_of_cic_term status m (ctx_of m) in
+        match m with 
+        | NCic.Meta(i,_) -> IntSet.add i acc
+        | _ -> assert false)
+      IntSet.empty metas
+  in IntSet.subset menv clos;;
 
 let is_a_fact_obj s uri = 
   let obj = NCicEnvironment.get_checked_obj uri in
@@ -75,6 +79,14 @@ let is_a_fact_obj s uri =
 (* aggiungere i costruttori *)
     | _ -> false
 
+let is_a_fact_ast status subst metasenv ctx cand = 
+ debug_print ~depth:0 
+   (lazy ("------- checking " ^ CicNotationPp.pp_term cand)); 
+ let status, t = disambiguate status ctx ("",0,cand) None in
+ let status,t = term_of_cic_term status t ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+   is_a_fact status (mk_cic_term ctx ty)
+
 let current_goal status = 
   let open_goals = head_goals status#stack in
   assert (List.length open_goals  = 1);
@@ -112,7 +124,7 @@ let solve fast status eq_cache goal =
                     (status#set_coerc_db NCicCoercion.empty_db) 
             metasenv subst ctx pt (Some gty) *)
        in 
-         print (lazy (Printf.sprintf "Refined in %fs"
+         debug_print (lazy (Printf.sprintf "Refined in %fs"
                     (Unix.gettimeofday() -. stamp))); 
          let status = status#set_obj (n,h,metasenv,subst,o) in
          let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
@@ -163,8 +175,12 @@ let index_local_equations eq_cache status =
        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
+           if is_a_fact status (mk_cic_term ctx ty) then
+             (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+             NCicParamod.forward_infer_step eq_cache t ty)
+          else 
+            (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
+             eq_cache)
         with 
           | NCicTypeChecker.TypeCheckerFailure _
           | NCicTypeChecker.AssertFailure _ -> eq_cache) 
@@ -1418,7 +1434,7 @@ let sort_new_elems l =
 
 let try_candidate ?(smart=0) flags depth status eq_cache t =
  try
-   print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
+   debug_print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
   let status = 
     if smart= 0 then NTactics.apply_tac ("",0,t) status 
     else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status 
@@ -1429,7 +1445,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache t =
   let og_no = openg_no status in 
     if (* og_no > flags.maxwidth || *)
       ((depth + 1) = flags.maxdepth && og_no <> 0) then
-       (print ~depth (lazy "pruned immediately"); None)
+       (debug_print ~depth (lazy "pruned immediately"); None)
    else
      (incr candidate_no;
       Some ((!candidate_no,t),status))
@@ -1498,12 +1514,17 @@ let applicative_case depth signature status flags gty (cache:cache) =
   let sm = 0 in 
   let smart_candidates = [] in *)
   let sm = if is_eq then 0 else 2 in
-  let only_one = flags.last && (depth + 1 = flags.maxdepth) in 
-  print (lazy ("only_one: " ^ (string_of_bool only_one)));
+  let maxd = ((depth + 1) = flags.maxdepth) in 
+  let only_one = flags.last && maxd in
+  debug_print (lazy ("only_one: " ^ (string_of_bool only_one))); 
+  debug_print (lazy ("maxd: " ^ (string_of_bool maxd)));
   let elems =  
     List.fold_left 
       (fun elems cand ->
         if (only_one && (elems <> [])) then elems 
+        else 
+          if (maxd && not(is_a_fact_ast status subst metasenv context cand)) 
+          then (debug_print (lazy "pruned: not a fact"); elems)
         else
           match try_candidate (~smart:sm) 
             flags depth status cache.unit_eq cand with
@@ -1517,6 +1538,9 @@ let applicative_case depth signature status flags gty (cache:cache) =
       List.fold_left 
        (fun elems cand ->
         if (only_one && (elems <> [])) then elems 
+        else 
+          if (maxd && not(is_a_fact_ast status subst metasenv context cand)) 
+          then (debug_print (lazy "pruned: not a fact"); elems)
         else
            match try_candidate (~smart:1) 
             flags depth status cache.unit_eq cand with
@@ -1738,7 +1762,6 @@ let focus_tac focus status =
 let rec auto_clusters ?(top=false)  
     flags signature cache depth status : unit =
   debug_print ~depth (lazy "entering auto clusters");
-  print (lazy ("auto cluster: " ^ (string_of_bool flags.last)));
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = clean_up_tac status in
   let goals = head_goals status#stack in
@@ -1747,7 +1770,7 @@ let rec auto_clusters ?(top=false)
   else if List.length goals < 2 then 
     auto_main flags signature cache depth status 
   else
-    print ~depth (lazy ("goals = " ^ 
+    debug_print ~depth (lazy ("goals = " ^ 
       String.concat "," (List.map string_of_int goals)));
     let classes = HExtlib.clusters (deps status) goals in
     let classes = if top then List.rev classes else classes in
@@ -1779,7 +1802,6 @@ and
    of the initial head goals in the stack *)
 
 auto_main flags signature (cache:cache) depth status: unit =
-  print (lazy ("auto enter: " ^ (string_of_bool flags.last)));
   debug_print ~depth (lazy "entering auto main");
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = sort_tac (clean_up_tac status) in
@@ -1789,7 +1811,7 @@ auto_main flags signature (cache:cache) depth status: unit =
     | orig::_ ->
        let ng = List.length goals in 
         if ng > flags.maxwidth then 
-         (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
+         (debug_print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
         else let branch = ng>1 in
        if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
         else
@@ -1829,7 +1851,8 @@ auto_main flags signature (cache:cache) depth status: unit =
                 (* sistemare *)
               let flags' = 
                 {flags' with last = flags'.last && (not branch)} in 
-               print (lazy ("auto last: " ^ (string_of_bool flags'.last)));
+               debug_print 
+                (lazy ("auto last: " ^ (string_of_bool flags'.last)));
               try auto_clusters flags' signature loop_cache
                 depth' status; unsat
                with 
@@ -1905,7 +1928,7 @@ let auto_tac ~params:(_univ,flags) status =
     if x > y then
       (print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
-       print(lazy
+       debug_print(lazy
         ("Applicative nodes:"^string_of_int !app_counter)); 
        raise (Error (lazy "auto gave up", None)))
     else
@@ -1916,7 +1939,7 @@ let auto_tac ~params:(_univ,flags) status =
        with
          | Gaveup _ -> up_to (x+1) y
          | Proved s -> 
-              print (lazy ("proved at depth " ^ string_of_int x));
+              debug_print (lazy ("proved at depth " ^ string_of_int x));
               let stack = 
                match s#stack with
                  | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
@@ -1926,9 +1949,9 @@ let auto_tac ~params:(_univ,flags) status =
                oldstatus#set_status s 
   in
   let s = up_to depth depth in
-    print(lazy
+    debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
-    print(lazy
+    debug_print(lazy
         ("Applicative nodes:"^string_of_int !app_counter));
     s
 ;;