From: Enrico Tassi Date: Fri, 29 Sep 2006 14:41:27 +0000 (+0000) Subject: renamed inference in founif that is more appropriate X-Git-Tag: 0.4.95@7852~969 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b1a0b78ea59c7f0fe2bf7ffda4a5cda260add35;p=helm.git renamed inference in founif that is more appropriate --- diff --git a/components/tactics/.depend b/components/tactics/.depend index 5f8f9060e..2a44e78cc 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -11,7 +11,7 @@ paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/equality_retrieval.cmi: proofEngineTypes.cmi \ paramodulation/equality.cmi autoTypes.cmi autoCache.cmi -paramodulation/inference.cmi: paramodulation/subst.cmi +paramodulation/founif.cmi: paramodulation/subst.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/indexing.cmi: paramodulation/utils.cmi \ @@ -88,31 +88,31 @@ 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 paramodulation/inference.cmi -paramodulation/inference.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx paramodulation/inference.cmi +paramodulation/founif.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \ + paramodulation/founif.cmi +paramodulation/founif.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \ + paramodulation/founif.cmi paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/equality_indexing.cmi paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ paramodulation/equality.cmx paramodulation/equality_indexing.cmi paramodulation/indexing.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi paramodulation/inference.cmi \ + paramodulation/subst.cmi paramodulation/founif.cmi \ paramodulation/equality_indexing.cmi paramodulation/equality.cmi \ paramodulation/indexing.cmi paramodulation/indexing.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx paramodulation/inference.cmx \ + paramodulation/subst.cmx paramodulation/founif.cmx \ paramodulation/equality_indexing.cmx paramodulation/equality.cmx \ paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi \ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \ - paramodulation/indexing.cmi paramodulation/equality_retrieval.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/indexing.cmi \ + paramodulation/founif.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_retrieval.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/indexing.cmx \ + paramodulation/founif.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 \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 08df7d546..dee83c756 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -12,7 +12,7 @@ INTERFACE_FILES = \ paramodulation/subst.mli\ paramodulation/equality.mli\ paramodulation/equality_retrieval.mli\ - paramodulation/inference.mli\ + paramodulation/founif.mli\ paramodulation/equality_indexing.mli\ paramodulation/indexing.mli \ paramodulation/saturation.mli \ diff --git a/components/tactics/paramodulation/founif.ml b/components/tactics/paramodulation/founif.ml new file mode 100644 index 000000000..ac80099b0 --- /dev/null +++ b/components/tactics/paramodulation/founif.ml @@ -0,0 +1,201 @@ +(* 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/. + *) + +(* let _profiler = <:profiler<_profiler>>;; *) + +(* $Id$ *) + +open Utils;; +open Printf;; + +let debug_print s = ();;(*prerr_endline (Lazy.force s);;*) + +let check_disjoint_invariant subst metasenv msg = + if (List.exists + (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv) + then + begin + prerr_endline ("not disjoint: " ^ msg); + assert false + end +;; + +let rec check_irl start = function + | [] -> true + | None::tl -> check_irl (start+1) tl + | (Some (Cic.Rel x))::tl -> + if x = start then check_irl (start+1) tl else false + | _ -> false +;; + +let rec is_simple_term = function + | Cic.Appl ((Cic.Meta _)::_) -> false + | Cic.Appl l -> List.for_all is_simple_term l + | Cic.Meta (i, l) -> let l = [] in check_irl 1 l + | Cic.Rel _ -> true + | Cic.Const _ -> true + | Cic.MutInd (_, _, []) -> true + | Cic.MutConstruct (_, _, _, []) -> true + | _ -> false +;; + +let locked menv i = + List.exists (fun (j,_,_) -> i = j) menv +;; + +let unification_simple locked_menv metasenv context t1 t2 ugraph = + let module C = Cic in + let module M = CicMetaSubst in + let module U = CicUnification in + let lookup = Subst.lookup_subst in + let rec occurs_check subst what where = + match where with + | Cic.Meta(i,_) when i = what -> true + | C.Appl l -> List.exists (occurs_check subst what) l + | C.Meta _ -> + let t = lookup where subst in + if t <> where then occurs_check subst what t else false + | _ -> false + in + let rec unif subst menv s t = + let s = match s with C.Meta _ -> lookup s subst | _ -> s + and t = match t with C.Meta _ -> lookup t subst | _ -> t + + in + match s, t with + | s, t when s = t -> subst, menv + (* sometimes the same meta has different local contexts; this + could create "cyclic" substitutions *) + | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv + | C.Meta (i, _), C.Meta (j, _) + when (locked locked_menv i) &&(locked locked_menv j) -> + raise + (U.UnificationFailure (lazy "Inference.unification.unif")) + | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) -> + unif subst menv t s + | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> + unif subst menv t s + | C.Meta (i,_), t when occurs_check subst i t -> + raise + (U.UnificationFailure (lazy "Inference.unification.unif")) + | C.Meta (i, l), t when (locked locked_menv i) -> + raise + (U.UnificationFailure (lazy "Inference.unification.unif")) + | C.Meta (i, l), t -> ( + try + let _, _, ty = CicUtil.lookup_meta i menv in + assert (not (Subst.is_in_subst i subst)); + let subst = Subst.buildsubst i context t ty subst in + let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *) + subst, menv + with CicUtil.Meta_not_found m -> + let names = names_of_context context in + (*debug_print + (lazy*) prerr_endline + (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m + (CicPp.pp t1 names) (CicPp.pp t2 names) + (print_metasenv menv) (print_metasenv metasenv)); + assert false + ) + | _, C.Meta _ -> unif subst menv t s + | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> + raise (U.UnificationFailure (lazy "Inference.unification.unif")) + | C.Appl (hds::tls), C.Appl (hdt::tlt) -> ( + try + List.fold_left2 + (fun (subst', menv) s t -> unif subst' menv s t) + (subst, menv) tls tlt + with Invalid_argument _ -> + raise (U.UnificationFailure (lazy "Inference.unification.unif")) + ) + | _, _ -> + raise (U.UnificationFailure (lazy "Inference.unification.unif")) + in + let subst, menv = unif Subst.empty_subst metasenv t1 t2 in + let menv = Subst.filter subst menv in + subst, menv, ugraph +;; + +let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]" +let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]" +let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]" +let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]" + +let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = + let metasenv = + HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) + (* metasenv1 @ metasenv2 *) + in + let subst, menv, ug = + if not (is_simple_term t1) || not (is_simple_term t2) then ( + debug_print + (lazy + (Printf.sprintf "NOT SIMPLE TERMS: %s %s" + (CicPp.ppterm t1) (CicPp.ppterm t2))); + raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif")) + ) else + if b then + (* full unification *) + unification_simple [] metasenv context t1 t2 ugraph + else + (* matching: metasenv1 is locked *) + unification_simple metasenv1 metasenv context t1 t2 ugraph + in + if Utils.debug_res then + ignore(check_disjoint_invariant subst menv "unif"); + (* let flatten subst = + List.map + (fun (i, (context, term, ty)) -> + let context = apply_subst_context subst context in + let term = apply_subst subst term in + let ty = apply_subst subst ty in + (i, (context, term, ty))) subst + in + let flatten subst = profiler.HExtlib.profile flatten subst in + let subst = flatten subst in *) + subst, menv, ug +;; + +exception MatchingFailure;; + +(** matching takes in input the _disjoint_ metasenv of t1 and t2; +it perform unification in the union metasenv, then check that +the first metasenv has not changed *) +let matching metasenv1 metasenv2 context t1 t2 ugraph = + try + unification_aux false metasenv1 metasenv2 context t1 t2 ugraph + with + CicUnification.UnificationFailure _ -> + raise MatchingFailure +;; + +let unification m1 m2 c t1 t2 ug = + try + unification_aux true m1 m2 c t1 t2 ug + with exn -> + raise exn +;; + +let get_stats () = "" (*<:show>*) ;; diff --git a/components/tactics/paramodulation/founif.mli b/components/tactics/paramodulation/founif.mli new file mode 100644 index 000000000..ef1529210 --- /dev/null +++ b/components/tactics/paramodulation/founif.mli @@ -0,0 +1,45 @@ +(* 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/. + *) + +exception MatchingFailure + +(** matching between two terms. Can raise MatchingFailure *) +val matching: + Cic.metasenv -> Cic.metasenv -> Cic.context -> + Cic.term -> Cic.term -> + CicUniv.universe_graph -> + Subst.substitution * Cic.metasenv * CicUniv.universe_graph + +(** + special unification that checks if the two terms are "simple", and in + such case should be significantly faster than CicUnification.fo_unif +*) +val unification: + Cic.metasenv -> Cic.metasenv -> Cic.context -> + Cic.term -> Cic.term -> + CicUniv.universe_graph -> + Subst.substitution * Cic.metasenv * CicUniv.universe_graph + +val get_stats: unit -> string diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 34c601b35..546fff631 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -151,11 +151,11 @@ let check_target bag context target msg = (* try ignore(CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) + metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph) with e -> prerr_endline msg; - prerr_endline (Inference.string_of_proof proof); - prerr_endline (CicPp.ppterm (Inference.build_proof_term proof)); + prerr_endline (Founif.string_of_proof proof); + prerr_endline (CicPp.ppterm (Founif.build_proof_term proof)); prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left)); prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); raise e @@ -246,7 +246,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = ) else let do_match c = let subst', metasenv', ugraph' = - Inference.matching + Founif.matching metasenv metas context term (S.lift lift_amount c) ugraph in Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) @@ -259,7 +259,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = let res = try do_match c - with Inference.MatchingFailure -> + with Founif.MatchingFailure -> find_matches bag metasenv context ugraph lift_amount term termty tl in if Utils.debug_res then ignore (check_res res "find1"); @@ -267,7 +267,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = else let res = try do_match c - with Inference.MatchingFailure -> None + with Founif.MatchingFailure -> None in if Utils.debug_res then ignore (check_res res "find2"); match res with @@ -292,9 +292,9 @@ let find_matches metasenv context ugraph lift_amount term termty = (* as above, but finds all the matching equalities, and the matching condition - can be either Inference.matching or Inference.unification + can be either Founif.matching or Inference.unification *) -let rec find_all_matches ?(unif_fun=Inference.unification) +let rec find_all_matches ?(unif_fun=Founif.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in @@ -323,7 +323,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -343,7 +343,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -356,7 +356,7 @@ let find_all_matches find_all_matches ?unif_fun metasenv context ugraph lift_amount term termty l (*prerr_endline "CANDIDATES:"; - List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l; + List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l; prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int (List.length rc));*) ;; @@ -374,9 +374,9 @@ let subsumption_aux use_unification env table target = let metasenv = tmetas in let predicate, unif_fun = if use_unification then - Unification, Inference.unification + Unification, Founif.unification else - Matching, Inference.matching + Matching, Founif.matching in let leftr = match left with @@ -401,7 +401,7 @@ let subsumption_aux use_unification env table target = | None -> ok what leftorright tl | Some s -> Some (s, equation, leftorright <> pos )) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ -> ok what leftorright tl in match ok right Utils.Left leftr with @@ -824,7 +824,7 @@ let superposition_right bag if ordering = U.Gt then newgoal, apply_subst s right else apply_subst s left, newgoal in let neworder = !Utils.compare_terms left right in - let newmenv = (* Inference.filter s *) m in + let newmenv = (* Founif.filter s *) m in let stat = (eq_ty, left, right, neworder) in let eq' = let w = Utils.compute_equality_weight stat in @@ -953,7 +953,7 @@ let build_newgoal bag context goal posu rule expansion = let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in bo, (newgoalproofstep::goalproof) in - let newmetasenv = (* Inference.filter subst *) menv in + let newmetasenv = (* Founif.filter subst *) menv in (newgoalproof, newmetasenv, newterm) ;; diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml deleted file mode 100644 index ac80099b0..000000000 --- a/components/tactics/paramodulation/inference.ml +++ /dev/null @@ -1,201 +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/. - *) - -(* let _profiler = <:profiler<_profiler>>;; *) - -(* $Id$ *) - -open Utils;; -open Printf;; - -let debug_print s = ();;(*prerr_endline (Lazy.force s);;*) - -let check_disjoint_invariant subst metasenv msg = - if (List.exists - (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv) - then - begin - prerr_endline ("not disjoint: " ^ msg); - assert false - end -;; - -let rec check_irl start = function - | [] -> true - | None::tl -> check_irl (start+1) tl - | (Some (Cic.Rel x))::tl -> - if x = start then check_irl (start+1) tl else false - | _ -> false -;; - -let rec is_simple_term = function - | Cic.Appl ((Cic.Meta _)::_) -> false - | Cic.Appl l -> List.for_all is_simple_term l - | Cic.Meta (i, l) -> let l = [] in check_irl 1 l - | Cic.Rel _ -> true - | Cic.Const _ -> true - | Cic.MutInd (_, _, []) -> true - | Cic.MutConstruct (_, _, _, []) -> true - | _ -> false -;; - -let locked menv i = - List.exists (fun (j,_,_) -> i = j) menv -;; - -let unification_simple locked_menv metasenv context t1 t2 ugraph = - let module C = Cic in - let module M = CicMetaSubst in - let module U = CicUnification in - let lookup = Subst.lookup_subst in - let rec occurs_check subst what where = - match where with - | Cic.Meta(i,_) when i = what -> true - | C.Appl l -> List.exists (occurs_check subst what) l - | C.Meta _ -> - let t = lookup where subst in - if t <> where then occurs_check subst what t else false - | _ -> false - in - let rec unif subst menv s t = - let s = match s with C.Meta _ -> lookup s subst | _ -> s - and t = match t with C.Meta _ -> lookup t subst | _ -> t - - in - match s, t with - | s, t when s = t -> subst, menv - (* sometimes the same meta has different local contexts; this - could create "cyclic" substitutions *) - | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv - | C.Meta (i, _), C.Meta (j, _) - when (locked locked_menv i) &&(locked locked_menv j) -> - raise - (U.UnificationFailure (lazy "Inference.unification.unif")) - | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) -> - unif subst menv t s - | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> - unif subst menv t s - | C.Meta (i,_), t when occurs_check subst i t -> - raise - (U.UnificationFailure (lazy "Inference.unification.unif")) - | C.Meta (i, l), t when (locked locked_menv i) -> - raise - (U.UnificationFailure (lazy "Inference.unification.unif")) - | C.Meta (i, l), t -> ( - try - let _, _, ty = CicUtil.lookup_meta i menv in - assert (not (Subst.is_in_subst i subst)); - let subst = Subst.buildsubst i context t ty subst in - let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *) - subst, menv - with CicUtil.Meta_not_found m -> - let names = names_of_context context in - (*debug_print - (lazy*) prerr_endline - (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m - (CicPp.pp t1 names) (CicPp.pp t2 names) - (print_metasenv menv) (print_metasenv metasenv)); - assert false - ) - | _, C.Meta _ -> unif subst menv t s - | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> - raise (U.UnificationFailure (lazy "Inference.unification.unif")) - | C.Appl (hds::tls), C.Appl (hdt::tlt) -> ( - try - List.fold_left2 - (fun (subst', menv) s t -> unif subst' menv s t) - (subst, menv) tls tlt - with Invalid_argument _ -> - raise (U.UnificationFailure (lazy "Inference.unification.unif")) - ) - | _, _ -> - raise (U.UnificationFailure (lazy "Inference.unification.unif")) - in - let subst, menv = unif Subst.empty_subst metasenv t1 t2 in - let menv = Subst.filter subst menv in - subst, menv, ugraph -;; - -let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]" -let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]" -let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]" -let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]" - -let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = - let metasenv = - HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) - (* metasenv1 @ metasenv2 *) - in - let subst, menv, ug = - if not (is_simple_term t1) || not (is_simple_term t2) then ( - debug_print - (lazy - (Printf.sprintf "NOT SIMPLE TERMS: %s %s" - (CicPp.ppterm t1) (CicPp.ppterm t2))); - raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif")) - ) else - if b then - (* full unification *) - unification_simple [] metasenv context t1 t2 ugraph - else - (* matching: metasenv1 is locked *) - unification_simple metasenv1 metasenv context t1 t2 ugraph - in - if Utils.debug_res then - ignore(check_disjoint_invariant subst menv "unif"); - (* let flatten subst = - List.map - (fun (i, (context, term, ty)) -> - let context = apply_subst_context subst context in - let term = apply_subst subst term in - let ty = apply_subst subst ty in - (i, (context, term, ty))) subst - in - let flatten subst = profiler.HExtlib.profile flatten subst in - let subst = flatten subst in *) - subst, menv, ug -;; - -exception MatchingFailure;; - -(** matching takes in input the _disjoint_ metasenv of t1 and t2; -it perform unification in the union metasenv, then check that -the first metasenv has not changed *) -let matching metasenv1 metasenv2 context t1 t2 ugraph = - try - unification_aux false metasenv1 metasenv2 context t1 t2 ugraph - with - CicUnification.UnificationFailure _ -> - raise MatchingFailure -;; - -let unification m1 m2 c t1 t2 ug = - try - unification_aux true m1 m2 c t1 t2 ug - with exn -> - raise exn -;; - -let get_stats () = "" (*<:show>*) ;; diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli deleted file mode 100644 index ef1529210..000000000 --- a/components/tactics/paramodulation/inference.mli +++ /dev/null @@ -1,45 +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/. - *) - -exception MatchingFailure - -(** matching between two terms. Can raise MatchingFailure *) -val matching: - Cic.metasenv -> Cic.metasenv -> Cic.context -> - Cic.term -> Cic.term -> - CicUniv.universe_graph -> - Subst.substitution * Cic.metasenv * CicUniv.universe_graph - -(** - special unification that checks if the two terms are "simple", and in - such case should be significantly faster than CicUnification.fo_unif -*) -val unification: - Cic.metasenv -> Cic.metasenv -> Cic.context -> - Cic.term -> Cic.term -> - CicUniv.universe_graph -> - Subst.substitution * Cic.metasenv * CicUniv.universe_graph - -val get_stats: unit -> string diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index da4ef7826..b52e074fd 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -850,7 +850,7 @@ let check_if_goal_is_identity env = function (let _,context,_ = env in try let s,m,_ = - Inference.unification m m context left right CicUniv.empty_ugraph + Founif.unification m m context left right CicUniv.empty_ugraph in let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in let m = Subst.apply_subst_metasenv s m in @@ -1712,7 +1712,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let get_stats () = "" (* - <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ + <:show> ^ Indexing.get_stats () ^ Founif.get_stats () ^ Equality.get_stats () ;; *)