Numeral Notation for nat

 This parsing/printing method for nat should be just as fast as
 the previous dedicated code. Moreover, we could now parse large
 literals as nat numbers, by leaving them in a half-abstract form
 such as (Nat.of_uint 123456). This form is convertible to the
 closed (S (S (S ...))) form, so it shouldn't be a big deal for
 compatibility, except for if some Ltac stuff relies on (S ...) to be
 present after parsing. Of course, forcing the computation of
 a (Nat.of_uint ....) may take a while or raise a Stack Overflow.

2 files changed, 74 insertions, 10 deletions

diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
new file mode 100644
index 0000000000..595934ad89
--- /dev/null
+++ b/theories/Numbers/AltBinNotations.v
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Alternative Binary Numeral Notations *)
+
+(** Faster but less safe parsers and printers of [positive], [N], [Z]. *)
+
+(** Nowadays, literals in types [positive], [N], [Z] are parsed and
+    printed via the [Numeral Notation] command, by conversion from/to
+    the [Decimal.int] representation. This way, we do not need any
+    ML library of arbitrary precision integers (bigint.ml), hence
+    reducing the amount of ML code to trust during parsing and printing.
+    But this new method is slower than the older code, by a margin that
+    may become significant for literals of thousands of digits and more.
+    If that becomes a problem for your development, this file provides
+    some alternative [Numeral Notation] commmands that use [Z] as
+    bridge type : it hence relies on the bigint.ml library, the efficiency
+    should be almost the one of the legacy code, at the expense of a
+    larger ML trust base. To enable these commands, just be sure to
+    [Require] this file after the other files of
+
+    Please note anyway that literals above 10000 digits in [positive],
+    [N], [Z] will end up triggering Stack Overlow in various parts of
+    the Coq engine (type-checker, reduction, etc). So consider using
+    [BigN] or [BigZ] instead...
+*)
+
+Require Import BinNums.
+
+(** [positive] *)
+
+Definition pos_of_z z :=
+  match z with
+    | Zpos p => Some p
+    | _ => None
+  end.
+
+Definition pos_to_z p := Zpos p.
+
+Numeral Notation positive pos_of_z pos_to_z : positive_scope.
+
+(** [N] *)
+
+Definition n_of_z z :=
+  match z with
+    | Z0 => Some N0
+    | Zpos p => Some (Npos p)
+    | Zneg _ => None
+  end.
+
+Definition n_to_z n :=
+ match n with
+   | N0 => Z0
+   | Npos p => Zpos p
+ end.
+
+Numeral Notation N n_of_z n_to_z : N_scope.
+
+(** [Z] *)
+
+Definition z_of_z (z:Z) := z.
+
+Numeral Notation Z z_of_z z_of_z : Z_scope.
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index d5eb4f2681..3ba9d1f5ed 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -12,15 +12,11 @@
 
 Set Implicit Arguments.
 
-Declare ML Module "positive_syntax_plugin".
-Declare ML Module "n_syntax_plugin".
-Declare ML Module "z_syntax_plugin".
-
 (** [positive] is a datatype representing the strictly positive integers
    in a binary way. Starting from 1 (represented by [xH]), one can
    add a new least significant digit via [xO] (digit 0) or [xI] (digit 1).
-   Numbers in [positive] can also be denoted using a decimal notation;
-   e.g. [6%positive] abbreviates [xO (xI xH)] *)
+   Numbers in [positive] will also be denoted using a decimal notation;
+   e.g. [6%positive] will abbreviate [xO (xI xH)] *)
 
 Inductive positive : Set :=
   | xI : positive -> positive
@@ -34,8 +30,8 @@ Arguments xI _%positive.
 
 (** [N] is a datatype representing natural numbers in a binary way,
     by extending the [positive] datatype with a zero.
-    Numbers in [N] can also be denoted using a decimal notation;
-    e.g. [6%N] abbreviates [Npos (xO (xI xH))] *)
+    Numbers in [N] will also be denoted using a decimal notation;
+    e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *)
 
 Inductive N : Set :=
   | N0 : N
@@ -49,8 +45,8 @@ Arguments Npos _%positive.
     An integer is either zero or a strictly positive number
     (coded as a [positive]) or a strictly negative number
     (whose opposite is stored as a [positive] value).
-    Numbers in [Z] can also be denoted using a decimal notation;
-    e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *)
+    Numbers in [Z] will also be denoted using a decimal notation;
+    e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *)
 
 Inductive Z : Set :=
   | Z0 : Z