X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Ffosubst.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Ffosubst.ml;h=1b9f2624c77760b88f6e59184ecafca0ff12da60;hb=b97a7976503b2d2e5cbc9199f848135a324775a8;hp=0000000000000000000000000000000000000000;hpb=3fb8cc2606e15f256f93c653b5136f609b385208;p=helm.git

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