summaryrefslogtreecommitdiff
path: root/test-suite/modules
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules')
-rw-r--r--test-suite/modules/Demo.v55
-rw-r--r--test-suite/modules/Nametab.v48
-rw-r--r--test-suite/modules/Nat.v19
-rw-r--r--test-suite/modules/PO.v57
-rw-r--r--test-suite/modules/Przyklad.v193
-rw-r--r--test-suite/modules/Tescik.v30
-rw-r--r--test-suite/modules/fun_objects.v32
-rw-r--r--test-suite/modules/grammar.v15
-rw-r--r--test-suite/modules/ind.v13
-rw-r--r--test-suite/modules/mod_decl.v55
-rw-r--r--test-suite/modules/modeq.v22
-rw-r--r--test-suite/modules/modul.v39
-rw-r--r--test-suite/modules/obj.v26
-rw-r--r--test-suite/modules/objects.v33
-rw-r--r--test-suite/modules/pliczek.v3
-rw-r--r--test-suite/modules/plik.v4
-rw-r--r--test-suite/modules/sig.v29
-rw-r--r--test-suite/modules/sub_objects.v33
18 files changed, 706 insertions, 0 deletions
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v
new file mode 100644
index 00000000..1e9273f0
--- /dev/null
+++ b/test-suite/modules/Demo.v
@@ -0,0 +1,55 @@
+Module M.
+ Definition t:=nat.
+ Definition x:=O.
+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. \ No newline at end of file
diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v
new file mode 100644
index 00000000..61966c7c
--- /dev/null
+++ b/test-suite/modules/Nametab.v
@@ -0,0 +1,48 @@
+Module Q.
+ Module N.
+ Module K.
+ Definition id:=Set.
+ End K.
+ End N.
+End Q.
+
+(* Bad *) Locate id.
+(* Bad *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK *) Locate Q.N.K.id.
+(* OK *) Locate Top.Q.N.K.id.
+
+(* Bad *) Locate K.
+(* Bad *) Locate N.K.
+(* OK *) Locate Q.N.K.
+(* OK *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK *) Locate Q.N.
+(* OK *) Locate Top.Q.N.
+
+(* OK *) Locate Q.
+(* OK *) Locate Top.Q.
+
+
+
+Import Q.N.
+
+
+(* Bad *) Locate id.
+(* OK *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK *) Locate Q.N.K.id.
+(* OK *) Locate Top.Q.N.K.id.
+
+(* OK *) Locate K.
+(* Bad *) Locate N.K.
+(* OK *) Locate Q.N.K.
+(* OK *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK *) Locate Q.N.
+(* OK *) Locate Top.Q.N.
+
+(* OK *) Locate Q.
+(* OK *) Locate Top.Q.
diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
new file mode 100644
index 00000000..d3e98ae4
--- /dev/null
+++ b/test-suite/modules/Nat.v
@@ -0,0 +1,19 @@
+Definition T:=nat.
+
+Definition le:=Peano.le.
+
+Hints Unfold le.
+
+Lemma le_refl:(n:nat)(le n n).
+ Auto.
+Qed.
+
+Require Le.
+
+Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
+ EAuto with arith.
+Qed.
+
+Lemma le_antis:(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 00000000..9ba3fb2e
--- /dev/null
+++ b/test-suite/modules/PO.v
@@ -0,0 +1,57 @@
+Implicit Arguments On.
+
+Implicits fst.
+Implicits snd.
+
+Module Type PO.
+ Parameter T:Set.
+ Parameter le:T->T->Prop.
+
+ Axiom le_refl : (x:T)(le x x).
+ Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z).
+ Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y).
+
+ Hints Resolve le_refl le_trans le_antis.
+End PO.
+
+
+Module Pair[X:PO][Y:PO] <: PO.
+ Definition T:=X.T*Y.T.
+ Definition le:=[p1,p2]
+ (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
+
+ Hints Unfold le.
+
+ Lemma le_refl : (p:T)(le p p).
+ Info Auto.
+ Qed.
+
+ Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
+ Unfold le; Intuition; Info EAuto.
+ Qed.
+
+ Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2).
+ NewDestruct p1.
+ NewDestruct p2.
+ Unfold le.
+ Intuition.
+ CutRewrite t=t1.
+ CutRewrite t0=t2.
+ Reflexivity.
+
+ Info Auto.
+
+ Info Auto.
+ Qed.
+
+End Pair.
+
+
+
+Read Module Nat.
+
+Module NN := Pair Nat Nat.
+
+Lemma zz_min : (p:NN.T)(NN.le (O,O) 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 00000000..4f4c2066
--- /dev/null
+++ b/test-suite/modules/Przyklad.v
@@ -0,0 +1,193 @@
+Definition ifte := [T:Set][A:Prop][B:Prop][s:(sumbool A B)][th:T][el:T]
+ if s then [_]th else [_]el.
+
+Implicits ifte.
+
+Lemma Reflexivity_provable :
+ (A:Set)(a:A)(s:{a=a}+{~a=a})(EXT x| s==(left ? ? x)).
+Intros.
+Elim s.
+Intro x.
+Split with x; Reflexivity.
+
+Intro.
+Absurd a=a; Auto.
+
+Save.
+
+Lemma Disequality_provable :
+ (A:Set)(a,b:A)(~a=b)->(s:{a=b}+{~a=b})(EXT x| s==(right ? ? x)).
+Intros.
+Elim s.
+Intro.
+Absurd a=a; Auto.
+
+Intro.
+Split with b0; Reflexivity.
+
+Save.
+
+Module Type ELEM.
+ Parameter T : Set.
+ Parameter eq_dec : (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 :
+ (e:Elt.T) (find e empty) = false.
+
+ Axiom find_add_true :
+ (s:T) (e:Elt.T) (find e (add e s)) = true.
+
+ Axiom find_add_false :
+ (s:T) (e:Elt.T) (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 : (e:E.T) (find e empty) = false.
+ Auto.
+ Qed.
+
+ Lemma find_add_true :
+ (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 :
+ (s:T) (e:E.T) (e':E.T) ~(e=e') ->
+ (find e (add e' s))=(find e s).
+ Intros.
+ Unfold add find.
+ Cut (EXT 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 : (a,a':T){a=a'}+{~ a=a'}.
+ Decide Equality.
+ Qed.
+End Nat.
+
+
+Module SetNat:=F Nat.
+
+
+Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false.
+Apply SetNat.find_empty_false.
+Save.
+
+(***************************************************************************)
+Module Lemmas[G:SET][E:ELEM].
+
+ Module ESet:=G E.
+
+ Lemma commute : (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
+ (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).
+ Save.
+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] : bool :=
+ Cases s of
+ nil => false
+ | (cons e' s') => (ifte (E.eq_dec e e')
+ true
+ (find e s'))
+ end.
+
+ Definition find_empty_false := [e:elt] (refl_equal bool false).
+
+ Lemma find_add_true :
+ (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 :
+ (s:T) (e:E.T) (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.
+ Save.
+
+
+End ListDict.
+
+
+Module L : SET := ListDict.
+
+
+
+
+
+
+
+
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
new file mode 100644
index 00000000..13c28418
--- /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:=O.
+End Nat.
+
+Module List[X:ELEM].
+ Inductive list : Set := nil : list
+ | cons : X.A -> list -> list.
+
+ Definition head :=
+ [l:list]Cases l of
+ nil => X.x
+ | (cons x _) => x
+ end.
+
+ Definition singl := [x:X.A] (cons x nil).
+
+ Lemma head_singl : (x:X.A)(head (singl x))=x.
+ Auto.
+ Qed.
+
+End List.
+
+Module N:=(List Nat).
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
new file mode 100644
index 00000000..0f8eef84
--- /dev/null
+++ b/test-suite/modules/fun_objects.v
@@ -0,0 +1,32 @@
+Implicit Arguments On.
+
+Module Type SIG.
+ Parameter id:(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 := O.
+ Definition id := [A:Set][x:A]x.
+End Nat.
+
+Module Z:=(N Nat).
+
+Check (Z.idid O).
+
+Module P[Y:SIG] := N.
+
+Module Y:=P Nat Z.
+
+Check (Y.id O).
+
+
+
+
diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v
new file mode 100644
index 00000000..fb734b5d
--- /dev/null
+++ b/test-suite/modules/grammar.v
@@ -0,0 +1,15 @@
+Module N.
+Definition f:=plus.
+Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
+Check (f O O).
+End N.
+Check (N.f O O).
+Import N.
+Check (N.f O O).
+Check (f O O).
+Module M:=N.
+Check (f O O).
+Check (N.f O O).
+Import M.
+Check (f O O).
+Check (N.f O O).
diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v
new file mode 100644
index 00000000..94c344bb
--- /dev/null
+++ b/test-suite/modules/ind.v
@@ -0,0 +1,13 @@
+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]Cases x of A => A end.
+End M.
+
+Module N:=M.
+
+Check (N.f M.A).
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
new file mode 100644
index 00000000..867b8a11
--- /dev/null
+++ b/test-suite/modules/mod_decl.v
@@ -0,0 +1,55 @@
+Module Type SIG.
+ Definition A:Set. (*error*)
+ Axiom A:Set.
+End SIG.
+
+Module M0.
+ Definition A:Set.
+ Exact nat.
+ Save.
+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.
+
+
+Declare Module M6.
+
+
+Module Type T.
+
+ Declare Module M0.
+ Lemma A:Set (*error*).
+ Axiom A:Set.
+ End M0.
+
+ Declare Module M1:SIG.
+
+ Declare Module M2<:SIG.
+ Definition A:=nat.
+ End M2.
+
+ Declare Module M3:=M0.
+
+ Declare Module M4:SIG:=M0. (* error *)
+
+ Declare Module M5<:SIG:=M0.
+
+ Declare Module M6:=F M0. (* error *)
+
+ Module M7.
+End T. \ No newline at end of file
diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
new file mode 100644
index 00000000..73448dc7
--- /dev/null
+++ b/test-suite/modules/modeq.v
@@ -0,0 +1,22 @@
+Module M.
+ Definition T:=nat.
+ Definition x:T:=O.
+End M.
+
+Module Type SIG.
+ Declare Module M:=Top.M.
+ Module Type SIG.
+ Parameter T:Set.
+ End SIG.
+ Declare Module N:SIG.
+End SIG.
+
+Module Z.
+ Module M:=Top.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 00000000..5612ea75
--- /dev/null
+++ b/test-suite/modules/modul.v
@@ -0,0 +1,39 @@
+Module M.
+ Parameter rel:nat -> nat -> Prop.
+
+ Axiom w : (n:nat)(rel O (S n)).
+
+ Hints Resolve w.
+
+ Grammar constr constr8 :=
+ not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
+
+ Print Hint *.
+
+ Lemma w1 : (O#(S O)).
+ Auto.
+ Save.
+
+End M.
+
+(*Lemma w1 : (M.rel O (S O)).
+Auto.
+*)
+
+Import M.
+
+Print Hint *.
+Lemma w1 : (O#(S O)).
+Print Hint.
+Print Hint *.
+
+Auto.
+Save.
+
+Check (O#O).
+Locate rel.
+
+Locate M.
+
+Module N:=Top.M.
+
diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
new file mode 100644
index 00000000..2231e084
--- /dev/null
+++ b/test-suite/modules/obj.v
@@ -0,0 +1,26 @@
+Implicit Arguments On.
+
+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 1!A 2!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 00000000..418ece44
--- /dev/null
+++ b/test-suite/modules/objects.v
@@ -0,0 +1,33 @@
+Module Type SET.
+ Axiom T:Set.
+ Axiom x:T.
+End SET.
+
+Implicit Arguments On.
+
+Module M[X:SET].
+ Definition T := nat.
+ Definition x := O.
+ Definition f := [A:Set][x:A]X.x.
+End M.
+
+Module N:=M.
+
+Module Nat.
+ Definition T := nat.
+ Definition x := O.
+End Nat.
+
+Module Z:=(N Nat).
+
+Check (Z.f O).
+
+Module P[Y:SET] := N.
+
+Module Y:=P Z Nat.
+
+Check (Y.f O).
+
+
+
+
diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v
new file mode 100644
index 00000000..6061ace3
--- /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 00000000..f1f59df0
--- /dev/null
+++ b/test-suite/modules/plik.v
@@ -0,0 +1,4 @@
+Definition toto:=[x:Set]x.
+
+Grammar constr constr8 :=
+ toto [ "#" constr7($b) ] -> [ (toto $b) ].
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
new file mode 100644
index 00000000..eb8736bb
--- /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:=O.
+ End N.
+End M.
+
+Module N:=M.
+
+Module Type SPRYT.
+ Declare 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 00000000..1bd4faef
--- /dev/null
+++ b/test-suite/modules/sub_objects.v
@@ -0,0 +1,33 @@
+Set Implicit Arguments.
+
+
+Module M.
+ Definition id:=[A:Set][x:A]x.
+
+ Module Type SIG.
+ Parameter idid:(A:Set)A->A.
+ End SIG.
+
+ Module N.
+ Definition idid:=[A:Set][x:A](id x).
+ Grammar constr constr8 :=
+ not_eq [ "#" constr7($b) ] -> [ (idid $b) ].
+ Notation inc := (plus (S O)).
+ End N.
+
+ Definition zero:=(N.idid O).
+
+End M.
+
+Definition zero := (M.N.idid O).
+Definition jeden := (M.N.inc O).
+
+Module Goly:=M.N.
+
+Definition Gole_zero := (Goly.idid O).
+Definition Goly_jeden := (Goly.inc O).
+
+Module Ubrany : M.SIG := M.N.
+
+Definition Ubrane_zero := (Ubrany.idid O).
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 07:24:44 +0000