From 87fdda71e8e0dcf886852f70be9a4b3d627b8e9c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Nov 2008 21:29:05 +0000 Subject: [PATCH] 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) --- helm/software/components/tactics/auto.ml | 22 ++++++++++++------- helm/software/components/tactics/autoTypes.ml | 4 ++++ .../software/components/tactics/autoTypes.mli | 2 ++ .../components/tactics/declarative.ml | 4 +++- 4 files changed, 23 insertions(+), 9 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index d191c436a..07331220c 100644 --- 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 874a20dcc..9bced7618 100644 --- 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 ab05564ff..745438462 100644 --- 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 15fdbf725..be4724b55 100644 --- 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 ;; -- 2.39.2