From 7cb22a7f8107a6cde0b77b7879e04f586a347102 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 20 Apr 2009 07:58:14 +0000 Subject: [PATCH] - init_cache_and_tables rewritten using the automation_cache - new moo command Select to index an equality - new command pump to perform some given clause steps on the automation cache tables - no more imperative maxmeta in paramodulation: - paramodulation/* forlds a bag containing it - auto.ml folds tables, containing a bag --- .../components/binaries/transcript/.depend | 5 + .../software/components/grafite/grafiteAst.ml | 4 +- .../components/grafite/grafiteAstPp.ml | 1 + .../components/grafite/grafiteMarshal.ml | 2 + .../grafite_engine/grafiteEngine.ml | 16 + .../components/grafite_engine/grafiteSync.ml | 48 +- .../grafite_parser/grafiteDisambiguate.ml | 4 + .../grafite_parser/grafiteParser.ml | 2 + helm/software/components/tactics/.depend | 18 +- helm/software/components/tactics/.depend.opt | 31 +- helm/software/components/tactics/auto.ml | 541 +++++++++--------- .../components/tactics/automationCache.ml | 89 ++- .../components/tactics/automationCache.mli | 15 +- .../tactics/paramodulation/equality.ml | 122 ++-- .../tactics/paramodulation/equality.mli | 24 +- .../tactics/paramodulation/indexing.ml | 87 ++- .../tactics/paramodulation/indexing.mli | 12 +- .../tactics/paramodulation/saturation.ml | 516 ++++++++--------- .../tactics/paramodulation/saturation.mli | 17 +- helm/software/components/tactics/universe.ml | 6 +- helm/software/components/tactics/universe.mli | 6 + .../matita/library/demo/power_derivative.ma | 2 +- .../demo/propositional_sequent_calculus.ma | 4 +- .../library/didactic/exercises/duality.ma | 2 +- .../library/didactic/exercises/shannon.ma | 4 +- .../didactic/exercises/substitution.ma | 8 +- helm/software/matita/library/nat/gcd.ma | 3 +- helm/software/matita/library/nat/ord.ma | 5 +- helm/software/matita/library/nat/times.ma | 4 +- 29 files changed, 878 insertions(+), 720 deletions(-) diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index bb6f22a64..87d1ed25c 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 2e6f450ca..01053ca13 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -167,10 +167,12 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 17 +let magic = 18 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) + | Select of loc * UriManager.uri + | Pump of loc * int | Coercion of loc * 'term * bool (* add_obj *) * int (* arity *) * int (* saturations *) | PreferCoercion of loc * 'term diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 95600c182..4e10cfa8b 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -327,6 +327,7 @@ let pp_coercion ~term_pp t do_composites arity saturations= let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri + | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri | Coercion (_, t, do_composites, i, j) -> pp_coercion ~term_pp t do_composites i j | PreferCoercion (_,t) -> diff --git a/helm/software/components/grafite/grafiteMarshal.ml b/helm/software/components/grafite/grafiteMarshal.ml index 48525aed5..481a1b21d 100644 --- a/helm/software/components/grafite/grafiteMarshal.ml +++ b/helm/software/components/grafite/grafiteMarshal.ml @@ -50,6 +50,8 @@ let rehash_cmd_uris = GrafiteAst.Coercion (loc, CicUtil.rehash_term uri, close, arity, saturations) | GrafiteAst.Index (loc, key, uri) -> GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri) + | GrafiteAst.Select (loc, uri) -> + GrafiteAst.Select (loc, rehash_uri uri) | cmd -> prerr_endline "Found a command not expected in a .moo:"; let term_pp _ = assert false in diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 1f32e8c9e..c06750039 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -649,6 +649,22 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status *) let status = GrafiteTypes.add_moo_content [cmd] status in status,[] + | GrafiteAst.Select (_,uri) as cmd -> + if List.mem cmd status.GrafiteTypes.moo_content_rev then status, [] + else + let cache = + AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache + [] [] [] (CicUtil.term_of_uri uri) None + in + let status = { status with GrafiteTypes.automation_cache = cache } in + let status = GrafiteTypes.add_moo_content [cmd] status in + status, [] + | GrafiteAst.Pump (_,steps) -> + let cache = + AutomationCache.pump status.GrafiteTypes.automation_cache steps + in + let status = { status with GrafiteTypes.automation_cache = cache } in + status, [] | GrafiteAst.PreferCoercion (loc, coercion) -> eval_prefer_coercion status coercion | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 999d96136..759186c12 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -54,10 +54,27 @@ let uris_for_inductive_type uri obj = in uris | _ -> [uri] ;; + +let is_equational_fact ty = + let rec aux ctx t = + match CicReduction.whd ctx t with + | Cic.Prod (name,src,tgt) -> + let s,u = + CicTypeChecker.type_of_aux' [] ctx src CicUniv.oblivion_ugraph + in + if fst (CicReduction.are_convertible ctx s (Cic.Sort Cic.Prop) u) then + false + else + aux (Some (name,Cic.Decl src)::ctx) tgt + | Cic.Appl [ Cic.MutInd (u,_,_) ; _; _; _] -> LibraryObjects.is_eq_URI u + | _ -> false + in + aux [] ty +;; let add_obj ~pack_coercion_obj uri obj status = let lemmas = LibrarySync.add_obj ~pack_coercion_obj uri obj in - let add_to_universe (universe,status) uri = + let add_to_universe (automation_cache,status) uri = let term = CicUtil.term_of_uri uri in let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in let tkeys = Universe.keys [] ty in @@ -66,24 +83,39 @@ let add_obj ~pack_coercion_obj uri obj status = (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri)) tkeys in - let universe = Universe.index_term_and_unfolded_term universe [] term ty + let is_equational = is_equational_fact ty in + let select_cmd = + if is_equational then + [ GrafiteAst.Select(HExtlib.dummy_floc,uri) ] + else + [] + in + let universe = automation_cache.AutomationCache.univ in + let universe = Universe.index_term_and_unfolded_term universe [] term ty in + let automation_cache = + if is_equational then + AutomationCache.add_term_to_active automation_cache [] [] [] term None + else + automation_cache in + let automation_cache = + { automation_cache with AutomationCache.univ = universe } in let status = GrafiteTypes.add_moo_content index_cmd status in - (universe,status) + let status = GrafiteTypes.add_moo_content select_cmd status in + (automation_cache,status) in let uris_to_index = if is_a_variant obj then [] else (uris_for_inductive_type uri obj) @ lemmas in - let universe,status = + let automation_cache,status = List.fold_left add_to_universe - (status.GrafiteTypes.automation_cache.AutomationCache.univ,status) + (status.GrafiteTypes.automation_cache,status) uris_to_index in - let cache = { status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } in {status with GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects; - GrafiteTypes.automation_cache = cache }, + GrafiteTypes.automation_cache = automation_cache}, lemmas let add_coercion ~pack_coercion_obj ~add_composites status uri arity @@ -121,7 +153,7 @@ let initial_status lexicon_status baseuri = { proof_status = GrafiteTypes.No_proof; objects = []; coercions = CoercDb.empty_coerc_db; - automation_cache = AutomationCache.empty; + automation_cache = AutomationCache.empty (); baseuri = baseuri; ng_status = GrafiteTypes.CommandMode lexicon_status; } diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 323c8985e..76d553379 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -752,6 +752,10 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= in let metasenv,key = disambiguate_term_option metasenv key in !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri) + | GrafiteAst.Select (loc,uri) -> + lexicon_status, metasenv, GrafiteAst.Select(loc,uri) + | GrafiteAst.Pump(loc,i) -> + lexicon_status, metasenv, GrafiteAst.Pump(loc,i) | GrafiteAst.PreferCoercion (loc,t) -> let lexicon_status_ref = ref lexicon_status in let disambiguate_term = diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 2a5d3c0b0..b6930bf0d 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -743,6 +743,8 @@ EXTEND (loc, t, composites, arity, saturations) | IDENT "prefer" ; IDENT "coercion"; t = tactic_term -> GrafiteAst.PreferCoercion (loc, t) + | IDENT "pump" ; steps = int -> + GrafiteAst.Pump(loc,steps) | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> GrafiteAst.UnificationHint (loc, t, n) | IDENT "record" ; (params,name,ty,fields) = record_spec -> diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 9dca5c5fb..e7aa8868d 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -31,7 +31,7 @@ introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi -auto.cmi: universe.cmi proofEngineTypes.cmi +auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi inversion_principle.cmi: @@ -42,8 +42,8 @@ fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi -tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi -declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi +tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi +declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi @@ -118,9 +118,9 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ paramodulation/indexing.cmx paramodulation/founif.cmx \ paramodulation/equality.cmx paramodulation/saturation.cmi -automationCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ +automationCache.cmo: universe.cmi paramodulation/saturation.cmi \ automationCache.cmi -automationCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ +automationCache.cmx: universe.cmx paramodulation/saturation.cmx \ automationCache.cmi variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ variousTactics.cmi @@ -155,13 +155,13 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ auto.cmo: paramodulation/utils.cmi universe.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 + equalityTactics.cmi paramodulation/equality.cmi automationCache.cmi \ + autoTypes.cmi autoCache.cmi auto.cmi auto.cmx: paramodulation/utils.cmx universe.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 + equalityTactics.cmx paramodulation/equality.cmx automationCache.cmx \ + autoTypes.cmx autoCache.cmx auto.cmi destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index a278f6f08..03e70f034 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -1,11 +1,19 @@ +proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi +proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi +hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi +universe.cmi: autoTypes.cmi: proofEngineTypes.cmi +autoCache.cmi: +paramodulation/utils.cmi: +closeCoercionGraph.cmi: +paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -16,22 +24,27 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ paramodulation/indexing.cmi paramodulation/equality.cmi +automationCache.cmi: universe.cmi paramodulation/saturation.cmi \ + paramodulation/equality.cmi variousTactics.cmi: proofEngineTypes.cmi compose.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi -auto.cmi: universe.cmi proofEngineTypes.cmi +auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi +inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi +fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi +history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi -tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi -declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi +tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi +declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi @@ -106,6 +119,10 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ paramodulation/indexing.cmx paramodulation/founif.cmx \ paramodulation/equality.cmx paramodulation/saturation.cmi +automationCache.cmo: universe.cmi paramodulation/saturation.cmi \ + paramodulation/equality.cmi automationCache.cmi +automationCache.cmx: universe.cmx paramodulation/saturation.cmx \ + paramodulation/equality.cmx automationCache.cmi variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ variousTactics.cmi variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ @@ -139,13 +156,13 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ auto.cmo: paramodulation/utils.cmi universe.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 + equalityTactics.cmi paramodulation/equality.cmi automationCache.cmi \ + autoTypes.cmi autoCache.cmi auto.cmi auto.cmx: paramodulation/utils.cmx universe.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 + equalityTactics.cmx paramodulation/equality.cmx automationCache.cmx \ + autoTypes.cmx autoCache.cmx auto.cmi destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index a01ca8691..0e4394823 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1,5 +1,4 @@ (* Copyright (C) 2002, HELM Team. - * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -191,7 +190,8 @@ let lambda_close ?prefix_name t menv ctx = (* functions for retrieving theorems *) -exception FillingFailure of AutoCache.cache * int + +exception FillingFailure of AutoCache.cache * AutomationCache.tables let rec unfold context = function | Cic.Prod(name,s,t) -> @@ -231,7 +231,7 @@ let partition_equalities = List.partition (fun (_,ty) -> is_an_equality ty) -let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;; +let default_auto tables _ cache _ _ _ _ = [],cache,tables ;; (* giusto per provare che succede let is_unit_equation context metasenv oldnewmeta term = @@ -324,7 +324,7 @@ let retrieve_equations dont_filter signature universe cache context metasenv = (only (MetadataConstraints.UriManagerSet.add eq_uri signature) context metasenv) candidates -let build_equality bag head args proof newmetas maxmeta = +let build_equality bag head args proof newmetas = match head with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] -> let p = @@ -335,58 +335,97 @@ let build_equality bag head args proof newmetas maxmeta = (* let w = compute_equality_weight stat in *) let w = 0 in let proof = Equality.Exact p in - let e = Equality.mk_equality bag (w, proof, stat, newmetas) in + let bag, e = Equality.mk_equality bag (w, proof, stat, newmetas) in (* to clean the local context of metas *) - Equality.fix_metas bag maxmeta e + Equality.fix_metas bag e | _ -> assert false ;; let partition_unit_equalities context metasenv newmeta bag equations = List.fold_left - (fun (units,other,maxmeta)(t,ty) -> + (fun (bag,units,other,maxmeta)(t,ty) -> if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then let _ = HLog.warn ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context ^ " since it is not meta closed") in - units,(t,ty)::other,maxmeta + bag, units,(t,ty)::other,maxmeta else match is_unit_equation context metasenv maxmeta ty with | Some (args,metasenv,newmetas,head,newmeta') -> - let maxmeta,equality = - build_equality bag head args t newmetas newmeta' in - equality::units,other,maxmeta + let bag, equality = + build_equality bag head args t newmetas in + bag, equality::units,other,maxmeta | None -> - units,(t,ty)::other,maxmeta) - ([],[],newmeta) equations - -let empty_tables = - (Saturation.make_active [], - Saturation.make_passive [], - Equality.mk_equality_bag) - + bag, units,(t,ty)::other,maxmeta) + (bag,[],[],newmeta) equations +;; let init_cache_and_tables - ?dbd use_library paramod use_context dont_filter universe (proof, goal) + ?dbd ~use_library ~use_context + automation_cache restricted_univ (proof, goal) = - (* the local cache in initially empty *) - let cache = AutoCache.cache_empty in - let _, metasenv, _subst,_, _, _ = proof in - let signature = MetadataQuery.signature_of metasenv goal in - let newmeta = CicMkImplicit.new_meta metasenv [] in + let _, metasenv, _, _, _, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let ct = if use_context then find_context_theorems context metasenv else [] in - debug_print - (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct)))); - let lt = - match use_library, dbd with - | true, Some dbd -> find_library_theorems dbd metasenv goal - | _ -> [] - in - debug_print - (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt)))); - let cache = cache_add_list cache context (ct@lt) in + if restricted_univ = [] then + let ct = + if use_context then find_context_theorems context metasenv else [] + in + let lt = + match use_library, dbd with + | true, Some dbd -> find_library_theorems dbd metasenv goal + | _ -> [] + in + let cache = AutoCache.cache_empty in + let cache = cache_add_list cache context (ct@lt) in + let tables = + let env = metasenv, context, CicUniv.oblivion_ugraph in + List.fold_left + (fun (a,p,b) (t,ty) -> + let mes = CicUtil.metas_of_term ty in + Saturation.add_to_active b a p env ty t + (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv)) + automation_cache.AutomationCache.tables ct + in + automation_cache.AutomationCache.univ, tables, cache + else + let metasenv, t_ty, s_t_ty, _ = + List.fold_left + (fun (metasenv,acc, sacc, maxmeta) t -> + let ty, _ = + CicTypeChecker.type_of_aux' + metasenv ~subst:[] context t CicUniv.oblivion_ugraph + in + let head, metasenv, args, maxmeta = + TermUtil.saturate_term maxmeta metasenv context ty 0 + in + let st = if args = [] then t else Cic.Appl (t::args) in + metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta) + (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ + in + let automation_cache = AutomationCache.empty () in + let automation_cache = + let universe = automation_cache.AutomationCache.univ in + let universe = + Universe.index_list universe context t_ty + in + { automation_cache with AutomationCache.univ = universe } + in + let automation_cache = + List.fold_left + (fun c (t,ty) -> + AutomationCache.add_term_to_active c metasenv [] context t (Some ty)) + automation_cache s_t_ty + in +(* AutomationCache.pp_cache automation_cache; *) + automation_cache.AutomationCache.univ, + automation_cache.AutomationCache.tables, + cache_add_list cache_empty context t_ty +;; + (* +(* let signature = MetadataQuery.signature_of metasenv goal in *) +(* let newmeta = CicMkImplicit.new_meta metasenv [] in *) let equations = retrieve_equations dont_filter (* true *) signature universe cache context metasenv in @@ -429,11 +468,14 @@ let init_cache_and_tables context bag newmeta active passive (no+1) infinity in (active,passive,bag),cache,newmeta +*) -let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = - let head, metasenv, args, newmeta = - TermUtil.saturate_term oldnewmeta metasenv context term 0 +let fill_hypothesis context metasenv term tables (universe:Universe.universe) cache auto fast = + let actives, passives, bag = tables in + let bag, head, metasenv, args = + Equality.saturate_term bag metasenv context term in + let tables = actives, passives, bag in let propositional_args = HExtlib.filter_map (function @@ -447,10 +489,11 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u | _ -> assert false) args in - let results,cache,newmeta = + let results,cache,tables = if propositional_args = [] then - let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in - [args,metasenv,newmetas,head,newmeta],cache,newmeta + let _,_,bag = tables in + let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in + [args,metasenv,newmetas,head],cache,tables else (* let proof = @@ -468,54 +511,59 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u maxwidth = 2;maxdepth = 4; use_paramod=true;use_only_paramod=false} in - match auto newmeta tables universe cache context metasenv propositional_args flags with - | [],cache,newmeta -> raise (FillingFailure (cache,newmeta)) - | substs,cache,newmeta -> - List.map - (fun subst -> + match auto tables universe cache context metasenv propositional_args flags with + | [],cache,tables -> raise (FillingFailure (cache,tables)) + | substs,cache,tables -> + let actives, passaives, bag = tables in + let bag, res = + List.fold_right + (fun subst (bag,acc) -> let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let head = CicMetaSubst.apply_subst subst head in - let newmetas = - List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv - in + let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in let args = List.map (CicMetaSubst.apply_subst subst) args in let newm = CicMkImplicit.new_meta metasenv subst in - args,metasenv,newmetas,head,max newm newmeta) - substs, cache, newmeta + let bag = Equality.push_maxmeta bag newm in + bag, ((args,metasenv,newmetas,head) :: acc)) + substs (bag,[]) + in + let tables = actives, passives, bag in + res, cache, tables in - results,cache,newmeta + results,cache,tables +;; -let build_equalities auto context metasenv tables universe cache newmeta equations = +let build_equalities auto context metasenv tables universe cache equations = List.fold_left - (fun (facts,cache,newmeta) (t,ty) -> + (fun (tables,facts,cache) (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 universe cache auto true + let saturated, cache, tables = + fill_hypothesis context metasenv ty tables universe cache auto true in - let (active,passive,bag) = tables in - let eqs,bag,newmeta = + let eqs, tables = List.fold_left - (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') -> - let maxmeta,equality = - build_equality bag head args t newmetas newmeta' + (fun (acc, tables) (args,metasenv,newmetas,head) -> + let actives, passives, bag = tables in + let bag, equality = + build_equality bag head args t newmetas in - equality::acc,bag,maxmeta) - ([],bag,newmeta) saturated + let tables = actives, passives, bag in + equality::acc,tables) + ([],tables) saturated in - (eqs@facts, cache, newmeta) - with FillingFailure (cache,newmeta) -> + (tables, eqs@facts, cache) + with FillingFailure (cache,tables) -> (* if filling hypothesis fails we add the equation to the cache *) - (facts,cache,newmeta) + (tables,facts,cache) ) - ([],cache,newmeta) equations + (tables,[],cache) equations -let close_more tables maxmeta context status auto universe cache = - let (active,passive,bag) = tables in +let close_more tables context status auto universe cache = let proof, goalno = status in let _, metasenv,_subst,_,_, _ = proof in let signature = MetadataQuery.signature_of metasenv goalno in @@ -531,81 +579,75 @@ let close_more tables maxmeta context status auto universe cache = (* retrieve_equations could also return flexible terms *) if is_an_equality ty then Some(t,ty) else None) equations in - let units, cache, maxm = - build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in - debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ - string_of_int maxm)); - List.iter - (fun e -> debug_print (lazy (Equality.string_of_equality e))) - units; - debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>"); + let tables, units, cache = + build_equalities auto context metasenv tables universe cache eqs_and_types + in + let active,passive,bag = tables in let passive = Saturation.add_to_passive units passive in let no = List.length units in - debug_print (lazy ("No = " ^ (string_of_int no))); - let active,passive,newmeta = - Saturation.pump_actives context bag maxm active passive (no+1) infinity + let active, passive, bag = + Saturation.pump_actives context bag active passive (no+1) infinity in - (active,passive,bag),cache,newmeta + (active,passive,bag), cache +;; -let find_context_equalities - maxmeta bag context proof (universe:Universe.universe) cache +let find_context_equalities tables context proof (universe:Universe.universe) cache = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in let _,metasenv,_subst,_,_, _ = proof in - let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in (* if use_auto is true, we try to close the hypothesis of equational statements using auto; a naif, and probably wrong approach *) - let rec aux cache index newmeta = function - | [] -> [], newmeta,cache + let rec aux tables cache index = function + | [] -> tables, [], cache | (Some (_, C.Decl (term)))::tl -> debug_print (lazy (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term))); - let do_find context term = + let do_find tables context term = match term with | C.Prod (name, s, t) when is_an_equality t -> (try - let term = S.lift index term in - let saturated,cache,newmeta = - fill_hypothesis context metasenv newmeta term - empty_tables universe cache default_auto false + let saturated, cache, tables = + fill_hypothesis context metasenv term + tables universe cache default_auto false in - let eqs,newmeta = + let actives, passives, bag = tables in + let bag,eqs = List.fold_left - (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> - let newmeta, equality = - build_equality - bag head args (Cic.Rel index) newmetas (max newmeta newmeta') + (fun (bag,acc) (args,metasenv,newmetas,head) -> + let bag, equality = + build_equality bag head args (Cic.Rel index) newmetas in - equality::acc, newmeta + 1) - ([],newmeta) saturated + bag, equality::acc) + (bag,[]) saturated in - eqs, newmeta, cache - with FillingFailure (cache,newmeta) -> - [],newmeta,cache) + let tables = actives, passives, bag in + tables, eqs, cache + with FillingFailure (cache,tables) -> + tables, [], cache) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when LibraryObjects.is_eq_URI uri -> let term = S.lift index term in - let newmeta, e = - build_equality bag term [] (Cic.Rel index) [] newmeta + let actives, passives, bag = tables in + let bag, e = + build_equality bag term [] (Cic.Rel index) [] in - [e], (newmeta+1),cache - | _ -> [], newmeta, cache + let tables = actives, passives, bag in + tables, [e], cache + | _ -> tables, [], cache in - let eqs, newmeta, cache = do_find context term in - let rest, newmeta,cache = aux cache (index+1) newmeta tl in - List.map (fun x -> index,x) eqs @ rest, newmeta, cache + let tables, eqs, cache = do_find tables context term in + let tables, rest, cache = aux tables cache (index+1) tl in + tables, List.map (fun x -> index,x) eqs @ rest, cache | _::tl -> - aux cache (index+1) newmeta tl - in - let il, maxm, cache = - aux cache 1 newmeta context + aux tables cache (index+1) tl in + let tables, il, cache = aux tables cache 1 context in let indexes, equalities = List.split il in - indexes, equalities, maxm, cache + tables, indexes, equalities, cache ;; (********** PARAMETERS PASSING ***************) @@ -673,23 +715,10 @@ let flags_of_params params ?(for_applyS=false) () = AutoTypes.skip_context = skip_context; } -let universe_of_params metasenv context universe tl = - if tl = [] then universe else - let tys = - List.map - (fun term -> - fst (CicTypeChecker.type_of_aux' metasenv context term - CicUniv.oblivion_ugraph)) - tl - in - Universe.index_list Universe.empty context (List.combine tl tys) -;; - - (***************** applyS *******************) -let new_metasenv_and_unify_and_t - dbd flags automation_cache proof goal ?tables newmeta' metasenv' +let apply_smart_aux + dbd flags automation_cache univ proof goal newmeta' metasenv' context term' ty termty goal_arity = (* let ppterm = ppterm context in *) @@ -728,20 +757,18 @@ let new_metasenv_and_unify_and_t (PrimitiveTactics.apply_tac term'') (proof''',goal) in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ in - let (active, passive,bag), cache, maxm = - init_cache_and_tables ~dbd flags.use_library false (* was true *) - true false universe - (proof'''',newmeta) - in + let universe, tables, cache = + init_cache_and_tables ~dbd ~use_library:flags.use_library + ~use_context:true automation_cache univ (proof'''',newmeta) + in + let active, passive, bag = tables in match - Saturation.given_clause bag maxm (proof'''',newmeta) active passive + Saturation.given_clause bag (proof'''',newmeta) active passive 20 10 flags.timeout with | None, _,_,_ -> raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) - | Some (_,proof''''',_), active,passive,_ -> + | Some (_,proof''''',_), active,passive,bag -> proof''''', ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive @@ -766,7 +793,7 @@ let rec count_prods context ty = | _ -> 0 let apply_smart - ~dbd ~term ~subst ~automation_cache ?tables ~params:(univ,params) (proof, goal) + ~dbd ~term ~subst ~automation_cache ~params:(univ,params) (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in @@ -774,11 +801,6 @@ let apply_smart let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params ~for_applyS:true () in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ in - let universe = universe_of_params metasenv context universe univ in - let automation_cache = { automation_cache with AutomationCache.univ = universe } in - let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -819,7 +841,7 @@ let apply_smart let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in let goal_arity = count_prods context ty in let proof, gl, active, passive = - new_metasenv_and_unify_and_t dbd flags automation_cache proof goal ?tables + apply_smart_aux dbd flags automation_cache univ proof goal newmeta' metasenv' context term' ty termty goal_arity in proof, gl, active, passive @@ -865,8 +887,6 @@ type goal = ProofEngineTypes.goal * int * AutoTypes.sort let candidate_no = ref 0;; type candidate = int * Cic.term Lazy.t type cache = AutoCache.cache -type tables = - Saturation.active_table * Saturation.passive_table * Equality.equality_bag type fail = (* the goal (mainly for depth) and key of the goal *) @@ -885,9 +905,9 @@ type status = * end with the same (S(g,_)) *) elem list type auto_result = - (* menv, subst, alternatives, tables, cache, maxmeta *) - | Proved of menv * subst * elem list * tables * cache * int - | Gaveup of tables * cache * int + (* menv, subst, alternatives, tables, cache *) + | Proved of menv * subst * elem list * AutomationCache.tables * cache + | Gaveup of AutomationCache.tables * cache (* the status exported to the external observer *) @@ -1203,7 +1223,7 @@ let mk_fake_proof metasenv subst (goalno,_,_) goalty context = None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] ;; let equational_case - tables maxm cache depth fake_proof goalno goalty subst context + tables cache depth fake_proof goalno goalty subst context flags = let active,passive,bag = tables in @@ -1218,13 +1238,13 @@ let equational_case in match - Saturation.given_clause bag maxm status active passive + Saturation.given_clause bag status active passive goal_steps saturation_steps timeout with - | None, active, passive, maxmeta -> - [], (active,passive,bag), cache, maxmeta, flags + | None, active, passive, bag -> + [], (active,passive,bag), cache, flags | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active, - passive,maxmeta -> + passive,bag -> assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = @@ -1234,19 +1254,15 @@ let equational_case List.map (fun (x,sort) -> x,depth-1,sort) open_goals in incr candidate_no; - [(!candidate_no,proof),metasenv,subst,open_goals], - (active,passive,bag), - cache, maxmeta, flags + [(!candidate_no,proof),metasenv,subst,open_goals], + (active,passive,bag), cache, flags end else begin debug_print (lazy ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty)); - let res, maxmeta = - Saturation.all_subsumed bag maxm status active passive - in - assert (maxmeta >= maxm); + let res = Saturation.all_subsumed bag status active passive in let res' = List.map (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) -> @@ -1262,28 +1278,30 @@ let equational_case (!candidate_no,proof),metasenv,subst,open_goals) res in - res', (active,passive,bag), cache, maxmeta, flags + res', (active,passive,bag), cache, flags end ;; let try_candidate - goalty tables maxm subst fake_proof goalno depth context cand + goalty tables subst fake_proof goalno depth context cand = let ppterm = ppterm context in try + let actives, passives, bag = tables in let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta = - (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand) + (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:(Equality.maxmeta bag) ~term:cand) (fake_proof,goalno) in + let tables = actives, passives, Equality.push_maxmeta bag maxmeta in debug_print (lazy (" OK: " ^ ppterm cand)); let metasenv = CicRefine.pack_coercion_metasenv metasenv 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 incr candidate_no; - Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta + Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables with - | ProofEngineTypes.Fail s -> None,tables, maxm - | CicUnification.Uncertain s -> None,tables, maxm + | ProofEngineTypes.Fail s -> None,tables + | CicUnification.Uncertain s -> None,tables ;; let sort_new_elems = @@ -1292,52 +1310,50 @@ let sort_new_elems = ;; let applicative_case - tables maxm depth subst fake_proof goalno goalty metasenv context universe + tables depth subst fake_proof goalno goalty metasenv context universe cache flags = let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in - let tables, elems, maxm = + let tables, elems = List.fold_left - (fun (tables,elems,maxm) cand -> + (fun (tables,elems) cand -> match try_candidate goalty - tables maxm subst fake_proof goalno depth context cand + tables subst fake_proof goalno depth context cand with - | None, tables,maxm -> tables,elems, maxm - | Some x, tables, maxm -> tables,x::elems, maxm) - (tables,[],maxm) candidates + | None, tables -> tables, elems + | Some x, tables -> tables, x::elems) + (tables,[]) candidates in let elems = sort_new_elems elems in - elems, tables, cache, maxm + elems, tables, cache ;; let equational_and_applicative_case - universe flags m s g gty tables cache maxm context + universe flags m s g gty tables cache context = let goalno, depth, sort = g in let fake_proof = mk_fake_proof m s g gty context in if is_equational_case gty flags then - let elems,tables,cache,maxm1, flags = - equational_case tables maxm cache + let elems,tables,cache, flags = + equational_case tables cache depth fake_proof goalno gty s context flags in - let maxm = maxm1 in - let more_elems, tables, cache, maxm1 = + let more_elems, tables, cache = if flags.use_only_paramod then - [],tables, cache, maxm + [],tables, cache else applicative_case - tables maxm depth s fake_proof goalno + tables depth s fake_proof goalno gty m context universe cache flags in - let maxm = maxm1 in - elems@more_elems, tables, cache, maxm, flags + elems@more_elems, tables, cache, flags else - let elems, tables, cache, maxm = - applicative_case tables maxm depth s fake_proof goalno + let elems, tables, cache = + applicative_case tables depth s fake_proof goalno gty m context universe cache flags in - elems, tables, cache, maxm, flags + elems, tables, cache, flags ;; let rec condition_for_hint i = function | [] -> false @@ -1430,9 +1446,9 @@ let filter_prune_hint l = if prune = [] then l else List.filter (condition_for_prune_hint prune) l ;; -let auto_main tables maxm context flags universe cache elems = +let auto_main tables context flags universe cache elems = auto_context := context; - let rec aux tables maxm flags cache (elems : status) = + let rec aux tables flags cache (elems : status) = (* pp_status context elems; *) (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration auto_status := elems; @@ -1444,23 +1460,23 @@ let auto_main tables maxm context flags universe cache elems = debug_print (lazy "skip"); (match !hint with | Some i when condition_for_hint i todo -> - aux tables maxm flags cache orlist + aux tables flags cache orlist | _ -> hint := None; - aux tables maxm flags cache elems) + aux tables flags cache elems) | [] -> (* complete failure *) debug_print (lazy "give up"); - Gaveup (tables, cache, maxm) + Gaveup (tables, cache) | (m, s, _, _, [],_)::orlist -> (* complete success *) debug_print (lazy "success"); - Proved (m, s, orlist, tables, cache, maxm) + Proved (m, s, orlist, tables, cache) | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist when not flags.AutoTypes.do_types -> (* skip since not Prop, don't even check if closed by side-effect *) debug_print (lazy "skip existential goal"); - aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist) + aux tables flags cache ((m, s, size, don, todo, fl)::orlist) | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist -> (* partial success, cache g and go on *) let cache, orlist, fl, sibling_pruned = @@ -1470,24 +1486,24 @@ let auto_main tables maxm context flags universe cache elems = debug_print (lazy (AutoCache.cache_print context cache)); let fl = remove_s_from_fl g fl in let don = if sibling_pruned then don else op::don in - aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist) + aux tables flags cache ((m, s, size, don, todo, fl)::orlist) | (m, s, size, don, todo, fl)::orlist when List.length(prop_only (d_goals todo)) > flags.maxwidth -> debug_print (lazy ("FAIL: WIDTH")); (* too many goals in and generated by last th *) let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize -> debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^ " > " ^ string_of_int flags.maxsize )); (* we already have a too large proof term *) let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | _ when Unix.gettimeofday () > flags.timeout -> (* timeout *) debug_print (lazy ("FAIL: TIMEOUT")); - Gaveup (tables, cache, maxm) + Gaveup (tables, cache) | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status -> (* attack g *) debug_print (lazy "attack goal"); @@ -1495,17 +1511,17 @@ let auto_main tables maxm context flags universe cache elems = | None -> (* closed by side effect *) debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno)); - aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist) + aux tables flags cache ((m,s,size,don,todo, fl)::orlist) | Some (canonical_ctx, gty) -> let gsize, _ = Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty in if gsize > flags.maxgoalsizefactor then (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize)); - aux tables maxm flags cache orlist) + aux tables flags cache orlist) else if prunable_for_size flags s m todo then (debug_print (lazy ("POTO at depth: "^(string_of_int depth))); - aux tables maxm flags cache orlist) + aux tables flags cache orlist) else (* still to be proved *) (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty)); @@ -1514,23 +1530,23 @@ let auto_main tables maxm context flags universe cache elems = (* fail depth *) debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno)); let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | UnderInspection -> (* fail loop *) debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno)); let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | Succeded t -> debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno)); let s, m = put_in_subst s m g canonical_ctx t gty in - aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist) + aux tables flags cache ((m, s, size, don,todo, fl)::orlist) | Notfound | Failed_in _ when depth > 0 -> ( (* more depth or is the first time we see the goal *) if prunable m s gty todo then (debug_print (lazy( "FAIL: LOOP: one father is equal")); - aux tables maxm flags cache orlist) + aux tables flags cache orlist) else let cache = cache_add_underinspection cache gty depth in auto_status := status; @@ -1540,14 +1556,14 @@ let auto_main tables maxm context flags universe cache elems = string_of_int gno ^ "("^ string_of_int size ^ "): "^ CicPp.ppterm gty)); (* elems are possible computations for proving gty *) - let elems, tables, cache, maxm, flags = + let elems, tables, cache, flags = equational_and_applicative_case - universe flags m s g gty tables cache maxm context + universe flags m s g gty tables cache context in if elems = [] then (* this goal has failed *) let cache = close_failures ((g,gty)::fl) cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist else (* elems = (cand,m,s,gl) *) let size_gl l = List.length @@ -1577,19 +1593,19 @@ let auto_main tables maxm context flags universe cache elems = in map elems in - aux tables maxm flags cache elems) + aux tables flags cache elems) | _ -> (* no more depth *) debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno)); let cache = close_failures fl cache in - aux tables maxm flags cache orlist) + aux tables flags cache orlist) in - (aux tables maxm flags cache elems : auto_result) + (aux tables flags cache elems : auto_result) ;; let - auto_all_solutions maxm tables universe cache context metasenv gl flags + auto_all_solutions tables universe cache context metasenv gl flags = let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = @@ -1597,20 +1613,20 @@ let (fun (x,s) -> D (x,flags.maxdepth,s)) goals in let elems = [metasenv,[],1,[],goals,[]] in - let rec aux tables maxm solutions cache elems flags = - match auto_main tables maxm context flags universe cache elems with - | Gaveup (tables,cache,maxm) -> - solutions,cache,maxm - | Proved (metasenv,subst,others,tables,cache,maxm) -> + let rec aux tables solutions cache elems flags = + match auto_main tables context flags universe cache elems with + | Gaveup (tables,cache) -> + solutions,cache, tables + | Proved (metasenv,subst,others,tables,cache) -> if Unix.gettimeofday () > flags.timeout then - ((subst,metasenv)::solutions), cache, maxm + ((subst,metasenv)::solutions), cache, tables else - aux tables maxm ((subst,metasenv)::solutions) cache others flags + aux tables ((subst,metasenv)::solutions) cache others flags in - let rc = aux tables maxm [] cache elems flags in + let rc = aux tables [] cache elems flags in match rc with - | [],cache,maxm -> [],cache,maxm - | solutions,cache,maxm -> + | [],cache,tables -> [],cache,tables + | solutions, cache,tables -> let solutions = HExtlib.filter_map (fun (subst,newmetasenv) -> @@ -1620,7 +1636,7 @@ let if opened = [] then Some subst else None) solutions in - solutions,cache,maxm + solutions,cache,tables ;; (******************* AUTO ***************) @@ -1630,12 +1646,12 @@ let auto flags metasenv tables universe cache context metasenv gl = let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in let elems = [metasenv,[],1,[],goals,[]] in - match auto_main tables 0 context flags universe cache elems with - | Proved (metasenv,subst,_, tables,cache,_) -> + match auto_main tables context flags universe cache elems with + | Proved (metasenv,subst,_, tables,cache) -> debug_print(lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); Some (subst,metasenv), cache - | Gaveup (tables,cache,maxm) -> + | Gaveup (tables,cache) -> debug_print(lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); None,cache @@ -1655,30 +1671,29 @@ let applyS_tac ~dbd ~term ~params ~automation_cache = raise (ProofEngineTypes.Fail msg)) let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) = - let _,metasenv,_subst,_,_, _ = proof in - let _,context,goalty = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params () in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ 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 (not flags.skip_context) - false universe (proof, goal) in - let tables,cache,newmeta = + let universe, tables, cache = + init_cache_and_tables + ~dbd ~use_library ~use_context:(not flags.skip_context) + automation_cache univ (proof, goal) + in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,goalty = CicUtil.lookup_meta goal metasenv in + let tables,cache = if flags.close_more then close_more - tables newmeta context (proof, goal) + tables context (proof, goal) auto_all_solutions universe cache - else tables,cache,newmeta in + else tables,cache in let initial_time = Unix.gettimeofday() in let (_,oldmetasenv,_subst,_,_, _) = proof in hint := None; let elem = metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] in - match auto_main tables newmeta context flags universe cache [elem] with - | Proved (metasenv,subst,_, tables,cache,_) -> + match auto_main tables context flags universe cache [elem] with + | Proved (metasenv,subst,_, tables,cache) -> debug_print (lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); let proof,metasenv = @@ -1690,7 +1705,7 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa ~newmetasenv:metasenv in proof,opened - | Gaveup (tables,cache,maxm) -> + | Gaveup (tables,cache) -> debug_print (lazy ("TIME:"^ string_of_float(Unix.gettimeofday()-.initial_time))); @@ -1709,22 +1724,19 @@ let eq_of_goal = function (* performs steps of rewrite with the universe, obtaining if possible * a trivial goal *) let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)= + let steps = int_of_string (string params "steps" "1") in + let universe, tables, cache = + init_cache_and_tables ~use_library:false ~use_context:false + automation_cache univ (proof,goal) + in + let actives, passives, bag = tables in let _,metasenv,_subst,_,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in - let steps = int_of_string (string params "steps" "1") in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ in - let universe = universe_of_params metasenv context universe univ in let eq_uri = eq_of_goal ty in - let (active,passive,bag), cache, maxm = - (* we take the whole universe (no signature filtering) *) - init_cache_and_tables false true false true universe (proof,goal) - in let initgoal = [], metasenv, ty in let table = - let equalities = (Saturation.list_of_passive passive) in - (* we demodulate using both actives passives *) - List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities + let equalities = (Saturation.list_of_passive passives) in + List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities in let env = metasenv,context,CicUniv.oblivion_ugraph in match Indexing.solve_demodulating bag env table initgoal steps with @@ -1853,7 +1865,7 @@ let demodulate_theorem ~automation_cache uri = in let bag = Equality.mk_equality_bag () in - let units, _, newmeta = + let bag, units, _, newmeta = partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types in let table = @@ -1892,22 +1904,20 @@ let demodulate_theorem ~automation_cache uri = (* NEW DEMODULATE *) let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= - let curi,metasenv,_subst,pbo,pty, attrs = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ in - let universe = universe_of_params metasenv context universe univ in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let initgoal = [], metasenv, ty in + let universe, tables, cache = + init_cache_and_tables + ~dbd ~use_library:false ~use_context:true + automation_cache univ (proof,goal) + in let eq_uri = match LibraryObjects.eq_URI () with | Some (uri) -> uri | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in - (* let eq_uri = eq_of_goal ty in *) - let (active,passive,bag), cache, maxm = - init_cache_and_tables - ~dbd false false true true universe (proof,goal) - in + let active, passive, bag = tables in + let curi,metasenv,_subst,pbo,pty, attrs = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let initgoal = [], metasenv, ty in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let env = metasenv,context,CicUniv.empty_ugraph in @@ -1926,6 +1936,7 @@ let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= in if changed then begin + let maxm = CicMkImplicit.new_meta metasenv [] in let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in let proofterm,_ = Equality.build_goal_proof (~contextualize:false) bag diff --git a/helm/software/components/tactics/automationCache.ml b/helm/software/components/tactics/automationCache.ml index 84d4c8448..7d8e7d129 100644 --- a/helm/software/components/tactics/automationCache.ml +++ b/helm/software/components/tactics/automationCache.ml @@ -23,14 +23,97 @@ * http://cs.unibo.it/helm/. *) +type tables = + Saturation.active_table * Saturation.passive_table * Equality.equality_bag + type cache = { univ : Universe.universe; - tables : Saturation.active_table * Saturation.passive_table; + tables : Saturation.active_table * + Saturation.passive_table * + Equality.equality_bag; } +let empty_tables () = + Saturation.make_active [], + Saturation.make_passive [], + Equality.mk_equality_bag () +;; -let empty = { +let empty () = { univ = Universe.empty; - tables = (Saturation.make_active [], Saturation.make_passive []); + tables = empty_tables (); } +let pump cache steps = + let active, passive, bag = cache.tables in + let active, passive, bag = + Saturation.pump_actives + [] bag active passive steps infinity + in + let tables = active, passive, bag in + { cache with tables = tables } +;; + +let add_term_to_active cache metasenv subst context t ty_opt = + let actives, passives, bag = cache.tables in + let bag, metasenv, head, t, args, mes, ugraph = + match ty_opt with + | Some ty -> + bag, metasenv, ty, t, [], (CicUtil.metas_of_term (Cic.Appl [t;ty])), + CicUniv.oblivion_ugraph + | None -> + let ty, ugraph = + CicTypeChecker.type_of_aux' + ~subst metasenv context t CicUniv.oblivion_ugraph + in + let bag, head, metasenv, args = + Equality.saturate_term bag metasenv context ty + in + let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in + let t = if args = [] then t else Cic.Appl (t:: args) in + bag, metasenv, head, t, args, mes, ugraph + in + if List.exists + (function + | Cic.Meta(i,_) -> + (try + let _,mc, mt = CicUtil.lookup_meta i metasenv in + let sort, u = + CicTypeChecker.type_of_aux' metasenv mc mt ugraph + in + fst (CicReduction.are_convertible mc sort (Cic.Sort Cic.Prop) u) + with + | CicUtil.Meta_not_found _ -> false) + | _ -> assert false) + args + then + cache + else + let env = metasenv, context, CicUniv.oblivion_ugraph in + let newmetas = + List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv + in + let tables = + Saturation.add_to_active bag actives passives env head t newmetas + in + { cache with tables = tables } +;; + +let pp_cache cache = + prerr_endline "Automation cache"; + prerr_endline "----------------------------------------------"; + prerr_endline "universe:"; + Universe.iter cache.univ (fun _ ts -> + prerr_endline (" "^ + String.concat "\n " (List.map CicPp.ppterm ts))); + prerr_endline "tables/actives:"; + let active, passive, _ = cache.tables in + List.iter + (fun e -> prerr_endline (" " ^ Equality.string_of_equality e)) + (Saturation.list_of_active active); + prerr_endline "tables/passives:"; + List.iter + (fun e -> prerr_endline (" " ^ Equality.string_of_equality e)) + (Saturation.list_of_passive passive); + prerr_endline "----------------------------------------------"; +;; diff --git a/helm/software/components/tactics/automationCache.mli b/helm/software/components/tactics/automationCache.mli index 00fb516e2..8b032870f 100644 --- a/helm/software/components/tactics/automationCache.mli +++ b/helm/software/components/tactics/automationCache.mli @@ -23,11 +23,22 @@ * http://cs.unibo.it/helm/. *) +type tables = + Saturation.active_table * Saturation.passive_table * Equality.equality_bag + type cache = { univ : Universe.universe; - tables : Saturation.active_table * Saturation.passive_table; + tables : tables; } -val empty : cache +val empty_tables : unit -> tables +val empty : unit -> cache + +val add_term_to_active: + cache -> Cic.metasenv -> Cic.substitution -> Cic.context -> + Cic.term -> Cic.term option -> cache +val pump: cache -> int -> cache +val pp_cache: cache -> unit + diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 64f2faa7d..bf0e71bbd 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -1,4 +1,4 @@ -(* cOpyright (C) 2005, HELM Team. +(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -47,30 +47,26 @@ and proof = and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list ;; (* the hashtbl eq_id -> proof, max_eq_id *) -type equality_bag = (int,equality) Hashtbl.t * int ref +module IntOt = struct type t = int let compare = Pervasives.compare end +module M = Map.Make(IntOt) +type equality_bag = equality M.t * int type goal = goal_proof * Cic.metasenv * Cic.term (* globals *) -let mk_equality_bag () = - Hashtbl.create 1024, ref 0 -;; +let mk_equality_bag () = M.empty, 10000 ;; -let freshid (_,i) = - incr i; !i -;; +let freshid (m,i) = (m,i+1), i+1 ;; -let add_to_bag (id_to_eq,_) id eq = - Hashtbl.add id_to_eq id eq -;; +let add_to_bag (id_to_eq,i) id eq = M.add id eq id_to_eq,i ;; let uncomparable = fun _ -> 0 let mk_equality bag (weight,p,(ty,l,r,o),m) = - let id = freshid bag in + let bag, id = freshid bag in let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in - add_to_bag bag id eq; - eq + let bag = add_to_bag bag id eq in + bag, eq ;; let mk_tmp_equality (weight,(ty,l,r,o),m) = @@ -82,6 +78,11 @@ let mk_tmp_equality (weight,(ty,l,r,o),m) = let open_equality (_,weight,proof,(ty,l,r,o),m,id) = (weight,proof,(ty,l,r,o),m,id) +let id_of e = + let _,_,_,_,id = open_equality e in id +;; + + let string_of_rule = function | SuperpositionRight -> "SupR" | SuperpositionLeft -> "SupL" @@ -117,8 +118,8 @@ let rec max_weight_in_proof ((id_to_eq,_) as bag) current = function | Exact _ -> current | Step (_, (_,id1,(_,id2),_)) -> - let eq1 = Hashtbl.find id_to_eq id1 in - let eq2 = Hashtbl.find id_to_eq id2 in + let eq1 = M.find id1 id_to_eq in + let eq2 = M.find id2 id_to_eq in let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in let current = max current w1 in @@ -129,7 +130,7 @@ let rec max_weight_in_proof ((id_to_eq,_) as bag) current = let max_weight_in_goal_proof ((id_to_eq,_) as bag) = List.fold_left (fun current (_,_,id,_,_) -> - let eq = Hashtbl.find id_to_eq id in + let eq = M.find id id_to_eq in let (w,p,(_,_,_,_),_,_) = open_equality eq in let current = max current w in max_weight_in_proof bag current p) @@ -140,10 +141,17 @@ let max_weight bag goal_proof proof = let proof_of_id (id_to_eq,_) id = try - let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(_,l,r,_),_,_) = open_equality (M.find id id_to_eq) in p,l,r with - Not_found -> assert false + Not_found -> + prerr_endline ("Unable to find the proof of " ^ string_of_int id); + assert false +;; + +let is_in (id_to_eq,_) id = + M.mem id id_to_eq +;; let string_of_proof ?(names=[]) bag p gp = @@ -187,8 +195,8 @@ let rec depend ((id_to_eq,_) as bag) eq id seen = | Exact _ -> false,seen | Step (_,(_,id1,(_,id2),_)) -> let seen = ideq::seen in - let eq1 = Hashtbl.find id_to_eq id1 in - let eq2 = Hashtbl.find id_to_eq id2 in + let eq1 = M.find id1 id_to_eq in + let eq2 = M.find id2 id_to_eq in let b1,seen = depend bag eq1 id seen in if b1 then b1,seen else depend bag eq2 id seen ;; @@ -627,7 +635,7 @@ let wfo bag goalproof proof id = let string_of_id (id_to_eq,_) names id = if id = 0 then "" else try - let (_,p,(t,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(t,l,r,_),m,_) = open_equality (M.find id id_to_eq) in match p with | Exact t -> Printf.sprintf "%d = %s: %s = %s [%s]" id @@ -661,14 +669,6 @@ let pp_proof bag names goalproof proof subst id initial_goal = "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst ;; -module OT = - struct - type t = int - let compare = Pervasives.compare - end - -module M = Map.Make(OT) - let rec find_deps bag m i = if M.mem i m then m else @@ -896,7 +896,7 @@ let relocate newmeta menv to_be_relocated = let menv = Subst.apply_subst_metasenv subst (menv @ newmetasenv) in subst, menv, newmeta -let fix_metas_goal newmeta goal = +let fix_metas_goal (id_to_eq,newmeta) goal = let (proof, menv, ty) = goal in let to_be_relocated = HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty)) @@ -908,20 +908,12 @@ let fix_metas_goal newmeta goal = | [] -> assert false (* is a nonsense to relocate the initial goal *) | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl in - newmeta+1,(proof, menv, ty) + (id_to_eq,newmeta+1),(proof, menv, ty) ;; -let fix_metas bag newmeta eq = +let fix_metas (id_to_eq, newmeta) eq = let w, p, (ty, left, right, o), menv,_ = open_equality eq in - let to_be_relocated = - List.map (fun i ,_,_ -> i) menv -(* - HExtlib.list_uniq - (List.sort Pervasives.compare - (Utils.metas_of_term left @ Utils.metas_of_term right @ - Utils.metas_of_term ty)) -*) - in + let to_be_relocated = List.map (fun i ,_,_ -> i) menv in let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in let ty = Subst.apply_subst subst ty in let left = Subst.apply_subst subst left in @@ -932,8 +924,10 @@ let fix_metas bag newmeta eq = Step (Subst.concat s subst,(r,id1,(pos,id2), pred)) in let p = fix_proof p in - let eq' = mk_equality bag (w, p, (ty, left, right, o), metasenv) in - newmeta+1, eq' + let bag = id_to_eq, newmeta in + let bag, e = mk_equality bag (w, p, (ty, left, right, o), metasenv) in + bag, e +;; exception NotMetaConvertible;; @@ -1090,15 +1084,15 @@ let term_is_equality term = | _ -> false ;; -let equality_of_term bag proof term = +let equality_of_term bag proof term newmetas = match term with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when LibraryObjects.is_eq_URI uri -> let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = Utils.compute_equality_weight stat in - let e = mk_equality bag (w, Exact proof, stat,[]) in - e + let bag, e = mk_equality bag (w, Exact proof, stat,newmetas) in + bag, e | _ -> raise TermIsNotAnEquality ;; @@ -1152,12 +1146,12 @@ let symmetric bag eq_ty l id uri m = Exact (Cic.Appl [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) in - let id1 = - let eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in + let bag, id1 = + let bag, eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in let (_,_,_,_,id) = open_equality eq in - id + bag, id in - Step(Subst.empty_subst, + bag, Step(Subst.empty_subst, (Demodulation,id1,(Utils.Left,id),pred)) ;; @@ -1170,8 +1164,7 @@ module IntSet = Set.Make(IntOT);; let n_purged = ref 0;; -let collect ((id_to_eq,_) as bag) alive1 alive2 alive3 = -(* let _ = <:start> in *) +let collect ((id_to_eq,maxmeta) as bag) alive1 alive2 alive3 = let deps_of id = let p,_,_ = proof_of_id bag id in match p with @@ -1187,18 +1180,13 @@ let collect ((id_to_eq,_) as bag) alive1 alive2 alive3 = let alive_set = l_to_s (l_to_s (l_to_s IntSet.empty alive2) alive1) alive3 in let closed_alive_set = close alive_set in let to_purge = - Hashtbl.fold + M.fold (fun k _ s -> if not (IntSet.mem k closed_alive_set) then k::s else s) id_to_eq [] in n_purged := !n_purged + List.length to_purge; - List.iter (Hashtbl.remove id_to_eq) to_purge; -(* let _ = <:stop> in () *) -;; - -let id_of e = - let _,_,_,_,id = open_equality e in id + List.fold_right M.remove to_purge id_to_eq, maxmeta ;; let get_stats () = "" @@ -1319,7 +1307,7 @@ let remove_names_in_context (set,subst) names = let string_of_id2 (id_to_eq,_) names nameset id = if id = 0 then "" else try - let (_,_,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,_,(_,l,r,_),_,_) = open_equality (M.find id id_to_eq) in let nameset, l = freshname nameset l in let nameset, r = freshname nameset r in Printf.sprintf "%s = %s" (CicPp.pp l names) (CicPp.pp r names) @@ -1379,3 +1367,15 @@ let draw_proof bag names goal_proof proof id = ignore(Unix.system "gv /tmp/matita_paramod.eps"); ;; +let saturate_term (id_to_eq, maxmeta) metasenv context term = + let head, metasenv, args, newmeta = + TermUtil.saturate_term maxmeta metasenv context term 0 + in + (id_to_eq, newmeta), head, metasenv, args +;; + +let push_maxmeta (id_to_eq, maxmeta) m = id_to_eq, max maxmeta m ;; +let filter_metasenv_gt_maxmeta (_,maxmeta) = + List.filter (fun (j,_,_) -> j >= maxmeta) +;; +let maxmeta = snd;; diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index d3acf8950..b4aa66d29 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -65,8 +65,7 @@ val mk_eq_ind : val mk_equality : equality_bag -> int * proof * (Cic.term * Cic.term * Cic.term * Utils.comparison) * - Cic.metasenv -> - equality + Cic.metasenv -> equality_bag * equality val mk_tmp_equality : int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> @@ -101,8 +100,8 @@ val build_proof_term : UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term (** ensures that metavariables in equality are unique *) -val fix_metas_goal: int -> goal -> int * goal -val fix_metas: equality_bag -> int -> equality -> int * equality +val fix_metas_goal: equality_bag -> goal -> equality_bag * goal +val fix_metas: equality_bag -> equality -> equality_bag * equality val metas_of_proof: equality_bag -> proof -> int list (* this should be used _only_ to apply (efficiently) this subst on the @@ -114,7 +113,9 @@ exception TermIsNotAnEquality;; raises TermIsNotAnEquality if term is not an equation. The first Cic.term is a proof of the equation *) -val equality_of_term: equality_bag -> Cic.term -> Cic.term -> equality +val equality_of_term: + equality_bag -> Cic.term -> Cic.term -> Cic.metasenv -> + equality_bag * equality (** Re-builds the term corresponding to this equality @@ -122,6 +123,13 @@ val equality_of_term: equality_bag -> Cic.term -> Cic.term -> equality val term_of_equality: UriManager.uri -> equality -> Cic.term val term_is_equality: Cic.term -> bool +val saturate_term : equality_bag -> Cic.metasenv -> Cic.context -> Cic.term -> + equality_bag * Cic.term * Cic.metasenv * Cic.term list + +val push_maxmeta : equality_bag -> int -> equality_bag +val maxmeta : equality_bag -> int +val filter_metasenv_gt_maxmeta: equality_bag -> Cic.metasenv -> Cic.metasenv + (** tests a sort of alpha-convertibility between the two terms, but on the metavariables *) val meta_convertibility: Cic.term -> Cic.term -> bool @@ -134,6 +142,8 @@ val meta_convertibility_subst: val is_weak_identity: equality -> bool val is_identity: Utils.environment -> equality -> bool +val is_in: equality_bag -> int -> bool + (* symmetric [eq_ty] [l] [id] [uri] [m] * * given an equality (_,p,(_,[l],r,_),[m],[id]) of 'type' l=r @@ -144,12 +154,12 @@ val is_identity: Utils.environment -> equality -> bool *) val symmetric: equality_bag -> Cic.term -> Cic.term -> int -> UriManager.uri -> - Cic.metasenv -> proof + Cic.metasenv -> equality_bag * proof (* takes 3 lists of alive ids (they are threated the same way, the type is * funny just to not oblige you to concatenate them) and drops all the dead * equalities *) -val collect: equality_bag -> int list -> int list -> int list -> unit +val collect: equality_bag -> int list -> int list -> int list -> equality_bag (* given an equality, returns the numerical id *) val id_of: equality -> int diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 7d981cf31..0c9894680 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -164,8 +164,8 @@ let check_demod_res res metasenv msg = in if (not b) then begin - prerr_endline ("extended context " ^ msg); - prerr_endline (CicMetaSubst.ppmetasenv [] menv); + debug_print (lazy ("extended context " ^ msg)); + debug_print (lazy (CicMetaSubst.ppmetasenv [] menv)); end; b | None -> false @@ -565,7 +565,6 @@ let rec demodulation_aux bag ?from ?(typecheck=false) let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *) check_for_duplicates metasenv "in input a demodulation aux"; let candidates = get_candidates @@ -677,17 +676,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) exception Foo (** demodulation, when target is an equality *) -let rec demodulation_equality bag ?from eq_uri newmeta env table target = - (* - prerr_endline ("demodulation_eq:\n"); - Index.iter table (fun l -> - let l = Index.PosEqSet.elements l in - let l = - List.map (fun (p,e) -> - Utils.string_of_pos p ^ Equality.string_of_equality e) l in - prerr_endline (String.concat "\n" l) - ); - *) +let rec demodulation_equality bag ?from eq_uri env table target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -707,9 +696,8 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = if Utils.debug_metas then ignore(check_target bag context target "demod equalities input"); let metasenv' = (* metasenv @ *) metas in - let maxmeta = ref newmeta in - let build_newtarget is_left (t, subst, menv, ug, eq_found) = + let build_newtarget bag is_left (t, subst, menv, ug, eq_found) = if Utils.debug_metas then begin @@ -743,45 +731,44 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = let left, right = if is_left then newterm, right else left, newterm in let ordering = !Utils.compare_terms left right in let stat = (eq_ty, left, right, ordering) in - let res = + let bag, res = let w = Utils.compute_equality_weight stat in - (Equality.mk_equality bag (w, newproof, stat,newmenv)) + Equality.mk_equality bag (w, newproof, stat,newmenv) in if Utils.debug_metas then ignore(check_target bag context res "buildnew_target output"); - !maxmeta, res + bag, res in - let res = demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left in if Utils.debug_res then check_res res "demod result"; - let newmeta, newtarget = + let bag, newtarget = match res with | Some t -> - let newmeta, newtarget = build_newtarget true t in + let bag, newtarget = build_newtarget bag true t in (* assert (not (Equality.meta_convertibility_eq target newtarget)); *) if (Equality.is_weak_identity newtarget) (* || *) (*Equality.meta_convertibility_eq target newtarget*) then - newmeta, newtarget + bag, newtarget else - demodulation_equality bag ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri env table newtarget | None -> let res = demodulation_aux bag metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; match res with | Some t -> - let newmeta, newtarget = build_newtarget false t in + let bag, newtarget = build_newtarget bag false t in if (Equality.is_weak_identity newtarget) || (Equality.meta_convertibility_eq target newtarget) then - newmeta, newtarget + bag, newtarget else - demodulation_equality bag ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri env table newtarget | None -> - newmeta, target + bag, target in (* newmeta, newtarget *) - newmeta,newtarget + bag, newtarget ;; (** @@ -924,7 +911,7 @@ let rec betaexpand_term index: its updated value is also returned *) let superposition_right bag - ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target= + ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target= let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -937,7 +924,6 @@ let superposition_right bag if Utils.debug_metas then ignore (check_target bag context target "superpositionright"); let metasenv' = newmetas in - let maxmeta = ref newmeta in let res1, res2 = match ordering with | U.Gt -> @@ -955,7 +941,7 @@ let superposition_right bag in (res left right), (res right left) in - let build_new ordering (bo, s, m, ug, eq_found) = + let build_new bag ordering (bo, s, m, ug, eq_found) = if Utils.debug_metas then ignore (check_target bag context (snd eq_found) "buildnew1" ); @@ -981,33 +967,41 @@ let superposition_right bag (s,(Equality.SuperpositionRight, id,(pos,id'),(Cic.Lambda(name,ty,bo'')))) in - let newmeta, newequality = + let bag, newequality = let left, right = if ordering = U.Gt then newgoal, apply_subst s right else apply_subst s left, newgoal in let neworder = !Utils.compare_terms left right in let newmenv = (* Founif.filter s *) m in let stat = (eq_ty, left, right, neworder) in - let eq' = + let bag, eq' = let w = Utils.compute_equality_weight stat in Equality.mk_equality bag (w, newproof, stat, newmenv) in if Utils.debug_metas then ignore (check_target bag context eq' "buildnew3"); - let newm, eq' = Equality.fix_metas bag !maxmeta eq' in + let bag, eq' = Equality.fix_metas bag eq' in if Utils.debug_metas then ignore (check_target bag context eq' "buildnew4"); - newm, eq' + bag, eq' in - maxmeta := newmeta; if Utils.debug_metas then ignore(check_target bag context newequality "buildnew2"); - newequality + bag, newequality + in + let bag, new1 = + List.fold_right + (fun x (bag,acc) -> + let bag, e = build_new bag U.Gt x in + bag, e::acc) res1 (bag,[]) + in + let bag, new2 = + List.fold_right + (fun x (bag,acc) -> + let bag, e = build_new bag U.Lt x in + bag, e::acc) res2 (bag,[]) in - let new1 = List.map (build_new U.Gt) res1 - and new2 = List.map (build_new U.Lt) res2 in let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in - (!maxmeta, - (List.filter ok (new1 @ new2))) + bag, List.filter ok (new1 @ new2) ;; (** demodulation, when the target is a theorem *) @@ -1164,7 +1158,7 @@ let build_newgoal bag context goal posu rule expansion = returns a list of new clauses inferred with a left superposition step the negative equation "target" and one of the positive equations in "table" *) -let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = +let superposition_left bag (metasenv, context, ugraph) table goal = let names = Utils.names_of_context context in let proof,menv,eq,ty,l,r = open_goal goal in let c = !Utils.compare_terms l r in @@ -1203,9 +1197,10 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = in (* rinfresco le meta *) List.fold_right - (fun g (max,acc) -> - let max,g = Equality.fix_metas_goal max g in max,g::acc) - newgoals (maxmeta,[]) + (fun g (b,acc) -> + let b,g = Equality.fix_metas_goal b g in + b,g::acc) + newgoals (bag,[]) ;; (** demodulation, when the target is a goal *) diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 1caa5ed41..8895b89a0 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -63,18 +63,17 @@ val subsumption_all : val superposition_left : Equality.equality_bag -> Cic.conjecture list * Cic.context * CicUniv.universe_graph -> - Index.t -> Equality.goal -> int -> - int * Equality.goal list + Index.t -> Equality.goal -> + Equality.equality_bag * Equality.goal list val superposition_right : Equality.equality_bag -> ?subterms_only:bool -> UriManager.uri -> - int -> - 'a * Cic.context * CicUniv.universe_graph -> + Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> Equality.equality -> - int * Equality.equality list + Equality.equality_bag * Equality.equality list val demod : Equality.equality_bag -> @@ -86,10 +85,9 @@ val demodulation_equality : Equality.equality_bag -> ?from:string -> UriManager.uri -> - int -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> - Equality.equality -> int * Equality.equality + Equality.equality -> Equality.equality_bag * Equality.equality val demodulation_goal : Equality.equality_bag -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index aed51e35b..ceb8ab5af 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -64,9 +64,6 @@ let symbols_counter = ref 0;; let derived_clauses = ref 0;; let kept_clauses = ref 0;; -(* index of the greatest Cic.Meta created - TODO: find a better way! *) -let maxmeta = ref 0;; - (* varbiables controlling the search-space *) let maxdepth = ref 3;; let maxwidth = ref 3;; @@ -114,12 +111,14 @@ type active_table = Equality.equality list * Indexing.Index.t type new_proof = Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv type result = - | ParamodulationFailure of string * active_table * passive_table - | ParamodulationSuccess of new_proof * active_table * passive_table + | ParamodulationFailure of + string * active_table * passive_table * Equality.equality_bag + | ParamodulationSuccess of + new_proof * active_table * passive_table * Equality.equality_bag ;; -let list_of_passive (l,s) = l -;; +let list_of_passive (l,s) = l ;; +let list_of_active (l,s) = l ;; let make_passive eq_list = let set = @@ -357,53 +356,44 @@ let infer bag eq_uri env current (active_list, active_table) = if Utils.debug_metas then (ignore(Indexing.check_target bag c current "infer1"); ignore(List.map (function current -> Indexing.check_target bag c current "infer2") active_list)); - let new_pos = - let maxm, copy_of_current = Equality.fix_metas bag !maxmeta current in - maxmeta := maxm; + let bag, new_pos = + let bag, copy_of_current = Equality.fix_metas bag current in let active_table = Indexing.index active_table copy_of_current in (* let _ = <:start> in *) - let maxm, res = - Indexing.superposition_right bag eq_uri !maxmeta env active_table current + let bag, res = + Indexing.superposition_right bag eq_uri env active_table current in (* let _ = <:stop> in *) if Utils.debug_metas then ignore(List.map (function current -> Indexing.check_target bag c current "sup0") res); - maxmeta := maxm; - let rec infer_positive table = function - | [] -> [] + let rec infer_positive bag table = function + | [] -> bag, [] | equality::tl -> - let maxm, res = + let bag, res = Indexing.superposition_right bag - ~subterms_only:true eq_uri !maxmeta env table equality + ~subterms_only:true eq_uri env table equality in - maxmeta := maxm; if Utils.debug_metas then ignore (List.map (function current -> Indexing.check_target bag c current "sup2") res); - let pos = infer_positive table tl in - res @ pos + let bag, pos = infer_positive bag table tl in + bag, res @ pos in -(* - let maxm, copy_of_current = Equality.fix_metas !maxmeta current in - maxmeta := maxm; -*) let curr_table = Indexing.index Indexing.empty current in -(* let _ = <:start> in *) - let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in -(* let _ = <:stop> in *) + let bag, pos = infer_positive bag curr_table ((*copy_of_current::*)active_list) in if Utils.debug_metas then ignore(List.map (function current -> Indexing.check_target bag c current "sup3") pos); - res @ pos + bag, res @ pos in derived_clauses := !derived_clauses + (List.length new_pos); match !maximal_retained_equality with - | None -> new_pos + | None -> bag, new_pos | Some eq -> ignore(assert false); (* if we have a maximal_retained_equality, we can discard all equalities @@ -411,7 +401,7 @@ let infer bag eq_uri env current (active_list, active_table) = greater than maximal_retained_equality if it is bigger wrt. OrderedEquality.compare and it is less similar than maximal_retained_equality to the current goal *) - List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos + bag, List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos ;; let check_for_deep_subsumption env active_table eq = @@ -448,32 +438,31 @@ let check_for_deep_subsumption env active_table eq = (** simplifies current using active and passive *) let forward_simplify bag eq_uri env current (active_list, active_table) = let _, context, _ = env in - let demodulate table current = - let newmeta, newcurrent = - Indexing.demodulation_equality bag eq_uri !maxmeta env table current + let demodulate bag table current = + let bag, newcurrent = + Indexing.demodulation_equality bag eq_uri env table current in - maxmeta := newmeta; - if Equality.is_identity env newcurrent then None else Some newcurrent + bag, if Equality.is_identity env newcurrent then None else Some newcurrent in - let demod current = + let demod bag current = if Utils.debug_metas then ignore (Indexing.check_target bag context current "demod0"); - let res = demodulate active_table current in + let bag, res = demodulate bag active_table current in if Utils.debug_metas then ignore ((function None -> () | Some x -> ignore (Indexing.check_target bag context x "demod1");()) res); - res + bag, res in - let res = demod current in + let bag, res = demod bag current in match res with - | None -> None + | None -> bag, None | Some c -> if Indexing.in_index active_table c || check_for_deep_subsumption env active_table c then - None + bag, None else - res + bag, res ;; (** simplifies new using active and passive *) @@ -486,15 +475,19 @@ let forward_simplify_new bag eq_uri env new_pos active = new_pos;) end; let active_list, active_table = active in - let demodulate table target = - let newmeta, newtarget = - Indexing.demodulation_equality bag eq_uri !maxmeta env table target + let demodulate bag table target = + let bag, newtarget = + Indexing.demodulation_equality bag eq_uri env table target in - maxmeta := newmeta; - newtarget + bag, newtarget in (* we could also demodulate using passive. Currently we don't *) - let new_pos = List.map (demodulate active_table) new_pos in + let bag, new_pos = + List.fold_right (fun x (bag,acc) -> + let bag, y = demodulate bag active_table x in + bag, y::acc) + new_pos (bag,[]) + in let new_pos_set = List.fold_left (fun s e -> @@ -504,10 +497,9 @@ let forward_simplify_new bag eq_uri env new_pos active = EqualitySet.empty new_pos in let new_pos = EqualitySet.elements new_pos_set in - let subs e = Indexing.subsumption env active_table e = None in let is_duplicate e = not (Indexing.in_index active_table e) in - List.filter subs (List.filter is_duplicate new_pos) + bag, List.filter subs (List.filter is_duplicate new_pos) ;; @@ -536,23 +528,23 @@ let backward_simplify_active bag eq_uri env new_pos new_table min_weight active = let active_list, active_table = active in - let active_list, newa, pruned = + let bag, active_list, newa, pruned = List.fold_right - (fun equality (res, newn,pruned) -> + (fun equality (bag, res, newn,pruned) -> let ew, _, _, _,id = Equality.open_equality equality in if ew < min_weight then - equality::res, newn,pruned + bag, equality::res, newn,pruned else match forward_simplify bag eq_uri env equality (new_pos, new_table) with - | None -> res, newn, id::pruned - | Some e -> + | bag, None -> bag, res, newn, id::pruned + | bag, Some e -> if Equality.compare equality e = 0 then - e::res, newn, pruned + bag, e::res, newn, pruned else - res, e::newn, pruned) - active_list ([], [],[]) + bag, res, e::newn, pruned) + active_list (bag, [], [],[]) in let find eq1 where = List.exists (Equality.meta_convertibility_eq eq1) where @@ -578,8 +570,8 @@ let backward_simplify_active newa [] in match newa with - | [] -> (active1,tbl), None, pruned - | _ -> (active1,tbl), Some newa, pruned + | [] -> bag, (active1,tbl), None, pruned + | _ -> bag, (active1,tbl), Some newa, pruned ;; @@ -588,30 +580,32 @@ let backward_simplify_passive bag eq_uri env new_pos new_table min_weight passive = let (pl, ps), passive_table = passive in - let f equality (resl, ress, newn) = + let f bag equality (resl, ress, newn) = let ew, _, _, _ , _ = Equality.open_equality equality in if ew < min_weight then - equality::resl, ress, newn + bag, (equality::resl, ress, newn) else match forward_simplify bag eq_uri env equality (new_pos, new_table) with - | None -> resl, EqualitySet.remove equality ress, newn - | Some e -> + | bag, None -> + bag, (resl, EqualitySet.remove equality ress, newn) + | bag, Some e -> if equality = e then - equality::resl, ress, newn + bag, (equality::resl, ress, newn) else let ress = EqualitySet.remove equality ress in - resl, ress, e::newn + bag, (resl, ress, e::newn) in - let pl, ps, newp = List.fold_right f pl ([], ps, []) in + let bag, (pl, ps, newp) = + List.fold_right (fun x (bag,acc) -> f bag x acc) pl (bag,([], ps, [])) in let passive_table = List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pl in match newp with - | [] -> ((pl, ps), passive_table), None - | _ -> ((pl, ps), passive_table), Some (newp) + | [] -> bag, ((pl, ps), passive_table), None + | _ -> bag, ((pl, ps), passive_table), Some (newp) ;; let build_table equations = @@ -625,10 +619,10 @@ let build_table equations = let backward_simplify bag eq_uri env new' active = let new_pos, new_table, min_weight = build_table new' in - let active, newa, pruned = + let bag, active, newa, pruned = backward_simplify_active bag eq_uri env new_pos new_table min_weight active in - active, newa, pruned + bag, active, newa, pruned ;; let close bag eq_uri env new' given = @@ -640,10 +634,10 @@ let close bag eq_uri env new' given = ([], Indexing.empty, 1000000) (snd new') in List.fold_left - (fun p c -> - let pos = infer bag eq_uri env c (new_pos,new_table) in - pos@p) - [] given + (fun (bag,p) c -> + let bag, pos = infer bag eq_uri env c (new_pos,new_table) in + bag, pos@p) + (bag,[]) given ;; let is_commutative_law eq = @@ -714,39 +708,6 @@ let activate_theorem (active, passive) = | [] -> false, (active, passive) ;; - -(* -let simplify_theorems bag env theorems ?passive (active_list, active_table) = - let pl, passive_table = - match passive with - | None -> [], None - | Some ((pn, _), (pp, _), pt) -> pn @ pp, Some pt - in - let a_theorems, p_theorems = theorems in - let demodulate table theorem = - let newmeta, newthm = - Indexing.demodulation_theorem bag !maxmeta env table theorem in - maxmeta := newmeta; - theorem != newthm, newthm - in - let foldfun table (a, p) theorem = - let changed, theorem = demodulate table theorem in - if changed then (a, theorem::p) else (theorem::a, p) - in - let mapfun table theorem = snd (demodulate table theorem) in - match passive_table with - | None -> - let p_theorems = List.map (mapfun active_table) p_theorems in - List.fold_left (foldfun active_table) ([], p_theorems) a_theorems - | Some passive_table -> - let p_theorems = List.map (mapfun active_table) p_theorems in - let p_theorems, a_theorems = - List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in - let p_theorems = List.map (mapfun passive_table) p_theorems in - List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems -;; -*) - let rec simpl bag eq_uri env e others others_simpl = let active = others @ others_simpl in let tbl = @@ -755,8 +716,8 @@ let rec simpl bag eq_uri env e others others_simpl = if Equality.is_identity env e then t else Indexing.index t e) Indexing.empty active in - let res = - forward_simplify bag eq_uri env e (active, tbl) + let bag, res = + forward_simplify bag eq_uri env e (active, tbl) in match others with | hd::tl -> ( @@ -766,8 +727,8 @@ let rec simpl bag eq_uri env e others others_simpl = ) | [] -> ( match res with - | None -> others_simpl - | Some e -> e::others_simpl + | None -> bag, others_simpl + | Some e -> bag, e::others_simpl ) ;; @@ -779,17 +740,16 @@ let simplify_equalities bag eq_uri env equalities = (List.map Equality.string_of_equality equalities)))); Utils.debug_print (lazy "SIMPLYFYING EQUALITIES..."); match equalities with - | [] -> [] + | [] -> bag, [] | hd::tl -> - let res = - List.rev (simpl bag eq_uri env hd tl []) - in + let bag, res = simpl bag eq_uri env hd tl [] in + let res = List.rev res in Utils.debug_print (lazy (Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" (List.map Equality.string_of_equality res)))); - res + bag, res ;; let print_goals goals = @@ -820,7 +780,7 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when LibraryObjects.is_eq_URI uri -> - (let goal_equation = + (let bag, goal_equation = Equality.mk_equality bag (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) in @@ -836,37 +796,38 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = *) let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in - let p = + let bag, p = if swapped then Equality.symmetric bag eq_ty l id uri m else - p + bag, p in - Some (goalproof, p, id, subst, cicmenv) - | None -> None) - | _ -> None + bag, Some (goalproof, p, id, subst, cicmenv) + | None -> bag, None) + | _ -> bag, None ;; -let find_all_subsumed bag maxm env table (goalproof,menv,ty) = +let find_all_subsumed bag env table (goalproof,menv,ty) = match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when LibraryObjects.is_eq_URI uri -> - let goal_equation = + let bag, goal_equation = (Equality.mk_equality bag (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)) in - List.map - (fun (subst, equality, swapped ) -> + List.fold_right + (fun (subst, equality, swapped) (bag,acc) -> let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in Indexing.check_for_duplicates cicmenv "from subsumption"; - let p = + let bag, p = if swapped then Equality.symmetric bag eq_ty l id uri m else - p - in (goalproof, p, id, subst, cicmenv)) - (Indexing.subsumption_all env table goal_equation) + bag, p + in + bag, (goalproof, p, id, subst, cicmenv)::acc) + (Indexing.subsumption_all env table goal_equation) (bag,[]) (* (Indexing.unification_all env table goal_equation) *) | _ -> assert false ;; @@ -891,12 +852,12 @@ let check_if_goal_is_identity env = function | _ -> None ;; -let rec check goal = function - | [] -> None +let rec check b goal = function + | [] -> b, None | f::tl -> - match f goal with - | None -> check goal tl - | (Some p) as ok -> ok + match f b goal with + | b, None -> check b goal tl + | b, (Some _ as ok) -> b, ok ;; let simplify_goal_set bag env goals active = @@ -922,60 +883,57 @@ let simplify_goal_set bag env goals active = let check_if_goals_set_is_solved bag env active goals = let active_goals, passive_goals = goals in List.fold_left - (fun proof goal -> + (fun (bag, proof) goal -> match proof with - | Some p -> proof + | Some p -> bag, proof | None -> - check goal [ - check_if_goal_is_identity env; - check_if_goal_is_subsumed bag env (snd active)]) + check bag goal [ + (fun b x -> b, check_if_goal_is_identity env x); + (fun bag -> check_if_goal_is_subsumed bag env (snd active))]) (* provare active and passive?*) - None active_goals + (bag,None) active_goals ;; let infer_goal_set bag env active goals = let active_goals, passive_goals = goals in - let rec aux = function - | [] -> active_goals, [] + let rec aux bag = function + | [] -> bag, (active_goals, []) | hd::tl -> - let changed,selected = simplify_goal bag env hd active in + let changed, selected = simplify_goal bag env hd active in let (_,_,t1) = selected in - (* - if changed && Utils.debug then - prerr_endline ("goal semplificato: " ^ CicPp.ppterm t1); *) let already_in = List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) active_goals in if already_in then - aux tl + aux bag tl else let passive_goals = tl in - let new_passive_goals = - if Utils.metas_of_term t1 = [] then passive_goals + let bag, new_passive_goals = + if Utils.metas_of_term t1 = [] then + bag, passive_goals else - let newmaxmeta,new' = + let bag, new' = Indexing.superposition_left bag env (snd active) selected - !maxmeta in - maxmeta := newmaxmeta; - passive_goals @ new' + bag, passive_goals @ new' in - selected::active_goals, new_passive_goals + bag, (selected::active_goals, new_passive_goals) in - aux passive_goals + aux bag passive_goals ;; let infer_goal_set_with_current bag env current goals active = let active_goals, passive_goals = simplify_goal_set bag env goals active in let l,table,_ = build_table [current] in - active_goals, - List.fold_left - (fun acc g -> - let newmaxmeta, new' = Indexing.superposition_left bag env table g !maxmeta in - maxmeta := newmaxmeta; - acc @ new') - passive_goals active_goals + let bag, passive_goals = + List.fold_left + (fun (bag, acc) g -> + let bag, new' = Indexing.superposition_left bag env table g in + bag, acc @ new') + (bag, passive_goals) active_goals + in + bag, active_goals, passive_goals ;; let ids_of_goal g = @@ -1013,6 +971,38 @@ let print_status iterno goals active passive = (size_of_goal_set_a goals) (size_of_goal_set_p goals))) ;; +let add_to_active_aux bag active passive env eq_uri current = + debug_print (lazy ("Adding to actives : " ^ + Equality.string_of_equality ~env current)); + match forward_simplify bag eq_uri env current active with + | bag, None -> None, active, passive, bag + | bag, Some current -> + let bag, new' = infer bag eq_uri env current active in + let active = + let al, tbl = active in + al @ [current], Indexing.index tbl current + in + let rec simplify bag new' active passive = + let bag, new' = + forward_simplify_new bag eq_uri env new' active + in + let bag, active, newa, pruned = + backward_simplify bag eq_uri env new' active + in + let passive = + List.fold_left (filter_dependent bag) passive pruned + in + match newa with + | None -> bag, active, passive, new' + | Some p -> simplify bag (new' @ p) active passive + in + let bag, active, passive, new' = + simplify bag new' active passive + in + let passive = add_to_passive passive new' [] in + Some new', active, passive, bag +;; + (** given-clause algorithm with full reduction strategy: NEW implementation *) (* here goals is a set of goals in OR *) let given_clause @@ -1030,11 +1020,11 @@ let given_clause let iterations_left = time_left /. iteration_medium_cost in int_of_float iterations_left in - let rec step goals passive active g_iterno s_iterno = + let rec step bag goals passive active g_iterno s_iterno = if g_iterno > goal_steps && s_iterno > saturation_steps then - (ParamodulationFailure ("No more iterations to spend",active,passive)) + (ParamodulationFailure ("No more iterations to spend",active,passive,bag)) else if Unix.gettimeofday () > max_time then - (ParamodulationFailure ("No more time to spend",active,passive)) + (ParamodulationFailure ("No more time to spend",active,passive,bag)) else let _ = print_status (max g_iterno s_iterno) goals active passive @@ -1053,123 +1043,78 @@ let given_clause passive in kept_clauses := (size_of_passive passive) + (size_of_active active); - let goals = + let bag, goals = if g_iterno < goal_steps then infer_goal_set bag env active goals else - goals + bag, goals in match check_if_goals_set_is_solved bag env active goals with - | Some p -> + | bag, Some p -> debug_print (lazy (Printf.sprintf "\nFound a proof in: %f\n" (Unix.gettimeofday() -. initial_time))); - ParamodulationSuccess (p,active,passive) - | None -> + ParamodulationSuccess (p,active,passive,bag) + | bag, None -> (* SELECTION *) if passive_is_empty passive then if no_more_passive_goals goals then ParamodulationFailure - ("No more passive equations/goals",active,passive) + ("No more passive equations/goals",active,passive,bag) (*maybe this is a success! *) else - step goals passive active (g_iterno+1) (s_iterno+1) + step bag goals passive active (g_iterno+1) (s_iterno+1) else begin (* COLLECTION OF GARBAGED EQUALITIES *) - if max g_iterno s_iterno mod 40 = 0 then - begin - print_status (max g_iterno s_iterno) goals active passive; + let bag = + if max g_iterno s_iterno mod 40 = 0 then + (print_status (max g_iterno s_iterno) goals active passive; let active = List.map Equality.id_of (fst active) in let passive = List.map Equality.id_of (fst passive) in let goal = ids_of_goal_set goals in - Equality.collect bag active passive goal - end; - let res, passive = - if s_iterno < saturation_steps then - let current, passive = select env goals passive in - (* SIMPLIFICATION OF CURRENT *) - debug_print (lazy - ("Selected : " ^ - Equality.string_of_equality ~env current)); - forward_simplify bag eq_uri env current active, passive + Equality.collect bag active passive goal) else - None, passive + bag in - match res with - | None -> step goals passive active (g_iterno+1) (s_iterno+1) - | Some current -> - (* GENERATION OF NEW EQUATIONS *) -(* prerr_endline "infer"; *) - let new' = infer bag eq_uri env current active in -(* prerr_endline "infer goal"; *) -(* - match check_if_goals_set_is_solved env active goals with - | Some p -> - prerr_endline - (Printf.sprintf "Found a proof in: %f\n" - (Unix.gettimeofday() -. initial_time)); - ParamodulationSuccess p - | None -> -*) - - let active = - let al, tbl = active in - al @ [current], Indexing.index tbl current - in - let goals = - infer_goal_set_with_current bag env current goals active - in - - (* FORWARD AND BACKWARD SIMPLIFICATION *) -(* prerr_endline "fwd/back simpl"; *) - let rec simplify new' active passive = - let new' = - forward_simplify_new bag eq_uri env new' active - in - let active, newa, pruned = - backward_simplify bag eq_uri env new' active - in - let passive = - List.fold_left (filter_dependent bag) passive pruned - in - match newa with - | None -> active, passive, new' - | Some p -> simplify (new' @ p) active passive - in - let active, passive, new' = - simplify new' active passive - in - -(* prerr_endline "simpl goal with new"; *) - let goals = - let a,b,_ = build_table new' in -(* let _ = <:start> in *) - let rc = simplify_goal_set bag env goals (a,b) in -(* let _ = <:stop> in *) - rc - in - let passive = add_to_passive passive new' [] in - step goals passive active (g_iterno+1) (s_iterno+1) + if s_iterno > saturation_steps then + ParamodulationFailure ("max saturation steps",active,passive,bag) + else + let current, passive = select env goals passive in + match add_to_active_aux bag active passive env eq_uri current with + | None, active, passive, bag -> + step bag goals passive active (g_iterno+1) (s_iterno+1) + | Some new', active, passive, bag -> + let bag, active_goals, passive_goals = + infer_goal_set_with_current bag env current goals active + in + let goals = + let a,b,_ = build_table new' in + let rc = + simplify_goal_set bag env (active_goals,passive_goals) (a,b) + in + rc + in + step bag goals passive active (g_iterno+1) (s_iterno+1) end in - step goals passive active 1 1 + step bag goals passive active 1 1 ;; let rec saturate_equations bag eq_uri env goal accept_fun passive active = elapsed_time := Unix.gettimeofday () -. !start_time; if !elapsed_time > !time_limit then - (active, passive) + bag, active, passive else let current, passive = select env ([goal],[]) passive in - let res = forward_simplify bag eq_uri env current active in + let bag, res = forward_simplify bag eq_uri env current active in match res with | None -> saturate_equations bag eq_uri env goal accept_fun passive active | Some current -> Utils.debug_print (lazy (Printf.sprintf "selected: %s" (Equality.string_of_equality ~env current))); - let new' = infer bag eq_uri env current active in + let bag, new' = infer bag eq_uri env current active in let active = if Equality.is_identity env current then active else @@ -1178,17 +1123,17 @@ let rec saturate_equations bag eq_uri env goal accept_fun passive active = in (* alla fine new' contiene anche le attive semplificate! * quindi le aggiungo alle passive insieme alle new *) - let rec simplify new' active passive = - let new' = forward_simplify_new bag eq_uri env new' active in - let active, newa, pruned = + let rec simplify bag new' active passive = + let bag, new' = forward_simplify_new bag eq_uri env new' active in + let bag, active, newa, pruned = backward_simplify bag eq_uri env new' active in let passive = List.fold_left (filter_dependent bag) passive pruned in match newa with - | None -> active, passive, new' - | Some p -> simplify (new' @ p) active passive + | None -> bag, active, passive, new' + | Some p -> simplify bag (new' @ p) active passive in - let active, passive, new' = simplify new' active passive in + let bag, active, passive, new' = simplify bag new' active passive in let _ = Utils.debug_print (lazy @@ -1216,7 +1161,6 @@ let default_depth = !maxdepth and default_width = !maxwidth;; let reset_refs () = - maxmeta := 0; symbols_counter := 0; weight_age_counter := !weight_age_ratio; processed_clauses := 0; @@ -1232,6 +1176,21 @@ let reset_refs () = kept_clauses := 0; ;; +let add_to_active bag active passive env ty term newmetas = + reset_refs (); + match LibraryObjects.eq_URI () with + | None -> active, passive, bag + | Some eq_uri -> + try + let bag, current = Equality.equality_of_term bag term ty newmetas in + let bag, current = Equality.fix_metas bag current in + match add_to_active_aux bag active passive env eq_uri current with + | _,a,p,b -> a,p,b + with + | Equality.TermIsNotAnEquality -> active, passive, bag +;; + + let eq_of_goal = function | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri -> uri @@ -1557,9 +1516,8 @@ let build_proof (* exported functions *) -let pump_actives context bag maxm active passive saturation_steps max_time = +let pump_actives context bag active passive saturation_steps max_time = reset_refs(); - maxmeta := maxm; (* let max_l l = List.fold_left @@ -1572,21 +1530,20 @@ let pump_actives context bag maxm active passive saturation_steps max_time = (* let ma = max_l active_l in *) (* let mp = max_l passive_l in *) match LibraryObjects.eq_URI () with - | None -> active, passive, !maxmeta + | None -> active, passive, bag | 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 + | ParamodulationFailure (_,a,p,b) -> + a, p, b | ParamodulationSuccess _ -> assert false) ;; -let all_subsumed bag maxm status active passive = - maxmeta := maxm; +let all_subsumed bag status active passive = let proof, goalno = status in let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in @@ -1608,7 +1565,7 @@ let all_subsumed bag maxm status active passive = let _,goal = simplify_goal bag env goal table in let (_,_,ty) = goal in debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty)); - let subsumed = find_all_subsumed bag !maxmeta env (snd table) goal in + let bag, subsumed = find_all_subsumed bag env (snd table) goal in debug_print (lazy ("dopo " ^ CicPp.ppterm ty)); let subsumed_or_id = match (check_if_goal_is_identity env goal) with @@ -1632,40 +1589,33 @@ let all_subsumed bag maxm status active passive = let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in (subst, proof,gl)) subsumed_or_id in - res, !maxmeta + res +;; let given_clause - bag maxm status active passive goal_steps saturation_steps max_time + bag status active passive goal_steps saturation_steps max_time = reset_refs(); - maxmeta := maxm; let active_l = fst active in -(* - let max_l l = - List.fold_left - (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in - List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) - 0 l - in - let passive_l = fst passive in - let ma = max_l active_l in - let mp = max_l passive_l in -*) let proof, goalno = status in let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let cleaned_goal = Utils.remove_local_context type_of_goal in + let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in let canonical_menv,other_menv = List.partition (fun (_,c,_) -> c = context) metasenv in - (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *) Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) let canonical_menv = List.map (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv in - let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in + let metasenv' = + List.filter + (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal) + canonical_menv + in let goal = [], metasenv', cleaned_goal in let env = metasenv,context,CicUniv.empty_ugraph in debug_print (lazy ">>>>>> ACTIVES >>>>>>>>"); @@ -1677,17 +1627,17 @@ let given_clause given_clause bag eq_uri env goals passive active goal_steps saturation_steps max_time with - | ParamodulationFailure (_,a,p) -> - None, a, p, !maxmeta + | ParamodulationFailure (_,a,p,b) -> + None, a, p, b | ParamodulationSuccess - ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) -> + ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p,b) -> let subst, proof, gl = - build_proof bag + build_proof b status goalproof newproof subsumption_id subsumption_subst proof_menv in let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in - Some (subst, proof,gl),a,p, !maxmeta + Some (subst, proof,gl),a,p, b ;; diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli index 20b564f4b..71764cddd 100644 --- a/helm/software/components/tactics/paramodulation/saturation.mli +++ b/helm/software/components/tactics/paramodulation/saturation.mli @@ -33,35 +33,38 @@ val reset_refs : unit -> unit val make_active: Equality.equality list -> active_table val make_passive: Equality.equality list -> passive_table val add_to_passive: Equality.equality list -> passive_table -> passive_table +val add_to_active: + Equality.equality_bag -> + active_table -> passive_table -> + Utils.environment -> Cic.term (* ty *) -> Cic.term -> Cic.metasenv -> + active_table * passive_table * Equality.equality_bag val list_of_passive: passive_table -> Equality.equality list +val list_of_active: active_table -> Equality.equality list val simplify_equalities : Equality.equality_bag -> UriManager.uri -> Utils.environment -> Equality.equality list -> - Equality.equality list + Equality.equality_bag * Equality.equality list val pump_actives : Cic.context -> Equality.equality_bag -> - int -> active_table -> passive_table -> int -> float -> - active_table * passive_table * int + active_table * passive_table * Equality.equality_bag val all_subsumed : Equality.equality_bag -> - int -> ProofEngineTypes.status -> active_table -> passive_table -> (Cic.substitution * ProofEngineTypes.proof * - ProofEngineTypes.goal list) list * int + ProofEngineTypes.goal list) list val given_clause: Equality.equality_bag -> - int -> (* maxmeta *) ProofEngineTypes.status -> active_table -> passive_table -> @@ -69,5 +72,5 @@ val given_clause: (Cic.substitution * ProofEngineTypes.proof * ProofEngineTypes.goal list) option * - active_table * passive_table * int + active_table * passive_table * Equality.equality_bag diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml index def2279ca..780b72daf 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -31,7 +31,11 @@ module S = Set.Make(Codomain) module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S) type universe = TI.t -let empty = TI.empty +let empty = TI.empty ;; + +let iter u f = + TI.iter u + (fun p s -> f p (S.elements s)) ;; let get_candidates univ ty = diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli index d74895114..5f9d612b5 100644 --- a/helm/software/components/tactics/universe.mli +++ b/helm/software/components/tactics/universe.mli @@ -27,6 +27,12 @@ type universe val empty : universe + +val iter : + universe -> + (UriManager.uri Discrimination_tree.path -> Cic.term list -> unit) -> + unit + (* retrieves the list of term that hopefully unify *) val get_candidates: universe -> Cic.term -> Cic.term list diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index 8a8fedb68..10cb21835 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -246,7 +246,7 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n). case left. suppose (0 < m) (m_pos). using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1). - by H1 done. + by H1 done. case right. suppose (0=m) (m_zero). by m_zero, Fmult_zero_f done. diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma index 6e389c2fa..5e337d1b8 100644 --- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma +++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma @@ -242,11 +242,13 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F). lapply (H4 i); clear H4; rewrite > symm_orb in ⊢ (? ? (? ? %) ?); rewrite > distributive_orb_andb; + STOP autobatch paramodulation | simplify in H2 ⊢ %; intros; lapply (H2 i); clear H2; - autobatch + pump 98. + autobatch. | simplify in H2 H4 ⊢ %; intros; lapply (H2 i); clear H2; diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma index aa1aa32f8..28e254f94 100644 --- a/helm/software/matita/library/didactic/exercises/duality.ma +++ b/helm/software/matita/library/didactic/exercises/duality.ma @@ -220,7 +220,7 @@ definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). -lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed. +lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed. (* Esercizio 3 =========== diff --git a/helm/software/matita/library/didactic/exercises/shannon.ma b/helm/software/matita/library/didactic/exercises/shannon.ma index 152cbb1e9..f978c91c5 100644 --- a/helm/software/matita/library/didactic/exercises/shannon.ma +++ b/helm/software/matita/library/didactic/exercises/shannon.ma @@ -406,7 +406,7 @@ case Left. = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). - = (max (min 0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H. + = (max (min 0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H1. = (max 0 (min 1 [[ F[FBot/x] ]]_v)). = (max 0 [[ F[FBot/x] ]]_v) by min_1_sem. = ([[ F[FBot/x] ]]_v). @@ -418,7 +418,7 @@ case Right. = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). - = (max (min 1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H. + = (max (min 1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H1. = (max (min 1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)). = (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem. = (max [[ F[FTop/x] ]]_v 0). diff --git a/helm/software/matita/library/didactic/exercises/substitution.ma b/helm/software/matita/library/didactic/exercises/substitution.ma index e3472c7a4..8ac8fbc1e 100644 --- a/helm/software/matita/library/didactic/exercises/substitution.ma +++ b/helm/software/matita/library/didactic/exercises/substitution.ma @@ -470,8 +470,8 @@ case FAnd. by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). conclude (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) - = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. - = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*). + = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111. + = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH222(*END*). (*END*) done. case FOr. @@ -492,8 +492,8 @@ case FOr. by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). conclude (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) - = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. - = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111. + = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111. + = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH222. (*END*) done. case FImpl. diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index b970fb0c3..958fddf97 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/matita/library/nat/gcd.ma @@ -761,7 +761,8 @@ cut (n \divides p \lor n \ndivides p) rewrite > (sym_times q (a1*p)). rewrite > (assoc_times a1). elim H1. - applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). + pump 39. + applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). (* rewrite < (sym_times n).rewrite < assoc_times. rewrite > (sym_times q).rewrite > assoc_times. diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index 9d7007145..cd53cc056 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -249,8 +249,9 @@ unfold.intro. elim (divides_times_to_divides ? ? ? H H9). apply (absurd ? ? H10 H5). apply (absurd ? ? H10 H7). -(* rewrite > H6. -rewrite > H8. *) +(* REGRESSION *) +rewrite > H6. +rewrite > H8. autobatch paramodulation. unfold prime in H. elim H. assumption. qed. diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma index 6bbdcec4d..87edf468b 100644 --- a/helm/software/matita/library/nat/times.ma +++ b/helm/software/matita/library/nat/times.ma @@ -129,6 +129,8 @@ variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def associative_times. lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z). -intros.autobatch paramodulation. +intros. +demodulate. reflexivity; +(* autobatch paramodulation. *) qed. -- 2.39.2