- 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)
let debug_print s =
if debug then prerr_endline (Lazy.force s);;
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
let is_propositional context sort =
match CicReduction.whd context sort with
| Cic.Sort Cic.Prop
-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
let candidates=
(Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
in
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 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
if dont_filter then candidates
else
let candidates = List.filter not_default_eq_term candidates in
let bool = bool params in
let close_more = bool "close_more" false in
let use_paramod = bool "use_paramod" true in
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"
let use_only_paramod =
if for_applyS then true else bool "paramodulation" false in
let use_library = bool "library"
AutoTypes.dont_cache_failures = false;
AutoTypes.maxgoalsizefactor = gsize;
AutoTypes.do_types = do_type;
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 =
}
let universe_of_params metasenv context universe tl =
let applicative_case
tables maxm depth subst fake_proof goalno goalty metasenv context universe
let applicative_case
tables maxm depth subst fake_proof goalno goalty metasenv context universe
- 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 ->
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
else
applicative_case
tables maxm depth s fake_proof goalno
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
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
;;
in
elems, tables, cache, maxm, flags
;;
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 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 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 =
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
false universe (proof, goal) in
let tables,cache,newmeta =
if flags.close_more then
close_more : bool;
dont_cache_failures: bool;
do_types: bool;
close_more : bool;
dont_cache_failures: bool;
do_types: bool;
+ skip_trie_filtering: bool;
+ skip_context: bool;
close_more=false;
dont_cache_failures=false;
do_types=false;
close_more=false;
dont_cache_failures=false;
do_types=false;
+ skip_trie_filtering=false;
+ skip_context=false;
close_more : bool;
dont_cache_failures: bool;
do_types: bool;
close_more : bool;
dont_cache_failures: bool;
do_types: bool;
+ skip_trie_filtering: bool;
+ skip_context : bool;
}
val default_flags : unit -> flags
}
val default_flags : unit -> flags
let mk_just ~dbd ~universe =
function
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
;;
| `Term t -> Tactics.apply t
;;