diff options
| author | herbelin | 2006-09-13 11:11:51 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-13 11:11:51 +0000 |
| commit | 7c387703f264666ab83b89b51ee270ff2c7c189c (patch) | |
| tree | bf1b2f2657ed16e200a7f27dee5b1ccb7f29f6af | |
| parent | ade5ae3ee5931180211260b943e5095188518c03 (diff) | |
Abandon unification pattern des evars dans apply: combiné avec le
backtrack de eauto et le partage des evars entre buts, cela fait
davantage de choix irréversibles avec rupture de compatibilité.
Exemple:
but 1: |- P ?f
but 2: H1:a=b, H2:c=c, H3:g a = g b |- ?f a = ?f b
eauto sur le but 2 peut trouver au moins 3 solutions:
1- avec unif premier ordre, il peut trouver ?f=g, en appliquant exact H3
2- avec unif pattern, il peut trouver ?f=\_.c, en appliquant exact H2
3- en s'y prenant bien, il devrait pouvoir laisser ?f ouvert en appliquant
f_equal H1
Dans certains exemples (Orsay/FSets/PrecedenceGraph/PrecedenceGraph.v en
l'occurrence), ajouter l'unif pattern fait adopter la solution 2
plutôt que la solution 3. En attente d'un meilleur algorithme, abandon
donc de l'unif pattern des evars pour apply (ce qui n'empêche pas que,
déjà, la situation actuelle, qui utilise l'unif premier ordre, peut
conduire à faire des mauvais choix -- mais au moins on reste
compatible...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9134 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/unification.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index abdf8c863f..30ae394124 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -54,6 +54,7 @@ let solve_pattern_eqn_array env f l c (metasubst,evarsubst) = | Meta k -> (k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst | Evar ev -> + (* Currently unused: incompatible with eauto/eassumption backtracking *) metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst | _ -> assert false @@ -104,10 +105,12 @@ let unify_0 env sigma cv_pb mod_delta m n = | _, LetIn (_,b,_,c) -> unirec_rec env pb substn cM (subst1 b c) | App (f1,l1), App (f2,l2) -> - if is_unification_pattern f1 l1 & not (dependent f1 cN) + if + isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) then solve_pattern_eqn_array env f1 l1 cN substn - else if is_unification_pattern f2 l2 & not (dependent f2 cM) + else if + isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) then solve_pattern_eqn_array env f2 l2 cM substn else |