exception UnificationFailure of string Lazy.t;;
-module Founif (B : Terms.Blob) = struct
- module Subst = FoSubst.Subst(B)
+let mem2 a b l =
+ let rec aux found_a found_b = function
+ | x :: tl ->
+ let found_a = found_a || x = a in
+ let found_b = found_b || x = b in
+ if found_a && found_b then true, true
+ else aux found_a found_b tl
+ | [] -> found_a, found_b
+ in
+ aux false false l
+;;
+
+module Founif (B : Orderings.Blob) = struct
+ module Subst = FoSubst
module U = FoUtils.Utils(B)
- let unification vars locked_vars t1 t2 =
- let lookup = Subst.lookup_subst in
+ let unification (* vars *) locked_vars t1 t2 =
let rec occurs_check subst what where =
match where with
| Terms.Var i when i = what -> true
| Terms.Var i ->
- let t = lookup i subst in
+ let t = Subst.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 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
+ 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 (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 t s
- | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
- unif subst t s
+ | Terms.Var i, Terms.Var j ->
+ (* TODO: look in locked vars for both i and j at once *)
+ let i_locked, j_locked = mem2 i j locked_vars in
+ if i_locked then
+ if j_locked then
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ else
+ Subst.build_subst j s subst
+ else
+ Subst.build_subst i t subst
| Terms.Var i, t when occurs_check subst i t ->
- raise
- (UnificationFailure (lazy "Inference.unification.unif"))
+ 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.build_subst i t subst in
- subst
- | _, Terms.Var _ -> unif subst t s
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ | Terms.Var i, t -> Subst.build_subst i t subst
+ | t, Terms.Var i when occurs_check subst i t ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ | t, Terms.Var i when (List.mem i locked_vars) ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ | t, Terms.Var i -> Subst.build_subst i t subst
| Terms.Node l1, Terms.Node l2 -> (
try
List.fold_left2
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)) ->
+ let subst = Subst.build_subst i t subst in
+ subst
+ | Terms.Node l1, Terms.Node l2 -> (
+ try
+ List.fold_left2
+ (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