aux false false l
;;
-module Founif (B : Terms.Blob) = struct
- module Subst = FoSubst (*.Subst(B)*)
+module Founif (B : Orderings.Blob) = struct
+ module Subst = FoSubst
module U = FoUtils.Utils(B)
- let unification vars locked_vars t1 t2 =
+ let unification (* vars *) locked_vars t1 t2 =
let rec occurs_check subst what where =
match where with
| Terms.Var i when i = what -> true
raise (UnificationFailure (lazy "Inference.unification.unif"))
in
let subst = unif Subst.id_subst t1 t2 in
- let vars = Subst.filter subst vars in
- subst, vars
+ subst
;;
+(* Sets of variables in s and t are assumed to be disjoint *)
let alpha_eq s t =
let rec equiv subst s t =
let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
-
+
in
match s, t with
- | s, t when U.eq_foterm s t -> subst
- | Terms.Var i, Terms.Var j
- when (not (List.exists (fun (_,k) -> k=t) subst)) ->
+ | s, t when U.eq_foterm s t -> subst
+ | Terms.Var i, Terms.Var j
+ when (not (List.exists (fun (_,k) -> k=t) subst)) ->
let subst = Subst.build_subst i t subst in
subst
- | Terms.Node l1, Terms.Node l2 -> (
+ | Terms.Node l1, Terms.Node l2 -> (
try
List.fold_left2
- (fun subst' s t -> equiv subst' s t)
- subst l1 l2
+ (fun subst' s t -> equiv subst' s t)
+ subst l1 l2
with Invalid_argument _ ->
raise (UnificationFailure (lazy "Inference.unification.unif"))
)
- | _, _ ->
+ | _, _ ->
raise (UnificationFailure (lazy "Inference.unification.unif"))
in
equiv Subst.id_subst s t
;;
+
end