functorial abstraction over term blobs

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

diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml
index 451524507b2f85fd77ef30c088c5f1e8a3b454c1..bc18aaf00f3248dc715df19ff72d2b680b791e81 100644 (file)
--- a/helm/software/components/ng_paramodulation/founif.ml
+++ b/helm/software/components/ng_paramodulation/founif.ml
@@ -13,55 +13,60 @@
 
 exception UnificationFailure of string Lazy.t;;
 
-let unification vars locked_vars t1 t2 =
-  let lookup = Subst.lookup_subst in
-  let rec occurs_check subst what where =
-    match where with
-    | Terms.Var i when i = what -> true
-    | Terms.Var _ ->
-        let t = lookup where subst in
-        if t <> where then occurs_check subst what t else false
-    | Terms.Node l -> List.exists (occurs_check subst what) l
-    | _ -> false
-  in
-  let rec unif subst vars s t =
-    let s = match s with Terms.Var _ -> lookup s subst | _ -> s
-    and t = match t with Terms.Var _ -> lookup t subst | _ -> t
-    
+module Founif (B : Terms.Blob) = struct
+  module Subst = Subst.Subst(B)
+
+  let unification vars locked_vars t1 t2 =
+    let lookup = Subst.lookup_subst in
+    let rec occurs_check subst what where =
+      match where with
+      | Terms.Var i when i = what -> true
+      | Terms.Var _ ->
+          let t = lookup where subst in
+          if t <> where then occurs_check subst what t else false
+      | Terms.Node l -> List.exists (occurs_check subst what) l
+      | _ -> false
     in
-    match s, t with
-    | s, t when s = t -> subst, vars
-    | Terms.Var i, Terms.Var j
-        when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
-        raise
-          (UnificationFailure (lazy "Inference.unification.unif"))
-    | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
-        unif subst vars t s
-    | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
-        unif subst vars t s
-    | Terms.Var i, t when occurs_check subst i t ->
-        raise
-          (UnificationFailure (lazy "Inference.unification.unif"))
-    | Terms.Var i, t when (List.mem i locked_vars) -> 
-        raise
-          (UnificationFailure (lazy "Inference.unification.unif"))
-    | Terms.Var i, t ->
-        let subst = Subst.buildsubst i t subst in
-        subst, vars
-    | _, Terms.Var _ -> unif subst vars t s
-    | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
-        raise (UnificationFailure (lazy "Inference.unification.unif"))
-    | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
-        try
-          List.fold_left2
-            (fun (subst', vars) s t -> unif subst' vars s t)
-            (subst, vars) tls tlt
-        with Invalid_argument _ ->
+    let rec unif subst vars s t =
+      let s = match s with Terms.Var _ -> lookup s subst | _ -> s
+      and t = match t with Terms.Var _ -> lookup t subst | _ -> t
+      
+      in
+      match s, t with
+      | s, t when s = t -> subst, vars
+      | Terms.Var i, Terms.Var j
+          when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
+          raise
+            (UnificationFailure (lazy "Inference.unification.unif"))
+      | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
+          unif subst vars t s
+      | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
+          unif subst vars t s
+      | Terms.Var i, t when occurs_check subst i t ->
+          raise
+            (UnificationFailure (lazy "Inference.unification.unif"))
+      | Terms.Var i, t when (List.mem i locked_vars) -> 
+          raise
+            (UnificationFailure (lazy "Inference.unification.unif"))
+      | Terms.Var i, t ->
+          let subst = Subst.buildsubst i t subst in
+          subst, vars
+      | _, Terms.Var _ -> unif subst vars t s
+      | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
+          raise (UnificationFailure (lazy "Inference.unification.unif"))
+      | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
+          try
+            List.fold_left2
+              (fun (subst', vars) s t -> unif subst' vars s t)
+              (subst, vars) tls tlt
+          with Invalid_argument _ ->
+            raise (UnificationFailure (lazy "Inference.unification.unif"))
+        )
+      | _, _ ->
           raise (UnificationFailure (lazy "Inference.unification.unif"))
-      )
-    | _, _ ->
-        raise (UnificationFailure (lazy "Inference.unification.unif"))
-  in
-  let subst, vars = unif Subst.empty_subst vars t1 t2 in
-  let vars = Subst.filter subst vars in
-  subst, vars
+    in
+    let subst, vars = unif Subst.empty_subst vars t1 t2 in
+    let vars = Subst.filter subst vars in
+    subst, vars
+  
+end