Numeral Notation: allow parsing from/to Decimal.int or Decimal.uint

 This way, we could fully bypass bigint.ml.

 The previous mechanism of parsing/printing Z is kept for now.
 Currently, the conversion functions accepted by Numeral Notation foo
 may have the following types.

 for parsing:

   int -> foo
   int -> option foo
   uint -> foo
   uint -> option foo
   Z -> foo
   Z -> option foo

 for printing:

   foo -> int
   foo -> option int
   foo -> uint
   foo -> option uint
   foo -> Z
   foo -> option Z

 Notes:

  - The Declare ML Module is directly done in Prelude
  - When doing a Numeral Notation, having the Z datatype around
    isn't mandatory anymore (but the error messages suggest that
    it can still be used).
  - An option (abstract after ...) allows to keep large numbers in
    an abstract form such as (Nat.of_uint 123456) instead of reducing
    to (S (S (S ...))) and ending immediately with Stack Overflow.
  - After checking with Matthieu, there is now a explicit check
    and an error message in case of polymorphic inductive types

2 files changed, 16 insertions, 0 deletions

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 57163b1b07..34b4e75814 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -161,3 +161,9 @@ with succ_double d :=
   end.
 
 End Little.
+
+(** Pseudo-conversion functions used when declaring
+    Numeral Notations on [uint] and [int]. *)
+
+Definition uint_of_uint (i:uint) := i.
+Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 390ff5e240..f99a6a7c60 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -26,5 +26,15 @@ Require Export Coq.Init.Tauto.
 *)
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
+Declare ML Module "numeral_notation_plugin".
+
+(* Parsing / printing of decimal numbers *)
+Arguments Nat.of_uint d%uint_scope.
+Arguments Nat.of_int d%int_scope.
+Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
+  : uint_scope.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
+  : int_scope.
+
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".