X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Ffounif.ml;fp=components%2Ftactics%2Fparamodulation%2Ffounif.ml;h=2a9de5ffa8c2d74440dbd2551debdf09ba499ce1;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/tactics/paramodulation/founif.ml b/components/tactics/paramodulation/founif.ml new file mode 100644 index 000000000..2a9de5ffa --- /dev/null +++ b/components/tactics/paramodulation/founif.ml @@ -0,0 +1,199 @@ +(* 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 + let subst = Subst.buildsubst i context t ty subst 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>*) ;;