feat: Add comprehensive real literal support with scientific notation and dot shorthand

Source/DafnyCore/Dafny.atg

@@ -75,7 +75,10 @@ TOKENS
         .
   digits = digit {['_'] digit}.
   hexdigits = "0x" hexdigit {['_'] hexdigit}.
-  decimaldigits = digit {['_'] digit} '.' digit {['_'] digit}.
+  realnumber = digit {['_'] digit}
+               ( '.' digit {['_'] digit} ['e' ['-'] digit {['_'] digit}]
+               | 'e' ['-'] digit {['_'] digit}
+               ).
   // NOTE: all alphabetic strings used in the grammar become reserved words automatically
   // The reason to include a definition here is so that a token can be referred to by its 'kind',
   // as in la.kind == _bool
@@ -3780,6 +3783,7 @@ LiteralExpression<out Expression e>
   ( "false"                                    (. e = new LiteralExpr(t, false); .)
   | "true"                                     (. e = new LiteralExpr(t, true); .)
   | "null"                                     (. e = new LiteralExpr(t); .)
+  | IF(la.kind == _digits && scanner.Peek().kind == _dot) Dec<out d> (. e = new LiteralExpr(t, d); .)
   | Nat<out n>                                 (. e = new LiteralExpr(t, n); .)
   | Dec<out d>                                 (. e = new LiteralExpr(t, d); .)
   | charToken                                  (. string s = t.val.Substring(1, t.val.Length - 2);
@@ -4742,11 +4746,11 @@ DotSuffix<out Token x, out Token y>
   .)
   ( Ident<out x>
   | digits         (. x = t; .)
-  | decimaldigits  (. x = t;
+  | realnumber  (. x = t;
                       int exponent = x.val.IndexOf('e');
                       if (0 <= exponent) {
                         // this is not a legal field/destructor name
-                        // Also it is not currently reachable, because decimaldigits does not yet support exponents
+                        // Scientific notation is not allowed in field/destructor names
                         SemErr(ErrorId.p_invalid_name_after_dot, x, "invalid name after a '.'");
                       } else {
                         int dot = x.val.IndexOf('.');
@@ -4906,17 +4910,26 @@ Nat<out BigInteger n>
 
 /*------------------------------------------------------------------------*/
 Dec<out BaseTypes.BigDec d>
-= (. d = BaseTypes.BigDec.ZERO; .)
-  (decimaldigits
-    (. var S = Util.RemoveUnderscores(t.val);
-       try {
-         d = BaseTypes.BigDec.FromString(S);
-       } catch (System.FormatException) {
-         SemErr(ErrorId.p_bad_decimal_number_format, t, "incorrectly formatted number");
-         d = BaseTypes.BigDec.ZERO;
-       }
-    .)
+= (. d = BaseTypes.BigDec.ZERO; string S = ""; .)
+  ( realnumber                              (. S = Util.RemoveUnderscores(t.val); .)
+  | digits                                  (. var digitToken = t; .)
+    "."                                     (. if (t.pos != digitToken.pos + digitToken.val.Length) {
+                                                 SemErr(ErrorId.p_bad_decimal_number_format, new SourceOrigin(digitToken, t), "invalid real literal (no whitespace allowed before trailing dot)");
+                                               }
+                                               S = Util.RemoveUnderscores(digitToken.val) + ".0"; .)
+  | "."                                     (. var dotToken = t; .)
+    ( digits | realnumber )                 (. if (t.pos != dotToken.pos + 1) {
+                                                 SemErr(ErrorId.p_bad_decimal_number_format, new SourceOrigin(dotToken, t), "invalid real literal (no whitespace allowed after leading dot)");
+                                               }
+                                               S = "0." + Util.RemoveUnderscores(t.val); .)
   )
+  (. try {
+       d = BaseTypes.BigDec.FromString(S);
+     } catch (System.FormatException) {
+       SemErr(ErrorId.p_bad_decimal_number_format, t, "incorrectly formatted number");
+       d = BaseTypes.BigDec.ZERO;
+     }
+  .)
   .
 
 /*------------------------------------------------------------------------*/

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ScientificNotation.dfy

@@ -0,0 +1,181 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=0 "%s"
+
+// Comprehensive test for scientific notation, trailing-dot shorthand, and leading-dot shorthand
+
+method BasicScientificNotation() {
+  // Basic positive exponents
+  var a := 1.23e2;     // 123.0
+  var b := 2.5e1;      // 25.0
+  var c := 1.0e3;      // 1000.0
+
+  // Basic negative exponents
+  var d := 1.23e-2;    // 0.0123
+  var e := 5.0e-1;     // 0.5
+
+  // Zero exponent
+  var f := 1.23e0;     // 1.23
+  var g := 42.0e0;     // 42.0
+  var h := 1.23e-0;    // 1.23 (same as e0)
+
+  // Verify values
+  assert a == 123.0;
+  assert b == 25.0;
+  assert c == 1000.0;
+  assert d == 0.0123;
+  assert e == 0.5;
+  assert f == 1.23;
+  assert g == 42.0;
+  assert h == 1.23;
+}
+
+method IntegerScientificNotation() {
+  // Integer base with scientific notation
+  var a := 5e2;        // 500.0
+  var b := 3e1;        // 30.0
+  var c := 7e0;        // 7.0
+  var d := 5e-1;       // 0.5
+  var e := 2e-2;       // 0.02
+
+  assert a == 500.0;
+  assert b == 30.0;
+  assert c == 7.0;
+  assert d == 0.5;
+  assert e == 0.02;
+}
+
+method TrailingDotShorthand() {
+  // Basic trailing-dot shorthand literals
+  var a := 1.;         // 1.0
+  var b := 123.;       // 123.0
+  var c := 0.;         // 0.0
+
+  // Trailing dots with underscores
+  var d := 1_000.;     // 1000.0
+
+  // Verify values
+  assert a == 1.0;
+  assert b == 123.0;
+  assert c == 0.0;
+  assert d == 1000.0;
+}
+
+method LeadingDotShorthand() {
+  // Basic leading-dot shorthand literals (new feature)
+  var a := .5;         // 0.5
+  var b := .25;        // 0.25
+  var c := .123;       // 0.123
+  var d := .0;         // 0.0
+
+  // Leading-dot with underscores
+  var e := .5_00;      // 0.500
+  var f := .1_23;      // 0.123
+
+  // Verify values
+  assert a == 0.5;
+  assert b == 0.25;
+  assert c == 0.123;
+  assert d == 0.0;
+  assert e == 0.500;
+  assert f == 0.123;
+}
+
+method LeadingDotScientificNotation() {
+  // Leading-dot shorthand with scientific notation (new feature)
+  var a := .5e2;       // 50.0
+  var b := .25e1;      // 2.5
+  var c := .123e3;     // 123.0
+  var d := .5e-1;      // 0.05
+  var e := .123e-4;    // 0.0000123
+  var f := .1e0;       // 0.1
+
+  // Leading-dot shorthand scientific with underscores
+  var g := .5_00e2;    // 50.0
+  var h := .1_23e-2;   // 0.00123
+
+  // Verify values
+  assert a == 50.0;
+  assert b == 2.5;
+  assert c == 123.0;
+  assert d == 0.05;
+  assert e == 0.0000123;
+  assert f == 0.1;
+  assert g == 50.0;
+  assert h == 0.00123;
+}
+
+method TupleAccessCompatibility() {
+  // Verify that tuple member access still works (no conflict)
+  var tuple := (1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15);
+  var first := tuple.0;
+  var fifth := tuple.5;
+  var tenth := tuple.10;
+  var fifteenth := tuple.14;
+
+  assert first == 1;
+  assert fifth == 6;
+  assert tenth == 11;
+  assert fifteenth == 15;
+}
+
+method ScientificNotationArithmetic() {
+  // Arithmetic with scientific notation
+  var a := 1.5e2;      // 150.0
+  var b := 3.0e1;      // 30.0
+  var c := 2.0e-1;     // 0.2
+
+  // Basic operations
+  assert a + b == 180.0;
+  assert a - b == 120.0;
+  assert a * c == 30.0;
+  assert a / b == 5.0;
+
+  // Mixed with regular literals
+  assert a + 50.0 == 200.0;
+  assert b * 2.0 == 60.0;
+
+  // Mixed with leading-dot shorthand literals
+  var d := .5e2;       // 50.0
+  assert a + d == 200.0;
+  assert d * 2.0 == 100.0;
+}
+
+method UnderscoreSupport() {
+  // Scientific notation with underscores
+  var a := 1_234.567_8e2;    // 123456.78
+  var b := 5_000e-3;         // 5.0
+  var c := 1_000.0e1;        // 10000.0 (proper syntax instead of 1_000.e1)
+
+  // Leading-dot shorthand with underscores
+  var d := .5_00e2;          // 50.0
+  var e := .1_23e-4;         // 0.0000123
+
+  // Verify values
+  assert a == 123456.78;
+  assert b == 5.0;
+  assert c == 10000.0;
+  assert d == 50.0;
+  assert e == 0.0000123;
+}
+
+method EdgeCases() {
+  // Very small and very large numbers
+  var small := 1.0e-10;     // 0.0000000001
+  var large := 1.0e10;      // 10000000000.0
+
+  // Zero with scientific notation
+  var zero1 := 0.0e5;       // 0.0
+  var zero2 := 0.0e-3;      // 0.0 (proper syntax instead of 0.e-3)
+  var zero3 := .0e5;        // 0.0 (leading-dot shorthand zero)
+
+  // Leading-dot shorthand edge cases
+  var tiny := .1e-10;       // 0.00000000001
+  var huge := .1e10;        // 1000000000.0
+
+  assert small == 0.0000000001;
+  assert large == 10000000000.0;
+  assert zero1 == 0.0;
+  assert zero2 == 0.0;
+  assert zero3 == 0.0;
+  assert tiny == 0.00000000001;
+  assert huge == 1000000000.0;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ScientificNotation.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 9 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ScientificNotationErrors.dfy

@@ -0,0 +1,56 @@
+// RUN: %exits-with 2 %resolve "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Test error cases for scientific notation, trailing-dot shorthand, and leading-dot shorthand
+
+method MalformedScientificNotation() {
+  // Incomplete scientific notation - missing exponent
+  var a := 1.23e;      // Error: incomplete
+  var b := 5e;         // Error: incomplete (no trailing-dot shorthand syntax)
+
+  // Invalid exponent syntax
+  var c := 1.23e+;     // Error: missing digits after +
+  var d := 1.23e-;     // Error: missing digits after -
+}
+
+method InvalidUnderscorePlacement() {
+  // Invalid underscore before dot
+  var a := 1_.;        // Error: underscore before dot
+  var b := 1_2_.;      // Error: underscore before dot
+
+  // Invalid underscore in exponent
+  var c := 1.23e_2;    // Error: underscore at start of exponent
+  var d := 1.23e2_;    // Error: underscore at end of exponent
+}
+
+method InvalidCombinations() {
+  // Multiple e's
+  var a := 1.23e2e3;   // Error: multiple exponents
+
+  // Invalid characters in scientific notation
+  var b := 1.23f5;     // Error: 'f' instead of 'e'
+  var c := 1.23E2;     // Error: uppercase 'E' not supported
+}
+
+method InvalidLeadingDotShorthand() {
+  // Leading-dot shorthand with space (should be error due to tokenization)
+  var a := . 5;        // Error: space between dot and digits
+  var b := . 5e2;      // Error: space between dot and digits
+
+  // Invalid leading-dot shorthand combinations
+  var c := ..5;        // Error: double dot
+  var d := .e2;        // Error: no digits after dot before e
+}
+
+method InvalidWhitespaceAroundDots() {
+  // Whitespace before trailing dot (should be error)
+  var a := 1 .;        // Error: space before trailing dot
+  var b := 123 .;      // Error: space before trailing dot
+
+  // Whitespace after leading dot (should be error) 
+  var c := . 5;        // Error: space after leading dot
+  var d := . 25;       // Error: space after leading dot
+
+  // Whitespace around normal decimal dot (should be error)
+  var e := 1 . 5;      // Error: spaces around decimal dot
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ScientificNotationErrors.dfy.expect

@@ -0,0 +1,24 @@
+ScientificNotationErrors.dfy(8,15): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(9,12): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(12,15): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(13,15): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(18,12): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(19,14): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(22,15): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(23,17): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(28,17): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(31,15): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(32,15): Error: this symbol not expected in VarDeclStatement
+ScientificNotationErrors.dfy(37,11): Error: invalid real literal (no whitespace allowed after leading dot)
+ScientificNotationErrors.dfy(38,11): Error: invalid real literal (no whitespace allowed after leading dot)
+ScientificNotationErrors.dfy(41,11): Error: invalid Rhs
+ScientificNotationErrors.dfy(42,12): Error: invalid Dec
+ScientificNotationErrors.dfy(42,11): Error: invalid real literal (no whitespace allowed after leading dot)
+ScientificNotationErrors.dfy(42,11): Error: incorrectly formatted number
+ScientificNotationErrors.dfy(47,11): Error: invalid real literal (no whitespace allowed before trailing dot)
+ScientificNotationErrors.dfy(48,11): Error: invalid real literal (no whitespace allowed before trailing dot)
+ScientificNotationErrors.dfy(51,11): Error: invalid real literal (no whitespace allowed after leading dot)
+ScientificNotationErrors.dfy(52,11): Error: invalid real literal (no whitespace allowed after leading dot)
+ScientificNotationErrors.dfy(55,11): Error: invalid real literal (no whitespace allowed before trailing dot)
+ScientificNotationErrors.dfy(55,15): Error: this symbol not expected in VarDeclStatement
+23 parse errors detected in ScientificNotationErrors.dfy

docs/DafnyRef/Grammar.md

@@ -300,9 +300,13 @@ prefaced by `0x` and
 possibly interspersed with underscores for readability (but not beginning or ending with an underscore).
 Example: `0xffff_ffff`.
 
-A `decimaldigits` token is a decimal fraction constant, possibly interspersed with underscores for readability (but not beginning or ending with an underscore).
-It has digits both before and after a single period (`.`) character. There is no syntax for floating point numbers with exponents.
-Example: `123_456.789_123`.
+A `realnumber` token is a real number literal, possibly interspersed with
+underscores for readability (but not beginning or ending with an underscore).
+Real numbers can be written as decimal fractions (like `123.456`) or using 
+scientific notation (like `1.23e5` or `123e5`). Real number literals can use
+trailing-dot shorthand (like `1.` for `1.0`). They also support
+leading-dot shorthand (like `.5` for `0.5` or `.5e2` for `50.0`). All produce real number values.
+Examples: `123_456.789_123`, `1.23e5`, `123e-2`, `5e10`, `1.`, `.5`, `.25e-3`.
 
 ### 2.6.4. Escaped Character {#sec-escaped-characters}
 
@@ -510,5 +514,5 @@ the `--quantifier-syntax:4` option needs to be provided to enable this feature (
 
 Integer and bitvector literals may be expressed in either decimal or hexadecimal (`digits` or `hexdigits`).
 
-Real number literals are written as decimal fractions (`decimaldigits`).
+Real number literals are written as real number tokens (`realnumber`).
 

docs/DafnyRef/GrammarDetails.md

@@ -129,7 +129,10 @@ digits = digit {["_"] digit}
 
 hexdigits = "0x" hexdigit {["_"] hexdigit}
 
-decimaldigits = digit {["_"] digit} '.' digit {["_"] digit}
+realnumber = digit {["_"] digit}
+             ( '.' digit {["_"] digit} ['e' ['-'] digit {["_"] digit}]
+             | 'e' ['-'] digit {["_"] digit}
+             )
 
 escapedChar =
     ( "\'" | "\"" | "\\" | "\0" | "\n" | "\r" | "\t"
@@ -1414,7 +1417,7 @@ LiteralExpression =
 
 Nat = ( digits | hexdigits )
 
-Dec = decimaldigits
+Dec = ( realnumber | digits "." | "." ( digits | realnumber ) )
 ````
 
 #### 17.2.7.21. This expression {#g-this-expression}