From 6551f14196784e323688e682877229bc7f901659 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 9 Sep 2020 23:33:05 +0200 Subject: Rename Numeral Notation command to Number Notation Keep Numeral Notation wit a deprecation warning. --- test-suite/interactive/PrimNotation.v | 12 +- test-suite/output/Notations4.v | 2 +- test-suite/output/NumberNotations.out | 236 +++++++++++++ test-suite/output/NumberNotations.v | 489 +++++++++++++++++++++++++++ test-suite/output/NumeralNotations.out | 236 ------------- test-suite/output/NumeralNotations.v | 489 --------------------------- test-suite/output/ZSyntax.v | 2 +- test-suite/output/bug_12159.v | 4 +- test-suite/output/sint63Notation.v | 4 +- test-suite/success/NumeralNotationsNoLocal.v | 2 +- 10 files changed, 738 insertions(+), 738 deletions(-) create mode 100644 test-suite/output/NumberNotations.out create mode 100644 test-suite/output/NumberNotations.v delete mode 100644 test-suite/output/NumeralNotations.out delete mode 100644 test-suite/output/NumeralNotations.v (limited to 'test-suite') diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v index 07986b0df3..55116dc78b 100644 --- a/test-suite/interactive/PrimNotation.v +++ b/test-suite/interactive/PrimNotation.v @@ -21,7 +21,7 @@ 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. +Number 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. @@ -31,10 +31,10 @@ Module A. := 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. + Number 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. + Number Notation pcunit to_pcunit of_pcunit : punit_scope. Check let v := 0%punit in v : pcunit. End A. Reset A. @@ -44,7 +44,7 @@ Module A. 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. + Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. End A. Local Set Universe Polymorphism. @@ -52,7 +52,7 @@ 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. +Number 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. @@ -60,5 +60,5 @@ 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. +Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 73445bad12..6dadd8c7fe 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -131,7 +131,7 @@ Module NumeralNotations. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Numeral Notation myint63 of_int to_int : test17_scope. + Number Notation myint63 of_int to_int : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. End NumeralNotations. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out new file mode 100644 index 0000000000..8065c8d311 --- /dev/null +++ b/test-suite/output/NumberNotations.out @@ -0,0 +1,236 @@ +The command has indeed failed with message: +Unexpected term (nat -> nat) while parsing a numeral notation. +The command has indeed failed with message: +Unexpected non-option term opaque4 while parsing a numeral notation. +The command has indeed failed with message: +Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral +notation. +let v := 0%ppp in v : punit + : punit +let v := 0%ppp in v : punit + : punit +let v := 0%ppp in v : punit + : punit +let v := 0%ppp in v : punit + : punit +let v := 0%uto in v : unit + : unit +The command has indeed failed with message: +Cannot interpret this number as a value of type unit +The command has indeed failed with message: +Cannot interpret this number as a value of type unit +let v := 0%upp in v : unit + : unit +let v := 0%upp in v : unit + : unit +let v := 0%upp in v : unit + : unit +let v := 0%ppps in v : punit + : punit +File "stdin", line 91, characters 2-46: +Warning: To avoid stack overflow, large numbers in punit are interpreted as +applications of pto_punits. [abstract-large-number,numbers] +The command has indeed failed with message: +In environment +v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit +The term "v" has type "punit@{Set}" while it is expected to have type + "punit@{u}". +S + : nat -> nat +S (ack 4 4) + : nat +let v := 0%wnat in v : wnat + : wnat +0%wnat + : wnat +{| unwrap := ack 4 4 |} + : wnat +{| Test6.unwrap := 0 |} + : Test6.wnat +let v := 0%wnat in v : Test6.wnat + : Test6.wnat +let v := 0%wuint in v : wuint + : wuint +let v := 1%wuint in v : wuint + : wuint +let v := 0%wuint8 in v : wuint + : wuint +let v := 0 in v : nat + : nat +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "wuint". + = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |} + : wuint +let v := 0%wuint8' in v : wuint + : wuint +let v := 0%wuint9 in v : wuint + : wuint +let v := 0%wuint9' in v : wuint + : wuint +let v := 0 in v : nat + : nat +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "wuint". +File "stdin", line 203, characters 2-71: +Warning: The 'abstract after' directive has no effect when the parsing +function (of_uint) targets an option type. +[abstract-large-number-no-op,numbers] +The command has indeed failed with message: +The 'abstract after' directive has no effect when the parsing function +(of_uint) targets an option type. [abstract-large-number-no-op,numbers] +let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit + : unit +let v := 0%test13 in v : unit + : unit +The command has indeed failed with message: +to_uint' is bound to a notation that does not denote a reference. +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +to_uint'' is bound to a notation that does not denote a reference. +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +let v := 0%test14' in v : unit + : unit +let v := 0%test14' in v : unit + : unit +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +let v := 0%test14' in v : unit + : unit +The command has indeed failed with message: +This command does not support the Global option in sections. +let v := 0%test14'' in v : unit + : unit +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +let v := 0%test15 in v : unit + : unit +let v := 0%test15 in v : unit + : unit +let v := 0%test15 in v : unit + : unit +let v := foo a.t in v : Foo + : Foo +The command has indeed failed with message: +Cannot interpret in test16_scope because NumberNotations.Test16.F.Foo could not be found in the current environment. +let v := 0%test17 in v : myint63 + : myint63 +let v := 0%Q in v : Q + : Q +let v := 1%Q in v : Q + : Q +let v := 2%Q in v : Q + : Q +let v := 3%Q in v : Q + : Q +let v := 4%Q in v : Q + : Q + = (0, 1) + : nat * nat + = (1, 1) + : nat * nat + = (2, 1) + : nat * nat + = (3, 1) + : nat * nat + = (4, 1) + : nat * nat +let v := (-1)%Zlike in v : Zlike + : Zlike +let v := 0%Zlike in v : Zlike + : Zlike +let v := 1%Zlike in v : Zlike + : Zlike +let v := 2%Zlike in v : Zlike + : Zlike +let v := 3%Zlike in v : Zlike + : Zlike +let v := 4%Zlike in v : Zlike + : Zlike +2%Zlike + : Zlike +0%Zlike + : Zlike +let v := 0%kt in v : ty + : ty +let v := 1%kt in v : ty + : ty +let v := 2%kt in v : ty + : ty +let v := 3%kt in v : ty + : ty +let v := 4%kt in v : ty + : ty +let v := 5%kt in v : ty + : ty +The command has indeed failed with message: +Cannot interpret this number as a value of type ty + = 0%kt + : ty + = 1%kt + : ty + = 2%kt + : ty + = 3%kt + : ty + = 4%kt + : ty + = 5%kt + : ty +let v : ty := Build_ty Empty_set zero in v : ty + : ty +let v : ty := Build_ty unit one in v : ty + : ty +let v : ty := Build_ty bool two in v : ty + : ty +let v : ty := Build_ty Prop prop in v : ty + : ty +let v : ty := Build_ty Set set in v : ty + : ty +let v : ty := Build_ty Type type in v : ty + : ty +1 + : nat +(-1000)%Z + : Z +0 + : Prop ++0 + : bool +-0 + : bool +00 + : nat * nat +1000 + : Prop +1_000 + : list nat diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v new file mode 100644 index 0000000000..e411005da3 --- /dev/null +++ b/test-suite/output/NumberNotations.v @@ -0,0 +1,489 @@ +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +Declare Scope opaque_scope. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Number Notation Numeral.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 Numeral.int. + Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. + Number Notation Numeral.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Declare Scope silly_scope. + +Module Test3. + Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). + Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Number Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + +Module Test4. + Declare Scope opaque_scope. + Declare Scope silly_scope. + Declare Scope pto. + Declare Scope ppo. + Declare Scope ptp. + Declare Scope ppp. + Declare Scope uto. + Declare Scope upo. + Declare Scope utp. + Declare Scope upp. + Declare Scope ppps. + Polymorphic NonCumulative Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. + Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. + Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. + Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. + Number Notation punit to_punit of_punit : pto. + Number Notation punit pto_punit of_punit : ppo. + Number Notation punit to_punit pof_punit : ptp. + Number Notation punit pto_punit pof_punit : ppp. + Number 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. + Number Notation unit pto_unit of_unit : upo. + Number Notation unit to_unit pof_unit : utp. + Number 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}. + Number 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) : Numeral.uint := Nat.to_num_uint x. + Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x. + Module Export Scopes. + Declare Scope wnat_scope. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Number Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Set Printing Coercions. + 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 : Numeral.uint }. + Declare Scope wuint_scope. + Delimit Scope wuint_scope with wuint. + Number 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 : Numeral.uint }. + Declare Scope wuint8_scope. + Declare Scope wuint8'_scope. + 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. + Number 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_num_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Number Notation wuint wrap'' unwrap'' : wuint8'_scope. + Check let v := 0%wuint8' in v : wuint. +End Test8. + +Module Test9. + Declare Scope wuint9_scope. + Declare Scope wuint9'_scope. + Delimit Scope wuint9_scope with wuint9. + Delimit Scope wuint9'_scope with wuint9'. + Section with_let. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Numeral.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Number Notation wuint wrap' unwrap' : wuint9_scope. + Check let v := 0%wuint9 in v : wuint. + Number 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_num_uint 0. + Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Numeral.uint) := tt. + Declare Scope unit_scope. + Declare Scope unit2_scope. + Delimit Scope unit_scope with unit. + Delimit Scope unit2_scope with unit2. + Number 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 Number Notation unit of_uint to_uint : unit2_scope (abstract after 1). + (* Check that there is no warning here *) + Number Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). +End Test10. + +Module Test12. + (* Test for numeral notations on context variables *) + Declare Scope test12_scope. + Delimit Scope test12_scope with test12. + Section test12. + Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit). + + Number 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 *) + Declare Scope test13_scope. + Declare Scope test13'_scope. + Declare Scope test13''_scope. + Delimit Scope test13_scope with test13. + Delimit Scope test13'_scope with test13'. + Delimit Scope test13''_scope with test13''. + Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint_good := to_uint tt. + Notation to_uint' := (to_uint tt). + Notation to_uint'' := (to_uint _). + Number Notation unit of_uint to_uint_good : test13_scope. + Check let v := 0%test13 in v : unit. + Fail Number Notation unit of_uint to_uint' : test13'_scope. + Fail Check let v := 0%test13' in v : unit. + Fail Number 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 Number Notation]s do not escape modules + nor sections. *) + Declare Scope test14_scope. + Declare Scope test14'_scope. + Declare Scope test14''_scope. + Declare Scope test14'''_scope. + 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) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Local Number Notation unit of_uint to_uint : test14_scope. + Global Number 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) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Local Number Notation unit of_uint to_uint : test14''_scope. + Fail Global Number 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 *) + Declare Scope test15_scope. + Delimit Scope test15_scope with test15. + Module Inner. + Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Number 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 *) + Declare Scope test16_scope. + 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) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : Foo := foo a.t. + Global Number 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. + +Require Import Coq.Numbers.Cyclic.Int63.Int63. +Module Test17. + (** Test int63 *) + Declare Scope test17_scope. + Declare Scope test17_scope. + Delimit Scope test17_scope with test17. + Local Set Primitive Projections. + Record myint63 := of_int { to_int : int }. + Number Notation myint63 of_int to_int : test17_scope. + Check let v := 0%test17 in v : myint63. +End Test17. + +Module Test18. + (** Test https://github.com/coq/coq/issues/9840 *) + Record Q := { num : nat ; den : nat ; reduced : Nat.gcd num den = 1 }. + Declare Scope Q_scope. + Delimit Scope Q_scope with Q. + + Definition nat_eq_dec (x y : nat) : {x = y} + {x <> y}. + Proof. decide equality. Defined. + + Definition transparentify {A} (D : {A} + {not A}) (H : A) : A := + match D with + | left pf => pf + | right npf => match npf H with end + end. + + Axiom gcd_good : forall x, Nat.gcd x 1 = 1. + + Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}. + Definition nat_of_Q (x : Q) : option nat + := if Nat.eqb x.(den) 1 then Some (x.(num)) else None. + Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x). + Definition uint_of_Q (x : Q) : option Numeral.uint + := option_map Nat.to_num_uint (nat_of_Q x). + + Number Notation Q Q_of_uint uint_of_Q : Q_scope. + + Check let v := 0%Q in v : Q. + Check let v := 1%Q in v : Q. + Check let v := 2%Q in v : Q. + Check let v := 3%Q in v : Q. + Check let v := 4%Q in v : Q. + Compute let v := 0%Q in (num v, den v). + Compute let v := 1%Q in (num v, den v). + Compute let v := 2%Q in (num v, den v). + Compute let v := 3%Q in (num v, den v). + Compute let v := 4%Q in (num v, den v). +End Test18. + +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Module Test19. + (** Test another thing related to https://github.com/coq/coq/issues/9840 *) + Record Zlike := { summands : list Z }. + Declare Scope Zlike_scope. + Delimit Scope Zlike_scope with Zlike. + + Definition Z_of_Zlike (x : Zlike) := List.fold_right Z.add 0%Z (summands x). + Definition Zlike_of_Z (x : Z) := {| summands := cons x nil |}. + + Number Notation Zlike Zlike_of_Z Z_of_Zlike : Zlike_scope. + + Check let v := (-1)%Zlike in v : Zlike. + Check let v := 0%Zlike in v : Zlike. + Check let v := 1%Zlike in v : Zlike. + Check let v := 2%Zlike in v : Zlike. + Check let v := 3%Zlike in v : Zlike. + Check let v := 4%Zlike in v : Zlike. + Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}. + Check {| summands := nil |}. +End Test19. + +Module Test20. + (** Test Sorts *) + Local Set Universe Polymorphism. + Inductive known_type : Type -> Type := + | prop : known_type Prop + | set : known_type Set + | type : known_type Type + | zero : known_type Empty_set + | one : known_type unit + | two : known_type bool. + + Existing Class known_type. + Existing Instances zero one two prop. + Existing Instance set | 2. + Existing Instance type | 4. + + Record > ty := { t : Type ; kt : known_type t }. + + Definition ty_of_uint (x : Numeral.uint) : option ty + := match Nat.of_num_uint x with + | 0 => @Some ty zero + | 1 => @Some ty one + | 2 => @Some ty two + | 3 => @Some ty prop + | 4 => @Some ty set + | 5 => @Some ty type + | _ => None + end. + Definition uint_of_ty (x : ty) : Numeral.uint + := Nat.to_num_uint match kt x with + | prop => 3 + | set => 4 + | type => 5 + | zero => 0 + | one => 1 + | two => 2 + end. + + Declare Scope kt_scope. + Delimit Scope kt_scope with kt. + + Number Notation ty ty_of_uint uint_of_ty : kt_scope. + + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. + Fail Check let v := 6%kt in v : ty. + Eval cbv in (_ : known_type Empty_set) : ty. + Eval cbv in (_ : known_type unit) : ty. + Eval cbv in (_ : known_type bool) : ty. + Eval cbv in (_ : known_type Prop) : ty. + Eval cbv in (_ : known_type Set) : ty. + Eval cbv in (_ : known_type Type) : ty. + Local Set Printing All. + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. +End Test20. + +Module Test21. + + Check 00001. + Check (-1_000)%Z. + +End Test21. + +Module Test22. + +Notation "0" := False. +Notation "+0" := true. +Notation "-0" := false. +Notation "00" := (0%nat, 0%nat). +Check 0. +Check +0. +Check -0. +Check 00. + +Notation "1000" := True. +Notation "1_000" := (cons 1 nil). +Check 1000. +Check 1_000. + +(* To do: preserve parsing of -0: +Require Import ZArith. +Check (-0)%Z. +*) + +End Test22. diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out deleted file mode 100644 index 34c31ff8a6..0000000000 --- a/test-suite/output/NumeralNotations.out +++ /dev/null @@ -1,236 +0,0 @@ -The command has indeed failed with message: -Unexpected term (nat -> nat) while parsing a numeral notation. -The command has indeed failed with message: -Unexpected non-option term opaque4 while parsing a numeral notation. -The command has indeed failed with message: -Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral -notation. -let v := 0%ppp in v : punit - : punit -let v := 0%ppp in v : punit - : punit -let v := 0%ppp in v : punit - : punit -let v := 0%ppp in v : punit - : punit -let v := 0%uto in v : unit - : unit -The command has indeed failed with message: -Cannot interpret this number as a value of type unit -The command has indeed failed with message: -Cannot interpret this number as a value of type unit -let v := 0%upp in v : unit - : unit -let v := 0%upp in v : unit - : unit -let v := 0%upp in v : unit - : unit -let v := 0%ppps in v : punit - : punit -File "stdin", line 91, characters 2-46: -Warning: To avoid stack overflow, large numbers in punit are interpreted as -applications of pto_punits. [abstract-large-number,numbers] -The command has indeed failed with message: -In environment -v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit -The term "v" has type "punit@{Set}" while it is expected to have type - "punit@{u}". -S - : nat -> nat -S (ack 4 4) - : nat -let v := 0%wnat in v : wnat - : wnat -0%wnat - : wnat -{| unwrap := ack 4 4 |} - : wnat -{| Test6.unwrap := 0 |} - : Test6.wnat -let v := 0%wnat in v : Test6.wnat - : Test6.wnat -let v := 0%wuint in v : wuint - : wuint -let v := 1%wuint in v : wuint - : wuint -let v := 0%wuint8 in v : wuint - : wuint -let v := 0 in v : nat - : nat -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "wuint". - = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |} - : wuint -let v := 0%wuint8' in v : wuint - : wuint -let v := 0%wuint9 in v : wuint - : wuint -let v := 0%wuint9' in v : wuint - : wuint -let v := 0 in v : nat - : nat -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "wuint". -File "stdin", line 203, characters 2-72: -Warning: The 'abstract after' directive has no effect when the parsing -function (of_uint) targets an option type. -[abstract-large-number-no-op,numbers] -The command has indeed failed with message: -The 'abstract after' directive has no effect when the parsing function -(of_uint) targets an option type. [abstract-large-number-no-op,numbers] -let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit - : unit -let v := 0%test13 in v : unit - : unit -The command has indeed failed with message: -to_uint' is bound to a notation that does not denote a reference. -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -to_uint'' is bound to a notation that does not denote a reference. -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -let v := 0%test14' in v : unit - : unit -let v := 0%test14' in v : unit - : unit -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -let v := 0%test14' in v : unit - : unit -The command has indeed failed with message: -This command does not support the Global option in sections. -let v := 0%test14'' in v : unit - : unit -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -let v := 0%test15 in v : unit - : unit -let v := 0%test15 in v : unit - : unit -let v := 0%test15 in v : unit - : unit -let v := foo a.t in v : Foo - : Foo -The command has indeed failed with message: -Cannot interpret in test16_scope because NumeralNotations.Test16.F.Foo could not be found in the current environment. -let v := 0%test17 in v : myint63 - : myint63 -let v := 0%Q in v : Q - : Q -let v := 1%Q in v : Q - : Q -let v := 2%Q in v : Q - : Q -let v := 3%Q in v : Q - : Q -let v := 4%Q in v : Q - : Q - = (0, 1) - : nat * nat - = (1, 1) - : nat * nat - = (2, 1) - : nat * nat - = (3, 1) - : nat * nat - = (4, 1) - : nat * nat -let v := (-1)%Zlike in v : Zlike - : Zlike -let v := 0%Zlike in v : Zlike - : Zlike -let v := 1%Zlike in v : Zlike - : Zlike -let v := 2%Zlike in v : Zlike - : Zlike -let v := 3%Zlike in v : Zlike - : Zlike -let v := 4%Zlike in v : Zlike - : Zlike -2%Zlike - : Zlike -0%Zlike - : Zlike -let v := 0%kt in v : ty - : ty -let v := 1%kt in v : ty - : ty -let v := 2%kt in v : ty - : ty -let v := 3%kt in v : ty - : ty -let v := 4%kt in v : ty - : ty -let v := 5%kt in v : ty - : ty -The command has indeed failed with message: -Cannot interpret this number as a value of type ty - = 0%kt - : ty - = 1%kt - : ty - = 2%kt - : ty - = 3%kt - : ty - = 4%kt - : ty - = 5%kt - : ty -let v : ty := Build_ty Empty_set zero in v : ty - : ty -let v : ty := Build_ty unit one in v : ty - : ty -let v : ty := Build_ty bool two in v : ty - : ty -let v : ty := Build_ty Prop prop in v : ty - : ty -let v : ty := Build_ty Set set in v : ty - : ty -let v : ty := Build_ty Type type in v : ty - : ty -1 - : nat -(-1000)%Z - : Z -0 - : Prop -+0 - : bool --0 - : bool -00 - : nat * nat -1000 - : Prop -1_000 - : list nat diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v deleted file mode 100644 index ca8a14cce1..0000000000 --- a/test-suite/output/NumeralNotations.v +++ /dev/null @@ -1,489 +0,0 @@ -(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) - -Declare Scope opaque_scope. - -(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) -Module Test1. - Axiom hold : forall {A B C}, A -> B -> C. - Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). - Numeral Notation Numeral.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 Numeral.int. - Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. - Numeral Notation Numeral.int opaque6 opaque6 : opaque_scope. - Delimit Scope opaque_scope with opaque. - Open Scope opaque_scope. - Fail Check 1%opaque. -End Test2. - -Declare Scope silly_scope. - -Module Test3. - Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). - Definition to_silly (v : Numeral.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. - Declare Scope opaque_scope. - Declare Scope silly_scope. - Declare Scope pto. - Declare Scope ppo. - Declare Scope ptp. - Declare Scope ppp. - Declare Scope uto. - Declare Scope upo. - Declare Scope utp. - Declare Scope upp. - Declare Scope ppps. - Polymorphic NonCumulative Inductive punit := ptt. - Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt. - Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_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) : Numeral.uint := Nat.to_num_uint x. - Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x. - Module Export Scopes. - Declare Scope wnat_scope. - 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. - Set Printing Coercions. - 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 : Numeral.uint }. - Declare Scope wuint_scope. - 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 : Numeral.uint }. - Declare Scope wuint8_scope. - Declare Scope wuint8'_scope. - 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_num_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. - Declare Scope wuint9_scope. - Declare Scope wuint9'_scope. - Delimit Scope wuint9_scope with wuint9. - Delimit Scope wuint9'_scope with wuint9'. - Section with_let. - Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.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_num_uint 0. - Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_any_uint (v : Numeral.uint) := tt. - Declare Scope unit_scope. - Declare Scope unit2_scope. - 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 Test12. - (* Test for numeral notations on context variables *) - Declare Scope test12_scope. - Delimit Scope test12_scope with test12. - Section test12. - Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.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 *) - Declare Scope test13_scope. - Declare Scope test13'_scope. - Declare Scope test13''_scope. - Delimit Scope test13_scope with test13. - Delimit Scope test13'_scope with test13'. - Delimit Scope test13''_scope with test13''. - Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.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. *) - Declare Scope test14_scope. - Declare Scope test14'_scope. - Declare Scope test14''_scope. - Declare Scope test14'''_scope. - 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) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.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) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.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 *) - Declare Scope test15_scope. - Delimit Scope test15_scope with test15. - Module Inner. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.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 *) - Declare Scope test16_scope. - 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) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.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. - -Require Import Coq.Numbers.Cyclic.Int63.Int63. -Module Test17. - (** Test int63 *) - Declare Scope test17_scope. - Declare Scope test17_scope. - Delimit Scope test17_scope with test17. - Local Set Primitive Projections. - Record myint63 := of_int { to_int : int }. - Numeral Notation myint63 of_int to_int : test17_scope. - Check let v := 0%test17 in v : myint63. -End Test17. - -Module Test18. - (** Test https://github.com/coq/coq/issues/9840 *) - Record Q := { num : nat ; den : nat ; reduced : Nat.gcd num den = 1 }. - Declare Scope Q_scope. - Delimit Scope Q_scope with Q. - - Definition nat_eq_dec (x y : nat) : {x = y} + {x <> y}. - Proof. decide equality. Defined. - - Definition transparentify {A} (D : {A} + {not A}) (H : A) : A := - match D with - | left pf => pf - | right npf => match npf H with end - end. - - Axiom gcd_good : forall x, Nat.gcd x 1 = 1. - - Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}. - Definition nat_of_Q (x : Q) : option nat - := if Nat.eqb x.(den) 1 then Some (x.(num)) else None. - Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x). - Definition uint_of_Q (x : Q) : option Numeral.uint - := option_map Nat.to_num_uint (nat_of_Q x). - - Numeral Notation Q Q_of_uint uint_of_Q : Q_scope. - - Check let v := 0%Q in v : Q. - Check let v := 1%Q in v : Q. - Check let v := 2%Q in v : Q. - Check let v := 3%Q in v : Q. - Check let v := 4%Q in v : Q. - Compute let v := 0%Q in (num v, den v). - Compute let v := 1%Q in (num v, den v). - Compute let v := 2%Q in (num v, den v). - Compute let v := 3%Q in (num v, den v). - Compute let v := 4%Q in (num v, den v). -End Test18. - -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. -Module Test19. - (** Test another thing related to https://github.com/coq/coq/issues/9840 *) - Record Zlike := { summands : list Z }. - Declare Scope Zlike_scope. - Delimit Scope Zlike_scope with Zlike. - - Definition Z_of_Zlike (x : Zlike) := List.fold_right Z.add 0%Z (summands x). - Definition Zlike_of_Z (x : Z) := {| summands := cons x nil |}. - - Numeral Notation Zlike Zlike_of_Z Z_of_Zlike : Zlike_scope. - - Check let v := (-1)%Zlike in v : Zlike. - Check let v := 0%Zlike in v : Zlike. - Check let v := 1%Zlike in v : Zlike. - Check let v := 2%Zlike in v : Zlike. - Check let v := 3%Zlike in v : Zlike. - Check let v := 4%Zlike in v : Zlike. - Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}. - Check {| summands := nil |}. -End Test19. - -Module Test20. - (** Test Sorts *) - Local Set Universe Polymorphism. - Inductive known_type : Type -> Type := - | prop : known_type Prop - | set : known_type Set - | type : known_type Type - | zero : known_type Empty_set - | one : known_type unit - | two : known_type bool. - - Existing Class known_type. - Existing Instances zero one two prop. - Existing Instance set | 2. - Existing Instance type | 4. - - Record > ty := { t : Type ; kt : known_type t }. - - Definition ty_of_uint (x : Numeral.uint) : option ty - := match Nat.of_num_uint x with - | 0 => @Some ty zero - | 1 => @Some ty one - | 2 => @Some ty two - | 3 => @Some ty prop - | 4 => @Some ty set - | 5 => @Some ty type - | _ => None - end. - Definition uint_of_ty (x : ty) : Numeral.uint - := Nat.to_num_uint match kt x with - | prop => 3 - | set => 4 - | type => 5 - | zero => 0 - | one => 1 - | two => 2 - end. - - Declare Scope kt_scope. - Delimit Scope kt_scope with kt. - - Numeral Notation ty ty_of_uint uint_of_ty : kt_scope. - - Check let v := 0%kt in v : ty. - Check let v := 1%kt in v : ty. - Check let v := 2%kt in v : ty. - Check let v := 3%kt in v : ty. - Check let v := 4%kt in v : ty. - Check let v := 5%kt in v : ty. - Fail Check let v := 6%kt in v : ty. - Eval cbv in (_ : known_type Empty_set) : ty. - Eval cbv in (_ : known_type unit) : ty. - Eval cbv in (_ : known_type bool) : ty. - Eval cbv in (_ : known_type Prop) : ty. - Eval cbv in (_ : known_type Set) : ty. - Eval cbv in (_ : known_type Type) : ty. - Local Set Printing All. - Check let v := 0%kt in v : ty. - Check let v := 1%kt in v : ty. - Check let v := 2%kt in v : ty. - Check let v := 3%kt in v : ty. - Check let v := 4%kt in v : ty. - Check let v := 5%kt in v : ty. -End Test20. - -Module Test21. - - Check 00001. - Check (-1_000)%Z. - -End Test21. - -Module Test22. - -Notation "0" := False. -Notation "+0" := true. -Notation "-0" := false. -Notation "00" := (0%nat, 0%nat). -Check 0. -Check +0. -Check -0. -Check 00. - -Notation "1000" := True. -Notation "1_000" := (cons 1 nil). -Check 1000. -Check 1_000. - -(* To do: preserve parsing of -0: -Require Import ZArith. -Check (-0)%Z. -*) - -End Test22. diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index be9dc543d6..7b2bb00ce0 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -19,7 +19,7 @@ Check (0 + Z.of_nat 11)%Z. (* Check hexadecimal printing *) Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n). -Numeral Notation Z Z.of_num_int to_num_int : Z_scope. +Number Notation Z Z.of_num_int to_num_int : Z_scope. Check 42%Z. Check (-42)%Z. Check 0%Z. diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v index 6ea90eab29..437b4a68e9 100644 --- a/test-suite/output/bug_12159.v +++ b/test-suite/output/bug_12159.v @@ -6,8 +6,8 @@ Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1. -Numeral Notation unit to_unit of_unit : A. -Numeral Notation unit to_unit of_unit' : B. +Number Notation unit to_unit of_unit : A. +Number Notation unit to_unit of_unit' : B. Definition f x : unit := x. Check f tt. Arguments f x%A. diff --git a/test-suite/output/sint63Notation.v b/test-suite/output/sint63Notation.v index 331d74ed3d..66ffbf2278 100644 --- a/test-suite/output/sint63Notation.v +++ b/test-suite/output/sint63Notation.v @@ -18,8 +18,8 @@ Definition as_signed (bw : Z) (v : Z) := (((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z. Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)). -Numeral Notation uint uof_Z uto_Z : uint_scope. -Numeral Notation sint sof_Z sto_Z : sint_scope. +Number Notation uint uof_Z uto_Z : uint_scope. +Number Notation sint sof_Z sto_Z : sint_scope. Open Scope uint_scope. Compute uof_Z 0. Compute uof_Z 1. diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumeralNotationsNoLocal.v index ea3907ef8a..fe97f10ddf 100644 --- a/test-suite/success/NumeralNotationsNoLocal.v +++ b/test-suite/success/NumeralNotationsNoLocal.v @@ -5,7 +5,7 @@ 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. + Fail Number Notation unit11 of_uint to_uint : uint11_scope. exact I. Unshelve. all: solve [ constructor ]. -- cgit v1.2.3