From b9d067ff0d66913b7ade9fadc79064dedb4aa86f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Jun 2006 12:58:20 +0000 Subject: [PATCH] occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are considered the same. --- .../components/tactics/paramodulation/inference.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index e2f85fa2b..1c3daffec 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -70,7 +70,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = let lookup = Subst.lookup_subst in let rec occurs_check subst what where = match where with - | t when what = t -> true + | Cic.Meta(i,_) when i = what -> true | C.Appl l -> List.exists (occurs_check subst what) l | C.Meta _ -> let t = lookup where subst in @@ -84,6 +84,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = in match s, t with | s, t when s = t -> subst, menv + (* sometimes the same meta has different local contexts; this + could create "cyclic" substitutions *) + | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) &&(locked locked_menv j) -> raise @@ -92,7 +95,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = unif subst menv t s | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> unif subst menv t s - | C.Meta _, t when occurs_check subst s t -> + | C.Meta (i,_), t when occurs_check subst i t -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t when (locked locked_menv i) -> -- 2.39.2