Merge PR #11948: Hexadecimal numerals

Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin

6 files changed, 339 insertions, 108 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d6097304ec..a8fb5a3f45 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -15,8 +15,8 @@ open Nameops
 open Libnames
 open Namegen
 open Glob_term
-open Constrexpr
 open Notation
+open Constrexpr
 
 (***********************)
 (* For binders parsing *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d5a5bde616..3f7bb6e330 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -19,13 +19,13 @@ open Libnames
 open Namegen
 open Impargs
 open CAst
+open Notation
 open Constrexpr
 open Constrexpr_ops
 open Notation_ops
 open Glob_term
 open Glob_ops
 open Pattern
-open Notation
 open Detyping
 
 module NamedDecl = Context.Named.Declaration
diff --git a/interp/notation.ml b/interp/notation.ml
index fb3cefd624..3f13476355 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -382,7 +382,7 @@ module InnerPrimToken = struct
     | _ -> false
 
   let mkNumeral n =
-    Numeral (NumTok.Signed.of_bigint n)
+    Numeral (NumTok.Signed.of_bigint CDec n)
 
   let mkString = function
     | None -> None
@@ -423,23 +423,32 @@ type numnot_option =
   | Abstract of NumTok.UnsignedNat.t
 
 type int_ty =
-  { uint : Names.inductive;
+  { dec_uint : Names.inductive;
+    dec_int : Names.inductive;
+    hex_uint : Names.inductive;
+    hex_int : Names.inductive;
+    uint : Names.inductive;
     int : Names.inductive }
 
 type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
-type decimal_ty =
+type numeral_ty =
   { int : int_ty;
-    decimal : Names.inductive }
+    decimal : Names.inductive;
+    hexadecimal : Names.inductive;
+    numeral : Names.inductive }
 
 type target_kind =
-  | Int of int_ty (* Coq.Init.Decimal.int + uint *)
-  | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+  | Int of int_ty (* Coq.Init.Numeral.int + uint *)
+  | UInt of int_ty (* Coq.Init.Numeral.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
-  | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
+  | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+  | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
+  | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
+  | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
@@ -601,17 +610,23 @@ let warn_abstract_large_num =
 (** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
 
 let digit_of_char c =
-  assert ('0' <= c && c <= '9');
-  Char.code c - Char.code '0' + 2
+  assert ('0' <= c && c <= '9' || 'a' <= c && c <= 'f');
+  if c <= '9' then Char.code c - Char.code '0' + 2
+  else Char.code c - Char.code 'a' + 12
 
 let char_of_digit n =
-  assert (2<=n && n<=11);
-  Char.chr (n-2 + Char.code '0')
+  assert (2<=n && n<=17);
+  if n <= 11 then Char.chr (n-2 + Char.code '0')
+  else Char.chr (n-12 + Char.code 'a')
 
-let coquint_of_rawnum uint n =
+let coquint_of_rawnum inds c n =
+  let uint = match c with CDec -> inds.dec_uint | CHex -> inds.hex_uint in
   let nil = mkConstruct (uint,1) in
   match n with None -> nil | Some n ->
   let str = NumTok.UnsignedNat.to_string n in
+  let str = match c with
+    | CDec -> str
+    | CHex -> String.sub str 2 (String.length str - 2) in  (* cut "0x" *)
   let rec do_chars s i acc =
     if i < 0 then acc
     else
@@ -620,61 +635,126 @@ let coquint_of_rawnum uint n =
   in
   do_chars str (String.length str - 1) nil
 
-let coqint_of_rawnum inds (sign,n) =
-  let uint = coquint_of_rawnum inds.uint (Some n) in
+let coqint_of_rawnum inds c (sign,n) =
+  let ind = match c with CDec -> inds.dec_int | CHex -> inds.hex_int in
+  let uint = coquint_of_rawnum inds c (Some n) in
   let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
-  mkApp (mkConstruct (inds.int, pos_neg), [|uint|])
+  mkApp (mkConstruct (ind, pos_neg), [|uint|])
 
-let coqdecimal_of_rawnum inds n =
-  let i, f, e = NumTok.Signed.to_decimal_and_exponent n in
-  let i = coqint_of_rawnum inds.int i in
-  let f = coquint_of_rawnum inds.int.uint f in
+let coqnumeral_of_rawnum inds c n =
+  let ind = match c with CDec -> inds.decimal | CHex -> inds.hexadecimal in
+  let i, f, e = NumTok.Signed.to_int_frac_and_exponent n in
+  let i = coqint_of_rawnum inds.int c i in
+  let f = coquint_of_rawnum inds.int c f in
   match e with
-  | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|])  (* Decimal *)
+  | None -> mkApp (mkConstruct (ind, 1), [|i; f|])  (* (D|Hexad)ecimal *)
   | Some e ->
-    let e = coqint_of_rawnum inds.int e in
-    mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|])  (* DecimalExp *)
+    let e = coqint_of_rawnum inds.int CDec e in
+    mkApp (mkConstruct (ind, 2), [|i; f; e|])  (* (D|Hexad)ecimalExp *)
 
