X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=09156224ec280e4d149486521af62895e52b9587;hb=89be8e257ea6a9b7e30a595c8294e0972d165a72;hp=5166ce503ea694ff54e92843d391a096a99af04f;hpb=2e28a15694f110bd462aa447b5be883d48e1fb7d;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 5166ce503..09156224e 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -26,10 +26,11 @@ open AutoTypes;; open AutoCache;; -let debug = true;; +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 @@ -180,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 *) @@ -203,11 +207,13 @@ 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 - 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 @@ -273,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)))); @@ -524,6 +530,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 +560,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 = @@ -613,15 +623,12 @@ let new_metasenv_and_unify_and_t 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 @@ -1254,9 +1261,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 -> @@ -1289,14 +1296,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 ;; @@ -1608,11 +1615,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