X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=4d56d30e963d9f0dcf5b8a55aac923fe21a4a6c6;hb=2e8243f12626854bdc1e06f2e3d9160ff7901bd3;hp=999666bca4652602566c3043c2cf4d967c8b4933;hpb=975da98810a335a759a3b5e5f96b1beb96c932d2;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 999666bca..4d56d30e9 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -292,7 +292,31 @@ let rec restore_subst (* context *) subst = subst ;; - + +exception MatchingFailure;; + +let matching metasenv context t1 t2 ugraph = + try + let subst, metasenv, ugraph = + CicUnification.fo_unif metasenv context t1 t2 ugraph + in + let t' = CicMetaSubst.apply_subst subst t1 in + if not (meta_convertibility t1 t') then + raise MatchingFailure + else + let metas = metas_of_term t1 in + let fix_subst = function + | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas -> + (j, (c, Cic.Meta (i, lc), ty)) + | s -> s + in + let subst = List.map fix_subst subst in + subst, metasenv, ugraph + with e -> + raise MatchingFailure +;; + + let beta_expand ?(metas_ok=true) ?(match_only=false) what type_of_what where context metasenv ugraph = let module S = CicSubstitution in @@ -559,47 +583,33 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) let subst', metasenv', ugraph' = (* Printf.printf "provo a unificare %s e %s\n" *) (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *) - CicUnification.fo_unif metasenv context - (S.lift lift_amount what) term ugraph + if match_only then + matching metasenv context term (S.lift lift_amount what)ugraph + else + CicUnification.fo_unif metasenv context + (S.lift lift_amount what) term ugraph in (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *) (* (CicPp.ppterm (S.lift lift_amount what)); *) (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *) (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *) (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *) - if match_only then - let t' = CicMetaSubst.apply_subst subst' term in - if not (meta_convertibility term t') then ( -(* if print_info then ( *) -(* let names = names_of_context context in *) -(* Printf.printf *) -(* "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *) -(* (CicPp.pp term names) (CicPp.pp t' names) *) -(* ); *) - res, lifted_term - ) else ( - let metas = metas_of_term term in -(* let ok = ref false in *) - let fix_subst = function - | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> -(* Printf.printf "fix_subst: scambio ?%d e ?%d\n" i j; *) -(* ok := true; *) - (j, (c, C.Meta (i, lc), ty)) - | s -> s - in - let subst' = List.map fix_subst subst' in -(* if !ok then ( *) -(* Printf.printf "aaa:\nterm: %s\nt'%s\n term subst': %s\n" *) -(* (CicPp.ppterm term) *) -(* (CicPp.ppterm t') *) -(* (CicPp.ppterm (CicMetaSubst.apply_subst subst' term)) *) -(* ); *) - ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, - lifted_term) - ) -(* ((C.Rel (1 + lift_amount), restore_subst context subst', *) -(* metasenv', ugraph')::res, lifted_term) *) - else +(* if match_only then *) +(* let t' = CicMetaSubst.apply_subst subst' term in *) +(* if not (meta_convertibility term t') then ( *) +(* res, lifted_term *) +(* ) else ( *) +(* let metas = metas_of_term term in *) +(* let fix_subst = function *) +(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *) +(* (j, (c, C.Meta (i, lc), ty)) *) +(* | s -> s *) +(* in *) +(* let subst' = List.map fix_subst subst' in *) +(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *) +(* lifted_term) *) +(* ) *) +(* else *) ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, lifted_term) with e -> @@ -1144,3 +1154,53 @@ let demodulation newmeta env target source = *) +let subsumption env target source = + let _, (ty, tl, tr), tmetas, _ = target + and _, (ty', sl, sr), smetas, _ = source in + if ty <> ty' then + false + else + let metasenv, context, ugraph = env in + let metasenv = metasenv @ tmetas @ smetas in + let names = names_of_context context in + let samesubst subst subst' = +(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *) +(* (print_subst subst) (print_subst subst'); *) +(* print_newline (); *) + let tbl = Hashtbl.create (List.length subst) in + List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst; + List.for_all + (fun (m, (c, t1, t2)) -> + try + let c', t1', t2' = Hashtbl.find tbl m in + if (c = c') && (t1 = t1') && (t2 = t2') then true + else false + with Not_found -> + true) + subst' + in + let subsaux left right left' right' = + try + let subst, menv, ug = matching metasenv context left left' ugraph + and subst', menv', ug' = matching metasenv context right right' ugraph + in +(* Printf.printf "left = right: %s = %s\n" *) +(* (CicPp.pp left names) (CicPp.pp right names); *) +(* Printf.printf "left' = right': %s = %s\n" *) +(* (CicPp.pp left' names) (CicPp.pp right' names); *) + samesubst subst subst' + with e -> +(* print_endline (Printexc.to_string e); *) + false + in + let res = + if subsaux tl tr sl sr then true + else subsaux tl tr sr sl + in + if res then ( + Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n" + (string_of_equality ~env target) (string_of_equality ~env source); + print_newline (); + ); + res +;;