From 06b128f1107fd579a696b83b2f8255f83ab29a92 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 23 Nov 2006 14:31:56 +0000 Subject: [PATCH] Modifications to auto due to the introduction of the universe in the status. --- components/tactics/.depend | 49 ++-- components/tactics/Makefile | 3 +- components/tactics/auto.ml | 221 +++++++------- components/tactics/auto.mli | 10 +- components/tactics/autoCache.ml | 69 ++--- components/tactics/autoTactic.ml | 14 +- components/tactics/autoTactic.mli | 5 +- components/tactics/autoTypes.ml | 2 +- components/tactics/declarative.ml | 8 +- components/tactics/metadataQuery.ml | 95 ++++-- components/tactics/metadataQuery.mli | 12 +- components/tactics/paramodulation/equality.ml | 25 +- components/tactics/paramodulation/indexing.ml | 7 +- .../tactics/paramodulation/saturation.ml | 272 +++++++++++++----- components/tactics/paramodulation/utils.ml | 6 + components/tactics/tactics.mli | 11 +- 16 files changed, 500 insertions(+), 309 deletions(-) diff --git a/components/tactics/.depend b/components/tactics/.depend index 398c2af39..c8317fca4 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -21,8 +21,8 @@ introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi -auto.cmi: proofEngineTypes.cmi -autoTactic.cmi: proofEngineTypes.cmi +auto.cmi: universe.cmi proofEngineTypes.cmi +autoTactic.cmi: universe.cmi proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi @@ -30,6 +30,7 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi +tactics.cmi: universe.cmi proofEngineTypes.cmi declarative.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi @@ -61,10 +62,12 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi +universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi +universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi autoTypes.cmo: autoTypes.cmi autoTypes.cmx: autoTypes.cmi -autoCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi autoCache.cmi -autoCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx autoCache.cmi +autoCache.cmo: universe.cmi autoCache.cmi +autoCache.cmx: universe.cmx autoCache.cmi paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi paramodulation/subst.cmo: paramodulation/subst.cmi @@ -92,15 +95,13 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \ paramodulation/equality_indexing.cmx paramodulation/equality.cmx \ paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ - proofEngineHelpers.cmi paramodulation/indexing.cmi \ - paramodulation/founif.cmi paramodulation/equality.cmi \ - paramodulation/saturation.cmi + paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ + paramodulation/indexing.cmi paramodulation/founif.cmi \ + paramodulation/equality.cmi paramodulation/saturation.cmi paramodulation/saturation.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ - proofEngineHelpers.cmx paramodulation/indexing.cmx \ - paramodulation/founif.cmx paramodulation/equality.cmx \ - paramodulation/saturation.cmi + paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ + paramodulation/indexing.cmx paramodulation/founif.cmx \ + paramodulation/equality.cmx paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ variousTactics.cmi @@ -129,16 +130,16 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmi -auto.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \ - paramodulation/saturation.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ - primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \ - equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \ - autoCache.cmi auto.cmi -auto.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \ - paramodulation/saturation.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ - primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \ - equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \ - autoCache.cmx auto.cmi +auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \ + paramodulation/saturation.cmi proofEngineTypes.cmi \ + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \ + paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi +auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \ + paramodulation/saturation.cmx proofEngineTypes.cmx \ + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \ + paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ primitiveTactics.cmi metadataQuery.cmi paramodulation/equality.cmi \ autoTypes.cmi auto.cmi autoTactic.cmi @@ -203,7 +204,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \ fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \ eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \ tactics.cmi -declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ +declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi -declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ +declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \ declarative.cmi diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 74117ed87..cdb16efe4 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -6,10 +6,11 @@ INTERFACE_FILES = \ continuationals.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ + universe.mli \ autoTypes.mli \ autoCache.mli \ paramodulation/utils.mli \ - paramodulation/subst.mli\ + paramodulation/subst.mli \ paramodulation/equality.mli\ paramodulation/founif.mli\ paramodulation/equality_indexing.mli\ diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 698053b40..1e326df10 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -26,16 +26,20 @@ open AutoTypes;; open AutoCache;; -let debug_print s = prerr_endline (Lazy.force s);; +let debug_print s = 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 +77,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 +97,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 +105,36 @@ 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 singature context t = + try + let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in + let consts = MetadataConstraints.constants_of ty in + MetadataConstraints.UriManagerSet.subset consts singature + with _ -> false +;; + +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 + List.filter (only signature context) candidates let build_equality bag head args proof newmetas maxmeta = match head with @@ -178,41 +170,58 @@ 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 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 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 AutoCache.cache_empty context (ct@lt) in *) + 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 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 +247,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 +263,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 +282,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 +309,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 +324,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 +340,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 +363,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 +403,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 +438,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 universe (proof'''',newmeta) in Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive max_int max_int flags.timeout @@ -446,7 +456,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 +502,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 @@ -673,18 +683,18 @@ let try_candidate 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 +739,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,7 +767,7 @@ 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 debug_print @@ -804,11 +814,10 @@ 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), @@ -839,14 +848,14 @@ 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 + goalty metasenv context universe cache in assert(maxm1 >= maxm); 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 +864,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 +896,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 @@ -937,7 +946,8 @@ let flags_of_params params ?(for_applyS=false) () = 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" (not use_only_paramod) 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 @@ -958,12 +968,12 @@ let flags_of_params params ?(for_applyS=false) () = 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 @@ -1003,6 +1013,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 @@ -1013,7 +1024,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 @@ -1093,8 +1104,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 @@ -1117,16 +1127,16 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) = (* just for testing *) 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 universe (proof, goal) in let tables,cache,newmeta = if flags.close_more then close_more - tables newmeta context (proof, goal) auto_all_solutions cache + 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 = @@ -1142,7 +1152,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 -> @@ -1158,7 +1169,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 Universe.empty (proof,goal) in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let table = diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli index 6e64fb66e..d749a26af 100644 --- a/components/tactics/auto.mli +++ b/components/tactics/auto.mli @@ -25,10 +25,16 @@ (* stops at the first solution *) val auto_tac: - dbd:HMysql.dbd -> params:(string * string) list -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> + params:(string * string) list -> + universe:Universe.universe -> + ProofEngineTypes.tactic val applyS_tac: - dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list -> + dbd:HMysql.dbd -> + term: Cic.term -> + params:(string * string) list -> + universe:Universe.universe -> ProofEngineTypes.tactic val demodulate_tac : dbd:HMysql.dbd -> ProofEngineTypes.tactic diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml index 0b42391fa..57701310c 100644 --- a/components/tactics/autoCache.ml +++ b/components/tactics/autoCache.ml @@ -23,72 +23,37 @@ * http://cs.unibo.it/helm/. *) -module Codomain = struct - type t = Cic.term - let compare = Pervasives.compare -end -module S = Set.Make(Codomain) -module TI = Discrimination_tree.DiscriminationTreeIndexing(S) -type universe = TI.t -(* (proof,ty) list *) type cache_key = Cic.term type cache_elem = | Failed_in of int | Succeded of Cic.term | UnderInspection | Notfound -type cache = (universe * ((cache_key * cache_elem) list));; +type cache = (Universe.universe * ((cache_key * cache_elem) list));; -let cache_empty = (TI.empty,[]);; -let get_candidates (univ,_) ty = - S.elements (TI.retrieve_unifiables univ ty) -;; - -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 cache_empty = (Universe.empty,[]);; -let rec collapse_head_metas = function - | Cic.Appl(a::l) -> - let a' = collapse_head_metas a in - (match a' with - | Cic.Meta(n,m) -> Cic.Meta(n,m) - | t -> - let l' = List.map collapse_head_metas l in - Cic.Appl(t::l')) - | t -> t -;; - -let rec head t = - let rec aux = function - | Cic.Prod(_,_,t) -> - CicSubstitution.subst (Cic.Meta (-1,[])) (aux t) - | t -> t - in collapse_head_metas (aux t) +let get_candidates (univ,_) ty = + Universe.get_candidates univ ty ;; -let index (univ,oldcache) key term = - prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term); - (TI.index univ key term,oldcache) +let index (univ,cache) key term = + Universe.index univ key term,cache ;; -let index_term_and_unfolded_term cache context t ty = - let key = head ty in - let cache = index cache key t in - try - let key = head (unfold context ty) in - index cache key t - with ProofEngineTypes.Fail _ -> cache +let index_term_and_unfolded_term (univ,cache) context t ty = + Universe.index_local_term univ context t ty, cache ;; -let cache_add_list cache context terms_and_types = - List.fold_left - (fun acc (term,ty) -> - index_term_and_unfolded_term acc context term ty) - cache terms_and_types +let cache_add_list (univ,cache) context terms_and_types = + let univ = + List.fold_left + (fun univ (t,ty) -> + Universe.index_local_term univ context t ty) + univ terms_and_types + in + univ, cache let cache_examine (_,oldcache) cache_key = try List.assoc cache_key oldcache with Not_found -> Notfound @@ -112,7 +77,7 @@ let cache_add_failure cache cache_key depth = assert false (* if succed it can't fail *) ;; let cache_add_success ((univ,_) as cache) cache_key proof = - TI.index univ cache_key proof,snd + Universe.index univ cache_key proof,snd (match cache_examine cache cache_key with | Failed_in _ -> cache_replace cache cache_key (Succeded proof) | UnderInspection -> cache_replace cache cache_key (Succeded proof) diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 8e94bba86..e8d034a32 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -317,22 +317,22 @@ let int params name default = raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) ;; -let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = +let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) = (* argument parsing *) let int = int params in let bool = bool params in - let newauto = bool "new" false in + let oldauto = bool "old" false in let use_only_paramod = bool "paramodulation" false in - let newauto = if use_only_paramod then true else newauto in + let oldauto = if use_only_paramod then false else oldauto in let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in - if not newauto then + if oldauto then auto_tac_old ~depth ~width ~dbd () (proof,goal) else - ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal) + ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal) -let auto_tac ~params ~dbd = - ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) +let auto_tac ~params ~dbd ~universe= + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe) ;; let pp_proofterm = Equality.pp_proofterm;; diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli index 23f1b813f..d96a82615 100644 --- a/components/tactics/autoTactic.mli +++ b/components/tactics/autoTactic.mli @@ -25,6 +25,9 @@ *) val auto_tac: - params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic + params:(string * string) list + -> dbd:HMysql.dbd + -> universe:Universe.universe + -> ProofEngineTypes.tactic val pp_proofterm: Cic.term -> string diff --git a/components/tactics/autoTypes.ml b/components/tactics/autoTypes.ml index 9031a0338..5a84c2c2b 100644 --- a/components/tactics/autoTypes.ml +++ b/components/tactics/autoTypes.ml @@ -38,7 +38,7 @@ let default_flags _ = {maxwidth=3; maxdepth=3; timeout=Unix.gettimeofday() +.3.0; - use_library=true; + use_library=false; use_paramod=true; use_only_paramod=false; close_more=false; diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 7561281a8..fc8b175a2 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -48,7 +48,7 @@ let suppose t id ty = let by_term_we_proved ~dbd t ty id ty' = let just = match t with - None -> Tactics.auto ~dbd ~params:[] + None -> Tactics.auto ~dbd ~params:[] (* da sistemare *) ~universe:Universe.empty | Some t -> Tactics.apply t in match id with @@ -80,7 +80,7 @@ let by_term_we_proved ~dbd t ty id ty' = let bydone ~dbd t = let just = match t with - None -> Tactics.auto ~dbd ~params:[] + None -> Tactics.auto ~dbd ~params:[] ~universe:Universe.empty | Some t -> Tactics.apply t in just @@ -150,8 +150,8 @@ let rewritingstep ~dbd lhs rhs just conclude = match just with None -> Tactics.auto ~dbd - ~params:["paramodulation","1"; "timeout","3"; "library","1"] - | Some just -> Tactics.apply just + ~params:["paramodulation","1"; "timeout","3"] ~universe:Universe.empty + | Some just -> Tactics.apply just in match lhs with None -> diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml index 9b4f565c8..443ae973f 100644 --- a/components/tactics/metadataQuery.ml +++ b/components/tactics/metadataQuery.ml @@ -240,22 +240,47 @@ let only constants uri = Constr.UriManagerSet.subset consts constants ;; -let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals = - let add_uris_for acc goal = - let (_, context, ty) = CicUtil.lookup_meta goal metasenv in - let main, sig_constants = Constr.signature_of ty in - let set = signature_of_hypothesis context metasenv in - let set = - match main with - None -> set - | Some (main,l) -> - List.fold_right Constr.UriManagerSet.add (main::l) set in - let set = Constr.UriManagerSet.union set sig_constants in - let all_constants_closed = close_with_types set metasenv context in - Constr.UriManagerSet.union all_constants_closed acc - in - let all_constants_closed = - List.fold_left add_uris_for Constr.UriManagerSet.empty goals in +let rec types_of_equality = function + | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _] + when (LibraryObjects.is_eq_URI uri) -> + let uri_set = Constr.constants_of ty in + if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then + Constr.SetSet.empty + else Constr.SetSet.singleton uri_set + | Cic.Prod (_, s, t) -> + Constr.SetSet.union (types_of_equality s) (types_of_equality t) + | _ -> Constr.SetSet.empty +;; + +let types_for_equality metasenv goal = + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let all = types_of_equality ty in + let _, all = + List.fold_left + (fun (i,acc) _ -> + let ty, _ = + CicTypeChecker.type_of_aux' + metasenv context (Cic.Rel i) CicUniv.empty_ugraph in + let newty = types_of_equality ty in + (i+1,Constr.SetSet.union newty acc)) + (1,all) context + in all +;; + +let signature_of metasenv goal = + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let ty_set = Constr.constants_of ty in + let hyp_set = signature_of_hypothesis context metasenv in + let set = Constr.UriManagerSet.union ty_set hyp_set in + close_with_types set metasenv context + + +let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal = + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let ty_set = Constr.constants_of ty in + let hyp_set = signature_of_hypothesis context metasenv in + let set = Constr.UriManagerSet.union ty_set hyp_set in + let all_constants_closed = close_with_types set metasenv context in (* we split predicates from the rest *) let predicates, rest = Constr.UriManagerSet.partition is_predicate all_constants_closed @@ -263,11 +288,34 @@ let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals = let uris = Constr.UriManagerSet.fold (fun u acc -> - let uris = - sigmatch ~dbd ~facts:false ~where:`Statement - (Some (u,[]),all_constants_closed) - in - acc @ uris) + prerr_endline ("processing "^(UriManager.string_of_uri u)); + let set_for_sigmatch = + Constr.UriManagerSet.remove u all_constants_closed in + if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then + (* equality has a special treatment *) + (prerr_endline "special treatment"; + let tfe = + Constr.SetSet.elements (types_for_equality metasenv goal) + in + List.fold_left + (fun acc l -> + let tyl = Constr.UriManagerSet.elements l in + prerr_endline ("tyl: "^(String.concat "\n" + (List.map UriManager.string_of_uri tyl))); + let set_for_sigmatch = + Constr.UriManagerSet.diff set_for_sigmatch l in + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement + (Some (u,tyl),set_for_sigmatch) in + acc @ uris) + acc tfe) + else + (prerr_endline "normal treatment"; + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement + (Some (u,[]),set_for_sigmatch) + in + acc @ uris)) predicates [] in (* @@ -277,8 +325,9 @@ let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals = *) let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in - let uris = List.filter (only all_constants_closed) uris in - uris + if apply_only then + List.filter (only all_constants_closed) uris + else uris ;; let filter_out_predicate set ctx menv = diff --git a/components/tactics/metadataQuery.mli b/components/tactics/metadataQuery.mli index aebe45198..1bc9fa363 100644 --- a/components/tactics/metadataQuery.mli +++ b/components/tactics/metadataQuery.mli @@ -33,8 +33,16 @@ val signature_of_goal: dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list -val universe_of_goals: - dbd:HMysql.dbd -> Cic.metasenv -> ProofEngineTypes.goal list -> +val signature_of: + Cic.metasenv -> + ProofEngineTypes.goal -> + MetadataConstraints.UriManagerSet.t + +val universe_of_goal: + dbd:HMysql.dbd -> + bool -> (* apply only or not *) + Cic.metasenv -> + ProofEngineTypes.goal -> UriManager.uri list val equations_for_goal: diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 7123c134a..10a64af19 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -372,7 +372,8 @@ let contextualize uri ty left right t = * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context * ctx_ty is the type of ctx *) - let rec aux uri ty left right ctx_d ctx_ty = function + let rec aux uri ty left right ctx_d ctx_ty t = + match t with | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) when LibraryObjects.is_sym_eq_URI uri_sym -> let ty,l,r,p = open_sym ens tl in @@ -407,8 +408,8 @@ let contextualize uri ty left right t = let c_what = put_in_ctx ctx_c what in (* now put the proofs in the compound context *) let p1 = (* p1: dc_what = d_m *) - if is_not_fixed_lp then - aux uri ty2 c_what m ctx_d ctx_ty p1 + if is_not_fixed_lp then + aux uri ty2 c_what m ctx_d ctx_ty p1 else mk_sym uri_sym ctx_ty d_m dc_what (aux uri ty2 m c_what ctx_d ctx_ty p1) @@ -417,7 +418,7 @@ let contextualize uri ty left right t = if avoid_eq_ind then mk_sym uri_sym ctx_ty dc_what dc_other (aux uri ty1 what other ctx_dc ctx_ty p2) - else + else aux uri ty1 other what ctx_dc ctx_ty p2 in (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m @@ -496,7 +497,7 @@ let build_proof_step eq lift subst p1 p2 pos l r pred = p ;; -let parametrize_proof p l r ty = +let parametrize_proof menv p l r ty = let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in let mot = CicUtil.metas_of_term_set in let parameters = uniq (mot p @ mot l @ mot r) in @@ -517,9 +518,21 @@ let parametrize_proof p l r ty = match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) ~what ~with_what ~where:p in + let ty_of_m _ = Cic.Implicit (Some `Type) +(* + let ty_of_m = function + | Cic.Meta (i,_) -> + (try + let _,_,ty = CicUtil.lookup_meta i menv in ty + with CicUtil.Meta_not_found _ -> + prerr_endline "eccoci";assert false) + | _ -> assert false +*) + (* let ty_of_m _ = ty (*function | Cic.Meta (i,_) -> List.assoc i menv | _ -> assert false *) + *) in let args, proof,_ = List.fold_left @@ -729,7 +742,7 @@ let build_goal_proof bag eq l initial ty se context menv = let p,l,r = proof_of_id bag id in let cic = build_proof_term bag eq h n p in let real_cic,instance = - parametrize_proof cic l r (CicSubstitution.lift n mty) + parametrize_proof menv cic l r (CicSubstitution.lift n mty) in let h = (id, instance)::lift_list h in acc@[id,real_cic],n+1,h) diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 7bbc4d43c..28c22a64e 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -1003,8 +1003,11 @@ let build_newgoal bag context goal posu rule expansion = Utils.guarded_simpl context (apply_subst subst (CicSubstitution.subst other t)) in - let bo' = (*apply_subst subst*) t in - let name = Cic.Name "x" in + let bo' = (*apply_subst subst*) t in + (* patch?? + let bo' = t in + let ty = apply_subst subst ty in *) + let name = Cic.Name "x" in let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in bo, (newgoalproofstep::goalproof) in diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 40d07e414..d9472601c 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1238,6 +1238,62 @@ let eq_and_ty_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; +(* fix proof takes in input a term and try to build a metasenv for it *) + +let fix_proof metasenv context all_implicits p = + let rec aux metasenv n p = + match p with + | Cic.Meta (i,_) -> + if all_implicits then + metasenv,Cic.Implicit None + else + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let meta = CicSubstitution.lift n (Cic.Meta (i,irl)) in + let metasenv = + try + let _ = CicUtil.lookup_meta i metasenv in metasenv + with CicUtil.Meta_not_found _ -> + prerr_endline ("not found: "^(string_of_int i)); + let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in + (i,context,Cic.Meta(j,irl))::metasenv + in + metasenv,meta + | Cic.Appl l -> + let metasenv,l= + List.fold_right + (fun a (metasenv,l) -> + let metasenv,a' = aux metasenv n a in + metasenv,a'::l) + l (metasenv,[]) + in metasenv,Cic.Appl l + | Cic.Lambda(name,s,t) -> + let metasenv,s = aux metasenv n s in + let metasenv,t = aux metasenv (n+1) t in + metasenv,Cic.Lambda(name,s,t) + | Cic.Prod(name,s,t) -> + let metasenv,s = aux metasenv n s in + let metasenv,t = aux metasenv (n+1) t in + metasenv,Cic.Prod(name,s,t) + | Cic.LetIn(name,s,t) -> + let metasenv,s = aux metasenv n s in + let metasenv,t = aux metasenv (n+1) t in + metasenv,Cic.LetIn(name,s,t) + | t -> metasenv,t + in + aux metasenv 0 p +;; + +let fix_metasenv metasenv context = + List.fold_left + (fun m (i,c,t) -> + let m,t = fix_proof m context false t in + let m = List.filter (fun (j,_,_) -> j<>i) m in + (i,c,t)::m) + metasenv metasenv +;; + (* status: input proof status * goalproof: forward steps on goal * newproof: backward steps @@ -1246,38 +1302,95 @@ let eq_and_ty_of_goal = function * subsumption_subst: subst to make newproof and goalproof match * proof_menv: final metasenv *) + let build_proof bag status goalproof newproof subsumption_id subsumption_subst proof_menv = + if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA" + else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv); let proof, goalno = status in let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in - let names = Utils.names_of_context context in - prerr_endline "Proof:"; - prerr_endline - (Equality.pp_proof bag names goalproof newproof subsumption_subst - subsumption_id type_of_goal); -(* prerr_endline "ENDOFPROOFS"; *) + let names = Utils.names_of_context context in + prerr_endline "Proof:"; + prerr_endline + (Equality.pp_proof bag names goalproof newproof subsumption_subst + subsumption_id type_of_goal); (* prerr_endline ("max weight: " ^ (string_of_int (Equality.max_weight goalproof newproof))); *) - (* generation of the CIC proof *) - let side_effects = - List.filter (fun i -> i <> goalno) - (ProofEngineHelpers.compare_metasenvs - ~newmetasenv:metasenv ~oldmetasenv:proof_menv) - in - let goal_proof, side_effects_t = - let initial = Equality.add_subst subsumption_subst newproof in - Equality.build_goal_proof bag - eq_uri goalproof initial type_of_goal side_effects - context proof_menv - in - (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *) - let goal_proof = Subst.apply_subst subsumption_subst goal_proof in + (* generation of the CIC proof *) + (* let metasenv' = List.filter (fun i,_,_ -> i<>goalno) metasenv in *) + let side_effects = + List.filter (fun i -> i <> goalno) + (ProofEngineHelpers.compare_metasenvs + ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in + let goal_proof, side_effects_t = + let initial = (* Equality.add_subst subsumption_subst*) newproof in + Equality.build_goal_proof bag + eq_uri goalproof initial type_of_goal side_effects + context proof_menv + in + let goal_proof = Subst.apply_subst subsumption_subst goal_proof in + let real_menv = fix_metasenv (proof_menv@metasenv) context in + let real_menv,goal_proof = + fix_proof real_menv context false goal_proof in +(* + let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in + (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *) +*) + let goal_proof,goal_ty,real_menv,_ = + (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *) + try + CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph + with + | CicUtil.Meta_not_found _ + | CicRefine.RefineFailure _ + | CicRefine.Uncertain _ + | CicRefine.AssertFailure _ + | Invalid_argument "list_fold_left2" as exn -> + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + prerr_endline (CicPp.pp goal_proof names); + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + raise exn + in + let subst_side_effects,real_menv,_ = + try + CicUnification.fo_unif_subst [] context real_menv + goal_ty type_of_goal CicUniv.empty_ugraph + with + | CicUnification.UnificationFailure s + | CicUnification.Uncertain s + | CicUnification.AssertFailure s -> assert false + (* fail "Maybe the local context of metas in the goal was not an IRL" s *) + in + prerr_endline "+++++++++++++ FINE UNIF"; + let final_subst = + (goalno,(context,goal_proof,type_of_goal))::subst_side_effects + in +(* + let metas_of_proof = Utils.metas_of_term goal_proof in +*) + let proof, real_metasenv = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goalno (CicMetaSubst.apply_subst final_subst) + (List.filter (fun i,_,_ -> i<>goalno ) real_menv) + in + let open_goals = + (ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in +(* + let open_goals = + List.map (fun i,_,_ -> i) real_metasenv in +*) + final_subst, proof, open_goals + + +(* + let metas_still_open_in_proof = Utils.metas_of_term goal_proof in (* prerr_endline (CicPp.pp goal_proof names); *) let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in @@ -1287,23 +1400,26 @@ let build_proof (* replacing fake mets with real ones *) (* prerr_endline "replacing metas..."; *) let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in - let goal_proof_menv, what, with_what,free_meta = + if proof_menv = [] then prerr_endline "VUOTA"; + CicMetaSubst.ppmetasenv [] proof_menv; + let what, with_what = List.fold_left - (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> - match uniq with - | Some m -> -(* acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *) - (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, - (Cic.Meta(i,irl))::acc3, uniq - | None -> - [i,context,ty], (Cic.Meta(i,[]))::acc2, - (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) - ([],[],[],None) + (fun (acc1,acc2) i -> + (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2) + ([],[]) + metas_still_open_in_proof +(* (List.filter (fun (i,_,_) -> List.mem i metas_still_open_in_proof (*&& not(List.mem i metas_still_open_in_goal)*)) proof_menv) +*) + in + let goal_proof_menv = + List.filter + (fun (i,_,_) -> List.mem i metas_still_open_in_proof) + proof_menv in let replace where = (* we need this fake equality since the metas of the hypothesis may be @@ -1332,54 +1448,58 @@ let build_proof ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false) ~where:type_of_goal in + let goal_proof,goal_ty,real_menv,_ = + prerr_endline "parte la refine"; + try + CicRefine.type_of_aux' metasenv context goal_proof + CicUniv.empty_ugraph + with + | CicUtil.Meta_not_found _ + | CicRefine.RefineFailure _ + | CicRefine.Uncertain _ + | CicRefine.AssertFailure _ + | Invalid_argument "list_fold_left2" as exn -> + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + prerr_endline (CicPp.pp goal_proof names); + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + raise exn + in + prerr_endline "+++++++++++++ METASENV"; + prerr_endline + (CicMetaSubst.ppmetasenv [] real_menv); let subst_side_effects,real_menv,_ = - let fail t s = raise (ProofEngineTypes.Fail (lazy (t^Lazy.force s))) in - let free_metas_menv = - List.map (fun i -> CicUtil.lookup_meta i goal_proof_menv) free_metas - in -(* +(* prerr_endline ("XX type_of_goal " ^ CicPp.ppterm type_of_goal); prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal); prerr_endline ("XX metasenv " ^ CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv)); *) try - CicUnification.fo_unif_subst [] context (metasenv @ free_metas_menv) - replaced_goal type_of_goal CicUniv.empty_ugraph + CicUnification.fo_unif_subst [] context real_menv + goal_ty type_of_goal CicUniv.empty_ugraph with | CicUnification.UnificationFailure s | CicUnification.Uncertain s - | CicUnification.AssertFailure s -> - fail "Maybe the local context of metas in the goal was not an IRL" s + | CicUnification.AssertFailure s -> assert false +(* fail "Maybe the local context of metas in the goal was not an IRL" s *) in let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in -(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *) - let _ = - try - CicTypeChecker.type_of_aux' real_menv context goal_proof - CicUniv.empty_ugraph - with - | CicUtil.Meta_not_found _ - | CicTypeChecker.TypeCheckerFailure _ - | CicTypeChecker.AssertFailure _ - | Invalid_argument "list_fold_left2" as exn -> - prerr_endline "THE PROOF DOES NOT TYPECHECK!"; - prerr_endline (CicPp.pp goal_proof names); - prerr_endline "THE PROOF DOES NOT TYPECHECK!"; - raise exn - in - +(* let metas_of_proof = Utils.metas_of_term goal_proof in - +*) let proof, real_metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goalno (CicMetaSubst.apply_subst final_subst) real_menv + proof goalno (CicMetaSubst.apply_subst final_subst) + (List.filter (fun i,_,_ -> i<>goalno ) real_menv) in - let open_goals = + let open_goals = + List.map (fun i,_,_ -> i) real_metasenv in + +(* HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof) - in + in *) (* match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] in @@ -1393,7 +1513,7 @@ let build_proof *) final_subst, proof, open_goals ;; - +*) (* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *) @@ -1411,20 +1531,19 @@ let pump_actives context bag maxm active passive saturation_steps max_time = let passive_l = fst passive in let ma = max_l active_l in let mp = max_l passive_l in - assert (maxm > max ma mp); - let eq_uri = - match LibraryObjects.eq_URI () with - | None -> assert false - | Some uri -> uri - in - let env = [],context,CicUniv.empty_ugraph in - match - given_clause bag eq_uri env ([],[]) passive active 0 saturation_steps max_time - with - | ParamodulationFailure (_,a,p) -> - a, p, !maxmeta - | ParamodulationSuccess _ -> - assert false + assert (maxm > max ma mp); + match LibraryObjects.eq_URI () with + | None -> active, passive, !maxmeta + | Some eq_uri -> + let env = [],context,CicUniv.empty_ugraph in + (match + given_clause bag eq_uri env ([],[]) + passive active 0 saturation_steps max_time + with + | ParamodulationFailure (_,a,p) -> + a, p, !maxmeta + | ParamodulationSuccess _ -> + assert false) ;; let all_subsumed bag maxm status active passive = @@ -1481,7 +1600,8 @@ let given_clause let eq_uri = eq_of_goal type_of_goal in let cleaned_goal = Utils.remove_local_context type_of_goal in Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) - let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in + let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in + let goal = [], metasenv', cleaned_goal in let env = metasenv,context,CicUniv.empty_ugraph in prerr_endline ">>>>>> ACTIVES >>>>>>>>"; List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e)) diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 81c84af35..00d745fd9 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -98,6 +98,12 @@ let metas_of_term term = | C.Meta _ as t -> TermSet.singleton t | C.Appl l -> List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l + | C.Lambda(n,s,t) -> + TermSet.union (aux s) (aux t) + | C.Prod(n,s,t) -> + TermSet.union (aux s) (aux t) + | C.LetIn(n,s,t) -> + TermSet.union (aux s) (aux t) | t -> TermSet.empty (* TODO: maybe add other cases? *) in aux term diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 16c0d1cd3..3379fbe77 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,12 +1,17 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Oct 23 23:15:05 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HMysql.dbd -> - term:Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic + term:Cic.term -> + params:(string * string) list -> + universe:Universe.universe -> + ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : - params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic + params:(string * string) list -> + dbd:HMysql.dbd -> + universe:Universe.universe -> + ProofEngineTypes.tactic val change : pattern:ProofEngineTypes.lazy_pattern -> Cic.lazy_term -> ProofEngineTypes.tactic -- 2.39.2