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

6 files changed, 94 insertions, 11 deletions

diff --git a/test-suite/check b/test-suite/check
index dd51c1e76..d01f9b51a 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -147,7 +147,7 @@ test_complexity() {
 
 test_bugs () {
     # Process verifications concerning submitted bugs. A message is
-    # printed for all opened bugs (still active or seem to be closed.
+    # printed for all opened bugs (still active or seems to be closed).
     # For closed bugs that behave as expected, no message is printed
 
     # All files are assumed to have <# of the bug>.v as a name
@@ -213,6 +213,26 @@ test_bugs () {
     
 }
 
+test_features () {
+    # Process verifications concerning submitted bugs. A message is
+    # printed for all opened bugs (still active or seem to be closed.
+    # For closed bugs that behave as expected, no message is printed
+
+    echo "Testing wishes..."
+    files=`/bin/ls -1 $1/*.v 2> /dev/null`
+    for f in $files; do 
+	nbtests=`expr $nbtests + 1`
+	printf "    "$f"..."
+	$command $f $2 > /dev/null 2>&1 
+	if [ $? != 0 ]; then
+	    echo "still wished"
+	    nbtestsok=`expr $nbtestsok + 1`
+        else 
+	    echo "Good news! (wish seems to be granted, please check)"
+        fi
+    done
+}
+
 # Programme principal
 
 echo "Success tests"
@@ -233,10 +253,9 @@ echo "Module tests"
 $coqtop -compile modules/Nat
 $coqtop -compile modules/plik
 test_success modules "-I modules -impredicative-set"
+#echo "Ideal-features tests"
+#test_features ideal-features
 
 pourcentage=`expr 100 \* $nbtestsok / $nbtests`
 echo
 echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"
-
-#echo "Ideal-features tests"
-#test_success ideal-features
diff --git a/test-suite/ideal-features/Case9.v b/test-suite/ideal-features/Case9.v
new file mode 100644
index 000000000..800c431ec
--- /dev/null
+++ b/test-suite/ideal-features/Case9.v
@@ -0,0 +1,12 @@
+(* Exemple soumis par Pierre Corbineau (bug #1671) *)
+
+CoInductive hdlist : unit -> Type :=
+| cons : hdlist tt -> hdlist tt.
+
+Variable P : forall bo, hdlist bo -> Prop.
+Variable all : forall bo l, P bo l.
+
+Definition F (l:hdlist tt) : P tt l := 
+match l in hdlist u return P u l with
+| cons (cons l') => all tt _
+end.
diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v
new file mode 100644
index 000000000..6f9f86a95
--- /dev/null
+++ b/test-suite/ideal-features/complexity/evars_subst.v
@@ -0,0 +1,53 @@
+(* Bug report #932 *)
+(* Expected time < 1.00s *)
+
+(* Let n be the number of let-in. The complexity comes from the fact
+   that each implicit arguments of f was in a larger and larger
+   context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", 
+   "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This
+   type is an evar instantiated on the n variables denoting the "f ?Ti 0".
+   One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the
+   type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another
+   substitution is done leading to 
+   "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]"
+   and so on. At the end, we get a term of exponential size *)
+
+(* A way to cut the complexity could have been to remove the dependency in
+   anonymous variables in evars but this breaks intuitive behaviour
+   (see Case15.v); another approach could be to substitute lazily
+   and/or to simultaneously substitute let binders and evars *)
+
+Variable P : Set -> Set.
+Variable f : forall A : Set, A -> P A.
+
+Time Check
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+ 
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+    f _ 0.
+
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 7c2b7c0bb..499c06606 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -10,6 +10,10 @@ Type match 0, eq, 0 return nat with
      | O, x, y => 0
      | S x, y, z => x
      end.
+Type match 0, eq, 0 return _ with
+     | O, x, y => 0
+     | S x, y, z => x
+     end.
 
 (* Non dependent form of annotation *)
 Type match 0, eq return nat with
@@ -406,7 +410,6 @@ Type match niln with
      | x => 0
      end.
 
-
 Type match niln return nat with
      | niln => 0
      | consn n a l => a
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index b625eb151..49bd77fcd 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -71,13 +71,9 @@ Inductive Setoid : Type :=
 
 Definition elem (A : Setoid) := let (S, R, e) := A in S.
 
-(* <Warning> : Grammar is replaced by Notation *)
-
 Definition equal (A : Setoid) :=
   let (S, R, e) as s return (Relation (elem s)) := A in R.
 
-(* <Warning> : Grammar is replaced by Notation *)
-
 
 Axiom prf_equiv : forall A : Setoid, Equivalence (elem A) (equal A).
 Axiom prf_refl : forall A : Setoid, Reflexive (elem A) (equal A).
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index bc9c8a374..cf8210733 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -29,8 +29,8 @@ CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p :=
 
 Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end).
 
-(* Check inference of simple types even in presence of (non ambiguous)
-   dependencies (needs revision ) *)
+(* Check inference of simple types in presence of non ambiguous
+   dependencies (needs revision 10125) *)
 
 Section folding.