Only modified for taking unfold into account.

Assertion made only in case of debug.

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 1e326df1086c25f7ce6f92640aff9d87b413dcc8..92d66ef726ab7d245f0072c9aec81f3f7e85ed1d 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -26,7 +26,9 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug_print s = prerr_endline (Lazy.force s);; 
+let debug = false;;
+let debug_print s = 
+  if debug then () else prerr_endline (Lazy.force s);;
 
 (* functions for retrieving theorems *)
 
@@ -108,7 +110,7 @@ let is_unit_equation context metasenv oldnewmeta term =
 ;;
 
 let get_candidates universe cache t =
-  let candidates = 
+  let candidates= 
     (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
   in 
   let debug_msg =
@@ -118,14 +120,27 @@ let get_candidates universe cache t =
   candidates
 ;;
 
-let only singature context t =
+let only signature context t =
   try
     let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
     let consts = MetadataConstraints.constants_of ty in
-      MetadataConstraints.UriManagerSet.subset consts singature 
+    let b = MetadataConstraints.UriManagerSet.subset consts signature in
+    if b then b 
+    else
+      try
+       let ty' = unfold context ty in
+       let consts' = MetadataConstraints.constants_of ty' in
+       MetadataConstraints.UriManagerSet.subset consts' signature 
+      with _-> false
   with _ -> false
 ;;
 
+let not_default_eq_term t =
+  try
+    let uri = CicUtil.uri_of_term t in
+      not (LibraryObjects.in_eq_URIs uri)
+  with Invalid_argument _ -> true
+
 let retrieve_equations signature universe cache context=
   match LibraryObjects.eq_URI() with
     | None -> [] 
@@ -134,7 +149,11 @@ let retrieve_equations signature universe cache context=
        let fake= Cic.Meta(-1,[]) in
        let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
        let candidates = get_candidates universe cache fake_eq in
-       List.filter (only signature context) candidates
+    (* defaults eq uris are built-in in auto *)
+        let candidates = List.filter not_default_eq_term candidates in
+       let candidates = List.filter (only signature context) candidates in
+       List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
+       candidates
 
 let build_equality bag head args proof newmetas maxmeta = 
   match head with
@@ -170,7 +189,7 @@ let empty_tables =
    Saturation.make_passive [],
    Equality.mk_equality_bag)
 
-let init_cache_and_tables dbd use_library universe (proof, goal) =
+let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
   (* the local cache in initially empty  *)
   let cache = AutoCache.cache_empty in
   let _, metasenv, _, _ = proof in
@@ -178,16 +197,17 @@ let init_cache_and_tables dbd use_library universe (proof, goal) =
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let ct = find_context_theorems context metasenv in
+  prerr_endline 
+    ("ho trovato nel contesto " ^ (string_of_int (List.length ct)));
   let lt = 
     if use_library then 
-      find_library_theorems dbd metasenv goal 
+       find_library_theorems dbd metasenv goal 
     else [] in
-   (* all equations are added to the cache *) 
   prerr_endline 
     ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
-  (* let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in *)
   let cache = cache_add_list cache context (ct@lt) in  
-  let equations = retrieve_equations signature universe cache context in
+  let equations = 
+    retrieve_equations signature universe cache context in
   prerr_endline 
     ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
   let eqs_and_types =
@@ -217,7 +237,10 @@ let init_cache_and_tables dbd use_library universe (proof, goal) =
   let no = List.length units in
   let active = Saturation.make_active [] in
   let active,passive,newmeta = 
-    Saturation.pump_actives context bag newmeta active passive (no+1) infinity
+    if paramod then active,passive,newmeta
+    else
+      Saturation.pump_actives 
+       context bag newmeta active passive (no+1) infinity
   in 
     (active,passive,bag),cache,newmeta
 
@@ -438,7 +461,7 @@ let new_metasenv_and_unify_and_t
  in
  match 
    let (active, passive,bag), cache, maxmeta =
