diff options
Diffstat (limited to 'test-suite')
19 files changed, 542 insertions, 20 deletions
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 117d6523a8..f8cedfff6e 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -23,7 +23,9 @@ Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. +Notation two := (S (S O)). Record prod (A B : Type) := pair { fst : A ; snd : B }. @@ -159,7 +161,7 @@ End Adjointify. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -220,12 +222,12 @@ Section ORecursion. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) : O_indpaths g h p (to O P x) = p x - := (fst (snd (extendable_to_O O 2) g h) p).2 x. + := (fst (snd (extendable_to_O O two) g h) p).2 x. End ORecursion. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index c3e0da1117..fd2380a070 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. + Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. + Notation one := (S O). + Notation two := (S one). Record prod (A B : Type) := pair { fst : A ; snd : B }. Notation "x * y" := (prod x y) : type_scope. Delimit Scope nat_scope with nat. @@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l} (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). Definition O_rec {P Q : Type} {Q_inO : In O Q} (f : P -> Q) : O P -> Q - := (fst (extendable_to_O O 1%nat) f).1. + := (fst (extendable_to_O O one) f).1. Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} (f : P -> Q) (x : P) : O_rec f (to O P x) = f x - := (fst (extendable_to_O O 1%nat) f).2 x. + := (fst (extendable_to_O O one) f).2 x. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. End ORecursion. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 4ad53bc629..13c47edc8f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. Notation "x + y" := (sum x y) : type_scope. @@ -449,7 +450,7 @@ Section Extensions. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), diff --git a/test-suite/bugs/closed/7867.v b/test-suite/bugs/closed/7867.v new file mode 100644 index 0000000000..d0c7902756 --- /dev/null +++ b/test-suite/bugs/closed/7867.v @@ -0,0 +1,4 @@ +(* Was a printer anomaly due to an internal lambda with no binders *) + +Class class := { foo : nat }. +Fail Instance : class := { foo := 0 ; bar := 0 }. diff --git a/test-suite/bugs/closed/7900.v b/test-suite/bugs/closed/7900.v new file mode 100644 index 0000000000..583ef0ef3b --- /dev/null +++ b/test-suite/bugs/closed/7900.v @@ -0,0 +1,53 @@ +Require Import Coq.Program.Program. +(* Set Universe Polymorphism. *) +Set Printing Universes. + +Axiom ALL : forall {T:Prop}, T. + +Inductive Expr : Set := E (a : Expr). + +Parameter Value : Set. + +Fixpoint eval (e: Expr): Value := + match e with + | E a => eval a + end. + +Class Quote (n: Value) : Set := + { quote: Expr + ; eval_quote: eval quote = n }. + +Program Definition quote_mult n + `{!Quote n} : Quote n := + {| quote := E (quote (n:=n)) |}. + +Set Printing Universes. +Next Obligation. +Proof. + Show Universes. + destruct Quote0 as [q eq]. + Show Universes. + rewrite <- eq. + clear n eq. + Show Universes. + apply ALL. + Show Universes. +Qed. +Print quote_mult_obligation_1. +(* quote_mult_obligation_1@{} = +let Top_internal_eq_rew_dep := + fun (A : Type@{Coq.Init.Logic.8}) (x : A) (P : forall a : A, x = a -> Type@{Top.5} (* <- XXX *)) + (f : P x eq_refl) (y : A) (e : x = y) => + match e as e0 in (_ = y0) return (P y0 e0) with + | eq_refl => f + end in +fun (n : Value) (Quote0 : Quote n) => +match Quote0 as q return (eval quote = n) with +| {| quote := q; eval_quote := eq0 |} => + Top_internal_eq_rew_dep Value (eval q) (fun (n0 : Value) (eq1 : eval q = n0) => eval quote = n0) + ALL n eq0 +end + : forall (n : Value) (Quote0 : Quote n), eval (E quote) = n + +quote_mult_obligation_1 is universe polymorphic +*) diff --git a/test-suite/bugs/closed/8106.v b/test-suite/bugs/closed/8106.v new file mode 100644 index 0000000000..a711c5adef --- /dev/null +++ b/test-suite/bugs/closed/8106.v @@ -0,0 +1,4 @@ +(* Was raising an anomaly "already assigned a level" on the second line *) + +Notation "c1 ; c2" := (c1 + c2) (only printing, at level 76, right associativity, c1 at level 76, c2 at level 76). +Notation "c1 ; c2" := (c1 + c2) (only parsing, at level 76, right associativity, c2 at level 76). diff --git a/test-suite/bugs/closed/8121.v b/test-suite/bugs/closed/8121.v new file mode 100644 index 0000000000..99267612ca --- /dev/null +++ b/test-suite/bugs/closed/8121.v @@ -0,0 +1,46 @@ +Require Import Coq.Strings.String. + +Section T. + Eval native_compute in let x := tt in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval native_compute in let _ := Set in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval native_compute in let _ := Prop in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End T. + +Section U0. + Let n : unit := tt. + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End U0. + +Section S0. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End S0. + +Class T := { }. +Section S1. + Context {p : T}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) +End S1. + +Class M := { m : Type }. +Section S2. + Context {p : M}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) +End S2. diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 56815d241e..72c520218c 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -1,6 +1,6 @@ After | File Name | Before || Change | % Change -------------------------------------------------------- -0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56% +0m00.34s | Total | 0m00.49s || -0m00.14s | -30.61% -------------------------------------------------------- -0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99% -0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89%
\ No newline at end of file +0m00.32s | Fast | 0m00.02s || +0m00.30s | +1500.00% +0m00.02s | Slow | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired index 18f0f34b28..74dad73332 100644 --- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -1,9 +1,9 @@ -After | Code | Before || Change | % Change ---------------------------------------------------------------------------------------------------- -0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% ---------------------------------------------------------------------------------------------------- -0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% -0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% - N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A -0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A -0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
\ No newline at end of file +After | Code | Before || Change | % Change +---------------------------------------------------------------------------------------------------- +0m04.35s | Total | 0m00.58s || +0m03.77s | +649.05% +---------------------------------------------------------------------------------------------------- +0m03.87s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.246s || +0m03.62s | +1473.17% +0m00.322s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.189s || +0m00.13s | +70.37% +0m00.16s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.146s || +0m00.01s | +9.58% +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | N/A || +0m00.00s | N/A + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 6737197ee4..78a3f7c63a 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -5,6 +5,10 @@ set -e . ../template/path-init.sh +# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues + +MAKEFLAGS= + cd precomputed-time-tests ./run.sh || exit $? diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v new file mode 100644 index 0000000000..07986b0df3 --- /dev/null +++ b/test-suite/interactive/PrimNotation.v @@ -0,0 +1,64 @@ +(* Until recently, the Notation.declare_numeral_notation wasn't synchronized + w.r.t. backtracking. This should be ok now. + This test is pretty artificial (we must declare Z_scope for this to work). +*) + +Delimit Scope Z_scope with Z. +Open Scope Z_scope. +Check let v := 0 in v : nat. +(* let v := 0 in v : nat : nat *) +Require BinInt. +Check let v := 0 in v : BinNums.Z. +(* let v := 0 in v : BinNums.Z : BinNums.Z *) +Back 2. +Check let v := 0 in v : nat. +(* Expected answer: let v := 0 in v : nat : nat *) +(* Used to fail with: +Error: Cannot interpret in Z_scope without requiring first module BinNums. +*) + +Local Set Universe Polymorphism. +Delimit Scope punit_scope with punit. +Delimit Scope pcunit_scope with pcunit. +Delimit Scope int_scope with int. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +Module A. + NonCumulative Inductive punit@{u} : Type@{u} := ptt. + Cumulative Inductive pcunit@{u} : Type@{u} := pctt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition to_pcunit : Decimal.int -> option pcunit + := fun v => match v with 0%int => Some pctt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. + Back 2. + Numeral Notation pcunit to_pcunit of_pcunit : punit_scope. + Check let v := 0%punit in v : pcunit. +End A. +Reset A. +Local Unset Universe Polymorphism. +Module A. + Inductive punit : Set := ptt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. +End A. +Local Set Universe Polymorphism. +Inductive punit@{u} : Type@{u} := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. +Back 6. (* check backtracking of registering universe polymorphic constants *) +Local Unset Universe Polymorphism. +Inductive punit : Set := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/ssr/delayed_clear_rename.v index 951e5aff79..951e5aff79 100644 --- a/test-suite/success/ssr_delayed_clear_rename.v +++ b/test-suite/ssr/delayed_clear_rename.v diff --git a/test-suite/ssr/ssr_rew_illtyped.v b/test-suite/ssr/rewrite_illtyped.v index 7358068c8d..7358068c8d 100644 --- a/test-suite/ssr/ssr_rew_illtyped.v +++ b/test-suite/ssr/rewrite_illtyped.v diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v index ed035f5213..2f7425bce6 100644 --- a/test-suite/success/BracketsWithGoalSelector.v +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -14,3 +14,12 @@ Proof. Fail Qed. } Qed. + +Lemma foo (n: nat) (P : nat -> Prop): + P n. +Proof. + intros. + refine (nat_ind _ ?[Base] ?[Step] _). + [Base]: { admit. } + [Step]: { admit. } +Abort. diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v new file mode 100644 index 0000000000..e2045900d5 --- /dev/null +++ b/test-suite/success/Compat88.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that various syntax usage is available without importing + relevant files. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Cyclic31. + +Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *) + +Check String.String "a" String.EmptyString. +Check String.eqb "a" "a". +Check Nat.eqb 1 1. +Check BinNat.N.eqb 1 1. +Check BinInt.Z.eqb 1 1. +Check BinPos.Pos.eqb 1 1. +Check Rdefinitions.Rplus 1 1. +Check Int31.iszero 1. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v new file mode 100644 index 0000000000..288c9d1da0 --- /dev/null +++ b/test-suite/success/CompatCurrentFlag.v @@ -0,0 +1,3 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that the current compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v new file mode 100644 index 0000000000..b7bbc505b4 --- /dev/null +++ b/test-suite/success/CompatOldFlag.v @@ -0,0 +1,5 @@ +(* -*- coq-prog-args: ("-compat" "8.6") -*- *) +(** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq88. +Import Coq.Compat.Coq87. +Import Coq.Compat.Coq86. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v new file mode 100644 index 0000000000..9cfe60390f --- /dev/null +++ b/test-suite/success/CompatPreviousFlag.v @@ -0,0 +1,4 @@ +(* -*- coq-prog-args: ("-compat" "8.7") -*- *) +(** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq88. +Import Coq.Compat.Coq87. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v new file mode 100644 index 0000000000..47ef381270 --- /dev/null +++ b/test-suite/success/NumeralNotations.v @@ -0,0 +1,302 @@ +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Fail Check 1%opaque. +End Test1. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) +Module Test2. + Axiom opaque4 : option Decimal.int. + Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4. + Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Module Test3. + Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). + Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Numeral Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + + +Module Test4. + Polymorphic NonCumulative Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : pto. + Numeral Notation punit pto_punit of_punit : ppo. + Numeral Notation punit to_punit pof_punit : ptp. + Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation unit to_unit of_unit : uto. + Delimit Scope pto with pto. + Delimit Scope ppo with ppo. + Delimit Scope ptp with ptp. + Delimit Scope ppp with ppp. + Delimit Scope uto with uto. + Check let v := 0%pto in v : punit. + Check let v := 0%ppo in v : punit. + Check let v := 0%ptp in v : punit. + Check let v := 0%ppp in v : punit. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Numeral Notation unit pto_unit of_unit : upo. + Numeral Notation unit to_unit pof_unit : utp. + Numeral Notation unit pto_unit pof_unit : upp. + Delimit Scope upo with upo. + Delimit Scope utp with utp. + Delimit Scope upp with upp. + Check let v := 0%upo in v : unit. + Check let v := 0%utp in v : unit. + Check let v := 0%upp in v : unit. + + Polymorphic Definition pto_punits := pto_punit_all@{Set}. + Polymorphic Definition pof_punits := pof_punit@{Set}. + Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). + Delimit Scope ppps with ppps. + Universe u. + Constraint Set < u. + Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) + Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) +End Test4. + +Module Test5. + Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) +End Test5. + +Module Test6. + (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) + Fixpoint ack (n m : nat) : nat := + match n with + | O => S m + | S p => let fix ackn (m : nat) := + match m with + | O => ack p 1 + | S q => ack p (ackn q) + end + in ackn m + end. + + Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) + + Local Set Primitive Projections. + Record > wnat := wrap { unwrap :> nat }. + Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x. + Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x. + Module Export Scopes. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Check let v := 0%wnat in v : wnat. + Check wrap O. + Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) +End Test6. + +Module Test6_2. + Import Test6.Scopes. + Check Test6.wrap 0. + Import Test6.Notations. + Check let v := 0%wnat in v : Test6.wnat. +End Test6_2. + +Module Test7. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Numeral Notation wuint wrap unwrap : wuint_scope. + Check let v := 0%wuint in v : wuint. + Check let v := 1%wuint in v : wuint. +End Test7. + +Module Test8. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint8_scope with wuint8. + Delimit Scope wuint8'_scope with wuint8'. + Section with_var. + Context (dummy : unit). + Definition wrap' := let __ := dummy in wrap. + Definition unwrap' := let __ := dummy in unwrap. + Numeral Notation wuint wrap' unwrap' : wuint8_scope. + Check let v := 0%wuint8 in v : wuint. + End with_var. + Check let v := 0%wuint8 in v : nat. + Fail Check let v := 0%wuint8 in v : wuint. + Compute wrap (Nat.to_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. + Check let v := 0%wuint8' in v : wuint. +End Test8. + +Module Test9. + Delimit Scope wuint9_scope with wuint9. + Delimit Scope wuint9'_scope with wuint9'. + Section with_let. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Numeral Notation wuint wrap' unwrap' : wuint9_scope. + Check let v := 0%wuint9 in v : wuint. + Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. + Check let v := 0%wuint9' in v : wuint. + End with_let. + Check let v := 0%wuint9 in v : nat. + Fail Check let v := 0%wuint9 in v : wuint. +End Test9. + +Module Test10. + (* Test that it is only a warning to add abstract after to an optional parsing function *) + Definition to_uint (v : unit) := Nat.to_uint 0. + Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Decimal.uint) := tt. + Delimit Scope unit_scope with unit. + Delimit Scope unit2_scope with unit2. + Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1). + Local Set Warnings Append "+abstract-large-number-no-op". + (* Check that there is actually a warning here *) + Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1). + (* Check that there is no warning here *) + Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). +End Test10. + +Module Test11. + (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) + Inductive unit11 := tt11. + Delimit Scope unit11_scope with unit11. + Goal True. + evar (to_uint : unit11 -> Decimal.uint). + evar (of_uint : Decimal.uint -> unit11). + Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + exact I. + Unshelve. + all: solve [ constructor ]. + Qed. +End Test11. + +Module Test12. + (* Test for numeral notations on context variables *) + Delimit Scope test12_scope with test12. + Section test12. + Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit). + + Numeral Notation unit of_uint to_uint : test12_scope. + Check let v := 1%test12 in v : unit. + End test12. +End Test12. + +Module Test13. + (* Test for numeral notations on notations which do not denote references *) + Delimit Scope test13_scope with test13. + Delimit Scope test13'_scope with test13'. + Delimit Scope test13''_scope with test13''. + Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint_good := to_uint tt. + Notation to_uint' := (to_uint tt). + Notation to_uint'' := (to_uint _). + Numeral Notation unit of_uint to_uint_good : test13_scope. + Check let v := 0%test13 in v : unit. + Fail Numeral Notation unit of_uint to_uint' : test13'_scope. + Fail Check let v := 0%test13' in v : unit. + Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. + Fail Check let v := 0%test13'' in v : unit. +End Test13. + +Module Test14. + (* Test that numeral notations follow [Import], not [Require], and + also test that [Local Numeral Notation]s do not escape modules + nor sections. *) + Delimit Scope test14_scope with test14. + Delimit Scope test14'_scope with test14'. + Delimit Scope test14''_scope with test14''. + Delimit Scope test14'''_scope with test14'''. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14_scope. + Global Numeral Notation unit of_uint to_uint : test14'_scope. + Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + End Inner. + Fail Check let v := 0%test14 in v : unit. + Fail Check let v := 0%test14' in v : unit. + Import Inner. + Fail Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + Section InnerSection. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14''_scope. + Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. + Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. + End InnerSection. + Fail Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. +End Test14. + +Module Test15. + (** Test module include *) + Delimit Scope test15_scope with test15. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Numeral Notation unit of_uint to_uint : test15_scope. + Check let v := 0%test15 in v : unit. + End Inner. + Module Inner2. + Include Inner. + Check let v := 0%test15 in v : unit. + End Inner2. + Import Inner Inner2. + Check let v := 0%test15 in v : unit. +End Test15. + +Module Test16. + (** Test functors *) + Delimit Scope test16_scope with test16. + Module Type A. + Axiom T : Set. + Axiom t : T. + End A. + Module F (a : A). + Inductive Foo := foo (_ : a.T). + Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : Foo := foo a.t. + Global Numeral Notation Foo of_uint to_uint : test16_scope. + Check let v := 0%test16 in v : Foo. + End F. + Module a <: A. + Definition T : Set := unit. + Definition t : T := tt. + End a. + Module Import f := F a. + (** Ideally this should work, but it should definitely not anomaly *) + Fail Check let v := 0%test16 in v : Foo. +End Test16. |