diff options
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/int31.v | 17 | ||||
-rw-r--r-- | test-suite/failure/positivity.v | 46 |
2 files changed, 61 insertions, 2 deletions
diff --git a/test-suite/failure/int31.v b/test-suite/failure/int31.v new file mode 100644 index 00000000..b1d11224 --- /dev/null +++ b/test-suite/failure/int31.v @@ -0,0 +1,17 @@ +Require Import Int31 BigN. + +Open Scope int31_scope. + +(* This used to go through because of an unbalanced stack bug in the bytecode +interpreter *) + +Lemma bad : False. +assert (1 = 2). +change 1 with (add31 (addmuldiv31 65 (add31 1 1) 2) 1). +Fail vm_compute; reflexivity. +(* +discriminate. +Qed. +*) +Abort. + diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index 91de8733..8089de2b 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -5,5 +5,47 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Fail Inductive t : Set := - c : (t -> nat) -> t. + +(* Negative occurrence *) +Fail Inductive t : Type := + c : (t -> nat) -> t. + +(* Non-strictely positive occurrence *) +Fail Inductive t : Type := + c : ((t -> nat) -> nat) -> t. + +(* Self-nested type (no proof of + soundness yet *) +Fail Inductive t (A:Type) : Type := + c : t (t A) -> t A. + +(* Nested inductive types *) + +Inductive pos (A:Type) := + p : pos A -> pos A. + +Inductive nnpos (A:Type) := + nnp : ((A -> nat) -> nat) -> nnpos A. + +Inductive neg (A:Type) := + n : (A->neg A) -> neg A. + +Inductive arg : Type -> Prop := + a : forall A, arg A -> arg A. + +(* Strictly covariant parameter: accepted. *) +Fail Fail Inductive t := + c : pos t -> t. + +(* Non-strictly covariant parameter: not + strictly positive. *) +Fail Inductive t := + c : nnpos t -> t. + +(* Contravariant parameter: not positive. *) +Fail Inductive t := + c : neg t -> t. + +(* Strict index: not positive. *) +Fail Inductive t := + c : arg t -> t. |