-let rawnum_of_coquint c =
+let mkDecHex ind c n = match c with
+  | CDec -> mkApp (mkConstruct (ind, 1), [|n|])  (* (UInt|Int|)Dec *)
+  | CHex -> mkApp (mkConstruct (ind, 2), [|n|])  (* (UInt|Int|)Hex *)
+
+exception NonDecimal
+
+let decimal_coqnumeral_of_rawnum inds n =
+  if NumTok.Signed.classify n <> CDec then raise NonDecimal;
+  coqnumeral_of_rawnum inds CDec n
+
+let coqnumeral_of_rawnum inds n =
+  let c = NumTok.Signed.classify n in
+  let n = coqnumeral_of_rawnum inds c n in
+  mkDecHex inds.numeral c n
+
+let decimal_coquint_of_rawnum inds n =
+  if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
+  coquint_of_rawnum inds CDec (Some n)
+
+let coquint_of_rawnum inds n =
+  let c = NumTok.UnsignedNat.classify n in
+  let n = coquint_of_rawnum inds c (Some n) in
+  mkDecHex inds.uint c n
+
+let decimal_coqint_of_rawnum inds n =
+  if NumTok.SignedNat.classify n <> CDec then raise NonDecimal;
+  coqint_of_rawnum inds CDec n
+
+let coqint_of_rawnum inds n =
+  let c = NumTok.SignedNat.classify n in
+  let n = coqint_of_rawnum inds c n in
+  mkDecHex inds.int c n
+
+let rawnum_of_coquint cl c =
   let rec of_uint_loop c buf =
     match Constr.kind c with
     | Construct ((_,1), _) (* Nil *) -> ()
     | App (c, [|a|]) ->
        (match Constr.kind c with
-        | Construct ((_,n), _) (* D0 to D9 *) ->
+        | Construct ((_,n), _) (* D0 to Df *) ->
            let () = Buffer.add_char buf (char_of_digit n) in
            of_uint_loop a buf
         | _ -> raise NotAValidPrimToken)
     | _ -> raise NotAValidPrimToken
   in
   let buf = Buffer.create 64 in
+  if cl = CHex then (Buffer.add_char buf '0'; Buffer.add_char buf 'x');
   let () = of_uint_loop c buf in
-  if Int.equal (Buffer.length buf) 0 then
+  if Int.equal (Buffer.length buf) (match cl with CDec -> 0 | CHex -> 2) then
     (* To avoid ambiguities between Nil and (D0 Nil), we choose
        to not display Nil alone as "0" *)
     raise NotAValidPrimToken
   else NumTok.UnsignedNat.of_string (Buffer.contents buf)
 
