X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoSubst.ml;h=aab2401684238b0d3e59ed3bc9c141c846a776d0;hb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;hp=92d6aba25a7ef99e6b24e0d39e187c84737761e0;hpb=6b0a195b180e3526af7b55771b2df7b10acd7c30;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index 92d6aba25..aab240168 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -9,22 +9,22 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-module Subst (B : Terms.Blob) = struct
+(* module Subst (B : Terms.Blob) = struct *)
   
   let id_subst = [];;
   
   let build_subst n t tail = (n,t) :: tail ;;
   
-  let rec lookup_subst var subst =
+  let rec lookup var subst =
     match var with
       | Terms.Var i ->
           (try
-            lookup_subst (List.assoc i subst) subst
+            lookup (List.assoc i subst) subst
           with
               Not_found -> var)
       | _ -> var
   ;;
-  let lookup_subst i subst = lookup_subst (Terms.Var i) subst;;
+  let lookup i subst = lookup (Terms.Var i) subst;;
   
   let is_in_subst i subst = List.mem_assoc i subst;;
   
@@ -36,7 +36,31 @@ module Subst (B : Terms.Blob) = struct
       varlist
   ;;
 
-  let apply_subst = assert false;;
-  let concat = assert false
+  let rec reloc_subst subst = function
+    | (Terms.Leaf _) as t -> t
+    | Terms.Var i -> 
+        (try
+           List.assoc i subst
+         with
+             Not_found -> assert false)
+    | (Terms.Node l) ->
+	Terms.Node (List.map (fun t -> reloc_subst subst t) l)
+;;
+
+  let rec apply_subst subst = function
+    | (Terms.Leaf _) as t -> t
+    | Terms.Var i -> 
+        (match lookup i subst with
+        | Terms.Node _ as t -> apply_subst subst t
+        | t -> t)
+    | (Terms.Node l) ->
+	Terms.Node (List.map (fun t -> apply_subst subst t) l)
+;;
+
+  let flat subst =
+    List.map (fun (x,t) -> (x, apply_subst subst t)) subst
+;;
+
+  let concat x y = x @ y;;
   
-end
+(* end *)