-exception UnificationFailure of string Lazy.t;;
-
-
-(* DUPLICATE CODE FOR TESTS (see FoUnif) *)
- let alpha_eq s t =
- let rec equiv subst s t =
- let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
- and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
-
- in
- match s, t with
- | s, t when eq_foterm s t -> subst
- | Terms.Var i, Terms.Var j
- when (not (List.exists (fun (_,k) -> k=t) subst)) ->
- let subst = FoSubst.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 FoSubst.id_subst s t
-;;
-
-let relocate maxvar varlist subst =
- List.fold_right
- (fun i (maxvar, varlist, s) ->
- maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
- varlist (maxvar+1, [], subst)
- ;;
-
- let are_invertible l r =
- let varlist = Terms.vars_of_term l in
- let maxvar = List.fold_left max 0 varlist in
- let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
- let l = FoSubst.apply_subst subst l in
- try (ignore(alpha_eq l r);true) with
- UnificationFailure _ -> false