diff options
Diffstat (limited to 'test-suite')
23 files changed, 322 insertions, 25 deletions
diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v new file mode 100644 index 0000000000..a079d672d3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9294.v @@ -0,0 +1,29 @@ +Set Printing Universes. + +Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A. +Arguments foo {_} _. +Print Universes Subgraph (Foo.i). +Definition bar : Foo True -> Set := fun '(foo x) => x. + +Definition foo_bar (n : Foo True) : foo (bar n) = n. +Proof. destruct n;reflexivity. Qed. + +Definition bar_foo (n : Set) : bar (foo n) = n. +Proof. reflexivity. Qed. + +Require Import Hurkens. + +Inductive box (A : Set) : Prop := Box : A -> box A. + +Definition Paradox : False. +Proof. +Fail unshelve refine ( + NoRetractFromSmallPropositionToProp.paradox + (Foo True) + (fun A => foo A) + (fun A => box (bar A)) + _ + _ + False +). +Abort. diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v index bc5cd0fb68..4b6916af55 100644 --- a/test-suite/coqchk/inductive_functor_template.v +++ b/test-suite/coqchk/inductive_functor_template.v @@ -2,7 +2,7 @@ Module Type E. Parameter T : Type. End E. Module F (X:E). - #[universes(template)] Inductive foo := box : X.T -> foo. + Inductive foo := box : X.T -> foo. End F. Module ME. Definition T := nat. End ME. diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v new file mode 100644 index 0000000000..75b2a56169 --- /dev/null +++ b/test-suite/failure/Template.v @@ -0,0 +1,32 @@ +(* +Module TestUnsetTemplateCheck. + Unset Template Check. + + Section Foo. + + Context (A : Type). + + Definition cstr := nat : ltac:(let ty := type of A in exact ty). + + Inductive myind := + | cons : A -> myind. + End Foo. + + (* Can only succeed if no template check is performed *) + Check myind True : Prop. + + Print Assumptions myind. + (* + Axioms: + myind is template polymorphic on all its universe parameters. + *) + About myind. +(* +myind : Type@{Top.60} -> Type@{Top.60} + +myind is assumed template universe polymorphic on Top.60 +Argument scope is [type_scope] +Expands to: Inductive Top.TestUnsetTemplateCheck.myind +*) +End TestUnsetTemplateCheck. +*) diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4e949dcb04..a040b69b44 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -84,7 +84,6 @@ Print f. (* Was enhancement request #5142 (error message reported on the most general return clause heuristic) *) -#[universes(template)] Inductive gadt : Type -> Type := | gadtNat : nat -> gadt nat | gadtTy : forall T, T -> gadt T. diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 6976f35a88..0e84bf3966 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,7 +1,7 @@ (* Submitted by Randy Pollack *) -#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. +Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. Variables (S : Set) (P : pred S) (R : rel S) (x : S). diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index f9398fdca9..1ecd9771eb 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -101,7 +101,7 @@ Section decoder_result. Variable inst : Type. - #[universes(template)] Inductive decoder_result : Type := + Inductive decoder_result : Type := | DecUndefined : decoder_result | DecUnpredictable : decoder_result | DecInst : inst -> decoder_result diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 9b25c2dbd3..61ae4edbd1 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -#[universes(template)] CoInductive Inf := S { projS : Inf }. +CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 29614c032a..aeebc0f98b 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). (**********************************************************************) (* Test printing of #4932 *) -#[universes(template)] Inductive ftele : Type := +Inductive ftele : Type := | fb {T:Type} : T -> ftele | fr {T} : (T -> ftele) -> ftele. diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0c1b08f5a3..d671053c07 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. +Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index ab4172711e..e788977fb7 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,6 +1,6 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} -existT is template universe polymorphic +existT is template universe polymorphic on sigT.u0 sigT.u1 Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 35f36e87d7..14d63d39c4 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -6,7 +6,7 @@ Class HostFunction := host_func : Type. Section store. Context `{HostFunction}. - #[universes(template)] Record store := { store_funcs : host_func }. + Record store := { store_funcs : host_func }. End store. Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 4fe7b051f8..d9a649fadc 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,12 +20,12 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. -#[universes(template)] Record N := C { T : Type; _ : True }. +Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). -#[universes(template)] Record M := D { U : Type; a := 0; q : True }. +Record M := D { U : Type; a := 0; q : True }. Check fun x:M => let 'D T _ p := x in p. Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 99183f2064..9cf6ad35b8 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -3,12 +3,12 @@ *) Module A. - #[universes(template)] Inductive foo := f. + Inductive foo := f. Show Match foo. (* no need to disambiguate *) End A. Module B. - #[universes(template)] Inductive foo := f. + Inductive foo := f. (* local foo shadows A.foo, so constructor "f" needs disambiguation *) Show Match A.foo. End B. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 222a808768..a89fd64999 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -68,9 +68,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.32} in -let ff := Type@{UnivBinders.34} in tt -> ff - : Type@{max(UnivBinders.31,UnivBinders.33)} +let tt := Type@{UnivBinders.33} in +let ff := Type@{UnivBinders.35} in tt -> ff + : Type@{max(UnivBinders.32,UnivBinders.34)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = @@ -143,16 +143,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.56} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axfoo@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.57} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axbar@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.58} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axbar is universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 0eb5db1733..7465442cab 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -#[universes(template)] Record A := { B:Type; b:B->B }. +Record A := { B:Type; b:B->B }. Definition a B := {| B:=B; b:=fun x => x |}. Canonical Structure a. diff --git a/test-suite/output/bug7191.out b/test-suite/output/bug7191.out new file mode 100644 index 0000000000..005455e30c --- /dev/null +++ b/test-suite/output/bug7191.out @@ -0,0 +1,9 @@ + +type unit0 = +| Tt + +(** val f : unit0 -> unit0 **) + +let f _ = + assert false (* absurd case *) + diff --git a/test-suite/output/bug7191.v b/test-suite/output/bug7191.v new file mode 100644 index 0000000000..1aa4625b6c --- /dev/null +++ b/test-suite/output/bug7191.v @@ -0,0 +1,3 @@ +Require Extraction. +Definition f (x : False) : unit -> unit := match x with end. +Recursive Extraction f. diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 209fedc343..57a4739e9f 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -21,6 +21,6 @@ Print P. (* Note: exact numbers of evars are not important... *) -#[universes(template)] Inductive T (n:nat) : Type := A : T n. +Inductive T (n:nat) : Type := A : T n. Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/ssr/bang_rewrite.v b/test-suite/ssr/bang_rewrite.v new file mode 100644 index 0000000000..30e6d57a7a --- /dev/null +++ b/test-suite/ssr/bang_rewrite.v @@ -0,0 +1,13 @@ +Set Universe Polymorphism. + +Require Import ssreflect. + +Axiom mult@{i} : nat -> nat -> nat. +Notation "m * n" := (mult m n). + +Axiom multA : forall a b c, (a * b) * c = a * (b * c). + +(* Previously the following gave a universe error: *) + +Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)). +Proof. by rewrite !multA. Qed. diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v index 026f7538e8..f85791b00b 100644 --- a/test-suite/ssr/congr.v +++ b/test-suite/ssr/congr.v @@ -32,3 +32,11 @@ Coercion f : nat >-> Equality.sort. Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a). Proof. move=> a b Eba; congr (_ + _); exact: Eba. Qed. + +Open Scope type_scope. + +Lemma test5 : forall (P Q Q' : Type) (h : Q = Q'), P * Q = P * Q'. +Proof. move=>*; by congr (_ * _). Qed. + +Lemma test6 : forall (P Q Q' : Type) (h : Q = Q'), P * Q -> P * Q'. +Proof. move=> P Q Q' h; by congr (_ * _). Qed. diff --git a/test-suite/success/RewriteRegisteredElim.v b/test-suite/success/RewriteRegisteredElim.v new file mode 100644 index 0000000000..39b103747c --- /dev/null +++ b/test-suite/success/RewriteRegisteredElim.v @@ -0,0 +1,35 @@ + +Set Universe Polymorphism. + +Cumulative Inductive EQ {A} (x : A) : A -> Type + := EQ_refl : EQ x x. + +Register EQ as core.eq.type. + +Lemma renamed_EQ_rect {A} (x:A) (P : A -> Type) + (c : P x) (y : A) (e : EQ x y) : P y. +Proof. destruct e. assumption. Qed. + +Register renamed_EQ_rect as core.eq.rect. +Register renamed_EQ_rect as core.eq.ind. + +Lemma renamed_EQ_rect_r {A} (x:A) (P : A -> Type) + (c : P x) (y : A) (e : EQ y x) : P y. +Proof. destruct e. assumption. Qed. + +Register renamed_EQ_rect_r as core.eq.rect_r. +Register renamed_EQ_rect_r as core.eq.ind_r. + +Lemma EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x. +Proof. rewrite e. reflexivity. Qed. + +Lemma EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x. +Proof. rewrite <- e. reflexivity. Qed. + +Require Import ssreflect. + +Lemma ssr_EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x. +Proof. rewrite e. reflexivity. Qed. + +Lemma ssr_EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x. +Proof. rewrite -e. reflexivity. Qed. diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index cfc25c3346..656362b8fc 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -46,3 +46,129 @@ Module No. Definition j_lebox (A:Type@{j}) := Box A. Fail Definition box_lti A := Box A : Type@{i}. End No. + +Module DefaultProp. + Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a. + + (* By default template polymorphism does not interact with inductives + which naturally fall in Prop *) + Check (identity nat 0 0 : Prop). +End DefaultProp. + +Module ExplicitTemplate. + #[universes(template)] + Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a. + + (* Weird interaction of template polymorphism and inductive types + which naturally fall in Prop: this one is template polymorphic but not on i: + it just lives in any universe *) + Check (identity Type nat nat : Prop). +End ExplicitTemplate. + +Polymorphic Definition f@{i} : Type@{i} := nat. +Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x. + +Section Foo. + Universe u. + Context (A : Type@{u}). + + Inductive Bar := + | bar : A -> Bar. + + Set Universe Minimization ToSet. + Inductive Baz := + | cbaz : A -> baz Baz -> Baz. + + Inductive Baz' := + | cbaz' : A -> baz@{Set} nat -> Baz'. + + (* 2 constructors, at least in Set *) + Inductive Bazset@{v} := + | cbaz1 : A -> baz@{v} Bazset -> Bazset + | cbaz2 : Bazset. + + Eval compute in ltac:(let T := type of A in exact T). + + Inductive Foo : Type := + | foo : A -> f -> Foo. + +End Foo. + +Set Printing Universes. +(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *) +Fail Check Bar True : Prop. +Fail Check Bar nat : Set. +About Baz. + +Check cbaz True I. + +(** Neither can it be Set *) +Fail Check Baz nat : Set. + +(** No longer possible for Baz' which contains a type in Set *) +Fail Check Baz' True : Prop. +Fail Check Baz' nat : Set. + +Fail Check Bazset True : Prop. +Fail Check Bazset True : Set. + +(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *) +Constraint u = Bazset.v. +(** As u is global it is already > Set, so: *) +Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}. + +(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *) +Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X. + +(** Would otherwise break singleton elimination and extraction. *) +Fail Check Foo True : Prop. +Fail Check Foo True : Set. + +Definition foo_proj {A} (f : Foo A) : nat := + match f with foo _ _ n => n end. + +Definition ex : Foo True := foo _ I 0. +Check foo_proj ex. + +(** See failure/Template.v for a test of the unsafe Unset Template Check usage *) + +Module AutoTemplateTest. +Set Warnings "+auto-template". +Section Foo. + Universe u'. + Context (A : Type@{u'}). + + (* Not failing as Bar cannot be made template polymorphic at all *) + Inductive Bar := + | bar : A -> Bar. +End Foo. +End AutoTemplateTest. + +Module TestTemplateAttribute. + Section Foo. + Universe u. + Context (A : Type@{u}). + + (* Failing as Bar cannot be made template polymorphic at all *) + Fail #[universes(template)] Inductive Bar := + | bar : A -> Bar. + + End Foo. +End TestTemplateAttribute. + +Module SharingWithoutSection. +Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty)) + := foo : S A -> Foo A. +Fail Check Foo True : Prop. +End SharingWithoutSection. + +Module OkNotCovered. +(* Here it happens that box is safe but we don't see it *) +Section S. +Universe u. +Variable A : Type@{u}. +Inductive box (A:Type@{u}) := Box : A -> box A. +Definition B := Set : Type@{u}. +End S. +Fail Check box True : Prop. +End OkNotCovered. diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v new file mode 100644 index 0000000000..bd20d9c804 --- /dev/null +++ b/test-suite/success/typing_flags.v @@ -0,0 +1,43 @@ + +Print Typing Flags. +Unset Guard Checking. +Fixpoint f' (n : nat) : nat := f' n. + +Fixpoint f (n : nat) : nat. +Proof. + exact (f n). +Defined. + +Fixpoint bla (A:Type) (n:nat) := match n with 0 =>0 | S n => n end. + +Print Typing Flags. + +Set Guard Checking. + +Print Assumptions f. + +Unset Universe Checking. + +Definition T := Type. +Fixpoint g (n : nat) : T := T. + +Print Typing Flags. +Set Universe Checking. + +Fail Definition g2 (n : nat) : T := T. + +Fail Definition e := fix e (n : nat) : nat := e n. + +Unset Positivity Checking. + +Inductive Cor := +| Over : Cor +| Next : ((Cor -> list nat) -> list nat) -> Cor. + +Set Positivity Checking. +Print Assumptions Cor. + +Inductive Box := +| box : forall n, f n = n -> g 2 -> Box. + +Print Assumptions Box. |