From 24ccc118ccfb4c1223cd37bd43c9d26a77851176 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 15 Mar 2017 03:11:23 +0100
Subject: 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.
---
 theories/Numbers/AltBinNotations.v | 68 ++++++++++++++++++++++++++++++++++++++
 theories/Numbers/BinNums.v         | 16 ++++-----
 2 files changed, 74 insertions(+), 10 deletions(-)
 create mode 100644 theories/Numbers/AltBinNotations.v

(limited to 'theories/Numbers')

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
-- 
cgit v1.2.3


From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 14 Jul 2018 06:25:22 -0400
Subject: Fix numeral notation for a rebase on top of master

Some of this code is cargo-culted or kludged to work.

As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter.  In
   this case, the function registration must be synchronized with the
   document state, but the functions should not be marshelled / stored
   in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
   In this case, the registration must be synchronized, and the function
   should be marshelled / stored in the .vo.

In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.

In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.

The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality.  For
plugins, a simple string suffices, as long as the string does not clash
between different plugins.  In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files.  Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.

----

Some of this code is response to comments on the PR

----

Some code is to fix an issue that bignums revealed:

Both Int31 and bignums registered numeral notations in int31_scope.  We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins.  This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).
---
 theories/Numbers/AltBinNotations.v | 45 +++++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 22 deletions(-)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index 595934ad89..c7e3999691 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -1,34 +1,35 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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]. *)
 
-(** Nowadays, literals in types [positive], [N], [Z] are parsed and
+(** 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. 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...
-*)
+    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.
 
-- 
cgit v1.2.3


From 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 11:03:29 -0400
Subject: Make Numeral Notation follow Import, not Require

Because that's the sane thing to do.

This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.

We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax.  Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.
---
 theories/Numbers/Cyclic/Int31/Cyclic31.v | 4 +---
 theories/Numbers/Cyclic/Int31/Int31.v    | 2 ++
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Numbers')

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
-- 
cgit v1.2.3