From 1f80b6362bf8a9311c2eb1f7d270f363956b5969 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 4 Jun 2009 10:19:04 +0000
Subject: [PATCH] =?utf8?q?minor=20changes=20here=20and=20there.=20We=20ext?=
 =?utf8?q?end=20fo-unification=20with=20(X=20...)=20=3D=3F=3D=20(f=20...)?=
 =?utf8?q?=20-->=20X=20:=3D=20f?=

---
 .../components/ng_paramodulation/founif.ml    | 32 +++++++++----------
 .../components/ng_paramodulation/subst.ml     |  5 +--
 .../components/ng_paramodulation/subst.mli    |  6 ++--
 3 files changed, 21 insertions(+), 22 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml
index 5a3f67ae9..048d082c5 100644
--- a/helm/software/components/ng_paramodulation/founif.ml
+++ b/helm/software/components/ng_paramodulation/founif.ml
@@ -22,27 +22,27 @@ module Founif (B : Terms.Blob) = struct
     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
+      | Terms.Var i ->
+          let t = lookup i subst in
           if not (U.eq_foterm 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
+    let rec unif subst s t =
+      let s = match s with Terms.Var i -> lookup i subst | _ -> s
+      and t = match t with Terms.Var i -> lookup i subst | _ -> t
       
       in
       match s, t with
-      | s, t when U.eq_foterm s t -> subst, vars
+      | s, t when U.eq_foterm s t -> subst
       | 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
+          unif subst t s
       | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
-          unif subst vars t s
+          unif subst t s
       | Terms.Var i, t when occurs_check subst i t ->
           raise
             (UnificationFailure (lazy "Inference.unification.unif"))
@@ -50,23 +50,21 @@ module Founif (B : Terms.Blob) = struct
           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 not(U.eq_foterm hds hdt)->
-          raise (UnificationFailure (lazy "Inference.unification.unif"))
-      | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
+          let subst = Subst.build_subst i t subst in
+          subst
+      | _, Terms.Var _ -> unif subst t s
+      | Terms.Node l1, Terms.Node l2 -> (
           try
             List.fold_left2
-              (fun (subst', vars) s t -> unif subst' vars s t)
-              (subst, vars) tls tlt
+              (fun subst' s t -> unif subst' s t)
+              subst l1 l2
           with Invalid_argument _ ->
             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 subst = unif Subst.id_subst t1 t2 in
     let vars = Subst.filter subst vars in
     subst, vars
   
diff --git a/helm/software/components/ng_paramodulation/subst.ml b/helm/software/components/ng_paramodulation/subst.ml
index b8cadf48c..1b9f2624c 100644
--- a/helm/software/components/ng_paramodulation/subst.ml
+++ b/helm/software/components/ng_paramodulation/subst.ml
@@ -11,9 +11,9 @@
 
 module Subst (B : Terms.Blob) = struct
   
-  let empty_subst = [];;
+  let id_subst = [];;
   
-  let buildsubst n t tail = (n,t) :: tail ;;
+  let build_subst n t tail = (n,t) :: tail ;;
   
   let rec lookup_subst var subst =
     match var with
@@ -24,6 +24,7 @@ module Subst (B : Terms.Blob) = struct
               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;;
   
diff --git a/helm/software/components/ng_paramodulation/subst.mli b/helm/software/components/ng_paramodulation/subst.mli
index 8747a478f..dd7e0c2ec 100644
--- a/helm/software/components/ng_paramodulation/subst.mli
+++ b/helm/software/components/ng_paramodulation/subst.mli
@@ -13,11 +13,11 @@
 
 module Subst (B : Terms.Blob) : 
   sig
-    val empty_subst : B.t Terms.substitution
-    val buildsubst : 
+    val id_subst : B.t Terms.substitution
+    val build_subst : 
       int -> B.t Terms.foterm -> B.t Terms.substitution -> 
        B.t Terms.substitution
     val lookup_subst : 
-          B.t Terms.foterm -> B.t Terms.substitution -> B.t Terms.foterm
+          int -> B.t Terms.substitution -> B.t Terms.foterm
     val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
   end
-- 
2.39.2