-     init_cache_and_tables dbd flags.use_library universe (proof'''',newmeta)
+     init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta)
    in
      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive 
        max_int max_int flags.timeout
@@ -521,26 +544,35 @@ let is_in_prop context subst metasenv ty =
   let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
   fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
 ;;
+
 let assert_proof_is_valid proof metasenv context goalty =
-  let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
-  let b,_ = CicReduction.are_convertible context ty goalty u in
-  if not b then
+  if debug then
     begin
-      let names = 
-        List.map (function None -> None | Some (x,_) -> Some x) context 
-      in
-      prerr_endline ("PROOF:" ^ CicPp.pp proof names);
-      prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
-      prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
-      prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
-    end;
-  assert b
+      let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
+      let b,_ = CicReduction.are_convertible context ty goalty u in
+       if not b then
+         begin
+           let names = 
+              List.map (function None -> None | Some (x,_) -> Some x) context 
+           in
+             prerr_endline ("PROOF:" ^ CicPp.pp proof names);
+             prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
+             prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
+             prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
+         end;
+       assert b
+    end
+  else ()
 ;;
+
 let assert_subst_are_disjoint subst subst' =
-  assert(List.for_all
-    (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
-    subst)
+  if debug then
+    assert(List.for_all
+            (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
+            subst)
+  else ()
 ;;
+
 let sort_new_elems = 
   List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) 
 ;;
@@ -676,8 +708,6 @@ let try_candidate
     in
     debug_print (lazy ("   OK: " ^ ppterm cand));
     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
-    assert (maxmeta >= maxm);
-    (*FIXME:sicuro che posso @?*)
     assert_subst_are_disjoint subst subst';
     let subst = subst@subst' in
     let open_goals = order_new_goals metasenv subst open_goals ppterm in
@@ -769,7 +799,7 @@ let rec auto_main tables maxm context flags elems universe cache =
           else
           match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
           | Fail s, tables, cache, maxm' -> 
-              assert(maxm' >= maxm);let maxm = maxm' in
+              let maxm = maxm' in
               debug_print
                 (lazy 
                   (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
@@ -780,7 +810,7 @@ let rec auto_main tables maxm context flags elems universe cache =
               in
               aux flags tables maxm cache tl
           | Success (metasenv,subst,others), tables, cache, maxm' ->
-              assert(maxm' >= maxm);let maxm = maxm' in
+              let maxm = maxm' in
               (* others are alternatives in OR *)
               try
                 let goal = Cic.Meta(goalno,irl) in
@@ -823,7 +853,6 @@ let rec auto_main tables maxm context flags elems universe cache =
         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
         tables,cache,maxm(*FAILURE(depth)*)
     | Succeded t -> 
-        assert(List.for_all (fun (i,_) -> i <> goalno) subst);
         let entry = goalno, (cc, t,goalty) in
         assert_subst_are_disjoint subst [entry];
         let subst = entry :: subst in
@@ -840,7 +869,6 @@ let rec auto_main tables maxm context flags elems universe cache =
             let elems,tables,cache,maxm1, flags =
               equational_case tables maxm cache
                 depth fake_proof goalno goalty subst context flags in
-            assert(maxm1 >= maxm);
              let maxm = maxm1 in
            let more_elems, tables, cache, maxm1 =
              if flags.use_only_paramod then
@@ -849,7 +877,6 @@ let rec auto_main tables maxm context flags elems universe cache =
                applicative_case 
                  tables maxm depth subst fake_proof goalno 
                  goalty metasenv context universe cache in
-             assert(maxm1 >= maxm);
              let maxm = maxm1 in
              elems@more_elems, tables, cache, maxm, flags            
           else
@@ -1127,7 +1154,8 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
       (* just for testing *)
       let use_library = flags.use_library in
       let tables,cache,newmeta =
-       init_cache_and_tables dbd use_library universe (proof, goal) in
+       init_cache_and_tables dbd use_library flags.use_only_paramod 
+         universe (proof, goal) in
       let tables,cache,newmeta =
         if flags.close_more then
          close_more 
@@ -1169,7 +1197,7 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
   let initgoal = [], [], ty in
   let eq_uri = eq_of_goal ty in
   let (active,passive,bag), cache, maxm =
-     init_cache_and_tables dbd true Universe.empty (proof,goal) in
+     init_cache_and_tables dbd true true Universe.empty (proof,goal) in
   let equalities = (Saturation.list_of_passive passive) in
   (* we demodulate using both actives passives *)
   let table =