Merge PR #8064: Numeral notation (revisited again)

6 files changed, 398 insertions, 8 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/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/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/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.