From 8e76ac2823de8cffc0b5f75b36264f86e3d0b52d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 7 Nov 2008 16:53:55 +0000 Subject: [PATCH] The signature in "retrieve equations" must be extended with the equality if not already there, otherwise it may hardly find any equation. --- helm/software/components/tactics/auto.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 07331220c..e7c11d43d 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -26,7 +26,7 @@ open AutoTypes;; open AutoCache;; -let debug = false;; +let debug = true;; let debug_print s = if debug then prerr_endline (Lazy.force s);; @@ -182,11 +182,13 @@ let only signature context metasenv t = in let consts = MetadataConstraints.constants_of ty in let b = MetadataConstraints.UriManagerSet.subset consts signature in - if b then b + if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); 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 *) @@ -207,9 +209,11 @@ let retrieve_equations dont_filter signature universe cache context metasenv = let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] 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 @@ -275,7 +279,7 @@ let init_cache_and_tables (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)))); -- 2.39.2