new internal flags for auto:

- skip_context
- skip_trie_filtering

together they allow a decent semantics for
by H, H1, H2 we proved foo.

since only H, H1 and H2 are used (no other context entry, not library stuff)
and full blown unification is used (no terms are ignored, between the one
specified, because they fail a trie search)

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index d191c436a1bc6059bac2faee13221de29dee8303..07331220cbdcadee037d4a1459c80eb759970e0b 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -30,6 +30,7 @@ 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 +163,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 
@@ -203,7 +205,7 @@ 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
@@ -524,6 +526,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 +556,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 =
@@ -1251,9 +1257,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 ->
@@ -1286,14 +1292,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  
 ;;
@@ -1605,11 +1611,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

diff --git a/helm/software/components/tactics/autoTypes.ml b/helm/software/components/tactics/autoTypes.ml
index 874a20dccf4b366bda48cae857dbf6744a2702f6..9bced7618e08ad290726b01089e09a2a1a28b721 100644 (file)
--- a/helm/software/components/tactics/autoTypes.ml
+++ b/helm/software/components/tactics/autoTypes.ml
@@ -35,6 +35,8 @@ type flags = {
   close_more : bool; 
   dont_cache_failures: bool;
   do_types: bool;
+  skip_trie_filtering: bool;
+  skip_context: bool;
 }
 
 let default_flags _ =
@@ -49,6 +51,8 @@ let default_flags _ =
    close_more=false; 
    dont_cache_failures=false;
    do_types=false;
+   skip_trie_filtering=false;
+   skip_context=false;
 }
 ;;
 

diff --git a/helm/software/components/tactics/autoTypes.mli b/helm/software/components/tactics/autoTypes.mli
index ab05564ff3c2099819feab9d3e971d6d5d41d8a9..745438462c7bad0effb096c8edae1f4f7639df78 100644 (file)
--- a/helm/software/components/tactics/autoTypes.mli
+++ b/helm/software/components/tactics/autoTypes.mli
@@ -35,6 +35,8 @@ type flags = {
   close_more : bool;
   dont_cache_failures: bool;
   do_types: bool;
+  skip_trie_filtering: bool;
+  skip_context : bool;
 }
 
 val default_flags : unit -> flags

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 15fdbf7254c02ebecfc1744d3e26479d5207806a..be4724b55509124678137083d36c040e519d8dab 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -27,7 +27,9 @@ type just = [ `Term of Cic.term | `Auto of Auto.auto_params ]
 
 let mk_just ~dbd ~universe =
  function
-    `Auto params -> Tactics.auto ~dbd ~params ~universe
+    `Auto (l,params) -> 
+       Tactics.auto ~dbd 
+       ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~universe
   | `Term t -> Tactics.apply t
 ;;