From 7061f479eaf148779d216ad6779cf153076fb005 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:40:29 +0100 Subject: Fixing wrong rel_context in checking positivity condition. Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas. --- test-suite/success/Inductive.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 3d4257543a..04d92daad9 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -121,3 +121,12 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0. (* Check cross inference of evars from constructors *) Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0. + +(* An example with reduction removing an occurrence of the inductive type in one of its argument *) + +Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1). + +(* This type was considered as ill-formed before March 2015, while it + could be accepted considering that the type IND1 above was accepted *) + +Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). -- cgit v1.2.3 From 72b5c9d35dddf774c1d517889cb8f48a932d7095 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:29:38 +0100 Subject: Fixing computation of non-recursively uniform arguments in the presence of let-ins. This fixes #3491. --- test-suite/bugs/closed/3491.v | 4 ++++ test-suite/success/Inductive.v | 16 +++++++++++++++- 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/3491.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/3491.v b/test-suite/bugs/closed/3491.v new file mode 100644 index 0000000000..fd394ddbc3 --- /dev/null +++ b/test-suite/bugs/closed/3491.v @@ -0,0 +1,4 @@ +(* Was failing while building the _rect scheme, due to wrong computation of *) +(* the number of non recursively uniform parameters in the presence of let-ins*) +Inductive list (A : Type) (T := A) : Type := + nil : list A | cons : T -> list T -> list A. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 04d92daad9..de18ed96ef 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -126,7 +126,21 @@ Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0. Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1). -(* This type was considered as ill-formed before March 2015, while it +(* These types were considered as ill-formed before March 2015, while they could be accepted considering that the type IND1 above was accepted *) Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). + +Inductive IND3 (A:Type) (T:=fun _ : Type->Type => A) := CONS3 : IND3 (T IND3) -> IND3 A. + +Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A. + +(* This type was ok before March 2015 *) + +Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A. + +(* This type was raising an anomaly when building the _rect scheme, + because of a wrong computation of the number of non-recursively + uniform parameters in the presence of let-ins (see #3491) *) + +Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. -- cgit v1.2.3 From c801b004bcb71f4f1db5d4cf260ef5a01fc8dde0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:52:10 +0100 Subject: Updating test-suite (see previous commit). --- test-suite/bugs/opened/3491.v | 2 -- 1 file changed, 2 deletions(-) delete mode 100644 test-suite/bugs/opened/3491.v (limited to 'test-suite') diff --git a/test-suite/bugs/opened/3491.v b/test-suite/bugs/opened/3491.v deleted file mode 100644 index 9837b0ecb2..0000000000 --- a/test-suite/bugs/opened/3491.v +++ /dev/null @@ -1,2 +0,0 @@ -Fail Inductive list (A : Type) (T := A) : Type := - nil : list A | cons : T -> list T -> list A. -- cgit v1.2.3 From 1a519fc37e703b014e3bcc77de01edd82aabea5f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Mar 2015 09:44:12 +0100 Subject: Another example about the consequence of a wrong computation of the number of recursively uniform parameters in the presence of let-ins. In practice, more recursively non-uniform parameters were assumed and this was used especially for checking positivity of nested types, leading to refusing more nested types than necessary (see Inductive.v). --- test-suite/success/Inductive.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index de18ed96ef..0a4ae68733 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -144,3 +144,14 @@ Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IN uniform parameters in the presence of let-ins (see #3491) *) Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. + +(* An example of nested positivity which was rejected by the kernel + before 24 March 2015 (even with Unset Elimination Schemes to avoid + the _rect bug) due to the wrong computation of non-recursively + uniform parameters in list' *) + +Inductive list' (A:Type) (B:=A) := +| nil' : list' A +| cons' : A -> list' B -> list' A. + +Inductive tree := node : list' tree -> tree. -- cgit v1.2.3 From c1729637d4fe32ebe0268eb338fcf4d032bb5df7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Mar 2015 11:26:21 +0100 Subject: Fully fixing bug #3491 (anomaly when building _rect scheme in the presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli. --- test-suite/success/Inductive.v | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'test-suite') diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 0a4ae68733..9661b3bfac 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -139,12 +139,6 @@ Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A. Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A. -(* This type was raising an anomaly when building the _rect scheme, - because of a wrong computation of the number of non-recursively - uniform parameters in the presence of let-ins (see #3491) *) - -Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. - (* An example of nested positivity which was rejected by the kernel before 24 March 2015 (even with Unset Elimination Schemes to avoid the _rect bug) due to the wrong computation of non-recursively @@ -155,3 +149,16 @@ Inductive list' (A:Type) (B:=A) := | cons' : A -> list' B -> list' A. Inductive tree := node : list' tree -> tree. + +(* This type was raising an anomaly when building the _rect scheme, + because of a bug in Inductiveops.get_arity in the presence of + let-ins and recursively non-uniform parameters. *) + +Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A. + +(* This type was raising an anomaly when building the _rect scheme, + because of a wrong computation of the number of non-recursively + uniform parameters when conversion is needed, leading the example to + hit the Inductiveops.get_arity bug mentioned above (see #3491) *) + +Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. -- cgit v1.2.3 From 598ac5ca1ac87fbd9152c7da1812a6ae7aa1e7bb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 Mar 2015 15:16:09 +0200 Subject: Adding test for bug #4165. --- test-suite/bugs/closed/4165.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/closed/4165.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4165.v b/test-suite/bugs/closed/4165.v new file mode 100644 index 0000000000..8e0a62d35c --- /dev/null +++ b/test-suite/bugs/closed/4165.v @@ -0,0 +1,7 @@ +Lemma foo : True. +Proof. +pose (fun x : nat => (let H:=true in x)) as s. +match eval cbv delta [s] in s with +| context C[true] => + let C':=context C[false] in pose C' as s' +end. -- cgit v1.2.3 From d58900ce20a6a7144db386a02093d3fc1c54c894 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 11:14:01 +0200 Subject: camlp4: grep away warnings in output/* tests --- test-suite/Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'test-suite') diff --git a/test-suite/Makefile b/test-suite/Makefile index 4a3a287c08..cffbe48196 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -273,6 +273,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ + | grep -v "^" \ > $$tmpoutput; \ diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ -- cgit v1.2.3