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

1 files changed, 13 insertions, 1 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index a2015c2b1..ee01d2e71 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -48,10 +48,22 @@ val error_needs_inversion : env -> constr -> types -> 'a
 
 (*s Compilation of pattern-matching. *)
 
+type alias_constr =
+  | DepAlias
+  | NonDepAlias
+type dep_status = KnownDep | KnownNotDep | DepUnknown
+type tomatch_type =
+  | IsInd of types * inductive_type * name list
+  | NotInd of constr option * types
+type tomatch_status =
+  | Pushed of ((constr * tomatch_type) * int list * (name * dep_status))
+  | Alias of (constr * constr * alias_constr * constr)
+  | Abstract of rel_declaration
+
 module type S = sig
   val compile_cases :
     loc -> case_style ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
+    (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref ->
     type_constraint -> 
     env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment