From: denes Date: Mon, 1 Jun 2009 15:32:18 +0000 (+0000) Subject: First functions on substitutions for unification X-Git-Tag: make_still_working~3933 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46bfce7d0f09058ca063766192a1d4251ce7df63;p=helm.git First functions on substitutions for unification --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 75490d3ba..4ad2daaa3 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,8 +1,8 @@ -terms.cmi: pp.cmi: terms.cmi founif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi +subst.cmi: terms.cmi terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: pp.cmi @@ -13,3 +13,5 @@ index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi +subst.cmo: terms.cmi subst.cmi +subst.cmx: terms.cmx subst.cmi diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile index 8612f4bfc..ccf1b57a4 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 founif.mli index.mli orderings.mli + terms.mli pp.mli founif.mli index.mli orderings.mli subst.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_paramodulation/subst.ml b/helm/software/components/ng_paramodulation/subst.ml new file mode 100644 index 000000000..662a9f0d7 --- /dev/null +++ b/helm/software/components/ng_paramodulation/subst.ml @@ -0,0 +1,34 @@ +(* + ||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_______________________________________________________________ *) + +let empty_subst = [];; + +let buildsubst 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 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 +;; diff --git a/helm/software/components/ng_paramodulation/subst.mli b/helm/software/components/ng_paramodulation/subst.mli new file mode 100644 index 000000000..73f5115dd --- /dev/null +++ b/helm/software/components/ng_paramodulation/subst.mli @@ -0,0 +1,18 @@ +(* + ||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 $ *) + +val empty_subst : 'a Terms.substitution +val buildsubst : + int -> 'a Terms.foterm -> 'a Terms.substitution -> 'a Terms.substitution +val lookup_subst : 'a Terms.foterm -> 'a Terms.substitution -> 'a Terms.foterm +val filter : 'a Terms.substitution -> Terms.varlist -> Terms.varlist