From: Enrico Tassi Date: Tue, 24 Oct 2006 08:02:02 +0000 (+0000) Subject: removed equality_retrieval X-Git-Tag: 0.4.95@7852~860 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=465925337322a7295ef65e3ba73b2aa7ccb230bd;p=helm.git removed equality_retrieval --- diff --git a/components/tactics/.depend b/components/tactics/.depend index 2a44e78cc..398c2af39 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -6,26 +6,22 @@ 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/equality_retrieval.cmi: proofEngineTypes.cmi \ - paramodulation/equality.cmi autoTypes.cmi autoCache.cmi paramodulation/founif.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/equality_retrieval.cmi paramodulation/equality.cmi \ - autoCache.cmi +paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ + paramodulation/indexing.cmi paramodulation/equality.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 autoCache.cmi +auto.cmi: proofEngineTypes.cmi autoTactic.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi @@ -34,7 +30,6 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi -tactics.cmi: proofEngineTypes.cmi declarative.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi @@ -68,8 +63,8 @@ metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi autoTypes.cmo: autoTypes.cmi autoTypes.cmx: autoTypes.cmi -autoCache.cmo: metadataQuery.cmi autoCache.cmi -autoCache.cmx: metadataQuery.cmx autoCache.cmi +autoCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi autoCache.cmi +autoCache.cmx: proofEngineTypes.cmx proofEngineReduction.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 @@ -80,14 +75,6 @@ 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/founif.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \ paramodulation/founif.cmi paramodulation/founif.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \ @@ -106,14 +93,14 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \ paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi \ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/indexing.cmi \ - paramodulation/founif.cmi paramodulation/equality_retrieval.cmi \ - paramodulation/equality.cmi autoCache.cmi paramodulation/saturation.cmi + proofEngineHelpers.cmi paramodulation/indexing.cmi \ + paramodulation/founif.cmi paramodulation/equality.cmi \ + paramodulation/saturation.cmi paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/indexing.cmx \ - paramodulation/founif.cmx paramodulation/equality_retrieval.cmx \ - paramodulation/equality.cmx autoCache.cmx paramodulation/saturation.cmi + proofEngineHelpers.cmx paramodulation/indexing.cmx \ + paramodulation/founif.cmx paramodulation/equality.cmx \ + paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ variousTactics.cmi @@ -142,18 +129,22 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmi -auto.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \ - autoTypes.cmi autoCache.cmi auto.cmi -auto.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \ - autoTypes.cmx autoCache.cmx auto.cmi -autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \ - proofEngineHelpers.cmi paramodulation/equality.cmi autoTypes.cmi \ - autoCache.cmi auto.cmi autoTactic.cmi -autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \ - proofEngineHelpers.cmx paramodulation/equality.cmx autoTypes.cmx \ - autoCache.cmx auto.cmx autoTactic.cmi +auto.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \ + paramodulation/saturation.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \ + equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \ + autoCache.cmi auto.cmi +auto.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \ + paramodulation/saturation.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \ + equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \ + autoCache.cmx auto.cmi +autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi metadataQuery.cmi paramodulation/equality.cmi \ + autoTypes.cmi auto.cmi autoTactic.cmi +autoTactic.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx metadataQuery.cmx paramodulation/equality.cmx \ + autoTypes.cmx auto.cmx autoTactic.cmi discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \ @@ -200,18 +191,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi -tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi \ - paramodulation/saturation.cmi ring.cmi reductionTactics.cmi \ - proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \ - inversion.cmi introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ - equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ - autoTactic.cmi auto.cmi tactics.cmi -tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx \ - paramodulation/saturation.cmx ring.cmx reductionTactics.cmx \ - proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \ - inversion.cmx introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ - equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ - autoTactic.cmx auto.cmx tactics.cmi +tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \ + reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ + negationTactics.cmi inversion.cmi introductionTactics.cmi \ + fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \ + eliminationTactics.cmi discriminationTactics.cmi autoTactic.cmi auto.cmi \ + tactics.cmi +tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \ + reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \ + negationTactics.cmx inversion.cmx introductionTactics.cmx \ + fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \ + eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \ + tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index dee83c756..74117ed87 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -11,7 +11,6 @@ INTERFACE_FILES = \ paramodulation/utils.mli \ paramodulation/subst.mli\ paramodulation/equality.mli\ - paramodulation/equality_retrieval.mli\ paramodulation/founif.mli\ paramodulation/equality_indexing.mli\ paramodulation/indexing.mli \ diff --git a/components/tactics/paramodulation/equality_retrieval.ml b/components/tactics/paramodulation/equality_retrieval.ml deleted file mode 100644 index 962304d41..000000000 --- a/components/tactics/paramodulation/equality_retrieval.ml +++ /dev/null @@ -1,371 +0,0 @@ -(* 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;; - -(*****************************************************************) -exception AutoFailure of AutoCache.cache * int - -let default_auto maxm _ _ _ c _ = [],c,maxm ;; - -let close_hypothesis_of_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 (AutoFailure (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 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 auto = - match auto with - | None -> default_auto - | Some auto -> auto 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 - | (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 = - close_hypothesis_of_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 AutoFailure (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 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 auto = - match auto with - | None -> default_auto - | Some auto -> auto 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 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 = - close_hypothesis_of_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 AutoFailure (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 deleted file mode 100644 index 7a24e3a55..000000000 --- a/components/tactics/paramodulation/equality_retrieval.mli +++ /dev/null @@ -1,61 +0,0 @@ - -(* 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_type option -> - 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_type option-> - 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/tactics.mli b/components/tactics/tactics.mli index 7a7d92fdc..16c0d1cd3 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,8 +1,9 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Sep 28 10:29:58 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Oct 23 23:15:05 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : - dbd:HMysql.dbd -> term:Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> + term:Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic