...

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

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index 5cb84e1c938d1ff20b359bc738f7f0b713cfe87f..aab2401684238b0d3e59ed3bc9c141c846a776d0 100644 (file)
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -36,6 +36,17 @@
       varlist
   ;;
 
+  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 -> 
@@ -46,6 +57,10 @@
        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 *)