Merge PR #8064: Numeral notation (revisited again)

4 files changed, 78 insertions, 13 deletions

diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
new file mode 100644
index 0000000000..c7e3999691
--- /dev/null
+++ b/theories/Numbers/AltBinNotations.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * Alternative Binary Numeral Notations *)
+
+(** Faster but less safe parsers and printers of [positive], [N], [Z]. *)
+
+(** By default, literals in types [positive], [N], [Z] are parsed and
+    printed via the [Numeral Notation] command, by conversion from/to
+    the [Decimal.int] representation. When working with numbers with
+    thousands of digits and more, conversion from/to [Decimal.int] can
+    become significantly slow. If that becomes a problem for your
+    development, this file provides some alternative [Numeral
+    Notation] commmands that use [Z] as bridge type. To enable these
+    commands, just be sure to [Require] this file after other files
+    defining numeral notations.
+
+    Note: up to Coq 8.8, literals in types [positive], [N], [Z] were
+    parsed and printed using a native ML library of arbitrary
+    precision integers named bigint.ml. From 8.9, the default is to
+    parse and print using a Coq library converting sequences of
+    digits, hence reducing the amount of ML code to trust. But this
+    method is slower. This file then gives access to the legacy
+    method, trading efficiency against a larger ML trust base relying
+    on bigint.ml. *)
+
+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
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index bd4f0279d4..ec480bb1eb 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -23,8 +23,6 @@ Require Import Zpow_facts.
 Require Import CyclicAxioms.
 Require Import ROmega.
 
-Declare ML Module "int31_syntax_plugin".
-
 Local Open Scope nat_scope.
 Local Open Scope int31_scope.
 
@@ -128,7 +126,7 @@ Section Basics.
 
  Lemma nshiftl_S_tail :
   forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.
- Proof. 
+ Proof.
  intros n; elim n; simpl; intros; now f_equal.
  Qed.
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 9f8da831d8..39af62c32f 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,6 +15,8 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
+Declare ML Module "int31_syntax_plugin".
+
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer