removed some printings

[helm.git] / helm / software / components / tactics / auto.ml

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index e8131d9802a6227426e5cc7b95316eeaf6c2a2ee..6b25982d3bb7377b8a0a5019172e5f3f482ce678 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1,4 +1,5 @@
 (* Copyright (C) 2002, HELM Team.
+
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -26,10 +27,11 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug = true;;
+let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
+
 let is_propositional context sort = 
   match CicReduction.whd context sort with
   | Cic.Sort Cic.Prop 
@@ -162,7 +164,8 @@ let is_unit_equation context metasenv oldnewmeta term =
     else None
 ;;
 
-let get_candidates universe cache t =
+let get_candidates skip_trie_filtering universe cache t =
+  let t = if skip_trie_filtering then Cic.Meta(0,[]) else t in
   let candidates= 
     (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
   in 
@@ -180,11 +183,17 @@ let only signature context metasenv t =
     in
     let consts = MetadataConstraints.constants_of ty in
     let b = MetadataConstraints.UriManagerSet.subset consts signature in
+(*     if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b)  *)
     if b then b 
     else
       let ty' = unfold context ty in
       let consts' = MetadataConstraints.constants_of ty' in
-      MetadataConstraints.UriManagerSet.subset consts' signature 
+      let b = MetadataConstraints.UriManagerSet.subset consts' signature  in
+(*
+       if not b then prerr_endline ("filtering " ^ (CicPp.ppterm t))
+       else prerr_endline ("keeping " ^ (CicPp.ppterm t)); 
+*)
+      b
   with 
   | CicTypeChecker.TypeCheckerFailure _ -> assert false
   | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
@@ -203,11 +212,13 @@ let retrieve_equations dont_filter signature universe cache context metasenv =
         let eq_uri = UriManager.strip_xpointer eq_uri in
         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
+        let candidates = get_candidates false universe cache fake_eq in
         if dont_filter then candidates
-        else 
-          let candidates = List.filter not_default_eq_term candidates in
-          List.filter (only signature context metasenv) candidates 
+        else let eq_uri = UriManager.uri_of_uriref eq_uri 0 None in
+          (* let candidates = List.filter not_default_eq_term candidates in *)
+          List.filter 
+           (only (MetadataConstraints.UriManagerSet.add eq_uri signature) 
+              context metasenv) candidates 
 
 let build_equality bag head args proof newmetas maxmeta = 
   match head with
@@ -273,7 +284,7 @@ let init_cache_and_tables
     (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
   let cache = cache_add_list cache context (ct@lt) in  
   let equations = 
-    retrieve_equations dont_filter signature universe cache context metasenv 
+    retrieve_equations dont_filter (* true *) signature universe cache context metasenv 
   in
   debug_print 
     (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
@@ -524,6 +535,8 @@ let flags_of_params params ?(for_applyS=false) () =
  let bool = bool params in
  let close_more = bool "close_more" false in
  let use_paramod = bool "use_paramod" true in
+ let skip_trie_filtering = bool "skip_trie_filtering" false in
+ let skip_context = bool "skip_context" false in
  let use_only_paramod =
   if for_applyS then true else bool "paramodulation" false in
  let use_library = bool "library"  
@@ -552,6 +565,8 @@ let flags_of_params params ?(for_applyS=false) () =
     AutoTypes.dont_cache_failures = false;
     AutoTypes.maxgoalsizefactor = gsize;
     AutoTypes.do_types = do_type;
+    AutoTypes.skip_trie_filtering = skip_trie_filtering;
+    AutoTypes.skip_context = skip_context;
   }
 
 let universe_of_params metasenv context universe tl =
@@ -613,15 +628,12 @@ let new_metasenv_and_unify_and_t
      init_cache_and_tables ~dbd flags.use_library true true false universe
      (proof'''',newmeta)
    in
-     prerr_endline "chiamo given clause";
      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive 
        max_int max_int flags.timeout
  with
  | None, _,_,_ -> 
      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
  | Some (_,proof''''',_), active,passive,_  -> 
-     prerr_endline "torno";
-
      proof''''',
      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
        ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m),  active, passive
@@ -1254,9 +1266,9 @@ let sort_new_elems =
 
 let applicative_case 
   tables maxm depth subst fake_proof goalno goalty metasenv context universe
-  cache
+  cache flags
 = 
-  let candidates = get_candidates universe cache goalty in
+  let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in
   let tables, elems, maxm = 
     List.fold_left 
       (fun (tables,elems,maxm) cand ->
@@ -1289,14 +1301,14 @@ let equational_and_applicative_case
       else
         applicative_case 
           tables maxm depth s fake_proof goalno 
-            gty m context universe cache 
+            gty m context universe cache flags
     in
     let maxm = maxm1 in
       elems@more_elems, tables, cache, maxm, flags            
   else
     let elems, tables, cache, maxm =
       applicative_case tables maxm depth s fake_proof goalno 
-        gty m context universe cache 
+        gty m context universe cache flags
     in
       elems, tables, cache, maxm, flags  
 ;;
@@ -1608,11 +1620,11 @@ let applyS_tac ~dbd ~term ~params ~universe =
 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
   let _,metasenv,_subst,_,_, _ = proof in
   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
-  let universe = universe_of_params metasenv context universe univ in
   let flags = flags_of_params params () in
+  let universe = universe_of_params metasenv context universe univ in
   let use_library = flags.use_library in
   let tables,cache,newmeta =
-    init_cache_and_tables ~dbd use_library flags.use_only_paramod true 
+    init_cache_and_tables ~dbd use_library flags.use_only_paramod (not flags.skip_context)
       false universe (proof, goal) in
   let tables,cache,newmeta =
     if flags.close_more then
@@ -1741,7 +1753,7 @@ let is_subsumed univ context ty =
               try 
                  let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
                 let metasenv = [(0,context,ty)] in
-                let fake_proof = None,metasenv,[] ,Cic.Meta(0,mk_irl context),ty,[] in
+                let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
                 let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
                   (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
                 in