diff options
Diffstat (limited to 'test-suite/modules')
-rw-r--r-- | test-suite/modules/Demo.v | 2 | ||||
-rw-r--r-- | test-suite/modules/Nat.v | 2 | ||||
-rw-r--r-- | test-suite/modules/PO.v | 2 | ||||
-rw-r--r-- | test-suite/modules/SeveralWith.v | 12 | ||||
-rw-r--r-- | test-suite/modules/Tescik.v | 2 | ||||
-rw-r--r-- | test-suite/modules/WithDefUBinders.v | 15 | ||||
-rw-r--r-- | test-suite/modules/cumpoly.v | 19 | ||||
-rw-r--r-- | test-suite/modules/grammar.v | 2 | ||||
-rw-r--r-- | test-suite/modules/injection_discriminate_inversion.v | 2 | ||||
-rw-r--r-- | test-suite/modules/modeq.v | 2 | ||||
-rw-r--r-- | test-suite/modules/objects2.v | 2 | ||||
-rw-r--r-- | test-suite/modules/pliczek.v | 2 | ||||
-rw-r--r-- | test-suite/modules/plik.v | 2 | ||||
-rw-r--r-- | test-suite/modules/polymorphism.v | 81 | ||||
-rw-r--r-- | test-suite/modules/polymorphism2.v | 87 | ||||
-rw-r--r-- | test-suite/modules/pseudo_circular_with.v | 2 | ||||
-rw-r--r-- | test-suite/modules/sig.v | 2 |
17 files changed, 226 insertions, 12 deletions
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v index 1f27fe1b..820fda17 100644 --- a/test-suite/modules/Demo.v +++ b/test-suite/modules/Demo.v @@ -52,4 +52,4 @@ Print N'''.x. Import N'''. -Print t.
\ No newline at end of file +Print t. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index 57878a5f..d2116d21 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -16,4 +16,4 @@ Qed. Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m. eauto with arith. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 6198f29a..8ba8525c 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -54,4 +54,4 @@ Module NN := Pair Nat Nat. Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. info auto with arith. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v new file mode 100644 index 00000000..bbf72a76 --- /dev/null +++ b/test-suite/modules/SeveralWith.v @@ -0,0 +1,12 @@ +Module Type S. +Parameter A : Type. +End S. + +Module Type ES. +Parameter A : Type. +Parameter eq : A -> A -> Type. +End ES. + +Module Make + (AX : S) + (X : ES with Definition A := AX.A with Definition eq := @eq AX.A). diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v index 1d1b1e0a..ea495539 100644 --- a/test-suite/modules/Tescik.v +++ b/test-suite/modules/Tescik.v @@ -27,4 +27,4 @@ Module List (X: ELEM). End List. -Module N := List Nat.
\ No newline at end of file +Module N := List Nat. diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v new file mode 100644 index 00000000..e6834551 --- /dev/null +++ b/test-suite/modules/WithDefUBinders.v @@ -0,0 +1,15 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo@{u v|u < v} : Type@{v}. +End T. + +Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}. + Definition foo@{u v} := Type@{u} : Type@{v}. +End M. + +Fail Module M' : T with Definition foo := Type. + +(* Without the binder expression we have to do trickery to get the + universes in the right order. *) +Module M' : T with Definition foo := let t := Type in t. diff --git a/test-suite/modules/cumpoly.v b/test-suite/modules/cumpoly.v new file mode 100644 index 00000000..654b86cb --- /dev/null +++ b/test-suite/modules/cumpoly.v @@ -0,0 +1,19 @@ +Set Universe Polymorphism. + +(** Check that variance subtyping is respected. The signature T is asking for + invariance, while M provide an irrelevant implementation, which is deemed + legit. + + There is currently no way to go the other way around, so it's not possible + to generate a counter-example that should fail with the wrong subtyping. +*) + +Module Type T. +Parameter t@{i|Set <= i} : Type@{i}. +Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I. +End T. + +Module M : T. +Definition t@{i|Set <= i} : Type@{i} := nat. +Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I. +End M. diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v index 9657c685..11ad205e 100644 --- a/test-suite/modules/grammar.v +++ b/test-suite/modules/grammar.v @@ -12,4 +12,4 @@ Check (f 0 0). Check (f 0 0). Import M. Check (f 0 0). -Check (N.f 0 0).
\ No newline at end of file +Check (N.f 0 0). diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v index d4ac7b3a..8b5969dd 100644 --- a/test-suite/modules/injection_discriminate_inversion.v +++ b/test-suite/modules/injection_discriminate_inversion.v @@ -31,4 +31,4 @@ Goal forall x, M.C x = M1.C 0 -> x = 0. par des modules differents *) inversion H. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v index 1238ee9d..c8129eec 100644 --- a/test-suite/modules/modeq.v +++ b/test-suite/modules/modeq.v @@ -19,4 +19,4 @@ Module Z. Module N := M. End Z. -Module A : SIG := Z.
\ No newline at end of file +Module A : SIG := Z. diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v index 220e2b36..0a6b1f06 100644 --- a/test-suite/modules/objects2.v +++ b/test-suite/modules/objects2.v @@ -2,7 +2,7 @@ the logical objects in the environment *) -(* Bug #1118 (simplified version), submitted by Evelyne Contejean +(* BZ#1118 (simplified version), submitted by Evelyne Contejean (used to failed in pre-V8.1 trunk because of a call to lookup_mind for structure objects) *) diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v index f806a7c4..51f5f400 100644 --- a/test-suite/modules/pliczek.v +++ b/test-suite/modules/pliczek.v @@ -1,3 +1,3 @@ Require Export plik. -Definition tutu (X : Set) := toto X.
\ No newline at end of file +Definition tutu (X : Set) := toto X. diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v index 50bfd960..c2f0fe3c 100644 --- a/test-suite/modules/plik.v +++ b/test-suite/modules/plik.v @@ -1,3 +1,3 @@ Definition toto (x : Set) := x. -(* <Warning> : Grammar is replaced by Notation *)
\ No newline at end of file +(* <Warning> : Grammar is replaced by Notation *) diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v new file mode 100644 index 00000000..63eaa382 --- /dev/null +++ b/test-suite/modules/polymorphism.v @@ -0,0 +1,81 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Parameter foo : Type@{i} -> Type@{j}. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Definition foo@{i j} (A : Type@{i}) : Type@{j} := A. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive X@{i} : Type@{i} :=. +Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Definition foo@{i} (A : Type@{i}) : Type@{i} := A. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v new file mode 100644 index 00000000..7e3327ee --- /dev/null +++ b/test-suite/modules/polymorphism2.v @@ -0,0 +1,87 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive foo@{i j} : Type@{i} -> Type@{j} :=. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Inductive foo@{i} : Type@{i} -> Type@{i} :=. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. diff --git a/test-suite/modules/pseudo_circular_with.v b/test-suite/modules/pseudo_circular_with.v index 9e46d17e..6bf067fd 100644 --- a/test-suite/modules/pseudo_circular_with.v +++ b/test-suite/modules/pseudo_circular_with.v @@ -3,4 +3,4 @@ Module Type T. Declare Module M:S. End T. Module N:S. End N. Module NN:T. Module M:=N. End NN. -Module Type U := T with Module M:=NN.
\ No newline at end of file +Module Type U := T with Module M:=NN. diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v index da5d25fa..fc936a51 100644 --- a/test-suite/modules/sig.v +++ b/test-suite/modules/sig.v @@ -26,4 +26,4 @@ Module Type SIG. Parameter x : T. End SIG. -Module J : SIG := M.N.
\ No newline at end of file +Module J : SIG := M.N. |