First functions on substitutions for unification

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index 75490d3ba6c757d3a1fa321523163bb7cb3fb868..4ad2daaa3144fad7b98cc680898ab3515e2974d3 100644 (file)
--- 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 8612f4bfc93eadbfb0c87adc1ff2b4d8d2c68dbd..ccf1b57a4c4f51af56149fd40cfe1fa5a83f70e7 100644 (file)
--- 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 (file)
index 0000000..662a9f0
--- /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 (file)
index 0000000..73f5115
--- /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