diff options
Diffstat (limited to 'test-suite/output')
27 files changed, 273 insertions, 0 deletions
diff --git a/test-suite/output/Arith.out b/test-suite/output/Arith.out new file mode 100644 index 00000000..210dd6ad --- /dev/null +++ b/test-suite/output/Arith.out @@ -0,0 +1,4 @@ +[n:nat](S (S n)) + : nat->nat +[n:nat](S (plus n n)) + : nat->nat diff --git a/test-suite/output/Arith.v b/test-suite/output/Arith.v new file mode 100644 index 00000000..39989dfc --- /dev/null +++ b/test-suite/output/Arith.v @@ -0,0 +1,2 @@ +Check [n](S (S n)). +Check [n](S (plus n n)). diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out new file mode 100644 index 00000000..5f13caaf --- /dev/null +++ b/test-suite/output/Cases.out @@ -0,0 +1,4 @@ +t_rect = +[P:(t->Type); f:([x:=t](x0:x)(P x0)->(P (k x0)))] + Fix F{F [t:t] : (P t) := <P>Cases t of (k x x0) => (f x0 (F x0)) end} + : (P:(t->Type))([x:=t](x0:x)(P x0)->(P (k x0)))->(t:t)(P t) diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v new file mode 100644 index 00000000..7483e8c4 --- /dev/null +++ b/test-suite/output/Cases.v @@ -0,0 +1,5 @@ +(* Cases with let-in in constructors types *) + +Inductive t : Set := k : [x:=t]x -> x. + +Print t_rect. diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out new file mode 100644 index 00000000..63e042d8 --- /dev/null +++ b/test-suite/output/Coercions.out @@ -0,0 +1,4 @@ +(P x) + : Prop +(R x x) + : Prop diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v new file mode 100644 index 00000000..61b69038 --- /dev/null +++ b/test-suite/output/Coercions.v @@ -0,0 +1,9 @@ +(* Submitted by Randy Pollack *) + +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. +Check (P x). +Check (R x x). diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v new file mode 100644 index 00000000..270fff4e --- /dev/null +++ b/test-suite/output/Fixpoint.v @@ -0,0 +1,7 @@ +Require PolyList. + +Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) := + [_,_,f,l]Cases l of + nil => (nil ?) + | (cons a l) => (cons (f a) (F ? ? f l)) + end}. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out new file mode 100644 index 00000000..f9cf9efc --- /dev/null +++ b/test-suite/output/Implicit.out @@ -0,0 +1,5 @@ +d2 = [x:nat](d1 1!x) + : (x,x0:nat)x0=x ->x0=x + +Positions [1; 2] are implicit +Argument scopes are [nat_scope nat_scope _] diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v new file mode 100644 index 00000000..2dea0d18 --- /dev/null +++ b/test-suite/output/Implicit.v @@ -0,0 +1,18 @@ +Set Implicit Arguments. + +(* Suggested by Pierre Casteran (bug #169) *) +(* Argument 3 is needed to typecheck and should be printed *) +Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)). +Check (compose 3!nat S). + +(* Better to explicitly display the arguments inferable from a + position that could disappear after reduction *) +Inductive ex [A:Set;P:A->Prop] : Prop + := ex_intro : (x:A)(P x)->(ex P). +Check (ex_intro 2![_]True 3!O I). + +(* Test for V8 printing of implicit by names *) +Definition d1 [y;x;h:x=y:>nat] := h. +Definition d2 [x] := (!d1 x). + +Print d2. diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out new file mode 100644 index 00000000..d7120f89 --- /dev/null +++ b/test-suite/output/InitSyntax.out @@ -0,0 +1,6 @@ +Inductive sig2 [A : Set; P : A->Prop; Q : A->Prop] : Set := + exist2 : (x:A)(P x)->(Q x)->(sig2 A P Q) +(EX x:nat|x=x) + : Prop +[b:bool](if b then b else b) + : bool->bool diff --git a/test-suite/output/InitSyntax.v b/test-suite/output/InitSyntax.v new file mode 100644 index 00000000..90fad371 --- /dev/null +++ b/test-suite/output/InitSyntax.v @@ -0,0 +1,4 @@ +(* Soumis par Pierre *) +Print sig2. +Check (EX x:nat|x=x). +Check [b:bool]if b then b else b. diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out new file mode 100644 index 00000000..cadb35c6 --- /dev/null +++ b/test-suite/output/Intuition.out @@ -0,0 +1,7 @@ +1 subgoal + + m : Z + n : Z + H : `m >= n` + ============================ + `m >= m` diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v new file mode 100644 index 00000000..c0508c90 --- /dev/null +++ b/test-suite/output/Intuition.v @@ -0,0 +1,5 @@ +Require ZArith_base. +Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`. +Intros; Intuition. +Show. +Abort. diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out new file mode 100644 index 00000000..505821d7 --- /dev/null +++ b/test-suite/output/Nametab.out @@ -0,0 +1,28 @@ +id is not a defined object +K.id is not a defined object +N.K.id is not a defined object +Constant Top.Q.N.K.id +Constant Top.Q.N.K.id +K is not a defined object +N.K is not a defined object +Module Top.Q.N.K +Module Top.Q.N.K +N is not a defined object +Module Top.Q.N +Module Top.Q.N +Module Top.Q +Module Top.Q +id is not a defined object +Constant Top.Q.N.K.id +N.K.id is not a defined object +Constant Top.Q.N.K.id +Constant Top.Q.N.K.id +Module Top.Q.N.K +N.K is not a defined object +Module Top.Q.N.K +Module Top.Q.N.K +N is not a defined object +Module Top.Q.N +Module Top.Q.N +Module Top.Q +Module Top.Q diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v new file mode 100644 index 00000000..61966c7c --- /dev/null +++ b/test-suite/output/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/output/RealSyntax.out b/test-suite/output/RealSyntax.out new file mode 100644 index 00000000..fa30656b --- /dev/null +++ b/test-suite/output/RealSyntax.out @@ -0,0 +1,4 @@ +``32`` + : R +``-31`` + : R diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v new file mode 100644 index 00000000..d976dcc1 --- /dev/null +++ b/test-suite/output/RealSyntax.v @@ -0,0 +1,3 @@ +Require Reals. +Check ``32``. +Check ``-31``. diff --git a/test-suite/output/Remark2.out b/test-suite/output/Remark2.out new file mode 100644 index 00000000..adabc2fe --- /dev/null +++ b/test-suite/output/Remark2.out @@ -0,0 +1 @@ +B.C.t is not a defined object diff --git a/test-suite/output/Remark2.v b/test-suite/output/Remark2.v new file mode 100644 index 00000000..e1ef57a0 --- /dev/null +++ b/test-suite/output/Remark2.v @@ -0,0 +1,8 @@ +Section A. +Section B. +Section C. +Remark t : True. Proof I. +End C. +End B. +End A. +Locate B.C.t. diff --git a/test-suite/output/Sum.out b/test-suite/output/Sum.out new file mode 100644 index 00000000..22422602 --- /dev/null +++ b/test-suite/output/Sum.out @@ -0,0 +1,6 @@ +nat+nat+{True} + : Set +{True}+{True}+{True} + : Set +nat+{True}+{True} + : Set diff --git a/test-suite/output/Sum.v b/test-suite/output/Sum.v new file mode 100644 index 00000000..aceadd12 --- /dev/null +++ b/test-suite/output/Sum.v @@ -0,0 +1,3 @@ +Check nat+nat+{True}. +Check {True}+{True}+{True}. +Check nat+{True}+{True}. diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out new file mode 100644 index 00000000..41e8648b --- /dev/null +++ b/test-suite/output/TranspModtype.out @@ -0,0 +1,10 @@ +TrM.A = M.A + : Set + +OpM.A = M.A + : Set + +TrM.B = M.B + : Set + +*** [ OpM.B : Set ] diff --git a/test-suite/output/TranspModtype.v b/test-suite/output/TranspModtype.v new file mode 100644 index 00000000..27b1fb9f --- /dev/null +++ b/test-suite/output/TranspModtype.v @@ -0,0 +1,22 @@ +Module Type SIG. + Axiom A:Set. + Axiom B:Set. +End SIG. + +Module M:SIG. + Definition A:=nat. + Definition B:=nat. +End M. + +Module N<:SIG:=M. + +Module TranspId[X:SIG] <: SIG with Definition A:=X.A := X. +Module OpaqueId[X:SIG] : SIG with Definition A:=X.A := X. + +Module TrM := TranspId M. +Module OpM := OpaqueId M. + +Print TrM.A. +Print OpM.A. +Print TrM.B. +Print OpM.B. diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out new file mode 100644 index 00000000..0fdc5b7e --- /dev/null +++ b/test-suite/output/ZSyntax.out @@ -0,0 +1,26 @@ +`32` + : Z +[f:(nat->Z)]`(f O)+0` + : (nat->Z)->Z +[x:positive](POS (xO x)) + : positive->Z +[x:positive]`(POS x)+1` + : positive->Z +[x:positive](POS x) + : positive->Z +[x:positive](NEG (xO x)) + : positive->Z +[x:positive]`(POS (xO x))+0` + : positive->Z +[x:positive]`(Zopp (POS (xO x)))` + : positive->Z +[x:positive]`(Zopp (POS (xO x)))+0` + : positive->Z +`(inject_nat (0))+1` + : Z +`0+(inject_nat (plus (0) (0)))` + : Z +`(inject_nat (0)) = 0` + : Prop +`0+(inject_nat (11))` + : Z diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v new file mode 100644 index 00000000..49442b75 --- /dev/null +++ b/test-suite/output/ZSyntax.v @@ -0,0 +1,17 @@ +Require ZArith. +Check `32`. +Check [f:nat->Z]`(f O) + 0`. +Check [x:positive]`(POS (xO x))`. +Check [x:positive]`(POS x)+1`. +Check [x:positive]`(POS x)`. +Check [x:positive]`(NEG (xO x))`. +Check [x:positive]`(POS (xO x))+0`. +Check [x:positive]`(Zopp (POS (xO x)))`. +Check [x:positive]`(Zopp (POS (xO x)))+0`. +Check `(inject_nat O)+1`. +Check (Zplus `0` (inject_nat (plus O O))). +Check `(inject_nat O)=0`. + +(* Submitted by Pierre Casteran *) +Require Arith. +Check (Zplus `0` (inject_nat (11))). diff --git a/test-suite/output/implicits.out b/test-suite/output/implicits.out new file mode 100644 index 00000000..e4837199 --- /dev/null +++ b/test-suite/output/implicits.out @@ -0,0 +1,4 @@ +(compose 3!nat S) + : (nat->nat)->nat->nat +(ex_intro 2![_:nat]True 3!(0) I) + : (ex [_:nat]True) diff --git a/test-suite/output/implicits.v b/test-suite/output/implicits.v new file mode 100644 index 00000000..d7ea7227 --- /dev/null +++ b/test-suite/output/implicits.v @@ -0,0 +1,13 @@ +Set Implicit Arguments. + +(* Suggested by Pierre Casteran (bug #169) *) +(* Argument 3 is needed to typecheck and should be printed *) +Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)). +Check (compose 3!nat S). + +(* Better to explicitly display the arguments inferable from a + position that could disappear after reduction *) +Inductive ex [A:Set;P:A->Prop] : Prop + := ex_intro : (x:A)(P x)->(ex P). +Check (ex_intro 2![_]True 3!O I). + |