diff options
Diffstat (limited to 'test-suite')
34 files changed, 606 insertions, 30 deletions
diff --git a/test-suite/bugs/closed/5532.v b/test-suite/bugs/closed/5532.v new file mode 100644 index 0000000000..ee5446e548 --- /dev/null +++ b/test-suite/bugs/closed/5532.v @@ -0,0 +1,15 @@ +(* A wish granted by the new support for patterns in notations *) + +Local Notation mkmatch0 e p + := match e with + | p => true + | _ => false + end. +Local Notation "'mkmatch' [[ e ]] [[ p ]]" + := match e with + | p => true + | _ => false + end + (at level 0, p pattern). +Check mkmatch0 _ ((0, 0)%core). +Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]]. diff --git a/test-suite/bugs/closed/5726.v b/test-suite/bugs/closed/5726.v new file mode 100644 index 0000000000..53ef473572 --- /dev/null +++ b/test-suite/bugs/closed/5726.v @@ -0,0 +1,34 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Module GlobalReference. + + Definition type' := Type. + Notation type := type'. + Check type@{Set}. + +End GlobalReference. + +Module TypeLiteral. + + Notation type := Type. + Check type@{Set}. + Check type@{Prop}. + +End TypeLiteral. + +Module ExplicitSort. + Monomorphic Universe u. + Notation foo := Type@{u}. + Fail Check foo@{Set}. + Fail Check foo@{u}. + + Notation bar := Type. + Check bar@{u}. +End ExplicitSort. + +Module PropNotationUnsupported. + Notation foo := Prop. + Fail Check foo@{Set}. + Fail Check foo@{Type}. +End PropNotationUnsupported. diff --git a/test-suite/bugs/closed/6529.v b/test-suite/bugs/closed/6529.v new file mode 100644 index 0000000000..8d90819998 --- /dev/null +++ b/test-suite/bugs/closed/6529.v @@ -0,0 +1,16 @@ +Require Import Vector Program. + +Program Definition append_nil_def := + forall A n (ls: t A n), append ls (nil A) = ls. (* Works *) + +Lemma append_nil : append_nil_def. (* Works *) +Proof. +Admitted. + +Program Lemma append_nil' : + forall A n (ls: t A n), append ls (nil A) = ls. +Abort. + +Fail Program Lemma append_nil'' : + forall A B n (ls: t A n), append ls (nil A) = ls. +(* Error: Anomaly "Evar ?X25 was not declared." Please report at http://coq.inria.fr/bugs/. *) diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v new file mode 100644 index 0000000000..99e47bb87c --- /dev/null +++ b/test-suite/bugs/closed/6677.v @@ -0,0 +1,5 @@ +Set Universe Polymorphism. + +Definition T@{i} := Type@{i}. +Fail Definition U@{i} := (T@{i} <: Type@{i}). +Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl. diff --git a/test-suite/bugs/closed/6774.v b/test-suite/bugs/closed/6774.v new file mode 100644 index 0000000000..9625af91f5 --- /dev/null +++ b/test-suite/bugs/closed/6774.v @@ -0,0 +1,7 @@ +(* Was an anomaly with ill-typed template polymorphism *) +Definition huh (b:bool) := if b then Set else Prop. +Definition lol b: huh b := + if b return huh b then nat else True. +Goal (lol true) * unit. +Fail generalize true. (* should fail with error, not anomaly *) +Abort. diff --git a/test-suite/bugs/opened/6602.v b/test-suite/bugs/opened/6602.v new file mode 100644 index 0000000000..3690adf90a --- /dev/null +++ b/test-suite/bugs/opened/6602.v @@ -0,0 +1,17 @@ +Require Import Omega. + +Lemma test_nat: + forall n, (5 + pred n <= 5 + n). +Proof. + intros. + zify. + omega. +Qed. + +Lemma test_N: + forall n, (5 + N.pred n <= 5 + n)%N. +Proof. + intros. + zify. + omega. +Qed. diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject new file mode 100644 index 0000000000..5678a8edbb --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -0,0 +1,11 @@ +-R theories "" +-R src "" +-I src +-arg "-w default" + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject.sub b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub new file mode 100644 index 0000000000..90ac541e04 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub @@ -0,0 +1,3 @@ +-R ../theories "" +-I ../src +testsub.v diff --git a/test-suite/coq-makefile/emptyprefix/run.sh b/test-suite/coq-makefile/emptyprefix/run.sh new file mode 100755 index 0000000000..a10e63b42e --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/run.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +set -e + +. ../template/init.sh + +mv theories/sub theories2 + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make + +cp ../_CoqProject.sub theories2/_CoqProject +cd theories2 +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh new file mode 100755 index 0000000000..9e681223b4 --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make quick2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh new file mode 100755 index 0000000000..85656da419 --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make quick +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make vio2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v new file mode 100644 index 0000000000..bbf72a7648 --- /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/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/output/ErrorInCanonicalStructures.out b/test-suite/output/ErrorInCanonicalStructures.out new file mode 100644 index 0000000000..73da4f44f8 --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures.out @@ -0,0 +1,5 @@ +File "stdin", line 3, characters 0-24: +Error: +Could not declare a canonical structure Foo. +Expected an instance of a record or structure. + diff --git a/test-suite/output/ErrorInCanonicalStructures.v b/test-suite/output/ErrorInCanonicalStructures.v new file mode 100644 index 0000000000..49597df6f7 --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures.v @@ -0,0 +1,3 @@ +Record Foo := MkFoo { field1 : nat; field2 : nat -> nat }. + +Canonical Structure Foo. diff --git a/test-suite/output/ErrorInCanonicalStructures2.out b/test-suite/output/ErrorInCanonicalStructures2.out new file mode 100644 index 0000000000..63a2871b82 --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures2.out @@ -0,0 +1,5 @@ +File "stdin", line 3, characters 0-24: +Error: +Could not declare a canonical structure bar. +Expected an instance of a record or structure. + diff --git a/test-suite/output/ErrorInCanonicalStructures2.v b/test-suite/output/ErrorInCanonicalStructures2.v new file mode 100644 index 0000000000..10ee177aaf --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures2.v @@ -0,0 +1,3 @@ +Definition bar := 99. + +Canonical Structure bar. diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index e912003f03..af202ea01c 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,3 +1,7 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x + +For foo: Argument scopes are [type_scope _] +For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8db8956e32..8ff91268a6 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -1,3 +1,7 @@ Fail Inductive list' (A:Set) : Set := | nil' : list' A | cons' : A -> list' A -> list' (A*A). + +(* Check printing of let-ins *) +Inductive foo (A : Type) (x : A) (y := x) := Foo. +Print foo. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 2f0ee765db..891296b0a1 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,7 +41,7 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -x should not be bound in a recursive pattern of the right-hand side. +Cannot find where the recursive pattern starts. The command has indeed failed with message: in the right-hand side, y and z should appear in term position as part of a recursive pattern. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 121a369a94..6ffe56e11f 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -17,10 +17,9 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y ∃ n p : nat, n + p = 0 : Prop let a := 0 in -∃ x y : nat, -let b := 1 in -let c := b in -let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), +let e := 3 in +let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 531398bb0b..923caedace 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -36,8 +36,9 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x). (* Test notations with binders *) -Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) - (x binder, y binder, at level 200, right associativity). +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity, + format "'[ ' ∃ x .. y ']' , P"). Check (∃ n p, n+p=0). diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 1b57252752..e6a6e0288a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -138,3 +138,100 @@ amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit alist = [0; 1; 2] : list nat +! '{{x, y}}, x + y = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + : Prop +exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 + : Prop +exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), +(forall x : A, R x x) + : Prop +exists_true (x : nat) (A : Type) (R : A -> A -> Prop) +(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z + : Prop +{{{{True, nat -> True}}, nat -> True}} + : Prop * Prop * Prop +{{D 1, 2}} + : nat * nat * (nat * nat * (nat * nat)) +! a b : nat # True # + : Prop * (Prop * Prop) +!!!! a b : nat # True # + : Prop * Prop * (Prop * Prop * Prop) +@@ a b : nat # a = b # b = a # + : Prop * Prop +exists_non_null x y z t : nat , x = y /\ z = t + : Prop +forall_non_null x y z t : nat , x = y /\ z = t + : Prop +{{RL 1, 2}} + : nat * (nat * nat) +{{RR 1, 2}} + : nat * nat * nat +@pair nat (prod nat nat) (S (S O)) (@pair nat nat (S O) O) + : prod nat (prod nat nat) +@pair (prod nat nat) nat (@pair nat nat O (S (S O))) (S O) + : prod (prod nat nat) nat +{{RLRR 1, 2}} + : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * + (nat * nat * nat) +pair + (pair + (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) + (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + : prod + (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) + (prod nat (prod nat nat))) (prod (prod nat nat) nat) +fun x : nat => if x is n .+ 1 then n else 1 + : nat -> nat +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2' {{x, y}}, x = 0 & y = 0 + : Prop +myexists2 x : nat * nat, + let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y + : Prop +fun '({{x, y}} as z) => x + y = 0 /\ z = z + : nat * nat -> Prop +myexists ({{x, y}} as z), x + y = 0 /\ z = z + : Prop +exists '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +∀ '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y + : nat * nat * bool -> nat +myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +fun p : nat => if p is S n then n else 0 + : nat -> nat +fun p : comparison => if p is Lt then 1 else 0 + : comparison -> nat +fun S : nat => [S | S + S] + : nat -> nat * (nat -> nat) +fun N : nat => [N | N + 0] + : nat -> nat * (nat -> nat) +fun S : nat => [[S | S + S]] + : nat -> nat * (nat -> nat) +{I : nat | I = I} + : Set +{'I : True | I = I} + : Prop +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2 '{{y, z}} : nat * nat, y > z & z > y + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index a8d6c97fbd..c98bfff413 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -253,3 +253,170 @@ Definition alist := [0;1;2]. Print alist. End B. + +(* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) +(* for isolated "forall" (was not working already in 8.6) *) +Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). +Check ! '(x,y), x+y=0. + +(* Check that the terminator of a recursive pattern is interpreted in + the correct environment of bindings *) +Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder). +Check exists_mixed x y '(u,t), x+y=0/\u+t=0. +Check exists_mixed x y '(z,t), x+y=0/\z+t=0. + +(* Check that intermediary let-in are inserted inbetween instances of + the repeated pattern *) +Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). +Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. + +(* Check that generalized binders are correctly interpreted *) + +Module G. +Generalizable Variables A R. +Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. +Check exists_true `{Reflexive A R}, forall x, R x x. +Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +End G. + +(* Allows recursive patterns for binders to be associative on the left *) +Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). +Check !! a b : nat # True #. + +(* Examples where the recursive pattern refer several times to the recursive variable *) + +Notation "{{D x , .. , y }}" := ((x,x), .. ((y,y),(0,0)) ..). +Check {{D 1, 2 }}. + +Notation "! x .. y # A #" := + ((forall x, x=x), .. ((forall y, y=y), A) ..) + (at level 200, x binder). +Check ! a b : nat # True #. + +Notation "!!!! x .. y # A #" := + (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..) + (at level 200, x binder). +Check !!!! a b : nat # True #. + +Notation "@@ x .. y # A # B #" := + ((forall x, .. (forall y, A) ..), (forall x, .. (forall y, B) ..)) + (at level 200, x binder). +Check @@ a b : nat # a=b # b=a #. + +Notation "'exists_non_null' x .. y , P" := + (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) + (at level 200, x binder). +Check exists_non_null x y z t , x=y/\z=t. + +Notation "'forall_non_null' x .. y , P" := + (forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..) + (at level 200, x binder). +Check forall_non_null x y z t , x=y/\z=t. + +(* Examples where the recursive pattern is in reverse order *) + +Notation "{{RL c , .. , d }}" := (pair d .. (pair c 0) ..). +Check {{RL 1 , 2}}. + +Notation "{{RR c , .. , d }}" := (pair .. (pair 0 d) .. c). +Check {{RR 1 , 2}}. + +Set Printing All. +Check {{RL 1 , 2}}. +Check {{RR 1 , 2}}. +Unset Printing All. + +Notation "{{RLRR c , .. , d }}" := (pair d .. (pair c 0) .., pair .. (pair 0 d) .. c, pair c .. (pair d 0) .., pair .. (pair 0 c) .. d). +Check {{RLRR 1 , 2}}. +Unset Printing Notations. +Check {{RLRR 1 , 2}}. +Set Printing Notations. + +(* Check insensitivity of "match" clauses to order *) + +Notation "'if' t 'is' n .+ 1 'then' p 'else' q" := + (match t with S n => p | 0 => q end) + (at level 200). +Check fun x => if x is n.+1 then n else 1. + +(* Examples with binding patterns *) + +Check {'(x,y)|x+y=0}. + +Module D. +Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x pattern, p at level 200, right associativity, + format "'[' 'exists2'' '/ ' x , '/ ' '[' p & '/' q ']' ']'") + : type_scope. + +Check exists2' (x,y), x=0 & y=0. +End D. + +(* Ensuring for reparsability that printer of notations does not use a + pattern where only an ident could be reparsed *) + +Module E. +Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop := + myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q. +Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q)) + (at level 200, x ident, A at level 200, p at level 200, right associativity, + format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") + : type_scope. +Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). +End E. + +(* A canonical example of a notation with a non-recursive binder *) + +Parameter myex : forall {A}, (A -> Prop) -> Prop. +Notation "'myexists' x , p" := (myex (fun x => p)) + (at level 200, x pattern, p at level 200, right associativity). + +(* A canonical example of a notation with recursive binders *) + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +(* Check that printing 'pat uses an "as" when the variable bound to + the pattern is dependent. We check it for the three kinds of + notations involving bindings of patterns *) + +Check fun '((x,y) as z) => x+y=0/\z=z. (* Primitive fun/forall *) +Check myexists ((x,y) as z), x+y=0/\z=z. (* Isolated binding pattern *) +Check exists '((x,y) as z), x+y=0/\z=z. (* Applicative recursive binder *) +Check ∀ '((x,y) as z), x+y=0/\z=z. (* Other example of recursive binder, now treated as the exists case *) + +(* Check parsability and printability of irrefutable disjunctive patterns *) + +Check fun '(((x,y),true)|((x,y),false)) => x+y. +Check myexists (((x,y),true)|((x,y),false)), x>y. +Check exists '(((x,y),true)|((x,y),false)), x>y. +Check ∀ '(((x,y),true)|((x,y),false)), x>y. + +(* Check Georges' printability of a "if is then else" notation *) + +Notation "'if' c 'is' p 'then' u 'else' v" := + (match c with p => u | _ => v end) + (at level 200, p pattern at level 100). +Check fun p => if p is S n then n else 0. +Check fun p => if p is Lt then 1 else 0. + +(* Check that mixed binders and terms defaults to ident and not pattern *) +Module F. + (* First without an indirection *) +Notation "[ n | t ]" := (n, (fun n : nat => t)). +Check fun S : nat => [ S | S+S ]. +Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *) + (* Then with an indirection *) +Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)). +Notation "[[ n | t ]]" := [[ n | n | t ]]. +Check fun S : nat => [[ S | S+S ]]. +End F. + +(* Check parsability/printability of {x|P} and variants *) + +Check {I:nat|I=I}. +Check {'I:True|I=I}. +Check {'(x,y)|x+y=0}. + +(* Check exists2 with a pattern *) +Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 95be04c32c..8a6d94c732 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -31,7 +31,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : Prop both_z = fun pat : nat * nat => -let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p) +let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop @@ -39,3 +39,9 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop +f = fun x : nat => x + x + : nat -> nat + +Argument scope is [nat_scope] +fun x : nat => x + x + : nat -> nat diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0bad472f41..d671053c07 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -67,3 +67,8 @@ End Suboptimal. (** Test risk of collision for internal name *) Check fun pat => fun '(x,y) => x+y = pat. + +(** Test name in degenerate case *) +Definition f 'x := x+x. +Print f. +Check fun 'x => x+x. diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 45ff5e73b6..b0ac9ea29f 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -12,32 +12,37 @@ Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Nat.two: nat -Nat.zero: nat Nat.one: nat +Nat.zero: nat O: nat -Nat.double: nat -> nat -Nat.sqrt: nat -> nat Nat.div2: nat -> nat Nat.log2: nat -> nat +Nat.succ: nat -> nat +Nat.sqrt: nat -> nat Nat.pred: nat -> nat +Nat.double: nat -> nat Nat.square: nat -> nat S: nat -> nat -Nat.succ: nat -> nat Nat.ldiff: nat -> nat -> nat -Nat.add: nat -> nat -> nat -Nat.lor: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.land: nat -> nat -> nat -Nat.mul: nat -> nat -> nat -Nat.sub: nat -> nat -> nat -Nat.max: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat Nat.div: nat -> nat -> nat -Nat.pow: nat -> nat -> nat -Nat.min: nat -> nat -> nat -Nat.modulo: nat -> nat -> nat +Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.mul: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.of_uint: Decimal.uint -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat length: forall A : Type, list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat Nat.div2: nat -> nat @@ -53,14 +58,18 @@ Nat.pow: nat -> nat -> nat Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.div: nat -> nat -> nat -Nat.mul: nat -> nat -> nat -Nat.min: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.sub: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.mul: nat -> nat -> nat Nat.gcd: nat -> nat -> nat Nat.max: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d6d410d1ae..668b4e5788 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] For pwrap: Argument scopes are [type_scope _] punwrap@{u} = -fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p +fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap) : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) diff --git a/test-suite/output/bug6821.out b/test-suite/output/bug6821.out new file mode 100644 index 0000000000..7b12b53200 --- /dev/null +++ b/test-suite/output/bug6821.out @@ -0,0 +1,2 @@ +forall f : nat -> Type, f x where x : nat := 1 + : Type diff --git a/test-suite/output/bug6821.v b/test-suite/output/bug6821.v new file mode 100644 index 0000000000..40627e331e --- /dev/null +++ b/test-suite/output/bug6821.v @@ -0,0 +1,8 @@ +(* Was failing at printing time with stack overflow due to an infinite + eta-expansion *) + +Notation "x 'where' y .. z := v " := + ((fun y => .. ((fun z => x) v) ..) v) + (at level 11, v at next level, y binder, z binder). + +Check forall f, f x where x := 1. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 2655b651a0..7c2cf3ee52 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -92,16 +92,37 @@ Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. (* 10. Check computation of binding variable through other notations *) -(* i should be detected as binding variable and the scopes not being checked *) - +(* it should be detected as binding variable and the scopes not being checked *) Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). (* 11. Notations with needed factorization of a recursive pattern *) (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *) -Module A. +Module M11. Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..). Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..). Check [:: 1 ; 2 ; 3 ]. Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *) -End A. +End M11. + +(* 12. Preventively check that a variable which does not occur can be instantiated *) +(* by any term. In particular, it should not be restricted to a binder *) +Module M12. +Notation "N ++ x" := (S x) (only parsing). +Check 2 ++ 0. +End M12. + +(* 13. Check that internal data about associativity are not used in comparing levels *) +Module M13. +Notation "x ;; z" := (x + z) + (at level 100, z at level 200, only parsing, right associativity). +Notation "x ;; z" := (x * z) + (at level 100, z at level 200, only parsing) : foo_scope. +End M13. + +(* 14. Check that a notation with a "ident" binder does not include a pattern *) +Module M14. +Notation "'myexists' x , p" := (ex (fun x => p)) + (at level 200, x ident, p at level 200, right associativity) : type_scope. +Check myexists I, I = 0. (* Should not be seen as a constructor *) +End M14. diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 0ee85712e2..e05762477d 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -45,6 +45,15 @@ Section TpLift. End TpLift. +Record Tp' := { tp' : Tp }. + +Definition CTp := Tp. +(* here we have to reduce a constant to infer the correct subtyping. *) +Record Tp'' := { tp'' : CTp }. + +Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x. +Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x. + Lemma LiftC_Lem (t : Tp) : LiftTp t = t. Proof. reflexivity. Qed. @@ -98,3 +107,30 @@ Section down. intros H f g Hfg. exact (H f g Hfg). Defined. End down. + +Record Arrow@{i j} := { arrow : Type@{i} -> Type@{j} }. + +Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'} + : Arrow@{i j} -> Arrow@{i' j'} + := fun x => x. + +Definition arrow_lift@{i i' j j' | i' = i, j < j'} + : Arrow@{i j} -> Arrow@{i' j'} + := fun x => x. + +Inductive Mut1 A := +| Base1 : Type -> Mut1 A +| Node1 : (A -> Mut2 A) -> Mut1 A +with Mut2 A := + | Base2 : Type -> Mut2 A + | Node2 : Mut1 A -> Mut2 A. + +(* If we don't reduce T while inferring cumulativity for the + constructor we will see a Rel and believe i is irrelevant. *) +Inductive withparams@{i j} (T:=Type@{i}:Type@{j}) := mkwithparams : T -> withparams. + +Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. + +Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. |