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.

10 files changed, 105 insertions, 18 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index f448248468..0fa42cadad 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -226,6 +226,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
     theories/Numbers/NaryFunctions.v
+    theories/Numbers/AltBinNotations.v
     theories/Numbers/DecimalFacts.v
     theories/Numbers/DecimalNat.v
     theories/Numbers/DecimalPos.v
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 05b741f0ac..1e6843d511 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -12,7 +12,6 @@ Set Implicit Arguments.
 
 Require Import Notations.
 Require Import Logic.
-Declare ML Module "nat_syntax_plugin".
 
 (********************************************************************)
 (** * Datatypes with zero and one element *)
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index ad1bc717c4..eb4ba0e5e6 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -24,6 +24,10 @@ Definition t := nat.
 
 (** ** Constants *)
 
+Local Notation "0" := O.
+Local Notation "1" := (S O).
+Local Notation "2" := (S (S O)).
+
 Definition zero := 0.
 Definition one := 1.
 Definition two := 2.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index d5322d0945..65e5e76a22 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -31,6 +31,7 @@ Require Import Logic.
 Require Coq.Init.Nat.
 
 Open Scope nat_scope.
+Local Notation "0" := O.
 
 Definition eq_S := f_equal S.
 Definition f_equal_nat := f_equal (A:=nat).
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index f99a6a7c60..e8997d30b8 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -21,7 +21,6 @@ Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
 (* Some initially available plugins. See also:
    - ltac_plugin (in Notations)
-   - nat_syntax_plugin (in Datatypes)
    - tauto_plugin (in Tauto).
 *)
 Declare ML Module "cc_plugin".
@@ -36,5 +35,8 @@ Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
 Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
   : int_scope.
 
+(* Parsing / printing of [nat] numbers *)
+Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
+
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 5de75537cb..8bbecf9acb 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -13,6 +13,10 @@ Require Import BinPos.
 
 Local Open Scope N_scope.
 
+Local Notation "0" := N0.
+Local Notation "1" := (Npos 1).
+Local Notation "2" := (Npos 2).
+
 (**********************************************************************)
 (** * Binary natural numbers, definitions of operations *)
 (**********************************************************************)
@@ -399,3 +403,5 @@ Definition to_uint n :=
 Definition to_int n := Decimal.Pos (to_uint n).
 
 End N.
+
+Numeral Notation N N.of_uint N.to_uint : N_scope.
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
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 070314746a..39b609e9dd 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -26,6 +26,8 @@ Require Export BinNums.
     for the number 6 (which is 110 in binary notation).
 *)
 
+Local Notation "1" := xH.
+
 Notation "p ~ 1" := (xI p)
  (at level 7, left associativity, format "p '~' '1'") : positive_scope.
 Notation "p ~ 0" := (xO p)
@@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p :=
     let r' := g (f r) in
     if s' <=? r' then (s~1, sub_mask r' s')
     else (s~0, IsPos r')
-  | (s,_)  => (s~0, sub_mask (g (f 1)) 4)
+  | (s,_)  => (s~0, sub_mask (g (f 1)) 1~0~0)
  end.
 
 Fixpoint sqrtrem p : positive * mask :=
  match p with
   | 1 => (1,IsNul)
-  | 2 => (1,IsPos 1)
-  | 3 => (1,IsPos 2)
+  | 1~0 => (1,IsPos 1)
+  | 1~1 => (1,IsPos 1~0)
   | p~0~0 => sqrtrem_step xO xO (sqrtrem p)
   | p~0~1 => sqrtrem_step xO xI (sqrtrem p)
   | p~1~0 => sqrtrem_step xI xO (sqrtrem p)
@@ -615,3 +617,5 @@ Definition to_uint p := Decimal.rev (to_little_uint p).
 Definition to_int n := Decimal.Pos (to_uint n).
 
 End Pos.
+
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index db4de0b90c..8abcd15700 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -14,6 +14,10 @@ Require Import BinPos BinNat.
 
 Local Open Scope Z_scope.
 
+Local Notation "0" := Z0.
+Local Notation "1" := (Zpos 1).
+Local Notation "2" := (Zpos 2).
+
 (***********************************************************)
 (** * Binary Integers, Definitions of Operations *)
 (***********************************************************)
@@ -53,7 +57,7 @@ Definition succ_double x :=
 
 Definition pred_double x :=
   match x with
-    | 0 => -1
+    | 0 => neg 1
     | neg p => neg p~1
     | pos p => pos (Pos.pred_double p)
   end.
@@ -104,7 +108,7 @@ Definition succ x := x + 1.
 
 (** ** Predecessor *)
 
-Definition pred x := x + -1.
+Definition pred x := x + neg 1.
 
 (** ** Subtraction *)
 
@@ -171,7 +175,7 @@ Definition sgn z :=
   match z with
     | 0 => 0
     | pos p => 1
-    | neg p => -1
+    | neg p => neg 1
   end.
 
 (** Boolean equality and comparisons *)
@@ -636,3 +640,5 @@ Definition lxor a b :=
  end.
 
 End Z.
+
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.