Merge PR #8064: Numeral notation (revisited again)

16 files changed, 161 insertions, 26 deletions

diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 4142af05d2..578425bfb5 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,3 +9,17 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
+(** In Coq 8.9, prim token notations follow [Import] rather than
+    [Require].  So we make all of the relevant notations accessible in
+    compatibility mode. *)
+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.Int31.
+Declare ML Module "string_syntax_plugin".
+Declare ML Module "ascii_syntax_plugin".
+Declare ML Module "r_syntax_plugin".
+Declare ML Module "int31_syntax_plugin".
+Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope.
+Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope.
+Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope.
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/Decimal.v b/theories/Init/Decimal.v
index 57163b1b07..1ff00ec11c 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -42,10 +42,10 @@ Notation zero := (D0 Nil).
 
 Inductive int := Pos (d:uint) | Neg (d:uint).
 
-Delimit Scope uint_scope with uint.
-Bind Scope uint_scope with uint.
-Delimit Scope int_scope with int.
-Bind Scope int_scope with int.
+Delimit Scope dec_uint_scope with uint.
+Bind Scope dec_uint_scope with uint.
+Delimit Scope dec_int_scope with int.
+Bind Scope dec_int_scope with int.
 
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
@@ -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/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 802f18c0f2..6d98bcb34a 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,9 +19,24 @@ Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
-(* Initially available plugins
-   (+ nat_syntax_plugin loaded in Datatypes) *)
+(* Some initially available plugins. See also:
+   - ltac_plugin (in Notations)
+   - tauto_plugin (in 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%dec_uint_scope.
+Arguments Nat.of_int d%dec_int_scope.
+Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
+  : dec_uint_scope.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
+  : dec_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/BinNat.v b/theories/NArith/BinNat.v
index 5d3ec5abc7..bd27f94abd 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N.
 
 (** Exportation of notations *)
 
+Numeral Notation N N.of_uint N.to_uint : N_scope.
+
 Infix "+" := N.add : N_scope.
 Infix "-" := N.sub : N_scope.
 Infix "*" := N.mul : N_scope.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 5de75537cb..be12fffaaf 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 *)
 (**********************************************************************)
@@ -398,4 +402,9 @@ Definition to_uint n :=
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Numeral Notation N of_uint to_uint : N_scope.
+
 End N.
+
+(** Re-export the notation for those who just [Import NatIntDef] *)
+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..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
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 000d895e10..dcaae1606d 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive.
 
 (** Exportation of notations *)
 
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
+
 Infix "+" := Pos.add : positive_scope.
 Infix "-" := Pos.sub : positive_scope.
 Infix "*" := Pos.mul : positive_scope.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 070314746a..7f30733559 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)
@@ -614,4 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p).
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Numeral Notation positive of_int to_uint : positive_scope.
+
 End Pos.
+
+(** Re-export the notation for those who just [Import BinPosDef] *)
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index cf7397b57e..a11d491a8b 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z.
 
 (** Re-export Notations *)
 
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.
+
 Infix "+" := Z.add : Z_scope.
 Notation "- x" := (Z.opp x) : Z_scope.
 Infix "-" := Z.sub : Z_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index db4de0b90c..8cb62622db 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 *)
@@ -635,4 +639,9 @@ Definition lxor a b :=
    | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
  end.
 
+Numeral Notation Z of_int to_int : Z_scope.
+
 End Z.
+
+(** Re-export the notation for those who just [Import BinIntDef] *)
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.