diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /test-suite/ideal-features | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'test-suite/ideal-features')
-rw-r--r-- | test-suite/ideal-features/Case9.v | 12 | ||||
-rw-r--r-- | test-suite/ideal-features/complexity/evars_subst.v | 53 | ||||
-rw-r--r-- | test-suite/ideal-features/evars_subst.v | 53 | ||||
-rw-r--r-- | test-suite/ideal-features/universes.v | 43 |
4 files changed, 161 insertions, 0 deletions
diff --git a/test-suite/ideal-features/Case9.v b/test-suite/ideal-features/Case9.v new file mode 100644 index 00000000..800c431e --- /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 00000000..6f9f86a9 --- /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/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v new file mode 100644 index 00000000..6f9f86a9 --- /dev/null +++ b/test-suite/ideal-features/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/ideal-features/universes.v b/test-suite/ideal-features/universes.v new file mode 100644 index 00000000..6db4cfe1 --- /dev/null +++ b/test-suite/ideal-features/universes.v @@ -0,0 +1,43 @@ +(* Some issues with polymorphic inductive types *) + +(* 1- upper constraints with respect to non polymorphic inductive types *) + +Unset Elimination Schemes. +Definition Ty := Type (* Top.1 *). + +Inductive Q (A:Type (* Top.2 *)) : Prop := q : A -> Q A. +Inductive T (B:Type (* Top.3 *)) := t : B -> Q (T B) -> T B. +(* ajoute Top.4 <= Top.2 inutilement: + 4 est l'univers utilisé dans le calcul du type polymorphe de T *) +Definition C := T Ty. +(* ajoute Top.1 < Top.3 : + Top.3 jour le rôle de pivot pour propager les contraintes supérieures qu'on + a sur l'argument B de T: Top.3 sera réutilisé plus tard comme majorant + des arguments effectifs de T, propageant à cette occasion les contraintes + supérieures sur Top.3 *) + +(* We need either that Q is polymorphic on A (though it is in Type) or + that the constraint Top.1 < Top.2 is set (and it is not set!) *) + +(* 2- upper constraints with respect to unfoldable constants *) + +Definition f (A:Type (* Top.1 *)) := True. +Inductive R := r : f R -> R. +(* ajoute Top.3 <= Top.1 inutilement: + Top.3 est l'univers utilisé dans le calcul du type polymorphe de R *) + +(* mais il manque la contrainte que l'univers de R est plus petit que Top.1 + ce qui l'empêcherait en fait d'être vraiment polymorphe *) + +(* 3- constraints with respect to global constants *) + +Inductive S (A:Ty) := s : A -> S A. + +(* Q est considéré polymorphique vis à vis de A alors que le type de A + n'est pas une variable mais un univers déjà existant *) + +(* Malgré tout la contrainte Ty < Ty est ajoutée (car Ty est vu comme + un pivot pour propager les contraintes sur le type A, comme si Q était + vraiment polymorphique, ce qu'il n'est pas parce que Ty est une + constante). Et heureusement qu'elle est ajouté car elle évite de + pouvoir typer "Q Ty" *) |