From be87825f491f5eff5f02ee78dd23f34fc0e46e71 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 12:49:11 +0000 Subject: [PATCH] new version of auto that is able to prove the irrationality of sqrt(2) --- components/acic_content/.depend | 3 - components/cic/.depend | 4 +- components/extlib/.depend | 2 - components/library/.depend | 1 + components/tactics/.depend | 57 +-- components/tactics/Makefile | 2 + components/tactics/auto.ml | 91 ++-- components/tactics/auto.mli | 10 +- components/tactics/autoCache.ml | 153 +++++++ components/tactics/autoCache.mli | 48 +++ components/tactics/autoTactic.ml | 249 +---------- components/tactics/autoTypes.ml | 126 +----- components/tactics/autoTypes.mli | 26 +- components/tactics/paramodulation/equality.ml | 98 +---- .../tactics/paramodulation/equality.mli | 2 + .../paramodulation/equality_retrieval.ml | 359 ++++++++++++++++ .../paramodulation/equality_retrieval.mli | 61 +++ .../tactics/paramodulation/inference.ml | 397 +----------------- .../tactics/paramodulation/inference.mli | 34 -- .../tactics/paramodulation/saturation.ml | 38 +- .../tactics/paramodulation/saturation.mli | 14 +- components/tactics/tactics.mli | 2 +- 22 files changed, 771 insertions(+), 1006 deletions(-) create mode 100644 components/tactics/autoCache.ml create mode 100644 components/tactics/autoCache.mli create mode 100644 components/tactics/paramodulation/equality_retrieval.ml create mode 100644 components/tactics/paramodulation/equality_retrieval.mli diff --git a/components/acic_content/.depend b/components/acic_content/.depend index a0f6ba9ca..8ade458af 100644 --- a/components/acic_content/.depend +++ b/components/acic_content/.depend @@ -1,4 +1,3 @@ -contentPp.cmi: content.cmi acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmo @@ -8,8 +7,6 @@ acic2astMatcher.cmi: cicNotationPt.cmo termAcicContent.cmi: cicNotationPt.cmo content.cmo: content.cmi content.cmx: content.cmi -contentPp.cmo: content.cmi contentPp.cmi -contentPp.cmx: content.cmx contentPp.cmi acic2content.cmo: content.cmi acic2content.cmi acic2content.cmx: content.cmx acic2content.cmi content2cic.cmo: content.cmi content2cic.cmi diff --git a/components/cic/.depend b/components/cic/.depend index bc476d918..7829317ad 100644 --- a/components/cic/.depend +++ b/components/cic/.depend @@ -21,7 +21,7 @@ helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi libraryObjects.cmo: libraryObjects.cmi libraryObjects.cmx: libraryObjects.cmi -discrimination_tree.cmo: cic.cmo discrimination_tree.cmi -discrimination_tree.cmx: cic.cmx discrimination_tree.cmi +discrimination_tree.cmo: cicUtil.cmi cic.cmo discrimination_tree.cmi +discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi path_indexing.cmo: cic.cmo path_indexing.cmi path_indexing.cmx: cic.cmx path_indexing.cmi diff --git a/components/extlib/.depend b/components/extlib/.depend index c076e9f96..6d96e61e2 100644 --- a/components/extlib/.depend +++ b/components/extlib/.depend @@ -10,8 +10,6 @@ hLog.cmo: hLog.cmi hLog.cmx: hLog.cmi trie.cmo: trie.cmi trie.cmx: trie.cmi -trie.cmo: trie.cmi -trie.cmx: trie.cmi hTopoSort.cmo: hTopoSort.cmi hTopoSort.cmx: hTopoSort.cmi refCounter.cmo: refCounter.cmi diff --git a/components/library/.depend b/components/library/.depend index 94e20194f..bc1a71311 100644 --- a/components/library/.depend +++ b/components/library/.depend @@ -1,4 +1,5 @@ cicCoercion.cmi: refinementTool.cmo coercDb.cmi +coercGraph.cmi: coercDb.cmi librarySync.cmi: refinementTool.cmo cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi diff --git a/components/tactics/.depend b/components/tactics/.depend index 04154280b..5f8f9060e 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -6,23 +6,26 @@ proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi autoTypes.cmi: proofEngineTypes.cmi +autoCache.cmi: proofEngineTypes.cmi paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi -paramodulation/inference.cmi: paramodulation/subst.cmi proofEngineTypes.cmi \ - paramodulation/equality.cmi autoTypes.cmi +paramodulation/equality_retrieval.cmi: proofEngineTypes.cmi \ + paramodulation/equality.cmi autoTypes.cmi autoCache.cmi +paramodulation/inference.cmi: paramodulation/subst.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/equality_indexing.cmi \ paramodulation/equality.cmi paramodulation/saturation.cmi: proofEngineTypes.cmi \ - paramodulation/inference.cmi paramodulation/equality.cmi autoTypes.cmi + paramodulation/equality_retrieval.cmi paramodulation/equality.cmi \ + autoCache.cmi variousTactics.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi -auto.cmi: proofEngineTypes.cmi autoTypes.cmi +auto.cmi: proofEngineTypes.cmi autoTypes.cmi autoCache.cmi autoTactic.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi @@ -63,8 +66,10 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi -autoTypes.cmo: metadataQuery.cmi autoTypes.cmi -autoTypes.cmx: metadataQuery.cmx autoTypes.cmi +autoTypes.cmo: autoTypes.cmi +autoTypes.cmx: autoTypes.cmi +autoCache.cmo: metadataQuery.cmi autoCache.cmi +autoCache.cmx: metadataQuery.cmx autoCache.cmi paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi paramodulation/subst.cmo: paramodulation/subst.cmi @@ -75,14 +80,18 @@ paramodulation/equality.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ paramodulation/equality.cmi +paramodulation/equality_retrieval.cmo: paramodulation/utils.cmi \ + proofEngineTypes.cmi proofEngineHelpers.cmi metadataQuery.cmi \ + paramodulation/equality.cmi autoTypes.cmi autoCache.cmi \ + paramodulation/equality_retrieval.cmi +paramodulation/equality_retrieval.cmx: paramodulation/utils.cmx \ + proofEngineTypes.cmx proofEngineHelpers.cmx metadataQuery.cmx \ + paramodulation/equality.cmx autoTypes.cmx autoCache.cmx \ + paramodulation/equality_retrieval.cmi paramodulation/inference.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ - metadataQuery.cmi paramodulation/equality.cmi autoTypes.cmi \ - paramodulation/inference.cmi + paramodulation/subst.cmi paramodulation/inference.cmi paramodulation/inference.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ - metadataQuery.cmx paramodulation/equality.cmx autoTypes.cmx \ - paramodulation/inference.cmi + paramodulation/subst.cmx paramodulation/inference.cmi paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/equality_indexing.cmi paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ @@ -98,13 +107,13 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \ paramodulation/saturation.cmo: paramodulation/utils.cmi \ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \ - paramodulation/indexing.cmi paramodulation/equality.cmi autoTypes.cmi \ - paramodulation/saturation.cmi + paramodulation/indexing.cmi paramodulation/equality_retrieval.cmi \ + paramodulation/equality.cmi autoCache.cmi paramodulation/saturation.cmi paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \ - paramodulation/indexing.cmx paramodulation/equality.cmx autoTypes.cmx \ - paramodulation/saturation.cmi + paramodulation/indexing.cmx paramodulation/equality_retrieval.cmx \ + paramodulation/equality.cmx autoCache.cmx paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ variousTactics.cmi @@ -133,18 +142,18 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmi -auto.cmo: tacticals.cmi paramodulation/saturation.cmi proofEngineTypes.cmi \ +auto.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \ proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \ - autoTypes.cmi auto.cmi -auto.cmx: tacticals.cmx paramodulation/saturation.cmx proofEngineTypes.cmx \ + autoTypes.cmi autoCache.cmi auto.cmi +auto.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \ - autoTypes.cmx auto.cmi + autoTypes.cmx autoCache.cmx auto.cmi autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \ - paramodulation/equality.cmi autoTypes.cmi auto.cmi autoTactic.cmi + proofEngineHelpers.cmi paramodulation/equality.cmi autoTypes.cmi \ + autoCache.cmi auto.cmi autoTactic.cmi autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \ - paramodulation/equality.cmx autoTypes.cmx auto.cmx autoTactic.cmi + proofEngineHelpers.cmx paramodulation/equality.cmx autoTypes.cmx \ + autoCache.cmx auto.cmx autoTactic.cmi discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 3f4a78872..08df7d546 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -7,9 +7,11 @@ INTERFACE_FILES = \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ autoTypes.mli \ + autoCache.mli \ paramodulation/utils.mli \ paramodulation/subst.mli\ paramodulation/equality.mli\ + paramodulation/equality_retrieval.mli\ paramodulation/inference.mli\ paramodulation/equality_indexing.mli\ paramodulation/indexing.mli \ diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 6b1bf82ab..2db8cc001 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -24,16 +24,19 @@ *) open AutoTypes;; +open AutoCache;; let debug_print s = () (* prerr_endline s;; *) -let given_clause dbd ?tables maxm ?auto cache subst flags status = - prerr_endline ("given_clause " ^ string_of_int maxm); - let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout = +(* {{{ *********** local given_clause wrapper ***********) + +let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status = + let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout = match tables with | None -> + (* first time, do a huge saturation *) let bag, equalities, cache, maxmeta = - Saturation.find_equalities dbd status ?auto true cache + Saturation.find_equalities dbd status ?auto smart_flag cache in let passive = Saturation.make_passive equalities in let active = Saturation.make_active [] in @@ -44,9 +47,11 @@ let given_clause dbd ?tables maxm ?auto cache subst flags status = let maxm = max maxm maxmeta in active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout | Some (active,passive,bag,oldcache) -> + (* saturate a bit more if cache cahnged *) let bag, equalities, cache, maxm = if cache_size oldcache <> cache_size cache then - Saturation.saturate_more bag active maxm status true ?auto cache + Saturation.saturate_more + bag active maxm status smart_flag ?auto cache else bag, [], cache, maxm in @@ -54,17 +59,19 @@ let given_clause dbd ?tables maxm ?auto cache subst flags status = let passive = Saturation.add_to_passive equalities passive in let goal_steps, saturation_steps, timeout = if flags.use_only_paramod then max_int,max_int,flags.timeout - else max 30 minsteps, minsteps, infinity + else max 80 minsteps, minsteps, infinity in active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout in - let res,a,p, maxmeta = + let res,actives,passives,maxmeta = Saturation.given_clause bag maxmeta status active passive goal_steps saturation_steps timeout in - res,a,p,bag,cache,maxmeta + res,actives,passives,bag,cache,maxmeta ;; +(* }}} ****************************************************************) + (* {{{ **************** applyS *******************) let new_metasenv_and_unify_and_t @@ -101,11 +108,11 @@ let new_metasenv_and_unify_and_t PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) in match - let cache, flags = AutoTypes.cache_empty, AutoTypes.default_flags() in + let cache, flags = cache_empty, default_flags() in let flags = {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} in - given_clause dbd ?tables 0 cache [] flags (proof'''',newmeta) + given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta) with | None, active, passive, bag,_,_ -> raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) @@ -271,7 +278,7 @@ let equational_case prerr_endline (cache_print context cache); prerr_endline ""; match - given_clause dbd ?tables maxm ?auto cache subst flags (fake_proof,goalno) + given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) with | None, active,passive, bag, cache, maxmeta -> let tables = Some (active,passive,bag,cache) in @@ -307,9 +314,9 @@ let try_candidate ;; let applicative_case - dbd tables maxm depth subst fake_proof goalno goalty metasenv context universe + dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache = - let candidates = get_candidates universe goalty in + let candidates = get_candidates cache goalty in let tables, elems, maxm = List.fold_left (fun (tables,elems,maxm) cand -> @@ -322,7 +329,7 @@ let applicative_case (tables,[],maxm) candidates in let elems = sort_new_elems elems in - elems, tables, maxm + elems, tables, cache, maxm ;; (* Works if there is no dependency over proofs *) @@ -339,9 +346,11 @@ let calculate_timeout flags = let is_equational_case goalty flags = let ensure_equational t = if is_an_equational_goal t then true - else + else false + (* let msg="Not an equational goal.\nYou cant use the paramodulation flag"in raise (ProofEngineTypes.Fail (lazy msg)) + *) in (flags.use_paramod && is_an_equational_goal goalty) || (flags.use_only_paramod && ensure_equational goalty) @@ -350,14 +359,14 @@ let cache_add_success sort cache k v = if sort = P then cache_add_success cache k v else cache ;; -let rec auto_main dbd tables maxm context flags elems cache universe = +let rec auto_main dbd tables maxm context flags elems cache = let callback_for_paramod maxm flags proof commonctx cache l = - let flags = {flags with use_paramod = false} in + let flags = {flags with use_paramod = false;dont_cache_failures=true} in let _,metasenv,_,_ = proof in let oldmetasenv = metasenv in match auto_all_solutions - dbd tables maxm universe cache commonctx metasenv l flags + dbd tables maxm cache commonctx metasenv l flags with | [],cache,maxm -> [],cache,maxm | solutions,cache,maxm -> @@ -396,10 +405,15 @@ let rec auto_main dbd tables maxm context flags elems cache universe = aux tables maxm cache tl (* FAILURE (not in prop) *)) else match aux_single tables maxm cache metasenv subst elem goalty cc with - | Fail _, tables, cache, maxm' -> + | Fail s, tables, cache, maxm' -> assert(maxm' >= maxm);let maxm = maxm' in - debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty); - let cache = cache_add_failure cache goalty depth in + debug_print + (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty); + let cache = + if flags.dont_cache_failures then + cache_remove_underinspection cache goalty + else cache_add_failure cache goalty depth + in aux tables maxm cache tl | Success (metasenv,subst,others), tables, cache, maxm' -> assert(maxm' >= maxm);let maxm = maxm' in @@ -439,7 +453,8 @@ let rec auto_main dbd tables maxm context flags elems cache universe = (* FAILURE (euristic cut) *) match cache_examine cache goalty with | Failed_in d when d >= depth -> - Fail "depth",tables,cache,maxm(*FAILURE(depth)*) + Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth), + tables,cache,maxm(*FAILURE(depth)*) | Succeded t -> assert(List.for_all (fun (i,_) -> i <> goalno) subst); let entry = goalno, (cc, t,goalty) in @@ -463,15 +478,11 @@ let rec auto_main dbd tables maxm context flags elems cache universe = | Some elems, tables, cache, maxm -> elems, tables, cache, maxm (* manca cache *) | None, tables,cache,maxm -> - let elems, tables, maxm = applicative_case dbd tables maxm depth subst fake_proof goalno - goalty metasenv context universe - in elems, tables, cache, maxm + goalty metasenv context cache else - let elems, tables, maxm = applicative_case dbd tables maxm depth subst fake_proof goalno - goalty metasenv context universe - in elems, tables, cache, maxm + goalty metasenv context cache in aux tables maxm cache elems | _ -> Fail "??",tables,cache,maxm @@ -479,13 +490,13 @@ let rec auto_main dbd tables maxm context flags elems cache universe = aux tables maxm cache elems and - auto_all_solutions dbd tables maxm universe cache context metasenv gl flags + auto_all_solutions dbd tables maxm cache context metasenv gl flags = let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in let elems = [metasenv,[],goals] in let rec aux tables maxm solutions cache elems flags = - match auto_main dbd tables maxm context flags elems cache universe with + match auto_main dbd tables maxm context flags elems cache with | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm | Success (metasenv,subst,others),tables,cache,maxm -> if Unix.gettimeofday () > flags.timeout then @@ -500,25 +511,23 @@ and (* }}} ****************** AUTO ***************) -let auto_all_solutions dbd universe cache context metasenv gl flags = +let auto_all_solutions dbd cache context metasenv gl flags = let solutions, cache, _ = - auto_all_solutions dbd None 0 universe cache context metasenv gl flags + auto_all_solutions dbd None 0 cache context metasenv gl flags in solutions, cache ;; -let auto dbd universe cache context metasenv gl flags = +let auto dbd cache context metasenv gl flags = + let initial_time = Unix.gettimeofday() in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in let elems = [metasenv,[],goals] in - match auto_main dbd None 0 context flags elems cache universe with - | Success (metasenv,subst,_), tables,cache,_ -> Some (subst,metasenv), cache - | Fail s,tables,cache,maxm -> - let cache = cache_clean cache in - match auto_main dbd tables maxm context flags elems cache universe with - | Success (metasenv,subst,_), tables,cache,_ -> - Some (subst,metasenv), cache - | Fail s,tables,cache,maxm -> prerr_endline s;None,cache + match auto_main dbd None 0 context flags elems cache with + | Success (metasenv,subst,_), tables,cache,_ -> + prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); + Some (subst,metasenv), cache + | Fail s,tables,cache,maxm -> None,cache ;; let applyS_tac ~dbd ~term = diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli index 68057fa9c..5883f0bf2 100644 --- a/components/tactics/auto.mli +++ b/components/tactics/auto.mli @@ -26,23 +26,21 @@ (* stops at the first solution *) val auto: HMysql.dbd -> - AutoTypes.universe -> - AutoTypes.cache -> + AutoCache.cache -> Cic.context -> Cic.metasenv -> ProofEngineTypes.goal list -> (* goals in AND *) AutoTypes.flags -> - (Cic.substitution * Cic.metasenv) option * AutoTypes.cache + (Cic.substitution * Cic.metasenv) option * AutoCache.cache val auto_all_solutions: HMysql.dbd -> - AutoTypes.universe -> - AutoTypes.cache -> + AutoCache.cache -> Cic.context -> Cic.metasenv -> ProofEngineTypes.goal list -> AutoTypes.flags -> - (Cic.substitution * Cic.metasenv) list * AutoTypes.cache + (Cic.substitution * Cic.metasenv) list * AutoCache.cache val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml new file mode 100644 index 000000000..b4e074a64 --- /dev/null +++ b/components/tactics/autoCache.ml @@ -0,0 +1,153 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module Codomain = struct + type t = Cic.term + let compare = Pervasives.compare +end +module S = Set.Make(Codomain) +module TI = Discrimination_tree.DiscriminationTreeIndexing(S) +type universe = TI.t +(* (proof,ty) list *) +type cache_key = Cic.term +type cache_elem = + | Failed_in of int + | Succeded of Cic.term + | UnderInspection + | Notfound +type cache = (universe * ((cache_key * cache_elem) list));; + +let cache_empty = (TI.empty,[]);; +let get_candidates (univ,_) ty = + S.elements (TI.retrieve_unifiables univ ty) +;; +let rec head = function + | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t) + | t -> t +;; +let index ((univ,oldcache) as cache) key term = + match key with + | Cic.Meta _ -> cache + | _ -> + prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term); + (TI.index univ key term,oldcache) +;; +let cache_add_library dbd proof gl cache = + let univ = MetadataQuery.universe_of_goals ~dbd proof gl in + let terms = List.map CicUtil.term_of_uri univ in + let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in + List.fold_left + (fun acc term -> + let key = head (tyof term) in + index acc key term) + cache terms +;; +let cache_add_context ctx metasenv cache = + let tail = function [] -> [] | h::tl -> tl in + let rc,_,_ = + List.fold_left + (fun (acc,i,ctx) ctxentry -> + match ctxentry with + | Some (_,Cic.Decl t) -> + let key = CicSubstitution.lift i (head t) in + let elem = Cic.Rel i in + index acc key elem, i+1, tail ctx + | Some (_,Cic.Def (_,Some t)) -> + let key = CicSubstitution.lift i (head t) in + let elem = Cic.Rel i in + index acc key elem, i+1, tail ctx + | Some (_,Cic.Def (t,None)) -> + let ctx = tail ctx in + let key,_ = + CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph + in + let elem = Cic.Rel i in + let key = CicSubstitution.lift i (head key) in + index acc key elem, i+1, ctx + | _ -> acc,i+1,tail ctx) + (cache,1,ctx) ctx + in + rc +;; + +let cache_examine (_,oldcache) cache_key = + try List.assoc cache_key oldcache with Not_found -> Notfound +;; +let cache_replace (univ,oldcache) key v = + let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in + univ, (key,v)::oldcache +;; +let cache_remove (univ,oldcache) key = + let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in + univ,oldcache +;; +let cache_add_failure cache cache_key depth = + match cache_examine cache cache_key with + | Failed_in i when i > depth -> cache + | Notfound + | Failed_in _ + | UnderInspection -> cache_replace cache cache_key (Failed_in depth) + | Succeded t -> + prerr_endline (CicPp.ppterm t); + assert false (* if succed it can't fail *) +;; +let cache_add_success ((univ,_) as cache) cache_key proof = + TI.index univ cache_key proof,snd + (match cache_examine cache cache_key with + | Failed_in _ -> cache_replace cache cache_key (Succeded proof) + | UnderInspection -> cache_replace cache cache_key (Succeded proof) + | Succeded t -> (* we may decide to keep the smallest proof *) cache + | Notfound -> cache_replace cache cache_key (Succeded proof)) +;; +let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth = + match cache_examine cache cache_key with + | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection + | Notfound -> univ,(cache_key,UnderInspection)::oldcache + | Failed_in _ + | UnderInspection + | Succeded _ -> assert false (* it must be a new goal *) +;; +let cache_print context (_,oldcache) = + let names = List.map (function None -> None | Some (x,_) -> Some x) context in + String.concat "\n" + (HExtlib.filter_map + (function + | (k,Succeded _) -> Some (CicPp.pp k names) + | _ -> None) + oldcache) +;; +let cache_remove_underinspection ((univ,oldcache) as cache) cache_key = + match cache_examine cache cache_key with + | Notfound + | UnderInspection -> cache_remove cache cache_key + | Failed_in _ -> assert false + | Succeded _ -> assert false (* it must be a new goal *) +;; +let cache_size (_,oldcache) = + List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache) +;; +let cache_clean (univ,oldcache) = + univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache +;; diff --git a/components/tactics/autoCache.mli b/components/tactics/autoCache.mli new file mode 100644 index 000000000..b47a29925 --- /dev/null +++ b/components/tactics/autoCache.mli @@ -0,0 +1,48 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type cache +type cache_key = Cic.term +type cache_elem = + | Failed_in of int + | Succeded of Cic.term + | UnderInspection + | Notfound +val get_candidates: cache -> Cic.term -> Cic.term list +val cache_add_library: + HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list -> + cache -> cache +val cache_add_context: Cic.context -> Cic.metasenv -> cache -> cache + +val cache_examine: cache -> cache_key -> cache_elem +val cache_add_failure: cache -> cache_key -> int -> cache +val cache_add_success: cache -> cache_key -> Cic.term -> cache +val cache_add_underinspection: cache -> cache_key -> int -> cache +val cache_remove_underinspection: cache -> cache_key -> cache +val cache_empty: cache +val cache_print: Cic.context -> cache -> string +val cache_size: cache -> int +val cache_clean: cache -> cache + diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 03fdf9555..bb5399197 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -30,242 +30,6 @@ (* let debug_print = fun _ -> () *) -(* Profiling code -let new_experimental_hint = - let profile = CicUtil.profile "new_experimental_hint" in - fun ~dbd ~facts ?signature ~universe status -> - profile.profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status -*) let new_experimental_hint = MetadataQuery.new_experimental_hint - -(* In this versions of auto_tac we maintain an hash table of all inspected - goals. We assume that the context is invariant for application. - To this aim, it is essential to sall hint_verbose, that in turns calls - apply_verbose. *) - -type exitus = - No of int - | Yes of Cic.term * int - | NotYetInspected - -let inspected_goals = Hashtbl.create 503;; - -let search_theorems_in_context status = - let (proof, goal) = status in - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let module PET = ProofEngineTypes in - let module PT = PrimitiveTactics in - let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let rec find n = function - | [] -> [] - | hd::tl -> - let res = - (* we should check that the hypothesys has not been cleared *) - if List.nth context (n-1) = None then - None - else - try - let (subst,(proof, goal_list)) = - PT.apply_tac_verbose ~term:(C.Rel n) status - in - (* - let goal_list = - List.stable_sort (compare_goal_list proof) goal_list in - *) - Some (subst,(proof, goal_list)) - with - PET.Fail _ -> None - in - (match res with - | Some res -> res::(find (n+1) tl) - | None -> find (n+1) tl) - in - try - find 1 context - with Failure s -> [] -;; - - -let compare_goals proof goal1 goal2 = - let _,metasenv,_,_ = proof in - let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in - let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in - let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 - CicUniv.empty_ugraph in - let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2 - CicUniv.empty_ugraph in - let prop1 = - let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 - CicUniv.empty_ugraph in - if b then 0 else 1 - in - let prop2 = - let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 - CicUniv.empty_ugraph in - if b then 0 else 1 - in - prop1 - prop2 - - -let new_search_theorems f dbd proof goal depth sign = - let choices = f (proof,goal) - in - List.map - (function (subst,(proof, goallist)) -> - (* let goallist = reorder_goals dbd sign proof goallist in *) - let goallist = List.sort (compare_goals proof) goallist in - (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign))) - choices -;; - -exception NoOtherChoices;; - -let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals - universe - = - if depth = 0 then [] else - if List.mem ty already_seen_goals then [] else - let already_seen_goals = ty::already_seen_goals in - let facts = (depth = 1) in - let _,metasenv,p,_ = proof in - (* first of all we check if the goal has been already - inspected *) - assert (CicUtil.exists_meta goal metasenv); - let exitus = - try Hashtbl.find inspected_goals ty - with Not_found -> NotYetInspected in - let is_meta_closed = CicUtil.is_meta_closed ty in - begin - match exitus with - Yes (bo,_) -> - (* - debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); - debug_print (lazy (CicPp.ppterm ty)); - *) - let subst_in = - (* if we just apply the subtitution, the type - is irrelevant: we may use Implicit, since it will - be dropped *) - CicMetaSubst.apply_subst - [(goal,(ey, bo, Cic.Implicit None))] in - let (proof,_) = - ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goal subst_in metasenv in - [(subst_in,(proof,[],sign))] - | No d when (d >= depth) -> - (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *) - [] (* the empty list means no choices, i.e. failure *) - | No _ - | NotYetInspected -> - debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty)); - debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p)); - debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey)); - let sign, new_sign = - if is_meta_closed then - None, Some (MetadataConstraints.signature_of ty) - else sign,sign in (* maybe the union ? *) - let local_choices = - new_search_theorems - search_theorems_in_context dbd - proof goal (depth-1) new_sign in - let global_choices = - new_search_theorems - (fun status -> - List.map snd - (new_experimental_hint - ~dbd ~facts:facts ?signature:sign ~universe status)) - dbd proof goal (depth-1) new_sign in - let all_choices = - local_choices@global_choices in - let sorted_choices = - List.stable_sort - (fun (_, (_, goals1, _)) (_, (_, goals2, _)) -> - Pervasives.compare - (List.length goals1) (List.length goals2)) - all_choices in - (match (auto_new dbd width already_seen_goals universe sorted_choices) - with - [] -> - (* no proof has been found; we update the - hastable *) - (* if is_meta_closed then *) - Hashtbl.add inspected_goals ty (No depth); - [] - | (subst,(proof,[],sign))::tl1 -> - (* a proof for goal has been found: - in order to get the proof we apply subst to - Meta[goal] *) - if is_meta_closed then - begin - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable ey in - let meta_proof = - subst (Cic.Meta(goal,irl)) in - Hashtbl.add inspected_goals - ty (Yes (meta_proof,depth)); -(* - begin - let cty,_ = - CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph - in - if not (cty = ty) then - begin - debug_print (lazy ("ty = "^CicPp.ppterm ty)); - debug_print (lazy ("cty = "^CicPp.ppterm cty)); - assert false - end - Hashtbl.add inspected_goals - ty (Yes (meta_proof,depth)); - end; -*) - end; - (subst,(proof,[],sign))::tl1 - | _ -> assert false) - end - -and auto_new dbd width already_seen_goals universe = function - | [] -> [] - | (subst,(proof, goals, sign))::tl -> - let _,metasenv,_,_ = proof in - let goals'= - List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals - in - auto_new_aux dbd - width already_seen_goals universe ((subst,(proof, goals', sign))::tl) - -and auto_new_aux dbd width already_seen_goals universe = function - | [] -> [] - | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl - | (subst,(proof, (goal,0)::_, _))::tl -> - auto_new dbd width already_seen_goals universe tl - | (subst,(proof, goals, _))::tl when - (List.length goals) > width -> - auto_new dbd width already_seen_goals universe tl - | (subst,(proof, (goal,depth)::gtl, sign))::tl -> - let _,metasenv,p,_ = proof in - let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in - match (auto_single dbd proof goal ey ty depth - (width - (List.length gtl)) sign already_seen_goals) universe - with - [] -> auto_new dbd width already_seen_goals universe tl - | (local_subst,(proof,[],sign))::tl1 -> - let new_subst f t = f (subst t) in - let is_meta_closed = CicUtil.is_meta_closed ty in - let all_choices = - if is_meta_closed then - (new_subst local_subst,(proof,gtl,sign))::tl - else - let tl2 = - (List.map - (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1) - in - (new_subst local_subst,(proof,gtl,sign))::tl2@tl in - auto_new dbd width already_seen_goals universe all_choices - | _ -> assert false - ;; - let bool params name default = try let s = List.assoc name params in @@ -315,10 +79,10 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = (* this is the real auto *) let _, metasenv, _, _ = proof in let _, context, goalty = CicUtil.lookup_meta goal metasenv in - let universe = - AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe + let cache = + AutoCache.cache_add_library dbd proof [goal] AutoCache.cache_empty in - let universe = AutoTypes.universe_of_context context metasenv universe in + let cache = AutoCache.cache_add_context context metasenv cache in let oldmetasenv = metasenv in let flags = { AutoTypes.maxdepth = depth; @@ -327,10 +91,11 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = if timeout = 0 then float_of_int timeout else Unix.gettimeofday() +. (float_of_int timeout); AutoTypes.use_paramod = use_paramod; - AutoTypes.use_only_paramod = use_only_paramod} + AutoTypes.use_only_paramod = use_only_paramod; + AutoTypes.dont_cache_failures = false + } in - let cache = AutoTypes.cache_empty in - match Auto.auto dbd universe cache context metasenv [goal] flags with + match Auto.auto dbd cache context metasenv [goal] flags with | None,cache -> raise (ProofEngineTypes.Fail (lazy "Auto gave up")) | Some (subst,metasenv),cache -> diff --git a/components/tactics/autoTypes.ml b/components/tactics/autoTypes.ml index 60643d870..17005b06d 100644 --- a/components/tactics/autoTypes.ml +++ b/components/tactics/autoTypes.ml @@ -23,138 +23,18 @@ * http://cs.unibo.it/helm/. *) - -module Codomain = struct - type t = Cic.term - let compare = Pervasives.compare -end -module S = Set.Make(Codomain) -module TI = Discrimination_tree.DiscriminationTreeIndexing(S) -type universe = TI.t - -let empty_universe = TI.empty -let get_candidates universe ty = - S.elements (TI.retrieve_unifiables universe ty) -;; -let rec head = function - | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t) - | t -> t -;; -let index acc key term = - match key with - | Cic.Meta _ -> acc - | _ -> - prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term); - TI.index acc key term -;; -let universe_of_goals dbd proof gl universe = - let univ = MetadataQuery.universe_of_goals ~dbd proof gl in - let terms = List.map CicUtil.term_of_uri univ in - let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in - List.fold_left - (fun acc term -> - let key = head (tyof term) in - index acc key term) - universe terms -;; -let universe_of_context ctx metasenv universe = - let tail = function [] -> [] | h::tl -> tl in - let rc,_,_ = - List.fold_left - (fun (acc,i,ctx) ctxentry -> - match ctxentry with - | Some (_,Cic.Decl t) -> - let key = CicSubstitution.lift i (head t) in - let elem = Cic.Rel i in - index acc key elem, i+1, tail ctx - | Some (_,Cic.Def (_,Some t)) -> - let key = CicSubstitution.lift i (head t) in - let elem = Cic.Rel i in - index acc key elem, i+1, tail ctx - | Some (_,Cic.Def (t,None)) -> - let ctx = tail ctx in - let key,_ = - CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph - in - let elem = Cic.Rel i in - let key = CicSubstitution.lift i (head key) in - index acc key elem, i+1, ctx - | _ -> universe,i+1,tail ctx) - (universe,1,ctx) ctx - in - rc -;; -let add_to_universe key proof universe = - index universe key proof -;; - -(* (proof,ty) list *) -type cache_key = Cic.term -type cache_elem = - | Failed_in of int - | Succeded of Cic.term - | UnderInspection - | Notfound -type cache = (cache_key * cache_elem) list -let cache_examine cache cache_key = - try List.assoc cache_key cache with Not_found -> Notfound -;; -let cache_replace cache key v = - let cache = List.filter (fun (i,_) -> i <> key) cache in - (key,v)::cache -;; -let cache_add_failure cache cache_key depth = - match cache_examine cache cache_key with - | Failed_in i when i > depth -> cache - | Notfound - | Failed_in _ - | UnderInspection -> cache_replace cache cache_key (Failed_in depth) - | Succeded t -> - prerr_endline (CicPp.ppterm t); - assert false (* if succed it can't fail *) -;; -let cache_add_success cache cache_key proof = - match cache_examine cache cache_key with - | Failed_in _ -> cache_replace cache cache_key (Succeded proof) - | UnderInspection -> cache_replace cache cache_key (Succeded proof) - | Succeded t -> (* we may decide to keep the smallest proof *) cache - | Notfound -> cache_replace cache cache_key (Succeded proof) -;; -let cache_add_underinspection cache cache_key depth = - match cache_examine cache cache_key with - | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection - | Notfound -> (cache_key,UnderInspection)::cache - | Failed_in _ - | UnderInspection - | Succeded _ -> assert false (* it must be a new goal *) -;; -let cache_empty = [] -let cache_print context cache = - let names = List.map (function None -> None | Some (x,_) -> Some x) context in - String.concat "\n" - (HExtlib.filter_map - (function - | (k,Succeded _) -> Some (CicPp.pp k names) - | _ -> None) - cache) -;; -let cache_size cache = - List.length (List.filter (function (_,Succeded _) -> true | _ -> false) cache) -;; -let cache_clean cache = - List.filter (function (_,Succeded _) -> true | _ -> false) cache -;; - type flags = { maxwidth: int; maxdepth: int; timeout: float; use_paramod: bool; use_only_paramod : bool; + dont_cache_failures: bool; } let default_flags _ = - {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false} + {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. + 3.0;use_paramod=true;use_only_paramod=false;dont_cache_failures=false} ;; (* (metasenv, subst, (metano,depth)list *) diff --git a/components/tactics/autoTypes.mli b/components/tactics/autoTypes.mli index 1cf966ca0..f1a078359 100644 --- a/components/tactics/autoTypes.mli +++ b/components/tactics/autoTypes.mli @@ -23,37 +23,13 @@ * http://cs.unibo.it/helm/. *) -type universe -val empty_universe:universe -val get_candidates: universe -> Cic.term -> Cic.term list -val universe_of_goals: - HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list -> - universe -> universe -val universe_of_context: Cic.context -> Cic.metasenv -> universe -> universe -val add_to_universe: Cic.term -> Cic.term -> universe -> universe - -type cache -type cache_key = Cic.term -type cache_elem = - | Failed_in of int - | Succeded of Cic.term - | UnderInspection - | Notfound -val cache_examine: cache -> cache_key -> cache_elem -val cache_add_failure: cache -> cache_key -> int -> cache -val cache_add_success: cache -> cache_key -> Cic.term -> cache -val cache_add_underinspection: cache -> cache_key -> int -> cache -val cache_empty: cache -val cache_print: Cic.context -> cache -> string -val cache_size: cache -> int -val cache_clean: cache -> cache - type flags = { maxwidth: int; maxdepth: int; timeout: float; use_paramod: bool; use_only_paramod : bool; + dont_cache_failures: bool; } val default_flags : unit -> flags diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index cfef9452f..b229cc05f 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -46,6 +46,7 @@ and proof = (* subst, (rule,eq1, eq2,predicate) *) 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 type goal = goal_proof * Cic.metasenv * Cic.term @@ -95,8 +96,8 @@ let string_of_equality ?env eq = id w (CicPp.ppterm ty) (CicPp.ppterm left) (Utils.string_of_comparison o) (CicPp.ppterm right) - (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) -(* "..." *) +(* (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *) + "..." | Some (_, context, _) -> let names = Utils.names_of_context context in let w, _, (ty, left, right, o), m , id = open_equality eq in @@ -224,7 +225,8 @@ let mk_trans uri ty t1 t2 t3 p12 p23 = ;; let mk_eq_ind uri ty what pred p1 other p2 = - Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2] + let ens, args = build_ens uri [ty; what; pred; p1; other; p2] in + Cic.Appl (Cic.Const (uri, ens) :: args) ;; let p_of_sym ens tl = @@ -266,34 +268,6 @@ let is_not_fixed t = CicSubstitution.subst (Cic.Rel 1) t ;; -let head_of_apply = function | Cic.Appl (hd::_) -> hd | t -> t;; -let tail_of_apply = function | Cic.Appl (_::tl) -> tl | t -> [];; -let count_args t = List.length (tail_of_apply t);; -let rec build_nat = - let u = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in - function - | 0 -> Cic.MutConstruct(u,0,1,[]) - | n -> - Cic.Appl [Cic.MutConstruct(u,0,2,[]);build_nat (n-1)] -;; -let tyof context menv t = - try - fst(CicTypeChecker.type_of_aux' menv context t CicUniv.empty_ugraph) - with - | CicTypeChecker.TypeCheckerFailure _ - | CicTypeChecker.AssertFailure _ -> assert false -;; -let rec lambdaof left context = function - | Cic.Prod (n,s,t) -> - Cic.Lambda (n,s,lambdaof left context t) - | Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r] - when LibraryObjects.is_eq_URI uri -> if left then l else r - | t -> - let names = Utils.names_of_context context in - prerr_endline ("lambdaof: " ^ (CicPp.pp t names)); - assert false -;; - let canonical t context menv = let rec remove_refl t = match t with @@ -334,54 +308,6 @@ let canonical t context menv = Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, []) in Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p])) - -(* - let sym_eq = Cic.Const(uri_sym,ens) in - let eq_f = Cic.Const(uri_feq,[]) in - let b = Cic.MutConstruct (UriManager.uri_of_string - "cic:/matita/datatypes/bool/bool.ind",0,1,[]) - in - let u = ty1 in - let ctx = f in - let n = build_nat (count_args p) in - let h = head_of_apply p in - let predl = lambdaof true context (tyof context menv h) in - let predr = lambdaof false context (tyof context menv h) in - let args = tail_of_apply p in - let appl = - Cic.Appl - ([Cic.Const(UriManager.uri_of_string - "cic:/matita/paramodulation/rewrite.con",[]); - eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @ - args) - in - appl -*) -(* - | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) - when LibraryObjects.is_eq_ind_URI uri_ind || - LibraryObjects.is_eq_ind_r_URI uri_ind -> - let ty, what, pred, p1, other, p2 = - match tl with - | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2 - | _ -> assert false - in - let pred,l,r = - match pred with - | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r]) - when LibraryObjects.is_eq_URI uri -> - Cic.Lambda - (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r - | _ -> - prerr_endline (CicPp.ppterm pred); - assert false - in - let l = CicSubstitution.subst what l in - let r = CicSubstitution.subst what r in - Cic.Appl - [he;ty;what;pred; - canonical (mk_sym uri_sym ty l r p1);other;canonical p2] -*) | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t when LibraryObjects.is_eq_URI uri -> t | _ -> Cic.Appl (List.map (canonical context) args)) @@ -391,11 +317,6 @@ let canonical t context menv = remove_refl (canonical context t) ;; -let ty_of_lambda = function - | Cic.Lambda (_,ty,_) -> ty - | _ -> assert false -;; - let compose_contexts ctx1 ctx2 = ProofEngineReduction.replace_lifting ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1 @@ -407,11 +328,13 @@ let put_in_ctx ctx t = ;; let mk_eq uri ty l r = - Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] + let ens, args = build_ens uri [ty; l; r] in + Cic.Appl (Cic.MutInd(uri,0,ens) :: args) ;; let mk_refl uri ty t = - Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t] + let ens, args = build_ens uri [ty; t] in + Cic.Appl (Cic.MutConstruct(uri,0,1,ens) :: args) ;; let open_eq = function @@ -421,7 +344,8 @@ let open_eq = function ;; let mk_feq uri_feq ty ty1 left pred right t = - Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t] + let ens, args = build_ens uri_feq [ty;ty1;pred;left;right;t] in + Cic.Appl (Cic.Const(uri_feq,ens) :: args) ;; let rec look_ahead aux = function diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index bd3d4c2ac..3bc9e4309 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -25,6 +25,8 @@ type rule = SuperpositionRight | SuperpositionLeft | Demodulation +(* every equality group has its own bag. the bag contains the infos necessary + * for building the proof. FIXME: should also contain maxmeta! *) type equality_bag val mk_equality_bag: unit -> equality_bag diff --git a/components/tactics/paramodulation/equality_retrieval.ml b/components/tactics/paramodulation/equality_retrieval.ml new file mode 100644 index 000000000..4637a1a43 --- /dev/null +++ b/components/tactics/paramodulation/equality_retrieval.ml @@ -0,0 +1,359 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Utils;; + +let debug_print s = ();;(*prerr_endline (Lazy.force s);;*) + +type auto_type = + int -> + AutoTypes.flags -> + ProofEngineTypes.proof -> + Cic.context -> + AutoCache.cache -> + ProofEngineTypes.goal list -> + Cic.substitution list * AutoCache.cache * int + +let is_var_free (_,term,_ty) = + let rec is_var_free = function + | Cic.Var _ -> false + | Cic.Appl l -> List.for_all is_var_free l + | Cic.Prod (_, s, t) + | Cic.Lambda (_, s, t) + | Cic.LetIn (_, s, t) + | Cic.Cast (s, t) -> (is_var_free s) && (is_var_free t) + | _ -> true + in + is_var_free term +;; + +let rec is_an_equality = function + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] + when (LibraryObjects.is_eq_URI uri) -> true + | Cic.Prod (name, s, t) -> is_an_equality t + | _ -> false +;; + +let build_equality_of_hypothesis bag index head args newmetas maxmeta = + match head with + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] -> + let p = + if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args) + in + debug_print + (lazy + (Printf.sprintf "OK: %s" (CicPp.ppterm p))); + let o = !Utils.compare_terms t1 t2 in + let stat = (ty,t1,t2,o) in + (* 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 + (* to clean the local context of metas *) + Equality.fix_metas bag maxmeta e + | _ -> assert false +;; + +let build_equality bag ty t1 t2 proof menv maxmeta = + let o = !Utils.compare_terms t1 t2 in + let stat = (ty,t1,t2,o) in + let w = compute_equality_weight stat in + let proof = Equality.Exact proof in + let e = Equality.mk_equality bag (w, proof, stat, menv) in + (* to clean the local context of metas *) + Equality.fix_metas bag maxmeta e +;; + +let tty_of_u u = + let t = CicUtil.term_of_uri u in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + t, ty +;; + +let utty_of_u u = + let t,ty = tty_of_u u in + u, t, ty +;; + +let is_monomorphic_eq (_,term,termty) = + let rec last = function + | Cic.Prod(_,_,t) -> last t + | t -> t + in + match last termty with + | Cic.Appl [Cic.MutInd (_, _, []); Cic.Rel _; _; _] -> false + | Cic.Appl [Cic.MutInd (_, _, []); _; _; _] -> true + | _ -> false +;; + +(* +let equations_blacklist = + let blacklist = [ + "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; + "cic:/Coq/Init/Logic/trans_eq.con"; "cic:/Coq/Init/Logic/f_equal.con"; + "cic:/Coq/Init/Logic/f_equal2.con"; "cic:/Coq/Init/Logic/f_equal3.con"; + "cic:/Coq/Init/Logic/f_equal4.con"; "cic:/Coq/Init/Logic/f_equal5.con"; + "cic:/Coq/Init/Logic/sym_eq.con"; "cic:/Coq/Init/Logic/eq_ind.con"; + "cic:/Coq/Init/Logic/eq_ind_r.con"; "cic:/Coq/Init/Logic/eq_rec.con"; + "cic:/Coq/Init/Logic/eq_rec_r.con"; "cic:/Coq/Init/Logic/eq_rect.con"; + "cic:/Coq/Init/Logic/eq_rect_r.con"; "cic:/Coq/Logic/Eqdep/UIP.con"; + "cic:/Coq/Logic/Eqdep/UIP_refl.con";"cic:/Coq/Logic/Eqdep_dec/eq2eqT.con"; + "cic:/Coq/ZArith/Zcompare/rename.con"; + "cic:/Rocq/SUBST/comparith/mult_n_2.con"; + "cic:/matita/logic/equality/eq_f.con";"cic:/matita/logic/equality/eq_f2.con"; + "cic:/matita/logic/equality/eq_rec.con"; + "cic:/matita/logic/equality/eq_rect.con"; ] + in + List.fold_left + (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s) + UriManager.UriSet.empty blacklist +;; +*) +let equations_blacklist = UriManager.UriSet.empty;; + +(* {{{ ****************** SATURATION STUFF ***************************) +exception UnableToSaturate of AutoCache.cache * int + +let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;; + +let saturate_term context metasenv oldnewmeta term cache auto fast = + let head, metasenv, args, newmeta = + ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 + in + let args_for_auto = + HExtlib.filter_map + (function + | Cic.Meta(i,_) -> + let _,_,mt = CicUtil.lookup_meta i metasenv in + let sort,u = + CicTypeChecker.type_of_aux' metasenv context mt + CicUniv.empty_ugraph + in + let b, _ = + CicReduction.are_convertible ~metasenv context + sort (Cic.Sort Cic.Prop) u + in + if b then Some i else None + (* maybe unif or conv should be used instead of = *) + | _ -> assert false) + args + in + let results,cache,newmeta = + if args_for_auto = [] then + let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in + [args,metasenv,newmetas,head,newmeta],cache,newmeta + else + let proof = + None,metasenv,term,term (* term non e' significativo *) + in + let flags = + if fast then + {AutoTypes.default_flags() with + AutoTypes.timeout = Unix.gettimeofday() +. 1.0; + maxwidth = 2;maxdepth = 2; + use_paramod=true;use_only_paramod=false} + else + {AutoTypes.default_flags() with + AutoTypes.timeout = Unix.gettimeofday() +. 1.0; + maxwidth = 2;maxdepth = 4; + use_paramod=true;use_only_paramod=false} + in + match auto newmeta flags proof context cache args_for_auto with + | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta)) + | substs,cache,newmeta -> + List.map + (fun subst -> + 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 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 + in + results,cache,newmeta +;; +(* }}} ***************************************************************) + +let find_context_equalities + maxmeta bag ?(auto = default_auto) context proof cache += + prerr_endline "find_equalities"; + let module C = Cic in + let module S = CicSubstitution in + let module T = CicTypeChecker in + let _,metasenv,_,_ = proof in + let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in + let rec aux cache index newmeta = function + | [] -> [], newmeta,cache + | (Some (_, C.Decl (term)))::tl -> + debug_print + (lazy + (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term))); + let do_find 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 = + saturate_term context metasenv newmeta term + cache auto false + in + let eqs,newmeta = + List.fold_left + (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> + let newmeta, equality = + build_equality_of_hypothesis + bag index head args newmetas (max newmeta newmeta') + in + equality::acc, newmeta + 1) + ([],newmeta) saturated + in + eqs, newmeta, cache + with UnableToSaturate (cache,newmeta) -> + [],newmeta,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_of_hypothesis bag index term [] [] newmeta + in + [e], (newmeta+1),cache + | _ -> [], newmeta, 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 + | _::tl -> + aux cache (index+1) newmeta tl + in + let il, maxm, cache = + aux cache 1 newmeta context + in + let indexes, equalities = List.split il in + indexes, equalities, maxm, cache +;; + +let find_library_equalities bag + ?(auto = default_auto) caso_strano dbd context status maxmeta cache += + let module C = Cic in + let module S = CicSubstitution in + let module T = CicTypeChecker in + let proof, goalno = status in + let _,metasenv,_,_ = proof in + let metano,context,ty = CicUtil.lookup_meta goalno metasenv in + let signature = + if caso_strano then + begin + match ty with + | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] -> + (let mainl, sigl = MetadataConstraints.signature_of l in + let mainr, sigr = MetadataConstraints.signature_of r in + match mainl,mainr with + | Some (uril,tyl), Some (urir, tyr) + when LibraryObjects.is_eq_URI uril && + LibraryObjects.is_eq_URI urir && + tyl = tyr -> + Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr) + | _ -> + let u = (UriManager.uri_of_string + (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in + let main = Some (u, []) in + Some (main,MetadataConstraints.UriManagerSet.union sigl sigr)) + | _ -> assert false + end + else + None + in + let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in + let candidates = List.map utty_of_u eqs in + let candidates = List.filter is_monomorphic_eq candidates in + let candidates = List.filter is_var_free candidates in + let rec aux cache newmeta = function + | [] -> [], newmeta, cache + | (uri, term, termty)::tl -> + debug_print + (lazy + (Printf.sprintf "Examining: %s (%s)" + (CicPp.ppterm term) (CicPp.ppterm termty))); + let res, newmeta, cache = + match termty with + | C.Prod (name, s, t) -> + (try + let saturated,cache,newmeta = + saturate_term context metasenv newmeta termty + cache auto true + in + let eqs,newmeta = + List.fold_left + (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> + match head with + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when LibraryObjects.is_eq_URI uri -> + let proof = C.Appl (term::args) in + let maxmeta, equality = + build_equality bag ty t1 t2 proof newmetas + (max newmeta newmeta') + in + equality::acc,maxmeta + 1 + | _ -> assert false) + ([],newmeta) saturated + in + eqs, newmeta , cache + with UnableToSaturate (cache,newmeta) -> + [], newmeta , cache) + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> + let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in + [e], newmeta+1, cache + | _ -> assert false + in + let res = List.map (fun e -> uri, e) res in + let tl, newmeta, cache = aux cache newmeta tl in + res @ tl, newmeta, cache + in + let found, maxm, cache = + aux cache maxmeta candidates + in + let uriset, eqlist = + let mceq = Equality.meta_convertibility_eq in + (List.fold_left + (fun (s, l) (u, e) -> + if List.exists (mceq e) (List.map snd l) then ( + debug_print + (lazy + (Printf.sprintf "NO!! %s already there!" + (Equality.string_of_equality e))); + (UriManager.UriSet.add u s, l) + ) else (UriManager.UriSet.add u s, (u, e)::l)) + (UriManager.UriSet.empty, []) found) + in + uriset, eqlist, maxm, cache +;; + diff --git a/components/tactics/paramodulation/equality_retrieval.mli b/components/tactics/paramodulation/equality_retrieval.mli new file mode 100644 index 000000000..e9506580d --- /dev/null +++ b/components/tactics/paramodulation/equality_retrieval.mli @@ -0,0 +1,61 @@ + +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* the type for the callback used to saturate terms that are not + * equalities (but have = in main conclusion) *) +type auto_type = + int -> (* maxmeta *) + AutoTypes.flags -> + ProofEngineTypes.proof -> + Cic.context -> + AutoCache.cache -> + ProofEngineTypes.goal list -> + Cic.substitution list * AutoCache.cache * int + +(** + scans the context to find all Declarations "left = right"; returns a + list of equalities and their indexes, the maxmeta and the cache resulted + by calling auto. +*) +val find_context_equalities: + int -> (* maxmeta *) + Equality.equality_bag -> + ?auto:auto_type -> + Cic.context -> ProofEngineTypes.proof -> (* FIXME:Why bot context and proof?*) + AutoCache.cache -> + int list * Equality.equality list * int * AutoCache.cache + +(** + searches the library for equalities and operates as find_context_equalities +*) +val find_library_equalities: + Equality.equality_bag -> + ?auto:auto_type -> + bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> + AutoCache.cache -> + UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int * + AutoCache.cache + diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index 9ada69943..ac80099b0 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -30,16 +30,7 @@ open Utils;; open Printf;; -type auto_type = - int -> - AutoTypes.flags -> - ProofEngineTypes.proof -> - Cic.context -> - AutoTypes.cache -> - ProofEngineTypes.goal list -> - Cic.substitution list * AutoTypes.cache * int - -let debug_print s = prerr_endline (Lazy.force s);; +let debug_print s = ();;(*prerr_endline (Lazy.force s);;*) let check_disjoint_invariant subst metasenv msg = if (List.exists @@ -207,390 +198,4 @@ let unification m1 m2 c t1 t2 ug = raise exn ;; - -let check_eq context msg eq = - let w, proof, (eq_ty, left, right, order), metas = eq in - if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty - (fst (CicTypeChecker.type_of_aux' metas context left CicUniv.empty_ugraph)) - CicUniv.empty_ugraph)) - then - begin - prerr_endline msg; - assert false; - end - else () -;; - -let default_auto maxm _ _ _ _ _ = - [],AutoTypes.cache_empty,maxm -;; - -(* far sta roba e' un casino perche' bisogna pulire il contesto lasciando solo - * la roba che non dipende da i *) -let pi_of_ctx t i ctx = - let rec aux j = function - | [] -> t - | (Some (nam, Cic.Decl (term)))::tl -> Cic.Prod(nam,term,aux (j-1) tl) - | _ -> assert false (* not implemented *) - in - aux (List.length ctx-1) (List.rev ctx) -;; - -let lambda_of_ctx t i ctx = - let rec aux j = function - | [] -> t - | (Some (nam, Cic.Decl (term)))::tl -> Cic.Lambda(nam,term,aux (j-1) tl) - | _ -> assert false (* not implemented *) - in - aux (List.length ctx -1) (List.rev ctx) -;; - -let rec skip_lambda t l = - match t,l with - | Cic.Lambda (_,_,t), _::((_::_) as tl) -> skip_lambda t tl - | Cic.Lambda (_,_,t), _::[] -> t - | _ -> assert false -;; - -let ty_of_eq = function - | Cic.Appl [Cic.MutInd (_, _, _); ty; _; _] -> ty - | _ -> assert false -;; - -exception UnableToSaturate of AutoTypes.cache * int - -let saturate_term context metasenv oldnewmeta term cache auto fast = - let head, metasenv, args, newmeta = - ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 - in - let args_for_auto = - HExtlib.filter_map - (function - | Cic.Meta(i,_) -> - let _,_,mt = CicUtil.lookup_meta i metasenv in - let sort,u = - CicTypeChecker.type_of_aux' metasenv context mt - CicUniv.empty_ugraph - in - let b, _ = - CicReduction.are_convertible ~metasenv context - sort (Cic.Sort Cic.Prop) u - in - if b then Some i else None - (* maybe unif or conv should be used instead of = *) - | _ -> assert false) - args - in - let results,cache,newmeta = - if args_for_auto = [] then - let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in - [args,metasenv,newmetas,head,newmeta],cache,newmeta - else - let proof = - None,metasenv,term,term (* term non e' significativo *) - in - let flags = - if fast then - {AutoTypes.timeout = Unix.gettimeofday() +. 1.0; - maxwidth = 2;maxdepth = 2; - use_paramod=true;use_only_paramod=false} - else - {AutoTypes.timeout = Unix.gettimeofday() +. 1.0; - maxwidth = 3;maxdepth = 3; - use_paramod=true;use_only_paramod=false} - in - match auto newmeta flags proof context cache args_for_auto with - | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta)) - | substs,cache,newmeta -> - List.map - (fun subst -> - 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 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 - in - results,cache,newmeta -;; - -let rec is_an_equality = function - | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] - when (LibraryObjects.is_eq_URI uri) -> true - | Cic.Prod (name, s, t) -> is_an_equality t - | _ -> false -;; - -let build_equality_of_hypothesis bag index head args newmetas maxmeta = - match head with - | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] -> - let p = - if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args) - in - debug_print - (lazy - (Printf.sprintf "OK: %s" (CicPp.ppterm p))); - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - (* 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 - (* to clean the local context of metas *) - Equality.fix_metas bag maxmeta e - | _ -> assert false -;; - -let build_equality bag ty t1 t2 proof menv maxmeta = - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - let w = compute_equality_weight stat in - let proof = Equality.Exact proof in - let e = Equality.mk_equality bag (w, proof, stat, menv) in - (* to clean the local context of metas *) - Equality.fix_metas bag maxmeta e -;; - -let find_equalities maxmeta bag ?(auto = default_auto) context proof cache = - prerr_endline "find_equalities"; - let module C = Cic in - let module S = CicSubstitution in - let module T = CicTypeChecker in - let _,metasenv,_,_ = proof in - let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in - let rec aux cache index newmeta = function - | [] -> [], newmeta,cache - | (Some (_, C.Decl (term)))::tl -> - debug_print - (lazy - (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term))); - let do_find 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 = - saturate_term context metasenv newmeta term - cache auto false - in - let eqs,newmeta = - List.fold_left - (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> - let newmeta, equality = - build_equality_of_hypothesis - bag index head args newmetas (max newmeta newmeta') - in - equality::acc, newmeta + 1) - ([],newmeta) saturated - in - eqs, newmeta, cache - with UnableToSaturate (cache,newmeta) -> - [],newmeta,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_of_hypothesis bag index term [] [] newmeta - in - [e], (newmeta+1),cache - | _ -> [], newmeta, cache - in - let eqs, newmeta, cache = do_find context term in - if eqs = [] then - debug_print (lazy "skipped") - else - debug_print (lazy "ok"); - let rest, newmeta,cache = - aux cache (index+1) newmeta tl - in - List.map (fun x -> index,x) eqs @ rest, newmeta, cache - | _::tl -> - aux cache (index+1) newmeta tl - in - let il, maxm, cache = - aux cache 1 newmeta context - in - let indexes, equalities = List.split il in - (* ignore (List.iter (check_eq context "find") equalities); *) - indexes, equalities, maxm, cache -;; - - -(* -let equations_blacklist = - List.fold_left - (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s) - UriManager.UriSet.empty [ - "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; - "cic:/Coq/Init/Logic/trans_eq.con"; - "cic:/Coq/Init/Logic/f_equal.con"; - "cic:/Coq/Init/Logic/f_equal2.con"; - "cic:/Coq/Init/Logic/f_equal3.con"; - "cic:/Coq/Init/Logic/f_equal4.con"; - "cic:/Coq/Init/Logic/f_equal5.con"; - "cic:/Coq/Init/Logic/sym_eq.con"; - "cic:/Coq/Init/Logic/eq_ind.con"; - "cic:/Coq/Init/Logic/eq_ind_r.con"; - "cic:/Coq/Init/Logic/eq_rec.con"; - "cic:/Coq/Init/Logic/eq_rec_r.con"; - "cic:/Coq/Init/Logic/eq_rect.con"; - "cic:/Coq/Init/Logic/eq_rect_r.con"; - "cic:/Coq/Logic/Eqdep/UIP.con"; - "cic:/Coq/Logic/Eqdep/UIP_refl.con"; - "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con"; - "cic:/Coq/ZArith/Zcompare/rename.con"; - (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`... - perche' questo cacchio di teorema rompe le scatole :'( *) - "cic:/Rocq/SUBST/comparith/mult_n_2.con"; - - "cic:/matita/logic/equality/eq_f.con"; - "cic:/matita/logic/equality/eq_f2.con"; - "cic:/matita/logic/equality/eq_rec.con"; - "cic:/matita/logic/equality/eq_rect.con"; - ] -;; -*) -let equations_blacklist = UriManager.UriSet.empty;; - -let tty_of_u u = -(* let _ = <:start> in *) - let t = CicUtil.term_of_uri u in - let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in -(* let _ = <:stop> in *) - t, ty -;; - -let utty_of_u u = - let t,ty = tty_of_u u in - u, t, ty -;; - -let find_library_equalities bag - ?(auto = default_auto) caso_strano dbd context status maxmeta cache -= - prerr_endline "find_library_equalities"; - let module C = Cic in - let module S = CicSubstitution in - let module T = CicTypeChecker in -(* let _ = <:start> in *) - let proof, goalno = status in - let _,metasenv,_,_ = proof in - let metano,context,ty = CicUtil.lookup_meta goalno metasenv in - let signature = - if caso_strano then - begin - match ty with - | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] -> - (let mainl, sigl = MetadataConstraints.signature_of l in - let mainr, sigr = MetadataConstraints.signature_of r in - match mainl,mainr with - | Some (uril,tyl), Some (urir, tyr) - when LibraryObjects.is_eq_URI uril && - LibraryObjects.is_eq_URI urir && - tyl = tyr -> - Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr) - | _ -> - let u = (UriManager.uri_of_string - (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in - let main = Some (u, []) in - Some (main,MetadataConstraints.UriManagerSet.union sigl sigr)) - | _ -> assert false - end - else - None - in - prerr_endline "find_library_equalities.1"; - let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in -(* let _ = <:stop> in *) - prerr_endline "find_library_equalities.2"; - let is_var_free (_,term,_ty) = - let rec is_var_free = function - | C.Var _ -> false - | C.Appl l -> List.for_all is_var_free l - | C.Prod (_, s, t) | C.Lambda (_, s, t) - | C.LetIn (_, s, t) | C.Cast (s, t) -> (is_var_free s) && (is_var_free t) - | _ -> true - in - is_var_free term - in - let is_monomorphic_eq (_,term,termty) = - let rec last = function - | Cic.Prod(_,_,t) -> last t - | t -> t - in - match last termty with - | C.Appl [C.MutInd (_, _, []); Cic.Rel _; _; _] -> false - | C.Appl [C.MutInd (_, _, []); _; _; _] -> true - | _ -> false - in - let candidates = List.map utty_of_u eqs in - let candidates = List.filter is_monomorphic_eq candidates in - let candidates = List.filter is_var_free candidates in - let rec aux cache newmeta = function - | [] -> [], newmeta, cache - | (uri, term, termty)::tl -> - debug_print - (lazy - (Printf.sprintf "Examining: %s (%s)" - (CicPp.ppterm term) (CicPp.ppterm termty))); - let res, newmeta, cache = - match termty with - | C.Prod (name, s, t) -> - (try - let saturated,cache,newmeta = - saturate_term context metasenv newmeta termty - cache auto true - in - let eqs,newmeta = - List.fold_left - (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> - match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when LibraryObjects.is_eq_URI uri -> - let proof = C.Appl (term::args) in - prerr_endline ("PROVA: " ^ CicPp.ppterm proof); - let maxmeta, equality = - build_equality bag ty t1 t2 proof newmetas - (max newmeta newmeta') - in - equality::acc,maxmeta + 1 - | _ -> assert false) - ([],newmeta) saturated - in - eqs, newmeta , cache - with UnableToSaturate (cache,newmeta) -> - [], newmeta , cache) - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> - let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in - [e], newmeta+1, cache - | _ -> assert false - in - let res = List.map (fun e -> uri, e) res in - let tl, newmeta, cache = aux cache newmeta tl in - res @ tl, newmeta, cache - in - let found, maxm, cache = - aux cache maxmeta candidates - in - let uriset, eqlist = - let mceq = Equality.meta_convertibility_eq in - (List.fold_left - (fun (s, l) (u, e) -> - if List.exists (mceq e) (List.map snd l) then ( - debug_print - (lazy - (Printf.sprintf "NO!! %s already there!" - (Equality.string_of_equality e))); - (UriManager.UriSet.add u s, l) - ) else (UriManager.UriSet.add u s, (u, e)::l)) - (UriManager.UriSet.empty, []) found) - in - uriset, eqlist, maxm, cache -;; - let get_stats () = "" (*<:show>*) ;; diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli index 97c868985..ef1529210 100644 --- a/components/tactics/paramodulation/inference.mli +++ b/components/tactics/paramodulation/inference.mli @@ -42,38 +42,4 @@ val unification: CicUniv.universe_graph -> Subst.substitution * Cic.metasenv * CicUniv.universe_graph -type auto_type = (* the universe must be hardocded *) - int -> (* maxmeta *) - AutoTypes.flags -> - ProofEngineTypes.proof -> - Cic.context -> - AutoTypes.cache -> - ProofEngineTypes.goal list -> - Cic.substitution list * AutoTypes.cache * int - -(** - scans the context to find all Declarations "left = right"; returns a - list of tuples (proof, (type, left, right), newmetas). Uses - PrimitiveTactics.new_metasenv_for_apply to replace bound variables with - fresh metas... -*) -val find_equalities: - int -> - Equality.equality_bag -> - ?auto:auto_type -> - Cic.context -> ProofEngineTypes.proof -> - AutoTypes.cache -> - int list * Equality.equality list * int * AutoTypes.cache - -(** - searches the library for equalities that can be applied to the current goal -*) -val find_library_equalities: - Equality.equality_bag -> - ?auto:auto_type -> - bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> - AutoTypes.cache -> - UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int * - AutoTypes.cache - val get_stats: unit -> string diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 11966ef8d..7ddfd86fc 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1360,13 +1360,13 @@ let find_equalities dbd status smart_flag ?auto cache = let env = (metasenv, context, CicUniv.empty_ugraph) in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm, cache = - Inference.find_equalities 0 bag ?auto context proof cache + Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache in prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>"; List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities; prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; let lib_eq_uris, library_equalities, maxm, cache = - Inference.find_library_equalities bag + Equality_retrieval.find_library_equalities bag ?auto smart_flag dbd context (proof, goalno) (maxm+2) cache in @@ -1394,15 +1394,23 @@ let saturate_more bag active maxmeta status smart_flag ?auto cache = let eq_uri = eq_of_goal type_of_goal in let env = (metasenv, context, CicUniv.empty_ugraph) in let eq_indexes, equalities, maxm, cache = - Inference.find_equalities maxmeta bag ?auto context proof cache + Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache in + prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ + string_of_int maxm); + List.iter + (fun e -> prerr_endline (Equality.string_of_equality ~env e)) + equalities; + prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; let equalities = -(* HExtlib.filter_map (fun e -> forward_simplify bag eq_uri env e active) -*) equalities in + prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>"; + List.iter + (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities; + prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm); bag, equalities, cache, maxm let saturate @@ -1424,7 +1432,7 @@ let saturate let env = (metasenv, context, ugraph) in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in let bag, equalities, cache, maxm = - find_equalities dbd status smart_flag ?auto AutoTypes.cache_empty + find_equalities dbd status smart_flag ?auto AutoCache.cache_empty in let res, time = maxmeta := maxm+2; @@ -1508,6 +1516,10 @@ let given_clause Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in let env = metasenv,context,CicUniv.empty_ugraph in + prerr_endline ">>>>>> ACTIVES >>>>>>>>"; + List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e)) + active_l; + prerr_endline ">>>>>>>>>>>>>>"; let goals = make_goal_set goal in match given_clause bag eq_uri env goals passive active @@ -1530,10 +1542,10 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = let eq_uri = eq_of_goal ty in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm, cache = - Inference.find_equalities 0 bag context proof AutoTypes.cache_empty + Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in let lib_eq_uris, library_equalities, maxm, cache = - Inference.find_library_equalities bag + Equality_retrieval.find_library_equalities bag false dbd context (proof, goal) (maxm+2) cache in if library_equalities = [] then prerr_endline "VUOTA!!!"; @@ -1611,7 +1623,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let names = Utils.names_of_context context in let bag = Equality.mk_equality_bag () in let eq_index, equalities, maxm,cache = - Inference.find_equalities 0 bag context proof AutoTypes.cache_empty + Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in let eq_what = let what = find_in_ctx 1 target context in @@ -1716,12 +1728,12 @@ let retrieve_and_print dbd term metasenv ugraph = let eq_uri = eq_of_goal type_of_goal in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm,cache = - Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in + Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm, cache = - Inference.find_library_equalities bag + Equality_retrieval.find_library_equalities bag false dbd context (proof, goal') (maxm+2) cache in let t2 = Unix.gettimeofday () in @@ -1800,9 +1812,9 @@ let main_demod_equalities dbd term metasenv ugraph = let eq_uri = eq_of_goal goal in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm, cache = - Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in + Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in let lib_eq_uris, library_equalities, maxm,cache = - Inference.find_library_equalities bag + Equality_retrieval.find_library_equalities bag false dbd context (proof, goal') (maxm+2) cache in let library_equalities = List.map snd library_equalities in diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index 3bd04454c..d16c9e28a 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -32,7 +32,7 @@ val saturate : (* FIXME: should be exported a a tactic *) ?depth:int -> ?width:int -> ?timeout:float -> - ?auto:Inference.auto_type -> + ?auto:Equality_retrieval.auto_type -> ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list @@ -46,19 +46,19 @@ val find_equalities: HMysql.dbd -> ProofEngineTypes.status -> bool -> (* smart_flag *) - ?auto:Inference.auto_type -> - AutoTypes.cache -> + ?auto:Equality_retrieval.auto_type -> + AutoCache.cache -> Equality.equality_bag * - Equality.equality list * AutoTypes.cache * int + Equality.equality list * AutoCache.cache * int val saturate_more: Equality.equality_bag -> active_table -> int -> (* maxmeta *) ProofEngineTypes.status -> bool -> (* smart flag *) - ?auto:Inference.auto_type -> - AutoTypes.cache -> - Equality.equality_bag * Equality.equality list * AutoTypes.cache * int + ?auto:Equality_retrieval.auto_type -> + AutoCache.cache -> + Equality.equality_bag * Equality.equality list * AutoCache.cache * int val given_clause: Equality.equality_bag -> diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 9060afdd6..c49303555 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Sep 27 17:37:14 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Sep 28 10:29:58 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic -- 2.39.2