X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fauto.ml;h=92d66ef726ab7d245f0072c9aec81f3f7e85ed1d;hb=115915f23df4f56832d68b2f6b5b80c5afe019fc;hp=06aa8b303496b17942cc7e62d774ce510617bb88;hpb=9ab7d3460c70ee067f75bf6523d06b67d6e7750a;p=helm.git diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 06aa8b303..92d66ef72 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -26,16 +26,22 @@ open AutoTypes;; open AutoCache;; -let debug_print s = prerr_endline (Lazy.force s);; +let debug = false;; +let debug_print s = + if debug then () else prerr_endline (Lazy.force s);; (* functions for retrieving theorems *) exception FillingFailure of AutoCache.cache * int +let rec unfold context = function + | Cic.Prod(name,s,t) -> + let t' = unfold ((Some (name,Cic.Decl s))::context) t in + Cic.Prod(name,s,t') + | t -> ProofEngineReduction.unfold context t - -let find_library_theorems dbd proof gl = - let univ = MetadataQuery.universe_of_goals ~dbd proof gl in +let find_library_theorems dbd proof goal = + let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in let terms = List.map CicUtil.term_of_uri univ in List.map (fun t -> @@ -73,7 +79,7 @@ let partition_equalities = List.partition (fun (_,ty) -> is_an_equality ty) -let default_auto maxm _ cache _ _ _ _ = [],cache,maxm ;; +let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;; let is_unit_equation context metasenv oldnewmeta term = @@ -93,7 +99,7 @@ let is_unit_equation context metasenv oldnewmeta term = CicReduction.are_convertible ~metasenv context sort (Cic.Sort Cic.Prop) u in - if b then Some i else None + if b then Some i else None | _ -> assert false) args in @@ -101,48 +107,53 @@ let is_unit_equation context metasenv oldnewmeta term = let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in Some (args,metasenv,newmetas,head,newmeta) else None +;; -let retrieve_equations cache = - let eq_uri = - match LibraryObjects.eq_URI() with - | None ->assert false - | Some eq_uri -> eq_uri in - let fake= Cic.Meta(-1,[]) in - let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);Cic.Meta(-1,[]); - Cic.Meta(-2,[]); Cic.Meta(-3,[])] in - let candidates = get_candidates cache fake_eq in +let get_candidates universe cache t = + let candidates= + (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t) + in let debug_msg = - (lazy ("candidates for " ^ (CicPp.ppterm fake_eq) ^ " = " ^ + (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^ (String.concat "\n" (List.map CicPp.ppterm candidates)))) in debug_print debug_msg; candidates - -(* - let proof, goalno = status in - let _, metasenv,_,_ = proof in - let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in - let eq_uri = eq_of_goal type_of_goal in - let env = (metasenv, context, CicUniv.empty_ugraph) in - let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache - in - prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ - string_of_int maxm); - List.iter - (fun e -> prerr_endline (Equality.string_of_equality ~env e)) - equalities; - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; - let equalities = - HExtlib.filter_map - (fun e -> forward_simplify bag eq_uri env e active) - equalities - in - prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>"; - List.iter - (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities; - prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm); - bag, equalities, cache, maxm -*) +;; + +let only signature context t = + try + let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in + let consts = MetadataConstraints.constants_of ty in + let b = MetadataConstraints.UriManagerSet.subset consts signature in + if b then b + else + try + let ty' = unfold context ty in + let consts' = MetadataConstraints.constants_of ty' in + MetadataConstraints.UriManagerSet.subset consts' signature + with _-> false + with _ -> false +;; + +let not_default_eq_term t = + try + let uri = CicUtil.uri_of_term t in + not (LibraryObjects.in_eq_URIs uri) + with Invalid_argument _ -> true + +let retrieve_equations signature universe cache context= + match LibraryObjects.eq_URI() with + | None -> [] + | Some eq_uri -> + 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 + (* defaults eq uris are built-in in auto *) + let candidates = List.filter not_default_eq_term candidates in + let candidates = List.filter (only signature context) candidates in + List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates; + candidates let build_equality bag head args proof newmetas maxmeta = match head with @@ -178,41 +189,62 @@ let empty_tables = Saturation.make_passive [], Equality.mk_equality_bag) -let init_cache_and_tables dbd use_library (proof, goal) = +let init_cache_and_tables dbd use_library paramod universe (proof, goal) = + (* the local cache in initially empty *) + let cache = AutoCache.cache_empty in let _, metasenv, _, _ = proof in + let signature = MetadataQuery.signature_of metasenv goal in let newmeta = CicMkImplicit.new_meta metasenv [] in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let eq_uri = - match LibraryObjects.eq_URI() with - | None ->assert false - | Some eq_uri -> eq_uri in let ct = find_context_theorems context metasenv in + prerr_endline + ("ho trovato nel contesto " ^ (string_of_int (List.length ct))); let lt = if use_library then - find_library_theorems dbd metasenv [goal] + find_library_theorems dbd metasenv goal else [] in - (* all equations are added to the cache *) - prerr_endline ("ho trovato " ^ (string_of_int (List.length lt))); - let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in - let equations,others = partition_equalities (ct@lt) in + prerr_endline + ("ho trovato nella libreria " ^ (string_of_int (List.length lt))); + let cache = cache_add_list cache context (ct@lt) in + let equations = + retrieve_equations signature universe cache context in + prerr_endline + ("ho trovato equazioni n. " ^ (string_of_int (List.length equations))); + let eqs_and_types = + HExtlib.filter_map + (fun t -> + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in + (* retrieve_equations could also return flexible terms *) + if is_an_equality ty then Some(t,ty) + else + try + let ty' = unfold context ty in + if is_an_equality ty' then Some(t,ty') else None + with _ -> None) (* catturare l'eccezione giusta di unfold *) + equations in let bag = Equality.mk_equality_bag () in let units, other_equalities, newmeta = - partition_unit_equalities context metasenv newmeta bag equations in - (* other equations are added to the cache; note that untis equalities - are not)*) - let env = (metasenv, context, CicUniv.empty_ugraph) in - (* let equalities = + partition_unit_equalities context metasenv newmeta bag eqs_and_types in + (* let env = (metasenv, context, CicUniv.empty_ugraph) in + let equalities = + let eq_uri = + match LibraryObjects.eq_URI() with + | None ->assert false + | Some eq_uri -> eq_uri in Saturation.simplify_equalities bag eq_uri env units in *) let passive = Saturation.make_passive units in let no = List.length units in - prerr_endline ("No = " ^ (string_of_int no)); let active = Saturation.make_active [] in let active,passive,newmeta = - Saturation.pump_actives context bag newmeta active passive (no+1) infinity + if paramod then active,passive,newmeta + else + Saturation.pump_actives + context bag newmeta active passive (no+1) infinity in (active,passive,bag),cache,newmeta -let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast = +let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = let head, metasenv, args, newmeta = ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 in @@ -238,9 +270,10 @@ let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast = let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in [args,metasenv,newmetas,head,newmeta],cache,newmeta else + (* let proof = None,metasenv,term,term (* term non e' significativo *) - in + in *) let flags = if fast then {AutoTypes.default_flags() with @@ -253,7 +286,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast = maxwidth = 2;maxdepth = 4; use_paramod=true;use_only_paramod=false} in - match auto newmeta tables cache context metasenv propositional_args flags with + match auto newmeta tables universe cache context metasenv propositional_args flags with | [],cache,newmeta -> raise (FillingFailure (cache,newmeta)) | substs,cache,newmeta -> List.map @@ -272,14 +305,14 @@ let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast = in results,cache,newmeta -let build_equalities auto context metasenv tables cache newmeta equations = +let build_equalities auto context metasenv tables universe cache newmeta equations = List.fold_left (fun (facts,cache,newmeta) (t,ty) -> (* in any case we add the equation to the cache *) let cache = AutoCache.cache_add_list cache context [(t,ty)] in try let saturated,cache,newmeta = - fill_hypothesis context metasenv newmeta ty tables cache auto true + fill_hypothesis context metasenv newmeta ty tables universe cache auto true in let (active,passive,bag) = tables in let eqs,bag,newmeta = @@ -299,11 +332,12 @@ let build_equalities auto context metasenv tables cache newmeta equations = ) ([],cache,newmeta) equations -let close_more tables maxmeta context status auto cache = +let close_more tables maxmeta context status auto universe cache = let (active,passive,bag) = tables in let proof, goalno = status in - let _, metasenv,_,_ = proof in - let equations = retrieve_equations cache in + let _, metasenv,_,_ = proof in + let signature = MetadataQuery.signature_of metasenv goalno in + let equations = retrieve_equations signature universe cache context in let eqs_and_types = HExtlib.filter_map (fun t -> @@ -313,7 +347,7 @@ let close_more tables maxmeta context status auto cache = if is_an_equality ty then Some(t,ty) else None) equations in let units, cache, maxm = - build_equalities auto context metasenv tables cache maxmeta eqs_and_types in + build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ string_of_int maxm); List.iter @@ -329,9 +363,8 @@ let close_more tables maxmeta context status auto cache = (active,passive,bag),cache,newmeta let find_context_equalities - maxmeta bag context proof cache + maxmeta bag context proof (universe:Universe.universe) cache = - prerr_endline "find_equalities"; let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in @@ -353,7 +386,7 @@ let find_context_equalities let term = S.lift index term in let saturated,cache,newmeta = fill_hypothesis context metasenv newmeta term - empty_tables cache default_auto false + empty_tables universe cache default_auto false in let eqs,newmeta = List.fold_left @@ -393,8 +426,8 @@ let find_context_equalities (***************** applyS *******************) let new_metasenv_and_unify_and_t - dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty - goal_arity + dbd flags universe proof goal ?tables newmeta' metasenv' + context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in @@ -428,7 +461,7 @@ let new_metasenv_and_unify_and_t in match let (active, passive,bag), cache, maxmeta = - init_cache_and_tables dbd true (proof'''',newmeta) + init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta) in Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive max_int max_int flags.timeout @@ -446,7 +479,7 @@ let rec count_prods context ty = Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) = +let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in @@ -492,7 +525,7 @@ let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) = let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in let goal_arity = count_prods context ty in let subst, proof, gl, active, passive = - new_metasenv_and_unify_and_t dbd flags proof goal ?tables + new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity in subst, proof, gl, active, passive @@ -511,26 +544,35 @@ let is_in_prop context subst metasenv ty = let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u) ;; + let assert_proof_is_valid proof metasenv context goalty = - let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in - let b,_ = CicReduction.are_convertible context ty goalty u in - if not b then + if debug then begin - let names = - List.map (function None -> None | Some (x,_) -> Some x) context - in - prerr_endline ("PROOF:" ^ CicPp.pp proof names); - prerr_endline ("PROOFTY:" ^ CicPp.pp ty names); - prerr_endline ("GOAL:" ^ CicPp.pp goalty names); - prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv); - end; - assert b + let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in + let b,_ = CicReduction.are_convertible context ty goalty u in + if not b then + begin + let names = + List.map (function None -> None | Some (x,_) -> Some x) context + in + prerr_endline ("PROOF:" ^ CicPp.pp proof names); + prerr_endline ("PROOFTY:" ^ CicPp.pp ty names); + prerr_endline ("GOAL:" ^ CicPp.pp goalty names); + prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv); + end; + assert b + end + else () ;; + let assert_subst_are_disjoint subst subst' = - assert(List.for_all - (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') - subst) + if debug then + assert(List.for_all + (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') + subst) + else () ;; + let sort_new_elems = List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) ;; @@ -666,25 +708,23 @@ let try_candidate in debug_print (lazy (" OK: " ^ ppterm cand)); let metasenv = CicRefine.pack_coercion_metasenv metasenv in - assert (maxmeta >= maxm); - (*FIXME:sicuro che posso @?*) assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = order_new_goals metasenv subst open_goals ppterm in let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in Some (metasenv,subst,open_goals), tables , maxmeta - with ProofEngineTypes.Fail s -> + with + | ProofEngineTypes.Fail s -> (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm + | CicUnification.Uncertain s -> + (*debug_print(" BECCATO: "^Lazy.force s);*)None,tables, maxm ;; let applicative_case - tables maxm depth subst fake_proof goalno goalty metasenv context cache + tables maxm depth subst fake_proof goalno goalty metasenv context universe + cache = - let candidates = get_candidates cache goalty in - let debug_msg = - (lazy ("candidates for " ^ (CicPp.ppterm goalty) ^ " = " ^ - (String.concat "\n" (List.map CicPp.ppterm candidates)))) in - debug_print debug_msg; + let candidates = get_candidates universe cache goalty in let tables, elems, maxm = List.fold_left (fun (tables,elems,maxm) cand -> @@ -729,7 +769,7 @@ let cache_add_success sort cache k v = cache k ;; -let rec auto_main tables maxm context flags elems cache = +let rec auto_main tables maxm context flags elems universe cache = let flags = calculate_timeout flags in let ppterm = ppterm context in let irl = mk_irl context in @@ -757,9 +797,9 @@ let rec auto_main tables maxm context flags elems cache = (lazy (" FAILURE(not in prop)")); aux flags tables maxm cache tl (* FAILURE (not in prop) *)) else - match aux_single flags tables maxm cache metasenv subst elem goalty cc with + match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with | Fail s, tables, cache, maxm' -> - assert(maxm' >= maxm);let maxm = maxm' in + let maxm = maxm' in debug_print (lazy (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty)); @@ -770,7 +810,7 @@ let rec auto_main tables maxm context flags elems cache = in aux flags tables maxm cache tl | Success (metasenv,subst,others), tables, cache, maxm' -> - assert(maxm' >= maxm);let maxm = maxm' in + let maxm = maxm' in (* others are alternatives in OR *) try let goal = Cic.Meta(goalno,irl) in @@ -804,17 +844,15 @@ let rec auto_main tables maxm context flags elems cache = (lazy ("Goal "^string_of_int goalno^" closed by sideeffect")); aux flags tables maxm cache ((metasenv,subst,gl)::tl) - and aux_single flags tables maxm cache metasenv subst (goalno, depth, _) goalty cc = + and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc = let goalty = CicMetaSubst.apply_subst subst goalty in (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *) (* FAILURE (euristic cut) *) - prerr_endline ("DEPTH = +++++++= "^ (string_of_int depth)); match cache_examine cache goalty with | Failed_in d when d >= depth -> Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth), tables,cache,maxm(*FAILURE(depth)*) | Succeded t -> - assert(List.for_all (fun (i,_) -> i <> goalno) subst); let entry = goalno, (cc, t,goalty) in assert_subst_are_disjoint subst [entry]; let subst = entry :: subst in @@ -831,7 +869,6 @@ let rec auto_main tables maxm context flags elems cache = let elems,tables,cache,maxm1, flags = equational_case tables maxm cache depth fake_proof goalno goalty subst context flags in - assert(maxm1 >= maxm); let maxm = maxm1 in let more_elems, tables, cache, maxm1 = if flags.use_only_paramod then @@ -839,14 +876,13 @@ let rec auto_main tables maxm context flags elems cache = else applicative_case tables maxm depth subst fake_proof goalno - goalty metasenv context cache in - assert(maxm1 >= maxm); + goalty metasenv context universe cache in let maxm = maxm1 in elems@more_elems, tables, cache, maxm, flags else let elems, tables, cache, maxm = applicative_case tables maxm depth subst fake_proof goalno - goalty metasenv context cache in + goalty metasenv context universe cache in elems, tables, cache, maxm, flags in aux flags tables maxm cache elems @@ -855,13 +891,13 @@ let rec auto_main tables maxm context flags elems cache = aux flags tables maxm cache elems and - auto_all_solutions maxm tables cache context metasenv gl flags + auto_all_solutions maxm tables universe cache context metasenv gl flags = let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in let elems = [metasenv,[],goals] in let rec aux tables maxm solutions cache elems flags = - match auto_main tables maxm context flags elems cache with + match auto_main tables maxm context flags elems universe cache with | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm | Success (metasenv,subst,others),tables,cache,maxm -> if Unix.gettimeofday () > flags.timeout then @@ -887,19 +923,19 @@ and (* }}} ****************** AUTO ***************) -let auto_all tables cache context metasenv gl flags = +let auto_all tables universe cache context metasenv gl flags = let solutions, cache, _ = - auto_all_solutions 0 tables cache context metasenv gl flags + auto_all_solutions 0 tables universe cache context metasenv gl flags in solutions, cache ;; -let auto flags metasenv tables cache context metasenv gl = +let auto flags metasenv tables universe cache context metasenv gl = let initial_time = Unix.gettimeofday() in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in let elems = [metasenv,[],goals] in - match auto_main tables 0 context flags elems cache with + match auto_main tables 0 context flags elems universe cache with | Success (metasenv,subst,_), tables,cache,_ -> prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); Some (subst,metasenv), cache @@ -933,9 +969,12 @@ let int params name default = let flags_of_params params ?(for_applyS=false) () = let int = int params in let bool = bool params in + let close_more = bool "close_more" false in let use_paramod = bool "use_paramod" true in let use_only_paramod = if for_applyS then true else bool "paramodulation" false in + let use_library = bool "library" + ((AutoTypes.default_flags()).AutoTypes.use_library) in let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in let timeout = int "timeout" 0 in @@ -948,18 +987,20 @@ let flags_of_params params ?(for_applyS=false) () = else infinity else - Unix.gettimeofday() +. (float_of_int timeout); + Unix.gettimeofday() +. (float_of_int timeout); + AutoTypes.use_library = use_library; AutoTypes.use_paramod = use_paramod; AutoTypes.use_only_paramod = use_only_paramod; + AutoTypes.close_more = close_more; AutoTypes.dont_cache_failures = false; } -let applyS_tac ~dbd ~term ~params = +let applyS_tac ~dbd ~term ~params ~universe = ProofEngineTypes.mk_tactic (fun status -> try let _, proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] + apply_smart ~dbd ~term ~subst:[] ~universe (flags_of_params params ~for_applyS:true ()) status in proof, gl @@ -999,6 +1040,7 @@ let rec position_of i x = function | _ -> i ;; + let superposition_tac ~target ~table ~subterms_only ~demod_table status = Saturation.reset_refs(); let proof,goalno = status in @@ -1009,7 +1051,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let names = Utils.names_of_context context in let bag = Equality.mk_equality_bag () in let eq_index, equalities, maxm,cache = - find_context_equalities 0 bag context proof AutoCache.cache_empty + find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty in let eq_what = let what = find_in_ctx 1 target context in @@ -1089,8 +1131,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = proof,[goalno] ;; - -let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) = +let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) = (* argument parsing *) let string = string params in let bool = bool params in @@ -1111,15 +1152,19 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) = let _,context,_ = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params () in (* just for testing *) - let use_library = not flags.use_only_paramod in + let use_library = flags.use_library in let tables,cache,newmeta = - init_cache_and_tables dbd use_library (proof, goal) in + init_cache_and_tables dbd use_library flags.use_only_paramod + universe (proof, goal) in let tables,cache,newmeta = - close_more tables newmeta context (proof, goal) auto_all_solutions cache in + if flags.close_more then + close_more + tables newmeta context (proof, goal) auto_all_solutions universe cache + else tables,cache,newmeta in let initial_time = Unix.gettimeofday() in let (_,oldmetasenv,_,_) = proof in let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in - match auto_main tables newmeta context flags [elem] cache with + match auto_main tables newmeta context flags [elem] universe cache with | Success (metasenv,subst,_), tables,cache,_ -> prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); let proof,metasenv = @@ -1135,7 +1180,8 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) = raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; -let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);; +let auto_tac ~dbd ~params ~universe = + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);; let eq_of_goal = function | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri -> @@ -1151,7 +1197,7 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = let initgoal = [], [], ty in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = - init_cache_and_tables dbd true (proof,goal) in + init_cache_and_tables dbd true true Universe.empty (proof,goal) in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let table =