-let rawnum_of_coqint c =
+let rawnum_of_coqint cl c =
   match Constr.kind c with
   | App (c,[|c'|]) ->
      (match Constr.kind c with
-      | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c')
-      | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint c')
+      | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint cl c')
+      | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint cl c')
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
-let rawnum_of_decimal c =
+let rawnum_of_coqnumeral cl c =
   let of_ife i f e =
-    let n = rawnum_of_coqint i in
-    let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in
-    let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in
-    NumTok.Signed.of_decimal_and_exponent n f e in
+    let n = rawnum_of_coqint cl i in
+    let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in
+    let e = match e with None -> None | Some e -> Some (rawnum_of_coqint CDec e) in
+    NumTok.Signed.of_int_frac_and_exponent n f e in
   match Constr.kind c with
   | App (_,[|i; f|]) -> of_ife i f None
   | App (_,[|i; f; e|]) -> of_ife i f (Some e)
   | _ -> raise NotAValidPrimToken
 
+let destDecHex c = match Constr.kind c with
+  | App (c,[|c'|]) ->
+     (match Constr.kind c with
+      | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c'
+      | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c'
+      | _ -> raise NotAValidPrimToken)
+  | _ -> raise NotAValidPrimToken
+
+let decimal_rawnum_of_coqnumeral c =
+  rawnum_of_coqnumeral CDec c
+
+let rawnum_of_coqnumeral c =
+  let cl, c = destDecHex c in
+  rawnum_of_coqnumeral cl c
+
+let decimal_rawnum_of_coquint c =
+  rawnum_of_coquint CDec c
+
+let rawnum_of_coquint c =
+  let cl, c = destDecHex c in
+  rawnum_of_coquint cl c
+
+let decimal_rawnum_of_coqint c =
+  rawnum_of_coqint CDec c
+
+let rawnum_of_coqint c =
+  let cl, c = destDecHex c in
+  rawnum_of_coqint cl c
+
 (***********************************************************************)
 
 (** ** Conversion between Coq [Z] and internal bigint *)
@@ -768,15 +848,24 @@ let interp o ?loc n =
   let c = match fst o.to_kind, NumTok.Signed.to_int n with
     | Int int_ty, Some n ->
        coqint_of_rawnum int_ty n
-    | UInt uint_ty, Some (SPlus, n) ->
-       coquint_of_rawnum uint_ty (Some n)
+    | UInt int_ty, Some (SPlus, n) ->
+       coquint_of_rawnum int_ty n
+    | DecimalInt int_ty, Some n ->
+       (try decimal_coqint_of_rawnum int_ty n
+        with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
+    | DecimalUInt int_ty, Some (SPlus, n) ->
+       (try decimal_coquint_of_rawnum int_ty n
+        with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
     | Z z_pos_ty, Some n ->
        z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
     | Int63, Some n ->
        interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
-    | (Int _ | UInt _ | Z _ | Int63), _ ->
+    | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
        no_such_prim_token "number" ?loc o.ty_name
-    | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty n
+    | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n
+    | Decimal numeral_ty, _ ->
+       (try decimal_coqnumeral_of_rawnum numeral_ty n
+        with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
   in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -797,9 +886,12 @@ let uninterp o n =
     begin function
       | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c)
       | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
-      | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c)
-      | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c)
-      | (Decimal _, c) -> rawnum_of_decimal c
+      | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
+      | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c)
+      | (Numeral _, c) -> rawnum_of_coqnumeral c
+      | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
+      | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
+      | (Decimal _, c) -> decimal_rawnum_of_coqnumeral c
     end o n
 end
 
@@ -1126,8 +1218,8 @@ let find_notation ntn sc =
   NotationMap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
-  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
-  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
+  | Constrexpr.Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
+  | Constrexpr.Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -1333,14 +1425,14 @@ let availability_of_prim_token n printer_scope local_scopes =
       let uid = snd (String.Map.find scope !prim_token_interp_infos) in
       let open InnerPrimToken in
       match n, uid with
-      | Numeral _, NumeralNotation _ -> true
+      | Constrexpr.Numeral _, NumeralNotation _ -> true
       | _, NumeralNotation _ -> false
       | String _, StringNotation _ -> true
       | _, StringNotation _ -> false
       | _, Uid uid ->
         let interp = Hashtbl.find prim_token_interpreters uid in
         match n, interp with
-        | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+        | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
         | String _, StringInterp _ -> true
         | _ -> false
     with Not_found -> false
diff --git a/interp/notation.mli b/interp/notation.mli
index 96a76c4de6..e7e917463b 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -74,7 +74,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
 
-(** A numeral interpreter is the pair of an interpreter for **decimal**
+(** A numeral interpreter is the pair of an interpreter for **(hexa)decimal**
    numbers in terms and an optional interpreter in pattern, if
    non integer or negative numbers are not supported, the interpreter
    must fail with an appropriate error message *)
@@ -120,23 +120,32 @@ type numnot_option =
   | Abstract of NumTok.UnsignedNat.t
 
 type int_ty =
-  { uint : Names.inductive;
+  { dec_uint : Names.inductive;
+    dec_int : Names.inductive;
+    hex_uint : Names.inductive;
+    hex_int : Names.inductive;
+    uint : Names.inductive;
     int : Names.inductive }
 
 type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
-type decimal_ty =
+type numeral_ty =
   { int : int_ty;
-    decimal : Names.inductive }
+    decimal : Names.inductive;
+    hexadecimal : Names.inductive;
+    numeral : Names.inductive }
 
 type target_kind =
-  | Int of int_ty (* Coq.Init.Decimal.int + uint *)
-  | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+  | Int of int_ty (* Coq.Init.Numeral.int + uint *)
+  | UInt of int_ty (* Coq.Init.Numeral.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
-  | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
+  | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+  | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
+  | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
+  | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
diff --git a/interp/numTok.ml b/interp/numTok.ml
index e254e9e972..bb14649b91 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -12,6 +12,10 @@
     e.g. "e"/"E" or the presence of leading 0s, or the presence of a +
     in the exponent *)
 
+type num_class = CDec | CHex
+
+let string_del_head n s = String.sub s n (String.length s - n)
+
 module UnsignedNat =
 struct
   type t = string
@@ -20,12 +24,15 @@ struct
     assert (s.[0] >= '0' && s.[0] <= '9');
     s
   let to_string s =
-    String.(concat "" (split_on_char '_' s))
+    String.(map Char.lowercase_ascii (concat "" (split_on_char '_' s)))
 
   let sprint s = s
   let print s = Pp.str (sprint s)
 
-  (** Comparing two raw numbers (base 10, big-endian, non-negative).
+  let classify s =
+    if String.length s >= 2 && (s.[1] = 'x' || s.[1] = 'X') then CHex else CDec
+
+  (** Comparing two raw numbers (base 10 or 16, big-endian, non-negative).
       A bit nasty, but not critical: used e.g. to decide when a number
       is considered as large (see threshold warnings in notation.ml). *)
 
@@ -45,12 +52,20 @@ struct
         0
       with Comp c -> c
 
-   let is_zero s =
-     compare s "0" = 0
+  let compare n d =
+    assert (classify d = CDec);
+    match classify n with
+    | CDec -> compare (to_string n) (to_string d)
+    | CHex -> compare (string_del_head 2 (to_string n)) (to_string d)
+
+  let is_zero s =
+    compare s "0" = 0
 end
 
 type sign = SPlus | SMinus
 
+type 'a exp = EDec of 'a | EBin of 'a
+
 module SignedNat =
 struct
   type t = sign * UnsignedNat.t
@@ -58,26 +73,89 @@ struct
     assert (String.length s > 0);
     let sign,n =
       match s.[0] with
-      | '-' -> (SMinus,String.sub s 1 (String.length s - 1))
-      | '+' -> (SPlus,String.sub s 1 (String.length s - 1))
+      | '-' -> (SMinus,string_del_head 1 s)
+      | '+' -> (SPlus,string_del_head 1 s)
       | _ -> (SPlus,s) in
     (sign,UnsignedNat.of_string n)
   let to_string (sign,n) =
     (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
-  let to_bigint n = Bigint.of_string (to_string n)
-  let of_bigint n =
+  let classify (_,n) = UnsignedNat.classify n
+  let bigint_of_string (sign,n) =
+    (* nasty code to remove when switching to zarith
+       since zarith's of_string handles hexadecimal *)
+    match UnsignedNat.classify n with
+    | CDec -> Bigint.of_string (to_string (sign,n))
+    | CHex ->
+       let int_of_char c = match c with
+         | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
+         | _ -> int_of_char c - int_of_char '0' in
+       let c16 = Bigint.of_int 16 in
+       let s = UnsignedNat.to_string n in
+       let n = ref Bigint.zero in
+       let len = String.length s in
+       for d = 2 to len - 1 do
+         n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d])))
+       done;
+       match sign with SPlus -> !n | SMinus -> Bigint.neg !n
+  let to_bigint n = bigint_of_string n
+  let string_of_nonneg_bigint c n =
+    (* nasty code to remove when switching to zarith
+       since zarith's format handles hexadecimal *)
+    match c with
+    | CDec -> Bigint.to_string n
+    | CHex ->
+       let div16 n =
+         let n, r0 = Bigint.div2_with_rest n in
+         let n, r1 = Bigint.div2_with_rest n in
+         let n, r2 = Bigint.div2_with_rest n in
+         let n, r3 = Bigint.div2_with_rest n in
+         let r = match r3, r2, r1, r0 with
+           | false, false, false, false -> "0"
+           | false, false, false,  true -> "1"
+           | false, false,  true, false -> "2"
+           | false, false,  true,  true -> "3"
+           | false,  true, false, false -> "4"
+           | false,  true, false,  true -> "5"
+           | false,  true,  true, false -> "6"
+           | false,  true,  true,  true -> "7"
+           |  true, false, false, false -> "8"
+           |  true, false, false,  true -> "9"
+           |  true, false,  true, false -> "a"
+           |  true, false,  true,  true -> "b"
+           |  true,  true, false, false -> "c"
+           |  true,  true, false,  true -> "d"
+           |  true,  true,  true, false -> "e"
+           |  true,  true,  true,  true -> "f" in
+         n, r in
+       let n = ref n in
+       let l = ref [] in
+       while Bigint.is_strictly_pos !n do
+         let n', r = div16 !n in
+         n := n';
+         l := r :: !l
+       done;
+       "0x" ^ String.concat "" (List.rev !l)
+  let of_bigint c n =
     let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
-    (sign, Bigint.to_string n)
+    (sign, string_of_nonneg_bigint c n)
 end
 
 module Unsigned =
 struct
 
   type t = {
-    int : string;  (** \[0-9\]\[0-9_\]* *)
-    frac : string;  (** empty or \[0-9_\]+ *)
-    exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+    int : string;
+    frac : string;
+    exp : string
   }
+  (**
+    - int: \[0-9\]\[0-9_\]*
+    - frac: empty or \[0-9_\]+
+    - exp: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]*
+    or
+    - int: 0\[xX\]\[0-9a-fA-F\]\[0-9a-fA-F_\]*
+    - frac: empty or \[0-9a-fA-F_\]+
+    - exp: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
 
   let equal n1 n2 =
     String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
@@ -96,19 +174,35 @@ struct
       | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
       | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s
       | _ -> len in
+    (* reads [0-9a-fA-F_]* *)
+    let rec hex_number len s = match Stream.peek s with
+      | Some (('0'..'9' | 'a'..'f' | 'A'..'F') as c) ->
+         Stream.junk s; hex_number (store len c) s
+      | Some ('_' as c) when len > 0 ->
+         Stream.junk s; hex_number (store len c) s
+      | _ -> len in
     fun s ->
-    let i = get_buff (number 0 s) in
+    let hex, i =
+      match Stream.npeek 3 s with
+      | '0' :: (('x' | 'X') as x) :: (('0'..'9' | 'a'..'f' | 'A'..'F') as c) :: _ ->
+         Stream.junk s; Stream.junk s; Stream.junk s;
+         true, get_buff (hex_number (store (store (store 0 '0') x) c) s)
+      | _ -> false, get_buff (number 0 s) in
     assert (i <> "");
     let f =
-      match Stream.npeek 2 s with
-      | '.' :: (('0'..'9' | '_') as c) :: _ ->
+      match hex, Stream.npeek 2 s with
+      | true, '.' :: (('0'..'9' | 'a'..'f' | 'A'..'F' | '_') as c) :: _ ->
+         Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s)
+      | false, '.' :: (('0'..'9' | '_') as c) :: _ ->
          Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
       | _ -> "" in
     let e =
-      match (Stream.npeek 2 s) with
-      | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
+      match hex, Stream.npeek 2 s with
+      | true, (('p'|'P') as e) :: ('0'..'9' as c) :: _
+      | false, (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
          Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
-      | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
+      | true, (('p'|'P') as e) :: (('+'|'-') as sign) :: _
+      | false, (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
          begin match Stream.npeek 3 s with
          | _ :: _ :: ('0'..'9' as c) :: _ ->
             Stream.junk s; Stream.junk s; Stream.junk s;
@@ -146,6 +240,7 @@ struct
     | { int = _; frac = ""; exp = "" } -> true
     | _ -> false
 
+  let classify n = UnsignedNat.classify n.int
 end
 
 open Unsigned
@@ -162,19 +257,30 @@ struct
     | (SPlus,{int;frac;exp}) -> UnsignedNat.is_zero int && UnsignedNat.is_zero frac
     | _ -> false
 
-  let of_decimal_and_exponent (sign,int) f e =
-    let exp = match e with Some e -> "e" ^ SignedNat.to_string e | None -> "" in
-    let frac = match f with Some f -> UnsignedNat.to_string f | None -> "" in
+  let of_int_frac_and_exponent (sign,int) f e =
+    assert (match e with None -> true | Some e -> SignedNat.classify e = CDec);
+    let c = UnsignedNat.classify int in
+    let exp = match e with None -> "" | Some e ->
+      let e = SignedNat.to_string e in
+      match c with CDec -> "e" ^ e | CHex -> "p" ^ e in
+    let frac = match f with None -> "" | Some f ->
+      assert (c = UnsignedNat.classify f);
+      let f = UnsignedNat.to_string f in
+      match c with CDec -> f | CHex -> string_del_head 2 f in
     sign, { int; frac; exp }
 
-  let to_decimal_and_exponent (sign, { int; frac; exp }) =
+  let to_int_frac_and_exponent (sign, { int; frac; exp }) =
     let e =
       if exp = "" then None else
         Some (match exp.[1] with
-        | '-' -> SMinus, String.sub exp 2 (String.length exp - 2)
-        | '+' -> SPlus, String.sub exp 2 (String.length exp - 2)
-        | _ -> SPlus, String.sub exp 1 (String.length exp - 1)) in
-    let f = if frac = "" then None else Some frac in
+        | '-' -> SMinus, string_del_head 2 exp
+        | '+' -> SPlus, string_del_head 2 exp
+        | _ -> SPlus, string_del_head 1 exp) in
+    let f =
+      if frac = "" then None else
+        Some (match UnsignedNat.classify int with
+        | CDec -> frac
+        | CHex -> "0x" ^ frac) in
     (sign, int), f, e
 
   let of_nat i =
@@ -211,8 +317,8 @@ struct
   let of_string s =
     assert (s <> "");
     let sign,u = match s.[0] with
-    | '-' -> (SMinus, String.sub s 1 (String.length s - 1))
-    | '+' -> (SPlus, String.sub s 1 (String.length s - 1))
+    | '-' -> (SMinus, string_del_head 1 s)
+    | '+' -> (SPlus, string_del_head 1 s)
     | _ -> (SPlus, s) in
     (sign, Unsigned.of_string u)
 
@@ -224,27 +330,31 @@ struct
       Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n))
     | _ -> None
 
-  let of_bigint n =
-    let sign, int = SignedNat.of_bigint n in
-    (sign, { int; frac = ""; exp = "" })
+  let of_bigint c n =
+    of_int (SignedNat.of_bigint c n)
 
   let to_bigint_and_exponent (s, { int; frac; exp }) =
-    let s = match s with SPlus -> "" | SMinus -> "-" in
+    let c = UnsignedNat.classify int in
     let int = UnsignedNat.to_string int in
     let frac = UnsignedNat.to_string frac in
-    let i = Bigint.of_string (s ^ int ^ frac) in
+    let i = SignedNat.to_bigint (s, int ^ frac) in
     let e =
       let e = if exp = "" then Bigint.zero else match exp.[1] with
-      | '+' -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))
-      | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))))
-      | _ -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 1 (String.length exp - 1))) in
-      Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' frac))))) in
-    (i,e)
+      | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp))
+      | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
+      | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
+      let l = String.length frac in
+      let l = match c with CDec -> l | CHex -> 4 * l in
+      Bigint.(sub e (of_int l)) in
+    (i, match c with CDec -> EDec e | CHex -> EBin e)
 
   let of_bigint_and_exponent i e =
-    of_decimal_and_exponent (SignedNat.of_bigint i) None (Some (SignedNat.of_bigint e))
+    let c = match e with EDec _ -> CDec | EBin _ -> CHex in
+    let e = match e with EDec e | EBin e -> Some (SignedNat.of_bigint CDec e) in
+    of_int_frac_and_exponent (SignedNat.of_bigint c i) None e
 
   let is_bigger_int_than (s, { int; frac; exp }) i =
     frac = "" && exp = "" && UnsignedNat.compare int i >= 0
 
+  let classify (_, n) = Unsigned.classify n
 end
diff --git a/interp/numTok.mli b/interp/numTok.mli
index ea289df237..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,13 +57,16 @@ 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 classify : t -> num_class
+
+  val of_bigint : num_class -> Bigint.bigint -> t
   val to_bigint : t -> Bigint.bigint
-  val of_bigint : Bigint.bigint -> t
 end
 
 (** {6 Unsigned decimal numerals } *)
@@ -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_decimal_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
-  val to_decimal_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option
-    (** n, p and q such that the number is n.p*10^q *)
+  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 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 to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint
-  val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t
-    (** 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 *)