diff options
Diffstat (limited to 'test-suite/ideal-features')
-rw-r--r-- | test-suite/ideal-features/Case3.v | 29 | ||||
-rw-r--r-- | test-suite/ideal-features/Case9.v | 2 | ||||
-rw-r--r-- | test-suite/ideal-features/complexity/evars_subst.v | 6 | ||||
-rw-r--r-- | test-suite/ideal-features/eapply_evar.v | 9 | ||||
-rw-r--r-- | test-suite/ideal-features/evars_subst.v | 6 | ||||
-rw-r--r-- | test-suite/ideal-features/implicit_binders.v | 124 | ||||
-rw-r--r-- | test-suite/ideal-features/universes.v | 4 |
7 files changed, 142 insertions, 38 deletions
diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v deleted file mode 100644 index de7784ae..00000000 --- a/test-suite/ideal-features/Case3.v +++ /dev/null @@ -1,29 +0,0 @@ -Inductive Le : nat -> nat -> Set := - | LeO : forall n : nat, Le 0 n - | LeS : forall n m : nat, Le n m -> Le (S n) (S m). - -Parameter discr_l : forall n : nat, S n <> 0. - -Type - (fun n : nat => - match n return (n = 0 \/ n <> 0) with - | O => or_introl (0 <> 0) (refl_equal 0) - | S O => or_intror (1 = 0) (discr_l 0) - | S (S x) => or_intror (S (S x) = 0) (discr_l (S x)) - end). - -Parameter iguales : forall (n m : nat) (h : Le n m), Prop. - -Type - match LeO 0 as h in (Le n m) return Prop with - | LeO O => True - | LeS (S x) (S y) H => iguales (S x) (S y) H - | _ => False - end. - -Type - match LeO 0 as h in (Le n m) return Prop with - | LeO O => True - | LeS (S x) O H => iguales (S x) 0 H - | _ => False - end. diff --git a/test-suite/ideal-features/Case9.v b/test-suite/ideal-features/Case9.v index 800c431e..d95c2108 100644 --- a/test-suite/ideal-features/Case9.v +++ b/test-suite/ideal-features/Case9.v @@ -6,7 +6,7 @@ CoInductive hdlist : unit -> Type := Variable P : forall bo, hdlist bo -> Prop. Variable all : forall bo l, P bo l. -Definition F (l:hdlist tt) : P tt 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 index 6f9f86a9..b3dfb33c 100644 --- a/test-suite/ideal-features/complexity/evars_subst.v +++ b/test-suite/ideal-features/complexity/evars_subst.v @@ -3,12 +3,12 @@ (* 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", + 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 + 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 *) @@ -25,7 +25,7 @@ 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 diff --git a/test-suite/ideal-features/eapply_evar.v b/test-suite/ideal-features/eapply_evar.v new file mode 100644 index 00000000..547860bf --- /dev/null +++ b/test-suite/ideal-features/eapply_evar.v @@ -0,0 +1,9 @@ +(* Test propagation of evars from subgoal to brother subgoals *) + +(* This does not work (oct 2008) because "match goal" sees "?evar = O" + and not "O = O" *) + +Lemma eapply_evar : O=O -> 0=O. +intro H; eapply trans_equal; + [apply H | match goal with |- ?x = ?x => reflexivity end]. +Qed. diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v index 6f9f86a9..b3dfb33c 100644 --- a/test-suite/ideal-features/evars_subst.v +++ b/test-suite/ideal-features/evars_subst.v @@ -3,12 +3,12 @@ (* 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", + 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 + 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 *) @@ -25,7 +25,7 @@ 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 diff --git a/test-suite/ideal-features/implicit_binders.v b/test-suite/ideal-features/implicit_binders.v new file mode 100644 index 00000000..2ec72780 --- /dev/null +++ b/test-suite/ideal-features/implicit_binders.v @@ -0,0 +1,124 @@ +(** * Questions de syntaxe autour de la généralisation implicite + + ** Lieurs de classes + Aujourd'hui, les lieurs de classe [ ] et les + lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour + les lieurs de classes (où la variable liée peut être anonyme): + *) + +Class Foo (A : Type) := foo : A -> nat. + +Definition bar [ Foo A ] (x y : A) := foo x + foo y. + +Definition bar₀ {{ Foo A }} (x y : A) := foo x + foo y. + +Definition bar₁ {( Foo A )} (x y : A) := foo x + foo y. + +Definition bar₂ ({ Foo A }) (x y : A) := foo x + foo y. + +Definition bar₃ (( Foo A )) (x y : A) := foo x + foo y. + +Definition bar₄ {( F : Foo A )} (x y : A) := foo x + foo y. + +(** Les lieurs sont généralisés à tous les termes, pas seulement aux classes: *) + +Definition relation A := A -> A -> Prop. + +Definition inverse {( R : relation A )} := fun x y => R y x. + +(** Autres propositions: + [Definition inverse ..(R : relation A) := fun x y => R y x] et + + [Definition inverse ..[R : relation A] := fun x y => R y x] ou + [Definition inverse ..{R : relation A} := fun x y => R y x] + pour lier [R] implicitement. + + MS: Le .. empêche d'utiliser electric-terminator dans Proof General. Cependant, il existe + aussi les caractères utf8 ‥ (two dot leader) et … (horizontal ellipsis) qui permettraient + d'éviter ce souci moyennant l'utilisation d'unicode. + + [Definition inverse _(R : relation A) := fun x y => R y x] et + + [Definition inverse _[R : relation A] := fun x y => R y x] ou + [Definition inverse _{R : relation A} := fun x y => R y x] + + [Definition inverse `(R : relation A) := fun x y => R y x] et + + [Definition inverse `[R : relation A] := fun x y => R y x] ou + [Definition inverse `{R : relation A} := fun x y => R y x] + + + Toujours avec la possibilité de ne pas donner le nom de la variable: +*) + +Definition div (x : nat) ({ y <> 0 }) := 0. + +(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à + l'argument. Manque de variables anonymes pour l'utilisateur mais pas pour le système... *) + +Inductive bla [ Foo A ] : Type :=. + +(** *** Les autres syntaxes ne supportent pas de pouvoir spécifier séparément les statuts + des variables généralisées et celui de la variable liée. Ca peut être utile pour les + classes où l'on a les cas de figure: *) + +(** Trouve [A] et l'instance par unification du type de [x]. *) +Definition allimpl {{ Foo A }} (x : A) : A := x. + +(** Trouve l'instance à partir de l'index explicite *) + +Class SomeStruct (a : nat) := non_zero : a <> 0. + +Definition instimpl ({ SomeStruct a }) : nat := a + a. + +(** Donne l'instance explicitement (façon foncteur). *) + +Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) := + fun x => let (l, r) := x in foo l + foo r. + +(** *** Questions: + - Gardez les crochets [ ] pour {{ }} ? + - Quelle syntaxe pour la généralisation ? + - Veut-on toutes les combinaisons de statut pour les variables généralisées et la variable liée ? + *) + +(** ** Constructeur de généralisation implicite + + Permet de faire une généralisation n'importe où dans le terme: on + utilise un produit ou un lambda suivant le scope (fragile ?). + *) + +Goal `(x + y + z = x + (y + z)). +Admitted. + +(** La généralisation donne un statut implicite aux variables si l'on utilise + `{ }. *) + +Definition baz := `{x + y + z = x + (y + z)}. +Print baz. + +(** Proposition d'Arthur C.: déclarer les noms de variables généralisables à la [Implicit Types] + pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant + ne sont plus silencieuses: *) + +Check `(foob 0 + x). + +(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans + les déclarations d'instances (i.e. les deux defs suivantes sont équivalentes). *) + +Instance fooa : Foo A. +Admitted. +Definition fooa' : `(Foo A). +Admitted. + +(** Un peu différent de la généralisation des lieurs qui "explosent" les variables + libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans + la définition mais [F : Π a, SomeStruct a]. *) + +Definition qux {( F : SomeStruct a )} : nat := a. +Definition qux₁ {( F : `(SomeStruct a) )} : nat := 0. + +(** *** Questions + - Autres propositions de syntaxe ? + - Réactions sur la construction ? + *)
\ No newline at end of file diff --git a/test-suite/ideal-features/universes.v b/test-suite/ideal-features/universes.v index 6db4cfe1..49530ebc 100644 --- a/test-suite/ideal-features/universes.v +++ b/test-suite/ideal-features/universes.v @@ -7,7 +7,7 @@ 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: +(* 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 : @@ -23,7 +23,7 @@ Definition C := T Ty. Definition f (A:Type (* Top.1 *)) := True. Inductive R := r : f R -> R. -(* ajoute Top.3 <= Top.1 inutilement: +(* 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 |