diff options
| author |  leino <unknown> | 2014-10-23 21:52:12 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-23 21:52:12 -0700 |
| commit | 40f36d68b8cb9489d052ababada29539c7d8de92 (patch) | |
| tree | 46b3b65776325e0bb78b5a5bfae1d483fec0485a /Source/Dafny/Parser.cs | |
| parent | 07ac1e4cfe6cdaf73a5bfa8b863728beae2a4c86 (diff) | |
Allow underscores in numeric literals (and in field/destructor names that are written as numeric strings). The
underscores have no semantic meaning, but can help a human parse the numbers.
Diffstat (limited to 'Source/Dafny/Parser.cs')
| -rw-r--r-- | Source/Dafny/Parser.cs | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 8755d275..6ce29b9c 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -3632,11 +3632,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void Nat(out BigInteger n) {
- n = BigInteger.Zero;
+ n = BigInteger.Zero;
+ string S;
+
if (la.kind == 2) {
Get();
+ S = Util.RemoveUnderscores(t.val);
try {
- n = BigInteger.Parse(t.val);
+ n = BigInteger.Parse(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
@@ -3644,9 +3647,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 3) {
Get();
+ S = Util.RemoveUnderscores(t.val.Substring(2));
try {
// note: leading 0 required when parsing positive hex numbers
- n = BigInteger.Parse("0" + t.val.Substring(2), System.Globalization.NumberStyles.HexNumber);
+ n = BigInteger.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
@@ -3658,8 +3662,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Dec(out Basetypes.BigDec d) {
d = Basetypes.BigDec.ZERO;
Expect(4);
+ var S = Util.RemoveUnderscores(t.val);
try {
- d = Basetypes.BigDec.FromString(t.val);
+ d = Basetypes.BigDec.FromString(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
d = Basetypes.BigDec.ZERO;
|