From f4b250cac72454356728916fe3f8757822c26485 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 29 Aug 2006 17:00:14 +0000 Subject: Prise en compte de l'instance des evars dans la détection des 'motifs' d'unification à la Miller. Ceci devrait garantir la généralité de la solution modulo le problème résiduel de éta : en l'absence d'éta dans le CCI, le choix entre deux instances éta-convertibles distinctes d'une evar, conduira à des solutions non convertibles pour le CCI. Par exemple, le problème suivant, pour c et Q rigides, a deux solutions distinctes non convertibles. "fun (H: forall P:A->Prop, ~ c (fun x => P x)) (K: c (fun x => Q x)) => H _ K" MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9096 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarconv.ml | 8 ++++---- pretyping/evarutil.ml | 5 +++-- pretyping/evarutil.mli | 2 +- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6799671d1..9af633b0a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -231,7 +231,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, MaybeFlexible flex2 -> let f1 i = if - is_unification_pattern l1 & + is_unification_pattern ev1 l1 & not (occur_evar (fst ev1) (applist (term2,l2))) then (* Miller-Pfenning's patterns unification *) @@ -261,7 +261,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Flexible ev2 -> let f1 i = if - is_unification_pattern l2 & + is_unification_pattern ev2 l2 & not (occur_evar (fst ev2) (applist (term1,l1))) then (* Miller-Pfenning's patterns unification *) @@ -318,7 +318,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, Rigid _ -> if - is_unification_pattern l1 & + is_unification_pattern ev1 l1 & not (occur_evar (fst ev1) (applist (term2,l2))) then (* Miller-Pfenning's patterns unification *) @@ -344,7 +344,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Rigid _, Flexible ev2 -> if - is_unification_pattern l2 & + is_unification_pattern ev2 l2 & not (occur_evar (fst ev2) (applist (term1,l1))) then (* Miller-Pfenning's patterns unification *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f803fd9d7..c4c5ec922 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -493,8 +493,9 @@ let head_evar = that we don't care whether args itself contains Rel's or even Rel's distinct from the ones in l *) -let is_unification_pattern l = - List.for_all isRel l & list_uniquize l = l +let is_unification_pattern (_,args) l = + let l' = Array.to_list args @ l in + List.for_all (fun a -> isRel a or isVar a) l' & list_uniquize l' = l' (* From a unification problem "?X l1 = term1 l2" such that l1 is made of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 2aceece0b..5519b57c9 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -82,7 +82,7 @@ val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts -val is_unification_pattern : constr list -> bool +val is_unification_pattern : existential -> constr list -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr (***********************************************************) -- cgit v1.2.3