(X ...) =?= (f ...) --> X := f
let rec occurs_check subst what where =
match where with
| Terms.Var i when i = what -> true
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
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
- | 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) ->
| 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) ->
| Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
| Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
| Terms.Var i, t when occurs_check subst i t ->
raise
(UnificationFailure (lazy "Inference.unification.unif"))
| 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 ->
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 -> (
- (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
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
let vars = Subst.filter subst vars in
subst, vars
module Subst (B : Terms.Blob) = struct
module Subst (B : Terms.Blob) = struct
- 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
let rec lookup_subst var subst =
match var with
Not_found -> var)
| _ -> var
;;
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;;
let is_in_subst i subst = List.mem_assoc i subst;;
module Subst (B : Terms.Blob) :
sig
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 :
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
val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
end