diff options
author | 2008-05-05 13:55:24 +0000 | |
---|---|---|
committer | 2008-05-05 13:55:24 +0000 | |
commit | af8e8176a6ca63c59621e4775d50faf51627b4cc (patch) | |
tree | 94981efe24ba788e511a8e6b4657365cf2c1f1f8 /CHANGES | |
parent | 2e59cf3c09a8ee2c7b0dc97551f3c26497f4b67d (diff) |
Mise en place d'un algorithme d'inversion des contraintes de type lors
du filtrage. Cela permet de détecter les cas impossibles et de simuler
les contraintes d'inversion exprimables sous la forme d'un assignement
des arguments du constructeurs (cf le cas de Vtail dans Bvector.v).
Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi)
avec vi composé uniquement de constructeurs, et que le résultat final
est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on
construit le prédicat
Q:=fun x1 .. xn y =>
match x1 .. xn y with
| v1(z) .. vn(z) t => P(z)
| _ .. _ _ => ?evar-speciale-cas-impossible
end
qui vérifiera bien que Q u1 .. un = P(w1,..,wp).
En raison de limitations de l'unification (on aurait besoin d'eta
conversion pour résoudre des problèmes du genre
"terme rigide == match x with _ => ?evar end", et besoin d'instanciation par
constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"),
je n'ai pas réussi à traiter le cas général.
Aussi, on adopte une stratégie pragmatique consistant à tester
plusieurs prédicats possibles :
- si un type final est donné, on essaie d'abord l'algorithme de
Matthieu et sinon le nouvel algorithme (permet par exemple de traiter
certains cas d'élimination dépendante de Bvector.v),
- s'il n'y a pas de type final, on essaie d'abord le nouvel algo et
sinon, on essaie avec un prédicat sans dépendance (permet de traiter
des cas compliqués comme celui de par cas sur I' dans le fichier
Case13.v de la test-suite).
Dans la pratique, il y a beaucoup de changement dans le code de compile_case.
- Par exemple, la compilation est maintenant toujours appelé avec un
prédicat (là où l'on pouvait avoir None, on a maintenant toujours au
moins une evar).
- En revanche, le membre droit des clauses est maintenant
optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une
branche impossible au moment du calcul du prédicat de retour.
- Aussi, on renonce aux PrLetIn et PrProd dans l'expression du
predicat de retour mais il faut savoir que c'est maintenant la liste
des tomatchs qui spécifie le contexte exact dans lequel le prédicat
de retour est bien typé.
- Et d'autres...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 11 |
1 files changed, 8 insertions, 3 deletions
@@ -6,7 +6,6 @@ Language - If a fixpoint is not written with an explicit { struct ... }, then all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. (DOC TODO?) -- Improved inference of implicit arguments. - New experimental typeclass system giving ad-hoc polymorphism and overloading based on dependent records and implicit arguments. - New syntax "let 'pat := b in c" for let-binding using irrefutable patterns. @@ -90,8 +89,13 @@ Libraries (DOC TO CHECK) logic. Addition of files providing intuitionistic axiomatizations of descriptions: Epsilon.v, Description.v and IndefiniteDescription.v. -Notations, coercions and implicit arguments +Notations, coercions, implicit arguments and type inference +- More automation in the inference of the return clause of dependent + pattern-matching problems. +- Experimental allowance for omission of the clauses easily detectable as + impossible in pattern-matching problems. +- Improved inference of implicit arguments. - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit Defensive" for controlling inference and use of implicit arguments. @@ -159,7 +163,7 @@ Tactics occurrences. (DOC TODO) - New syntax "rewrite A,B" for "rewrite A; rewrite B" - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" -- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" +- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" to do induction-inversion on instantiated inductive families à la BasicElim. - Tactic "apply" now able to reason modulo unfolding of constants (possible source of incompatibility in situations where apply may fail, @@ -272,6 +276,7 @@ Setoid rewriting Tools +- New stand-alone .vo files verifier.a - CoqIDE font defaults to monospace so as indentation to be meaningful. Miscellaneous |