- 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 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
+ | 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, 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.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' s t -> unif subst' s t)
+ subst l1 l2
+ with Invalid_argument _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ )
+ | _, _ ->