Allow underscores as comments in numeral constants.

The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?

5 files changed, 13 insertions, 10 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index bb0a9fa1bd..5a1af9f9fa 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -77,7 +77,8 @@ Identifiers and access identifiers
 Numerals
   Numerals are sequences of digits with a potential fractional part
   and exponent. Integers are numerals without fractional nor exponent
-  part and optionally preceded by a minus sign.
+  part and optionally preceded by a minus sign. Underscores ``_`` can
+  be used as comments in numerals.
 
   .. productionlist:: coq
      digit   : 0..9
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8b93088515..59feb46dc1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1487,7 +1487,7 @@ let alias_of als = match als.alias_ids with
 
 let is_zero s =
   let rec aux i =
-    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
+    Int.equal (String.length s) i || ((s.[i] == '0' || s.[i] == '_') && aux (i+1))
   in aux 0
 let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
 
diff --git a/interp/notation.ml b/interp/notation.ml
index df8f6eb4f8..b9aca82cf4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -499,7 +499,9 @@ module InnerPrimToken = struct
     | StringInterp f, StringInterp f' -> f == f'
     | _ -> false
 
-  let ofNumeral s n = match s with
+  let ofNumeral s n =
+    let n = String.(concat "" (split_on_char '_' n)) in
+    match s with
     | SPlus -> Bigint.of_string n
     | SMinus -> Bigint.neg (Bigint.of_string n)
 
@@ -770,7 +772,7 @@ let coquint_of_rawnum uint str =
   let nil = mkConstruct (uint,1) in
   let rec do_chars s i acc =
     if i < 0 then acc
-    else
+    else if s.[i] == '_' then do_chars s (i-1) acc else
       let dg = mkConstruct (uint, digit_of_char s.[i]) in
       do_chars s (i-1) (mkApp(dg,[|acc|]))
   in
diff --git a/interp/numTok.ml b/interp/numTok.ml
index cdc6ddb62b..8f2004b889 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -20,15 +20,15 @@ let parse =
     set !buff len x;
     succ len in
   let get_buff len = Bytes.sub_string !buff 0 len in
-  (* reads [0-9]* *)
+  (* reads [0-9_]* *)
   let rec number len s = match Stream.peek s with
-    | Some (('0'..'9') as c) -> Stream.junk s; number (store len c) s
+    | Some (('0'..'9' | '_') as c) -> Stream.junk s; number (store len c) s
     | _ -> len in
   fun s ->
   let i = get_buff (number 0 s) in
   let f =
     match Stream.npeek 2 s with
-    | '.' :: (('0'..'9') as c) :: _ ->
+    | '.' :: (('0'..'9' | '_') as c) :: _ ->
        Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
     | _ -> "" in
   let e =
diff --git a/interp/numTok.mli b/interp/numTok.mli
index 46223c5faf..0b6a877cbd 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -1,7 +1,7 @@
 type t = {
-  int : string;  (** \[0-9\]+ *)
-  frac : string;  (** empty or \[0-9\]+ *)
-  exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]+ *)
+  int : string;  (** \[0-9\]\[0-9_\]* *)
+  frac : string;  (** empty or \[0-9_\]+ *)
+  exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
 }
 
 val equal : t -> t -> bool