diff options
Diffstat (limited to 'test-suite/modules')
29 files changed, 1146 insertions, 0 deletions
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v new file mode 100644 index 0000000000..820fda172a --- /dev/null +++ b/test-suite/modules/Demo.v @@ -0,0 +1,55 @@ +Module M. + Definition t := nat. + Definition x := 0. +End M. + +Print M.t. + + +Module Type SIG. + Parameter t : Set. + Parameter x : t. +End SIG. + + +Module F (X: SIG). + Definition t := X.t -> X.t. + Definition x : t. + intro. + exact X.x. + Defined. + Definition y := X.x. +End F. + + +Module N := F M. + +Print N.t. +Eval compute in N.t. + + +Module N' : SIG := N. + +Print N'.t. +Eval compute in N'.t. + + +Module N'' <: SIG := F N. + +Print N''.t. +Eval compute in N''.t. + +Eval compute in N''.x. + + +Module N''' : SIG with Definition t := nat -> nat := N. + +Print N'''.t. +Eval compute in N'''.t. + +Print N'''.x. + + +Import N'''. + +Print t. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v new file mode 100644 index 0000000000..95daa1bb0c --- /dev/null +++ b/test-suite/modules/Nat.v @@ -0,0 +1,19 @@ +Definition T := nat. + +Definition le := le. + +Hint Unfold le : core. + +Lemma le_refl : forall n : nat, le n n. + auto. +Qed. + +Require Import Le. + +Lemma le_trans : forall n m k : nat, le n m -> le m k -> le n k. + eauto with arith. +Qed. + +Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m. + eauto with arith. +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v new file mode 100644 index 0000000000..be33104918 --- /dev/null +++ b/test-suite/modules/PO.v @@ -0,0 +1,57 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Arguments fst : default implicits. +Arguments snd : default implicits. + +Module Type PO. + Parameter T : Set. + Parameter le : T -> T -> Prop. + + Axiom le_refl : forall x : T, le x x. + Axiom le_trans : forall x y z : T, le x y -> le y z -> le x z. + Axiom le_antis : forall x y : T, le x y -> le y x -> x = y. + + Hint Resolve le_refl le_trans le_antis. +End PO. + + +Module Pair (X: PO) (Y: PO) <: PO. + Definition T := (X.T * Y.T)%type. + Definition le p1 p2 := X.le (fst p1) (fst p2) /\ Y.le (snd p1) (snd p2). + + Hint Unfold le. + + Lemma le_refl : forall p : T, le p p. + info auto. + Qed. + + Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. + unfold le; intuition; info eauto. + Qed. + + Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. + destruct p1. + destruct p2. + unfold le. + intuition. + cutrewrite (t = t1). + cutrewrite (t0 = t2). + reflexivity. + + info auto. + + info auto. + Qed. + +End Pair. + + + +Require Nat. + +Module NN := Pair Nat Nat. + +Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. + info auto with arith. +Qed. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v new file mode 100644 index 0000000000..ece1b47b4f --- /dev/null +++ b/test-suite/modules/Przyklad.v @@ -0,0 +1,187 @@ +Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) + (th el : T) := if s then th else el. + +Arguments ifte : default implicits. + +Lemma Reflexivity_provable : + forall (A : Set) (a : A) (s : {a = a} + {a <> a}), + exists x : _, s = left _ x. +intros. +elim s. +intro x. +split with x; reflexivity. + +intro. + absurd (a = a); auto. + +Qed. + +Lemma Disequality_provable : + forall (A : Set) (a b : A), + a <> b -> forall s : {a = b} + {a <> b}, exists x : _, s = right _ x. +intros. +elim s. +intro. + absurd (a = a); auto. + +intro. +split with b0; reflexivity. + +Qed. + +Module Type ELEM. + Parameter T : Set. + Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}. +End ELEM. + +Module Type SET (Elt: ELEM). + Parameter T : Set. + Parameter empty : T. + Parameter add : Elt.T -> T -> T. + Parameter find : Elt.T -> T -> bool. + + (* Axioms *) + + Axiom find_empty_false : forall e : Elt.T, find e empty = false. + + Axiom find_add_true : forall (s : T) (e : Elt.T), find e (add e s) = true. + + Axiom + find_add_false : + forall (s : T) (e e' : Elt.T), e <> e' -> find e (add e' s) = find e s. + +End SET. + +Module FuncDict (E: ELEM). + Definition T := E.T -> bool. + Definition empty (e' : E.T) := false. + Definition find (e' : E.T) (s : T) := s e'. + Definition add (e : E.T) (s : T) (e' : E.T) := + ifte (E.eq_dec e e') true (find e' s). + + Lemma find_empty_false : forall e : E.T, find e empty = false. + auto. + Qed. + + Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. + + intros. + unfold find, add. + elim (Reflexivity_provable _ _ (E.eq_dec e e)). + intros. + rewrite H. + auto. + + Qed. + + Lemma find_add_false : + forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. + intros. + unfold add, find. + cut (exists x : _, E.eq_dec e' e = right _ x). + intros. + elim H0. + intros. + rewrite H1. + unfold ifte. + reflexivity. + + apply Disequality_provable. + auto. + + Qed. + +End FuncDict. + +Module F : SET := FuncDict. + + +Module Nat. + Definition T := nat. + Lemma eq_dec : forall a a' : T, {a = a'} + {a <> a'}. + decide equality. + Qed. +End Nat. + + +Module SetNat := F Nat. + + +Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. +apply SetNat.find_empty_false. +Qed. + +(***************************************************************************) +Module Lemmas (G: SET) (E: ELEM). + + Module ESet := G E. + + Lemma commute : + forall (S : ESet.T) (a1 a2 : E.T), + let S1 := ESet.add a1 (ESet.add a2 S) in + let S2 := ESet.add a2 (ESet.add a1 S) in + forall a : E.T, ESet.find a S1 = ESet.find a S2. + + intros. + unfold S1, S2. + elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2; + try rewrite <- H1; try rewrite <- H2; + repeat + (try ( rewrite ESet.find_add_true; auto); + try ( rewrite ESet.find_add_false; auto); auto). + Qed. +End Lemmas. + + +Inductive list (A : Set) : Set := + | nil : list A + | cons : A -> list A -> list A. + +Module ListDict (E: ELEM). + Definition T := list E.T. + Definition elt := E.T. + + Definition empty := nil elt. + Definition add (e : elt) (s : T) := cons elt e s. + Fixpoint find (e : elt) (s : T) {struct s} : bool := + match s with + | nil _ => false + | cons _ e' s' => ifte (E.eq_dec e e') true (find e s') + end. + + Definition find_empty_false (e : elt) := refl_equal false. + + Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. + intros. + simpl. + elim (Reflexivity_provable _ _ (E.eq_dec e e)). + intros. + rewrite H. + auto. + + Qed. + + + Lemma find_add_false : + forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. + intros. + simpl. + elim (Disequality_provable _ _ _ H (E.eq_dec e e')). + intros. + rewrite H0. + simpl. + reflexivity. + Qed. + + +End ListDict. + + +Module L : SET := ListDict. + + + + + + + diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v new file mode 100644 index 0000000000..4426f2710a --- /dev/null +++ b/test-suite/modules/SeveralWith.v @@ -0,0 +1,13 @@ +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). +End Make. diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v new file mode 100644 index 0000000000..ea49553942 --- /dev/null +++ b/test-suite/modules/Tescik.v @@ -0,0 +1,30 @@ + +Module Type ELEM. + Parameter A : Set. + Parameter x : A. +End ELEM. + +Module Nat. + Definition A := nat. + Definition x := 0. +End Nat. + +Module List (X: ELEM). + Inductive list : Set := + | nil : list + | cons : X.A -> list -> list. + + Definition head (l : list) := match l with + | nil => X.x + | cons x _ => x + end. + + Definition singl (x : X.A) := cons x nil. + + Lemma head_singl : forall x : X.A, head (singl x) = x. + auto. + Qed. + +End List. + +Module N := List Nat. diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v new file mode 100644 index 0000000000..00a93b5fdf --- /dev/null +++ b/test-suite/modules/WithDefUBinders.v @@ -0,0 +1,17 @@ + +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. +Definition foo := let t := Type in t. +End M'. diff --git a/test-suite/modules/cumpoly.v b/test-suite/modules/cumpoly.v new file mode 100644 index 0000000000..654b86cb44 --- /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/errors.v b/test-suite/modules/errors.v new file mode 100644 index 0000000000..487de5801c --- /dev/null +++ b/test-suite/modules/errors.v @@ -0,0 +1,90 @@ +(* coq-prog-args: ("-impredicative-set") *) +(* Inductive mismatches *) + +Module Type SA. Inductive TA : nat -> Prop := CA : nat -> TA 0. End SA. +Module MA : SA. Inductive TA : Prop := CA : bool -> TA. Fail End MA. +Reset Initial. + +Module Type SA0. Inductive TA0 := CA0 : nat -> TA0. End SA0. +Module MA0 : SA0. Inductive TA0 := CA0 : bool -> TA0. Fail End MA0. +Reset Initial. + +Module Type SA1. Inductive TA1 := CA1 : nat -> TA1. End SA1. +Module MA1 : SA1. Inductive TA1 := CA1 : bool -> nat -> TA1. Fail End MA1. +Reset Initial. + +Module Type SA2. Inductive TA2 := CA2 : nat -> TA2. End SA2. +Module MA2 : SA2. Inductive TA2 := CA2 : nat -> TA2 | DA2 : TA2. Fail End MA2. +Reset Initial. + +Module Type SA3. Inductive TA3 := CA3 : nat -> TA3. End SA3. +Module MA3 : SA3. Inductive TA3 := CA3 : nat -> TA3 with UA3 := DA3. Fail End MA3. +Reset Initial. + +Module Type SA4. Inductive TA4 := CA4 : nat -> TA4 with UA4 := DA4. End SA4. +Module MA4 : SA4. Inductive TA4 := CA4 : nat -> TA4 with VA4 := DA4. Fail End MA4. +Reset Initial. + +Module Type SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := DA5. End SA5. +Module MA5 : SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := EA5. Fail End MA5. +Reset Initial. + +Module Type SA6. Inductive TA6 (A:Type) := CA6 : A -> TA6 A. End SA6. +Module MA6 : SA6. Inductive TA6 (A B:Type):= CA6 : A -> TA6 A B. Fail End MA6. +Reset Initial. + +Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7. +Module MA7 : SA7. CoInductive TA7 (A:Type):= CA7 : A -> TA7 A. Fail End MA7. +Reset Initial. + +Module Type SA8. CoInductive TA8 (A:Type) := CA8 : A -> TA8 A. End SA8. +Module MA8 : SA8. Inductive TA8 (A:Type):= CA8 : A -> TA8 A. Fail End MA8. +Reset Initial. + +Module Type SA9. Record TA9 (A:Type) := { CA9 : A }. End SA9. +Module MA9 : SA9. Inductive TA9 (A:Type):= CA9 : A -> TA9 A. Fail End MA9. +Reset Initial. + +Module Type SA10. Inductive TA10 (A:Type) := CA10 : A -> TA10 A. End SA10. +Module MA10 : SA10. Record TA10 (A:Type):= { CA10 : A }. Fail End MA10. +Reset Initial. + +Module Type SA11. Record TA11 (A:Type):= { CA11 : A }. End SA11. +Module MA11 : SA11. Record TA11 (A:Type):= { DA11 : A }. Fail End MA11. +Reset Initial. + +(* Basic mismatches *) +Module Type SB. Inductive TB := CB : nat -> TB. End SB. +Module MB : SB. Module Type TB. End TB. Fail End MB. +Inductive TB := CB : nat -> TB. End MB. + +Module Type SC. Module Type TC. End TC. End SC. +Module MC : SC. Inductive TC := CC : nat -> TC. Fail End MC. +Reset Initial. + +Module Type SD. Module TD. End TD. End SD. +Module MD : SD. Inductive TD := DD : nat -> TD. Fail End MD. +Reset Initial. + +Module Type SE. Definition DE := nat. End SE. +Module ME : SE. Definition DE := bool. Fail End ME. +Reset Initial. + +Module Type SF. Parameter DF : nat. End SF. +Module MF : SF. Definition DF := bool. Fail End MF. +Reset Initial. + +(* Needs a type constraint in module type *) +Module Type SG. Definition DG := Type. End SG. +Module MG : SG. Definition DG := Type : Type. Fail End MG. +Reset Initial. + +(* Should work *) +Module Type SA70. Inductive TA70 (A:Type) := CA70 : A -> TA70 A. End SA70. +Module MA70 : SA70. Inductive TA70 (B:Type):= CA70 : B -> TA70 B. End MA70. + +Module Type SA12. Record TA12 (B:Type):= { CA12 : B }. End SA12. +Module MA12 : SA12. Record TA12 (A:Type):= { CA12 : A }. End MA12. + +Module Type SH. Parameter DH : Type. End SH. +Module MH : SH. Definition DH := Type : Type. End MH. diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v new file mode 100644 index 0000000000..fe1372298e --- /dev/null +++ b/test-suite/modules/fun_objects.v @@ -0,0 +1,33 @@ +(* coq-prog-args: ("-impredicative-set") *) +Set Implicit Arguments. +Unset Strict Implicit. + +Module Type SIG. + Parameter id : forall A : Set, A -> A. +End SIG. + +Module M (X: SIG). + Definition idid := X.id X.id. + Definition id := idid X.id. +End M. + +Module N := M. + +Module Nat. + Definition T := nat. + Definition x := 0. + Definition id (A : Set) (x : A) := x. +End Nat. + +Module Z := N Nat. + +Check (Z.idid 0). + +Module P (Y: SIG) := N. + +Module Y := P Nat Z. + +Check (Y.id 0). + + + diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v new file mode 100644 index 0000000000..11ad205e40 --- /dev/null +++ b/test-suite/modules/grammar.v @@ -0,0 +1,15 @@ +Module N. +Definition f := plus. +(* <Warning> : Syntax is discontinued *) +Check (f 0 0). +End N. +Check (N.f 0 0). +Import N. +Check (f 0 0). +Check (f 0 0). +Module M := N. +Check (f 0 0). +Check (f 0 0). +Import M. +Check (f 0 0). +Check (N.f 0 0). diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v new file mode 100644 index 0000000000..3af94c3b91 --- /dev/null +++ b/test-suite/modules/ind.v @@ -0,0 +1,49 @@ +Module Type SIG. + Inductive w : Set := + A : w. + Parameter f : w -> w. +End SIG. + +Module M : SIG. + Inductive w : Set := + A : w. + Definition f x := match x with + | A => A + end. +End M. + +Module N := M. + +Check (N.f M.A). + +(* Check use of equivalence on inductive types (bug #1242) *) + + Module Type ASIG. + Inductive t : Set := a | b : t. + Definition f := fun x => match x with a => true | b => false end. + End ASIG. + + Module Type BSIG. + Declare Module A : ASIG. + Definition f := fun x => match x with A.a => true | A.b => false end. + End BSIG. + + Module C (A : ASIG) (B : BSIG with Module A:=A). + + (* Check equivalence is considered in "case_info" *) + Lemma test : forall x, A.f x = B.f x. + intro x. unfold B.f, A.f. + destruct x; reflexivity. + Qed. + + (* Check equivalence is considered in pattern-matching *) + Definition f (x : A.t) := match x with B.A.a => true | B.A.b => false end. + + End C. + +(* Check subtyping of the context of parameters of the inductive types *) +(* Only the number of expected uniform parameters and the convertibility *) +(* of the inductive arities and constructors types are checked *) + +Module Type S. Inductive I (x:=0) (y:nat): Set := c: x=y -> I y. End S. +Module P : S. Inductive I (y':nat) (z:=y'): Set := c : 0=y' -> I y'. End P. diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v new file mode 100644 index 0000000000..8b5969dd76 --- /dev/null +++ b/test-suite/modules/injection_discriminate_inversion.v @@ -0,0 +1,34 @@ +Module M. + Inductive I : Set := C : nat -> I. +End M. + +Module M1 := M. + + +Goal forall x, M.C x = M1.C 0 -> x = 0 . + intros x H. + (* + injection sur deux constructeurs egaux mais appeles + par des modules differents + *) + injection H. + tauto. +Qed. + +Goal M.C 0 <> M1.C 1. + (* + Discriminate sur deux constructeurs egaux mais appeles + par des modules differents + *) + intro H;discriminate H. +Qed. + + +Goal forall x, M.C x = M1.C 0 -> x = 0. + intros x H. + (* + inversion sur deux constructeurs egaux mais appeles + par des modules differents + *) + inversion H. reflexivity. +Qed. diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v new file mode 100644 index 0000000000..8b40213a48 --- /dev/null +++ b/test-suite/modules/mod_decl.v @@ -0,0 +1,49 @@ +Module Type SIG. + Axiom A : Set. +End SIG. + +Module M0. + Definition A : Set. + exact nat. + Qed. +End M0. + +Module M1 : SIG. + Definition A := nat. +End M1. + +Module M2 <: SIG. + Definition A := nat. +End M2. + +Module M3 := M0. + +Module M4 : SIG := M0. + +Module M5 <: SIG := M0. + + +Module F (X: SIG) := X. + + +Module Type T. + + Module M0. + Axiom A : Set. + End M0. + + Declare Module M1: SIG. + + Module M2 <: SIG. + Definition A := nat. + End M2. + + Module M3 := M0. + + Module M4 : SIG := M0. + + Module M5 <: SIG := M0. + + Module M6 := F M0. + +End T. diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v new file mode 100644 index 0000000000..4ebcae82e5 --- /dev/null +++ b/test-suite/modules/modeq.v @@ -0,0 +1,23 @@ +(* coq-prog-args: ("-top" "modeq") *) +Module M. + Definition T := nat. + Definition x : T := 0. +End M. + +Module Type SIG. + Module M := modeq.M. + Module Type SIG. + Parameter T : Set. + End SIG. + Declare Module N: SIG. +End SIG. + +Module Z. + Module M := modeq.M. + Module Type SIG. + Parameter T : Set. + End SIG. + Module N := M. +End Z. + +Module A : SIG := Z. diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v new file mode 100644 index 0000000000..9b3772b0d9 --- /dev/null +++ b/test-suite/modules/modul.v @@ -0,0 +1,36 @@ +(* coq-prog-args: ("-top" "modul") *) +Module M. + Parameter rel : nat -> nat -> Prop. + + Axiom w : forall n : nat, rel 0 (S n). + + Hint Resolve w. + + (* <Warning> : Grammar is replaced by Notation *) + + Print Hint *. + + Lemma w1 : rel 0 1. + auto. + Qed. + +End M. + +Locate Module M. + +(*Lemma w1 : (M.rel O (S O)). +Auto. +*) + +Import M. + +Lemma w1 : rel 0 1. +auto. +Qed. + +Check (rel 0 0). +Locate rel. + +Locate Module M. + +Module N := modul.M. diff --git a/test-suite/modules/nested_mod_types.v b/test-suite/modules/nested_mod_types.v new file mode 100644 index 0000000000..f459f9ec38 --- /dev/null +++ b/test-suite/modules/nested_mod_types.v @@ -0,0 +1,26 @@ +Module Type T. + Module Type U. + Module Type V. + Variable b : nat. + End V. + Variable a : nat. + End U. + Declare Module u : U. + Declare Module v : u.V. +End T. + +Module F (t:T). +End F. + +Module M:T. + Module Type U. + Module Type V. + Variable b : nat. + End V. + Variable a : nat. + End U. + Declare Module u : U. + Declare Module v : u.V. +End M. + +Module FM := F M. diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v new file mode 100644 index 0000000000..fda1a074ae --- /dev/null +++ b/test-suite/modules/obj.v @@ -0,0 +1,26 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Module M. + Definition a (s : Set) := s. + Print a. +End M. + +Print M.a. + +Module K. + Definition app (A B : Set) (f : A -> B) (x : A) := f x. + Module N. + Definition apap (A B : Set) := app (app (A:=A) (B:=B)). + Print app. + Print apap. + End N. + Print N.apap. +End K. + +Print K.app. +Print K.N.apap. + +Module W := K.N. + +Print W.apap. diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v new file mode 100644 index 0000000000..d3a4c0b055 --- /dev/null +++ b/test-suite/modules/objects.v @@ -0,0 +1,33 @@ +Module Type SET. + Axiom T : Set. + Axiom x : T. +End SET. + +Set Implicit Arguments. +Unset Strict Implicit. + +Module M (X: SET). + Definition T := nat. + Definition x := 0. + Definition f (A : Set) (x : A) := X.x. +End M. + +Module N := M. + +Module Nat. + Definition T := nat. + Definition x := 0. +End Nat. + +Module Z := N Nat. + +Check (Z.f 0). + +Module P (Y: SET) := N. + +Module Y := P Z Nat. + +Check (Y.f 0). + + + diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v new file mode 100644 index 0000000000..0a6b1f06de --- /dev/null +++ b/test-suite/modules/objects2.v @@ -0,0 +1,11 @@ +(* Check that non logical object loading is done after registration of + the logical objects in the environment +*) + +(* 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) +*) + +Module Type S. Record t : Set := { a : nat; b : nat }. End S. +Module Make (X:S). Module Y:=X. End Make. diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v new file mode 100644 index 0000000000..51f5f40078 --- /dev/null +++ b/test-suite/modules/pliczek.v @@ -0,0 +1,3 @@ +Require Export plik. + +Definition tutu (X : Set) := toto X. diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v new file mode 100644 index 0000000000..c2f0fe3cee --- /dev/null +++ b/test-suite/modules/plik.v @@ -0,0 +1,3 @@ +Definition toto (x : Set) := x. + +(* <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 0000000000..63eaa382dc --- /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 0000000000..7e3327eee0 --- /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 new file mode 100644 index 0000000000..6bf067fd18 --- /dev/null +++ b/test-suite/modules/pseudo_circular_with.v @@ -0,0 +1,6 @@ +Module Type S. End S. +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. diff --git a/test-suite/modules/resolver.v b/test-suite/modules/resolver.v new file mode 100644 index 0000000000..dcfcc98d58 --- /dev/null +++ b/test-suite/modules/resolver.v @@ -0,0 +1,37 @@ +Module Type TA. +Parameter t : Set. +End TA. + +Module Type TB. +Declare Module A: TA. +End TB. + +Module Type TC. +Declare Module B : TB. +End TC. + +Module Type TD. + +Declare Module B: TB . +Declare Module C: TC + with Module B := B . +End TD. + +Module Type TE. +Declare Module D : TD. +End TE. + +Module Type TF. +Declare Module E: TE. +End TF. + +Module G (D: TD). +Module B' := D.C.B. +End G. + +Module H (F: TF). +Module I := G(F.E.D). +End H. + +Declare Module F: TF. +Module K := H(F). diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v new file mode 100644 index 0000000000..fc936a515a --- /dev/null +++ b/test-suite/modules/sig.v @@ -0,0 +1,29 @@ +Module M. + Module Type SIG. + Parameter T : Set. + Parameter x : T. + End SIG. + Module N : SIG. + Definition T := nat. + Definition x := 0. + End N. +End M. + +Module N := M. + +Module Type SPRYT. + Module N. + Definition T := M.N.T. + Parameter x : T. + End N. +End SPRYT. + +Module K : SPRYT := N. +Module K' : SPRYT := M. + +Module Type SIG. + Definition T : Set := M.N.T. + Parameter x : T. +End SIG. + +Module J : SIG := M.N. diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v new file mode 100644 index 0000000000..fdfd09f802 --- /dev/null +++ b/test-suite/modules/sub_objects.v @@ -0,0 +1,32 @@ +Set Implicit Arguments. +Unset Strict Implicit. + + +Module M. + Definition id (A : Set) (x : A) := x. + + Module Type SIG. + Parameter idid : forall A : Set, A -> A. + End SIG. + + Module N. + Definition idid (A : Set) (x : A) := id x. + (* <Warning> : Grammar is replaced by Notation *) + Notation inc := (plus 1). + End N. + + Definition zero := N.idid 0. + +End M. + +Definition zero := M.N.idid 0. +Definition jeden := M.N.inc 0. + +Module Goly := M.N. + +Definition Gole_zero := Goly.idid 0. +Definition Goly_jeden := Goly.inc 0. + +Module Ubrany : M.SIG := M.N. + +Definition Ubrane_zero := Ubrany.idid 0. diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v new file mode 100644 index 0000000000..dd7daf429d --- /dev/null +++ b/test-suite/modules/subtyping.v @@ -0,0 +1,46 @@ +(* Non regression for bug #1302 *) + +(* With universe polymorphism for inductive types, subtyping of + inductive types needs a special treatment: the standard conversion + algorithm does not work as it only knows to deal with constraints of + the form alpha = beta or max(alphas, alphas+1) <= beta, while + subtyping of inductive types in Type generates constraints of the form + max(alphas, alphas+1) <= max(betas, betas+1). + + These constraints are anyway valid by monotonicity of subtyping but we + have to detect it early enough to avoid breaking the standard + algorithm for constraints on algebraic universes. *) + +Module Type T. + + Parameter A : Type (* Top.1 *) . + + Inductive L : Type (* max(Top.1,1) *) := + | L0 + | L1 : (A -> Prop) -> L. + +End T. + +Axiom Tp : Type (* Top.5 *) . + +Module TT : T. + + Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *) + + Inductive L : Type (* max(Top.6,1) *) := + | L0 + | L1 : (A -> Prop) -> L. + +End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *) + +(* Note: Top.6 <= Top.1 is generated by subtyping on A; + subtyping of L follows and has not to be checked *) + + + +(* The same bug as #1302 but for Definition *) +(* Check that inferred algebraic universes in interfaces are considered *) + +Module Type U. Definition A := Type -> Type. End U. +Module M:U. Definition A := Type -> Type. End M. + |