*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature in
in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature 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 *)
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 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
- 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
(lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
let cache = cache_add_list cache context (ct@lt) in
let equations =
(lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
let cache = cache_add_list cache context (ct@lt) in
let equations =
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
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;
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,_ ->
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,_ ->
proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
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
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 use_library = flags.use_library in
let tables,cache,newmeta =
let use_library = flags.use_library in
let tables,cache,newmeta =
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