From 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 19 Oct 2018 13:16:25 +0200
Subject: Replace type sign = bool with SPlus | SMinus

---
 interp/constrexpr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 757d186c8b..f3d0888fee 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -53,11 +53,11 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
     sign flag. Note that this representation is not unique, due to possible
     multiple leading zeros, and -0 = +0 *)
 
-type sign = bool
+type sign = SPlus | SMinus
 type raw_natural_number = string
 
 type prim_token =
-  | Numeral of raw_natural_number * sign
+  | Numeral of sign * raw_natural_number
   | String of string
 
 type instance_expr = Glob_term.glob_level list
-- 
cgit v1.2.3


From 4dc3d04d0812005f221e88744c587de8ef0f38ee Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 15:10:54 +0200
Subject: Rename raw_natural_number to raw_numeral

In anticipation of an extension from natural numbers to other numeral
constants.
---
 interp/constrexpr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index f3d0888fee..fa19eb8ec4 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -54,10 +54,10 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
     multiple leading zeros, and -0 = +0 *)
 
 type sign = SPlus | SMinus
-type raw_natural_number = string
+type raw_numeral = string
 
 type prim_token =
-  | Numeral of sign * raw_natural_number
+  | Numeral of sign * raw_numeral
   | String of string
 
 type instance_expr = Glob_term.glob_level list
-- 
cgit v1.2.3


From 552bb5aba750785d8f19aa7b333baa59e9199369 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 14:40:23 +0200
Subject: Add parsing of decimal constants (e.g., 1.02e+01)

Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.

This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`

See examples of each use case in the next two commits.
---
 interp/constrexpr.ml | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index fa19eb8ec4..7a14a4e708 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -48,13 +48,23 @@ type abstraction_kind = AbsLambda | AbsPi
 
 type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
-(** Representation of integer literals that appear in Coq scripts.
-    We now use raw strings of digits in base 10 (big-endian), and a separate
-    sign flag. Note that this representation is not unique, due to possible
-    multiple leading zeros, and -0 = +0 *)
+(** Representation of decimal literals that appear in Coq scripts.
+   We now use raw strings following the format defined by
+   [NumTok.t] and a separate sign flag.
+
+   Note that this representation is not unique, due to possible
+   multiple leading or trailing zeros, and -0 = +0, for instances.
+   The reason to keep the numeral exactly as it was parsed is that
+   specific notations can be declared for specific numerals
+   (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
+   [Notation "2e1" := ...]). Those notations, which override the
+   generic interpretation as numeral, use the same representation of
+   numeral using the Numeral constructor. So the latter should be able
+   to record the form of the numeral which exactly matches the
+   notation. *)
 
 type sign = SPlus | SMinus
-type raw_numeral = string
+type raw_numeral = NumTok.t
 
 type prim_token =
   | Numeral of sign * raw_numeral
-- 
cgit v1.2.3