functorial abstraction over term blobs

[helm.git] / helm / software / components / ng_paramodulation / subst.ml

diff --git a/helm/software/components/ng_paramodulation/subst.ml b/helm/software/components/ng_paramodulation/subst.ml
index 662a9f0d71c8e4d067c8e77c7dbdce7a29e913d6..b8cadf48cda2955969009f8fe0bfe8735db12212 100644 (file)
--- a/helm/software/components/ng_paramodulation/subst.ml
+++ b/helm/software/components/ng_paramodulation/subst.ml
@@ -9,26 +9,30 @@
      \ /   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
-;;
+module Subst (B : Terms.Blob) = struct
+  
+  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
+  ;;
+  
+end