diff options
| -rw-r--r-- | Dafny/Dafny.atg | 9 | ||||
| -rw-r--r-- | Dafny/DafnyAst.ssc | 11 | ||||
| -rw-r--r-- | Dafny/DafnyPipeline.sscproj | 15 | ||||
| -rw-r--r-- | Dafny/Parser.ssc | 9 | ||||
| -rw-r--r-- | Dafny/Printer.ssc | 3 | ||||
| -rw-r--r-- | Dafny/Resolver.ssc | 3 | ||||
| -rw-r--r-- | Dafny/Translator.ssc | 5 |
7 files changed, 41 insertions, 14 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 77eba938..a6eba750 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -10,6 +10,7 @@ //--------------------------------------------------------------------------*/
using System.Collections.Generic;
+using System.Numerics;
using Microsoft.Boogie;
@@ -888,7 +889,7 @@ UnaryExpression<out Expression! e> NegOp = "!" | '\u00ac'.
ConstAtomExpression<out Expression! e>
-= (. Token! x, dtName, id; int n; List<Expression!>! elements;
+= (. Token! x, dtName, id; BigInteger n; List<Expression!>! elements;
e = dummyExpr;
.)
( "false" (. e = new LiteralExpr(token, false); .)
@@ -1116,14 +1117,14 @@ Ident<out Token! x> ident (. x = token; .)
.
-Nat<out int n>
+Nat<out BigInteger n>
=
digits
(. try {
- n = System.Convert.ToInt32(token.val);
+ n = BigInteger.Parse(token.val);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
- n = 0;
+ n = BigInteger.Zero;
}
.)
.
diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc index 9a121b01..38c3b87d 100644 --- a/Dafny/DafnyAst.ssc +++ b/Dafny/DafnyAst.ssc @@ -6,6 +6,7 @@ using System;
using System.Collections.Generic;
using Microsoft.Contracts;
+using System.Numerics;
namespace Microsoft.Dafny
{
@@ -830,13 +831,19 @@ namespace Microsoft.Dafny base(tok);
}
- public LiteralExpr(Token! tok, int n)
- requires 0 <= n;
+ public LiteralExpr(Token! tok, BigInteger n)
+ requires 0 <= n.Sign;
{
this.Value = n;
base(tok);
}
+ public LiteralExpr(Token! tok, int n)
+ requires 0 <= n;
+ {
+ this(tok, new BigInteger(n));
+ }
+
public LiteralExpr(Token! tok, bool b) {
this.Value = b;
base(tok);
diff --git a/Dafny/DafnyPipeline.sscproj b/Dafny/DafnyPipeline.sscproj index 38ff8646..e9c025fc 100644 --- a/Dafny/DafnyPipeline.sscproj +++ b/Dafny/DafnyPipeline.sscproj @@ -72,6 +72,21 @@ Private="false"
HintPath="../Core/bin/Debug/Core.dll"
/>
+ <Reference Name="FSharp.Core"
+ AssemblyName="FSharp.Core"
+ Private="true"
+ HintPath="../../Binaries/FSharp.Core.dll"
+ />
+ <Reference Name="FSharp.PowerPack"
+ AssemblyName="FSharp.PowerPack"
+ Private="true"
+ HintPath="../../Binaries/FSharp.PowerPack.dll"
+ />
+ <Reference Name="Basetypes"
+ AssemblyName="Basetypes"
+ Private="true"
+ HintPath="../Basetypes/bin/debug/Basetypes.dll"
+ />
</References>
</Build>
<Files>
diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc index 930aa2bf..50079f11 100644 --- a/Dafny/Parser.ssc +++ b/Dafny/Parser.ssc @@ -1,4 +1,5 @@ using System.Collections.Generic;
+using System.Numerics;
using Microsoft.Boogie;
using Microsoft.Contracts;
@@ -1347,7 +1348,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
static void ConstAtomExpression(out Expression! e) {
- Token! x, dtName, id; int n; List<Expression!>! elements;
+ Token! x, dtName, id; BigInteger n; List<Expression!>! elements;
e = dummyExpr;
switch (t.kind) {
@@ -1429,13 +1430,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
}
- static void Nat(out int n) {
+ static void Nat(out BigInteger n) {
Expect(2);
try {
- n = System.Convert.ToInt32(token.val);
+ n = BigInteger.Parse(token.val);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
- n = 0;
+ n = BigInteger.Zero;
}
}
diff --git a/Dafny/Printer.ssc b/Dafny/Printer.ssc index d676c942..d0a6b3c9 100644 --- a/Dafny/Printer.ssc +++ b/Dafny/Printer.ssc @@ -7,6 +7,7 @@ using System; using System.IO;
using System.Collections.Generic;
using Microsoft.Contracts;
+using System.Numerics;
using Bpl = Microsoft.Boogie;
namespace Microsoft.Dafny {
@@ -503,7 +504,7 @@ namespace Microsoft.Dafny { } else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
} else {
- wr.Write((int)e.Value);
+ wr.Write((BigInteger)e.Value);
}
} else if (expr is ThisExpr) {
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index 5eca038e..31f51424 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -5,6 +5,7 @@ //-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
+using System.Numerics;
using Microsoft.Contracts;
namespace Microsoft.Dafny {
@@ -1021,7 +1022,7 @@ namespace Microsoft.Dafny { LiteralExpr e = (LiteralExpr)expr;
if (e.Value == null) {
e.Type = new ObjectTypeProxy();
- } else if (e.Value is int) {
+ } else if (e.Value is BigInteger) {
e.Type = Type.Int;
} else if (e.Value is bool) {
e.Type = Type.Bool;
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc index ffd76bd6..85a09b1f 100644 --- a/Dafny/Translator.ssc +++ b/Dafny/Translator.ssc @@ -5,6 +5,7 @@ //-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
+using System.Numerics;
using Microsoft.Contracts;
using Bpl = Microsoft.Boogie;
using System.Text;
@@ -2216,8 +2217,8 @@ namespace Microsoft.Dafny { return predef.Null;
} else if (e.Value is bool) {
return Bpl.Expr.Literal((bool)e.Value);
- } else if (e.Value is int) {
- return Bpl.Expr.Literal((int)e.Value);
+ } else if (e.Value is BigInteger) {
+ return Bpl.Expr.Literal(Microsoft.Basetypes.BigNum.FromBigInt((BigInteger)e.Value));
} else {
assert false; // unexpected literal
}
|