diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-02-10 16:48:43 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-02-10 16:48:43 -0800 |
| commit | f0f4e3acbabc7386dafce96ea6b077896045bb73 (patch) | |
| tree | 84e8646b4e9bea0506473cb609b737fe94ff5d52 /Source/Dafny/Printer.cs | |
| parent | 783c272bb035c7ce419c312cd7ade5a8de378d75 (diff) | |
Preliminary support for reals in Dafny specs. No compiler suport yet.
Diffstat (limited to 'Source/Dafny/Printer.cs')
| -rw-r--r-- | Source/Dafny/Printer.cs | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index f4b4ccc8..952c8ef6 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1114,6 +1114,24 @@ namespace Microsoft.Dafny { wr.Write("null");
} else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
+ } else if (e.Value is Basetypes.BigDec) {
+ Basetypes.BigDec dec = (Basetypes.BigDec)e.Value;
+ wr.Write((dec.Mantissa >= 0) ? "" : "-");
+ string s = BigInteger.Abs(dec.Mantissa).ToString();
+ int digits = s.Length;
+ if (dec.Exponent >= 0) {
+ wr.Write("{0}{1}.0", s, new string('0', dec.Exponent));
+ } else {
+ int exp = -dec.Exponent;
+ if (exp < digits) {
+ int intDigits = digits - exp;
+ int fracDigits = digits - intDigits;
+ wr.Write("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
+ } else {
+ int fracDigits = digits;
+ wr.Write("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
+ }
+ }
} else {
wr.Write((BigInteger)e.Value);
}
|