From d28e499e10fda9fca6cd7767822f018aa2d5950d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 17 Dec 2003 11:27:30 +0000 Subject: [PATCH] * comments improved an possible code weakness (i.e. less than first order unification detected) made explicit in the comment and with a warning. --- helm/ocaml/cic_unification/cicUnification.ml | 25 ++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index ad1b47206..7221dd0a8 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -31,9 +31,15 @@ exception OpenTerm;; (**** DELIFT ****) -(* the delift function takes in input an ordered list of integers [n1,...,nk] - and a term t, and relocates rel(nk) to k. Typically, the list of integers - is a parameter of a metavariable occurrence. *) +(* the delift function takes in input an ordered list of optional terms *) +(* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with *) +(* rel(k). Typically, the list of optional terms is the explicit substitution *)(* that is applied to a metavariable occurrence and the result of the delift *) +(* function is a term the implicit variable can be substituted with to make *) +(* the term [t] unifiable with the metavariable occurrence. *) +(* In general, the problem is undecidable if we consider equivalence in place *) +(* of alpha convertibility. Our implementation, though, is even weaker than *) +(* alpha convertibility, since it replace the term [tk] if and only if [tk] *) +(* is a Rel (missing all the other cases). Does this matter in practice? *) exception NotInTheList;; @@ -143,7 +149,18 @@ let delift context metasenv l t = in C.CoFix (i, liftedfl) in - let res = deliftaux 0 t in + let res = + try + deliftaux 0 t + with + NotInTheList -> + (* This is the case where we fail even first order unification. *) + (* The reason is that our delift function is weaker than first *) + (* order (in the sense of alpha-conversion). See comment above *) + (* related to the delift function. *) +prerr_endline "!!!!!!!!!!! First Order UnificationFailed, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ; + raise UnificationFailed + in res, restrict !to_be_restricted metasenv ;; -- 2.39.2