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