(* Copyright (C) 2002, HELM Team.
+
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
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
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
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 *)
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
(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))));
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"
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 =
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
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 ->
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
;;
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