From: Enrico Tassi Date: Sat, 6 Jun 2009 08:59:51 +0000 (+0000) Subject: some renaming to make ocamlopt happy X-Git-Tag: make_still_working~3911 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=25cf2297c8d14c14cfb2ff7695c9b6331825f4c9;p=helm.git some renaming to make ocamlopt happy --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 0033d44db..8181c02de 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,18 +1,20 @@ +terms.cmi: pp.cmi: terms.cmi -fosubst.cmi: terms.cmi -founif.cmi: terms.cmi +foSubst.cmi: terms.cmi +foUnif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi +paramod.cmi: terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi -fosubst.cmo: terms.cmi fosubst.cmi -fosubst.cmx: terms.cmx fosubst.cmi -founif.cmo: terms.cmi fosubst.cmi founif.cmi -founif.cmx: terms.cmx fosubst.cmx founif.cmi +foSubst.cmo: terms.cmi foSubst.cmi +foSubst.cmx: terms.cmx foSubst.cmi +foUnif.cmo: terms.cmi foUnif.cmi +foUnif.cmx: terms.cmx foUnif.cmi index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi @@ -21,5 +23,5 @@ nCicBlob.cmo: terms.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi -paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi founif.cmi paramod.cmi -paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi +paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi +paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx paramod.cmi diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 0033d44db..8181c02de 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -1,18 +1,20 @@ +terms.cmi: pp.cmi: terms.cmi -fosubst.cmi: terms.cmi -founif.cmi: terms.cmi +foSubst.cmi: terms.cmi +foUnif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi +paramod.cmi: terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi -fosubst.cmo: terms.cmi fosubst.cmi -fosubst.cmx: terms.cmx fosubst.cmi -founif.cmo: terms.cmi fosubst.cmi founif.cmi -founif.cmx: terms.cmx fosubst.cmx founif.cmi +foSubst.cmo: terms.cmi foSubst.cmi +foSubst.cmx: terms.cmx foSubst.cmi +foUnif.cmo: terms.cmi foUnif.cmi +foUnif.cmx: terms.cmx foUnif.cmi index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi @@ -21,5 +23,5 @@ nCicBlob.cmo: terms.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi -paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi founif.cmi paramod.cmi -paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi +paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi +paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx paramod.cmi diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile index 152c74a1b..a48753c4a 100644 --- a/helm/software/components/ng_paramodulation/Makefile +++ b/helm/software/components/ng_paramodulation/Makefile @@ -1,7 +1,7 @@ PACKAGE = ng_paramodulation INTERFACE_FILES = \ - terms.mli pp.mli fosubst.mli founif.mli index.mli orderings.mli \ + terms.mli pp.mli foSubst.mli foUnif.mli index.mli orderings.mli \ nCicBlob.mli cicBlob.mli paramod.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml new file mode 100644 index 000000000..1b9f2624c --- /dev/null +++ b/helm/software/components/ng_paramodulation/foSubst.ml @@ -0,0 +1,39 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module Subst (B : Terms.Blob) = struct + + let id_subst = [];; + + let build_subst n t tail = (n,t) :: tail ;; + + let rec lookup_subst var subst = + match var with + | Terms.Var i -> + (try + lookup_subst (List.assoc i subst) subst + with + Not_found -> var) + | _ -> var + ;; + let lookup_subst i subst = lookup_subst (Terms.Var i) subst;; + + let is_in_subst i subst = List.mem_assoc i subst;; + + (* filter out from metasenv the variables in substs *) + let filter subst varlist = + List.filter + (fun m -> + not (is_in_subst m subst)) + varlist + ;; + +end diff --git a/helm/software/components/ng_paramodulation/foSubst.mli b/helm/software/components/ng_paramodulation/foSubst.mli new file mode 100644 index 000000000..dd7e0c2ec --- /dev/null +++ b/helm/software/components/ng_paramodulation/foSubst.mli @@ -0,0 +1,23 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +module Subst (B : Terms.Blob) : + sig + val id_subst : B.t Terms.substitution + val build_subst : + int -> B.t Terms.foterm -> B.t Terms.substitution -> + B.t Terms.substitution + val lookup_subst : + int -> B.t Terms.substitution -> B.t Terms.foterm + val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist + end diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml new file mode 100644 index 000000000..e4ea77c99 --- /dev/null +++ b/helm/software/components/ng_paramodulation/foUnif.ml @@ -0,0 +1,71 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +exception UnificationFailure of string Lazy.t;; + +module Founif (B : Terms.Blob) = struct + module Subst = FoSubst.Subst(B) + module U = Terms.Utils(B) + + let unification vars locked_vars t1 t2 = + let lookup = Subst.lookup_subst in + let rec occurs_check subst what where = + match where with + | Terms.Var i when i = what -> true + | Terms.Var i -> + let t = lookup i subst in + if not (U.eq_foterm t where) then occurs_check subst what t else false + | Terms.Node l -> List.exists (occurs_check subst what) l + | _ -> false + in + let rec unif subst s t = + let s = match s with Terms.Var i -> lookup i subst | _ -> s + and t = match t with Terms.Var i -> lookup i subst | _ -> t + + in + match s, t with + | s, t when U.eq_foterm s t -> subst + | Terms.Var i, Terms.Var j + when (List.mem i locked_vars) &&(List.mem j locked_vars) -> + raise + (UnificationFailure (lazy "Inference.unification.unif")) + | Terms.Var i, Terms.Var j when (List.mem i locked_vars) -> + unif subst t s + | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) -> + unif subst t s + | Terms.Var i, t when occurs_check subst i t -> + raise + (UnificationFailure (lazy "Inference.unification.unif")) + | Terms.Var i, t when (List.mem i locked_vars) -> + raise + (UnificationFailure (lazy "Inference.unification.unif")) + | Terms.Var i, t -> + let subst = Subst.build_subst i t subst in + subst + | _, Terms.Var _ -> unif subst t s + | Terms.Node l1, Terms.Node l2 -> ( + try + List.fold_left2 + (fun subst' s t -> unif subst' s t) + subst l1 l2 + with Invalid_argument _ -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + ) + | _, _ -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + in + let subst = unif Subst.id_subst t1 t2 in + let vars = Subst.filter subst vars in + subst, vars + +end diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli new file mode 100644 index 000000000..fc682c5fc --- /dev/null +++ b/helm/software/components/ng_paramodulation/foUnif.mli @@ -0,0 +1,28 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +exception UnificationFailure of string Lazy.t;; + +module Founif (B : Terms.Blob) : + sig + + val unification: + (* global varlist for both terms t1 and t2 *) + Terms.varlist -> + (* locked variables: if equal to FV(t2) we match t1 with t2*) + Terms.varlist -> + B.t Terms.foterm -> + B.t Terms.foterm -> + B.t Terms.substitution * Terms.varlist + + end diff --git a/helm/software/components/ng_paramodulation/fosubst.ml b/helm/software/components/ng_paramodulation/fosubst.ml deleted file mode 100644 index 1b9f2624c..000000000 --- a/helm/software/components/ng_paramodulation/fosubst.ml +++ /dev/null @@ -1,39 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module Subst (B : Terms.Blob) = struct - - let id_subst = [];; - - let build_subst n t tail = (n,t) :: tail ;; - - let rec lookup_subst var subst = - match var with - | Terms.Var i -> - (try - lookup_subst (List.assoc i subst) subst - with - Not_found -> var) - | _ -> var - ;; - let lookup_subst i subst = lookup_subst (Terms.Var i) subst;; - - let is_in_subst i subst = List.mem_assoc i subst;; - - (* filter out from metasenv the variables in substs *) - let filter subst varlist = - List.filter - (fun m -> - not (is_in_subst m subst)) - varlist - ;; - -end diff --git a/helm/software/components/ng_paramodulation/fosubst.mli b/helm/software/components/ng_paramodulation/fosubst.mli deleted file mode 100644 index dd7e0c2ec..000000000 --- a/helm/software/components/ng_paramodulation/fosubst.mli +++ /dev/null @@ -1,23 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -module Subst (B : Terms.Blob) : - sig - val id_subst : B.t Terms.substitution - val build_subst : - int -> B.t Terms.foterm -> B.t Terms.substitution -> - B.t Terms.substitution - val lookup_subst : - int -> B.t Terms.substitution -> B.t Terms.foterm - val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist - end diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml deleted file mode 100644 index bcea59ad5..000000000 --- a/helm/software/components/ng_paramodulation/founif.ml +++ /dev/null @@ -1,71 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -exception UnificationFailure of string Lazy.t;; - -module Founif (B : Terms.Blob) = struct - module Subst = Fosubst.Subst(B) - module U = Terms.Utils(B) - - let unification vars locked_vars t1 t2 = - let lookup = Subst.lookup_subst in - let rec occurs_check subst what where = - match where with - | Terms.Var i when i = what -> true - | Terms.Var i -> - let t = lookup i subst in - if not (U.eq_foterm t where) then occurs_check subst what t else false - | Terms.Node l -> List.exists (occurs_check subst what) l - | _ -> false - in - let rec unif subst s t = - let s = match s with Terms.Var i -> lookup i subst | _ -> s - and t = match t with Terms.Var i -> lookup i subst | _ -> t - - in - match s, t with - | s, t when U.eq_foterm s t -> subst - | Terms.Var i, Terms.Var j - when (List.mem i locked_vars) &&(List.mem j locked_vars) -> - raise - (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Var i, Terms.Var j when (List.mem i locked_vars) -> - unif subst t s - | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) -> - unif subst t s - | Terms.Var i, t when occurs_check subst i t -> - raise - (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Var i, t when (List.mem i locked_vars) -> - raise - (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Var i, t -> - let subst = Subst.build_subst i t subst in - subst - | _, Terms.Var _ -> unif subst t s - | Terms.Node l1, Terms.Node l2 -> ( - try - List.fold_left2 - (fun subst' s t -> unif subst' s t) - subst l1 l2 - with Invalid_argument _ -> - raise (UnificationFailure (lazy "Inference.unification.unif")) - ) - | _, _ -> - raise (UnificationFailure (lazy "Inference.unification.unif")) - in - let subst = unif Subst.id_subst t1 t2 in - let vars = Subst.filter subst vars in - subst, vars - -end diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli deleted file mode 100644 index fc682c5fc..000000000 --- a/helm/software/components/ng_paramodulation/founif.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -exception UnificationFailure of string Lazy.t;; - -module Founif (B : Terms.Blob) : - sig - - val unification: - (* global varlist for both terms t1 and t2 *) - Terms.varlist -> - (* locked variables: if equal to FV(t2) we match t1 with t2*) - Terms.varlist -> - B.t Terms.foterm -> - B.t Terms.foterm -> - B.t Terms.substitution * Terms.varlist - - end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 3206ff7d2..0414de7e3 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -8,7 +8,7 @@ let nparamod metasenv subst context t = let module B = NCicBlob.NCicBlob(C) in let module Pp = Pp.Pp (B) in let res,vars = B.embed t in - let module FU = Founif.Founif(B) in + let module FU = FoUnif.Founif(B) in let test_unification vars = function | Terms.Node [_; _; lhs; rhs] -> prerr_endline "Unification test :";