Add hexadecimal numerals

We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?

This is unfortunately a rather large commit. I suggest reading it in
the following order:

* test-suite/output/ZSyntax.{v,out}       new test
* test-suite/output/Int63Syntax.{v,out}   ''
* test-suite/output/QArithSyntax.{v,out}  ''
* test-suite/output/RealSyntax.{v,out}    ''
* test-suite/output/FloatSyntax.{v,out}   ''

* interp/numTok.ml{i,}  extending numeral tokens

* theories/Init/Hexadecimal.v  adaptation of Decimal.v
                               for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v  new interface for Numeral Notation (basically,
                           a numeral is either a decimal or an hexadecimal)

* theories/Init/Nat.v            add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v    ''                                  positive
* theories/ZArith/BinIntDef.v    ''                                  Z
* theories/NArith/BinNatDef.v    ''                                  N
* theories/QArith/QArith_base.v  ''                                  Q

* interp/notation.ml{i,}     adapting implementation of numeral notations
* plugins/syntax/numeral.ml  ''

* plugins/syntax/r_syntax.ml  adapt parser for real numbers

* plugins/syntax/float_syntax.ml  adapt parser for primitive floats

* theories/Init/Prelude.v  register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
  and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
  had to be permuted)

1 files changed, 34 insertions, 14 deletions

diff --git a/interp/numTok.mli b/interp/numTok.mli
index c48fad908d..11d5a0f980 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -11,7 +11,7 @@
 (** Numerals in different forms: signed or unsigned, possibly with
     fractional part and exponent.
 
-    Numerals are represented using raw strings of decimal
+    Numerals are represented using raw strings of (hexa)decimal
     literals and a separate sign flag.
 
     Note that this representation is not unique, due to possible
@@ -25,21 +25,29 @@
 
 type sign = SPlus | SMinus
 
+type num_class = CDec | CHex
+
+type 'a exp = EDec of 'a | EBin of 'a
+
 (** {6 String representation of a natural number } *)
 
 module UnsignedNat :
 sig
   type t
   val of_string : string -> t
-    (** Convert from a non-empty sequence of digits (which may contain "_") *)
+    (** Convert from a non-empty sequence of digits (which may contain "_")
+        (or hexdigits when starting with "0x" or "0X") *)
 
   val to_string : t -> string
-    (** Convert to a non-empty sequence of digit that does not contain "_" *)
+    (** Convert to a non-empty sequence of digit that does not contain "_"
+        (or hexdigits, starting with "0x", all hexdigits are lower case) *)
 
   val sprint : t -> string
   val print : t -> Pp.t
     (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
 
+  val classify : t -> num_class
+
   val compare : t -> t -> int
 end
 
@@ -49,12 +57,15 @@ module SignedNat :
 sig
   type t = sign * UnsignedNat.t
   val of_string : string -> t
-    (** Convert from a non-empty sequence of digits which may contain "_" *)
+    (** Convert from a non-empty sequence of (hex)digits which may contain "_" *)
 
   val to_string : t -> string
-    (** Convert to a non-empty sequence of digit that does not contain "_" *)
+    (** Convert to a non-empty sequence of (hex)digit that does not contain "_"
+        (hexadecimals start with "0x" and all hexdigits are lower case) *)
 
-  val of_bigint : Bigint.bigint -> t
+  val classify : t -> num_class
+
+  val of_bigint : num_class -> Bigint.bigint -> t
   val to_bigint : t -> Bigint.bigint
 end
 
@@ -78,11 +89,17 @@ sig
 
         The recognized syntax is:
         - integer part: \[0-9\]\[0-9_\]*
-        - decimal part: empty or .\[0-9_\]+
-        - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+        - fractional part: empty or .\[0-9_\]+
+        - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]*
+        or
+        - integer part: 0\[xX\]\[0-9a-fA-F\]\[0-9a-fA-F_\]*
+        - fractional part: empty or .\[0-9a-fA-F_\]+
+        - exponent part: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
 
   val parse_string : string -> t option
-    (** Parse the string as a positive Coq numeral, if possible *)
+    (** Parse the string as a non negative Coq numeral, if possible *)
+
+  val classify : t -> num_class
 
 end
 
@@ -114,17 +131,20 @@ sig
   val to_string : t -> string
     (** Returns a string in the syntax of OCaml's float_of_string *)
 
-  val of_bigint : Bigint.bigint -> t
+  val of_bigint : num_class -> Bigint.bigint -> t
   val to_bigint : t -> Bigint.bigint option
     (** Convert from and to bigint when the denotation of a bigint *)
 
   val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
   val to_int_frac_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option
-    (** n, p and q such that the number is n.p*10^q *)
+    (** n, p and q such that the number is n.p*10^q or n.p*2^q
+        pre/postcondition: classify n = classify p, classify q = CDec *)
+
+  val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t
+  val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp
+    (** n and p such that the number is n*10^p or n*2^p *)
 
-  val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t
-  val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint
-    (** n and p such that the number is n*10^p *)
+  val classify : t -> num_class
 
   val is_bigger_int_than : t -> UnsignedNat.t -> bool
     (** Test if an integer whose absolute value is bounded *)