[spec/test/interpreter] Allow underscores in numbers

document/core/text/values.rst

@@ -27,6 +27,7 @@ Integers
 ~~~~~~~~
 
 All :ref:`integers <syntax-int>` can be written in either decimal or hexadecimal notation.
+In both cases, digits can optionally be separated by underscores.
 
 .. math::
    \begin{array}{llclll@{\qquad}l}
@@ -43,10 +44,10 @@ All :ref:`integers <syntax-int>` can be written in either decimal or hexadecimal
    \\[1ex]
    \production{decimal number} & \Tnum &::=&
      d{:}\Tdigit &\Rightarrow& d \\ &&|&
-     n{:}\Tnum~~d{:}\Tdigit &\Rightarrow& 10\cdot n + d \\
+     n{:}\Tnum~~\text{\_}^?~~d{:}\Tdigit &\Rightarrow& 10\cdot n + d \\
    \production{hexadecimal number} & \Thexnum &::=&
      h{:}\Thexdigit &\Rightarrow& h \\ &&|&
-     n{:}\Thexnum~~h{:}\Thexdigit &\Rightarrow& 16\cdot n + h \\
+     n{:}\Thexnum~~\text{\_}^?~~h{:}\Thexdigit &\Rightarrow& 16\cdot n + h \\
    \end{array}
 
 The allowed syntax for integer literals depends on size and signedness.
@@ -88,10 +89,12 @@ Floating-Point
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{decimal floating-point fraction} & \Tfrac &::=&
      \epsilon &\Rightarrow& 0 \\ &&|&
-     d{:}\Tdigit~q{:}\Tfrac &\Rightarrow& (d+q)/10 \\
+     d{:}\Tdigit~~q{:}\Tfrac &\Rightarrow& (d+q)/10 \\ &&|&
+     d{:}\Tdigit~~\text{\_}~~p{:}\Tdigit~~q{:}\Tfrac &\Rightarrow& (d+(p+q)/10)/10 \\
    \production{hexadecimal floating-point fraction} & \Thexfrac &::=&
      \epsilon &\Rightarrow& 0 \\ &&|&
-     h{:}\Thexdigit~q{:}\Thexfrac &\Rightarrow& (h+q)/16 \\
+     h{:}\Thexdigit~~q{:}\Thexfrac &\Rightarrow& (h+q)/16 \\ &&|&
+     h{:}\Thexdigit~~\text{\_}~~~~p{:}\Thexdigit~~q{:}\Thexfrac &\Rightarrow& (h+(p+q)/16)/16 \\
    \production{decimal floating-point number} & \Tfloat &::=&
      p{:}\Tnum~\text{.}~q{:}\Tfrac
        &\Rightarrow& p+q \\ &&|&

interpreter/exec/int.ml

@@ -245,12 +245,14 @@ struct
     let len = String.length s in
     let rec parse_hex i num =
       if i = len then num else
+      if s.[i] = '_' then parse_hex (i + 1) num else
       let digit = of_int (hex_digit s.[i]) in
       require (le_u num (shr_u minus_one (of_int 4)));
       parse_hex (i + 1) (logor (shift_left num 4) digit)
     in
     let rec parse_dec i num =
       if i = len then num else
+      if s.[i] = '_' then parse_dec (i + 1) num else
       let digit = of_int (dec_digit s.[i]) in
       require (lt_u num max_upper || num = max_upper && le_u digit max_lower);
       parse_dec (i + 1) (add (mul num ten) digit)

interpreter/text/lexer.mll

@@ -91,8 +91,8 @@ let opt = Lib.Option.get
 let sign = '+' | '-'
 let digit = ['0'-'9']
 let hexdigit = ['0'-'9''a'-'f''A'-'F']
-let num = digit+
-let hexnum = hexdigit+
+let num = digit ('_'? digit)*
+let hexnum = hexdigit ('_'? hexdigit)*
 
 let letter = ['a'-'z''A'-'Z']
 let symbol =
@@ -123,11 +123,13 @@ let character =
 
 let nat = num | "0x" hexnum
 let int = sign nat
+let frac = num
+let hexfrac = hexnum
 let float =
-    sign? num '.' digit*
-  | sign? num ('.' digit*)? ('e' | 'E') sign? num
-  | sign? "0x" hexnum '.' hexdigit*
-  | sign? "0x" hexnum ('.' hexdigit*)? ('p' | 'P') sign? num
+    sign? num '.' frac?
+  | sign? num ('.' frac?)? ('e' | 'E') sign? num
+  | sign? "0x" hexnum '.' hexfrac?
+  | sign? "0x" hexnum ('.' hexfrac?)? ('p' | 'P') sign? num
   | sign? "inf"
   | sign? "nan"
   | sign? "nan:" "0x" hexnum