diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 15 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 32 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/RealTypes.dfy | 10 |
8 files changed, 76 insertions, 5 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index e81e5e67..9aca7306 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -351,6 +351,10 @@ namespace Microsoft.Dafny return new MatchExpr(Tok(e.tok), CloneExpr(e.Source),
e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
+ } else if (expr is NegationExpression) {
+ var e = (NegationExpression)expr;
+ return new NegationExpression(Tok(e.tok), CloneExpr(e.E));
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a74ec21d..51a4785b 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1776,7 +1776,7 @@ MulOp<out IToken x, out BinaryExpr.Opcode op> UnaryExpression<out Expression e, bool allowSemi>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; .)
( "-" (. x = t; .)
- UnaryExpression<out e, allowSemi> (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)
+ UnaryExpression<out e, allowSemi> (. e = new NegationExpression(x, e); .)
| NegOp (. x = t; .)
UnaryExpression<out e, allowSemi> (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
| EndlessExpression<out e, allowSemi> /* these have no further suffix */
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ba05d6a8..f29242ab 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -5642,6 +5642,21 @@ namespace Microsoft.Dafny { }
}
+ /// <summary>
+ /// A NegationExpression e represents the value -e and is syntactic shorthand
+ /// for 0-e (for integers) or 0.0-e (for reals).
+ /// </summary>
+ public class NegationExpression : ConcreteSyntaxExpression
+ {
+ public readonly Expression E;
+ public NegationExpression(IToken tok, Expression e)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(e != null);
+ E = e;
+ }
+ }
+
public class ChainingExpression : ConcreteSyntaxExpression
{
public readonly List<Expression> Operands;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 57284c8e..d064606f 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2842,7 +2842,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
x = t;
UnaryExpression(out e, allowSemi);
- e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
+ e = new NegationExpression(x, e);
break;
}
case 106: case 111: {
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 952c8ef6..601c5761 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1566,6 +1566,20 @@ namespace Microsoft.Dafny { // printing of parentheses is done optimally, not according to the parentheses in the given program
PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);
+ } else if (expr is NegationExpression) {
+ var e = (NegationExpression)expr;
+ string op = "-";
+ int opBindingStrength = 0x60;
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ bool containsNestedNegation = e.E is ParensExpression && ((ParensExpression)e.E).E is NegationExpression;
+
+ if (parensNeeded) { wr.Write("("); }
+ wr.Write(op);
+ PrintExpr(e.E, opBindingStrength, containsNestedNegation, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);
+ if (parensNeeded) { wr.Write(")"); }
+
} else if (expr is IdentifierSequence) {
var e = (IdentifierSequence)expr;
string sep = "";
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c18c30ea..564e4164 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1301,6 +1301,10 @@ namespace Microsoft.Dafny return new MatchExpr(e.tok, CloneExpr(e.Source),
e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
+ } else if (expr is NegationExpression) {
+ var e = (NegationExpression)expr;
+ return new NegationExpression(e.tok, CloneExpr(e.E));
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
@@ -5510,6 +5514,34 @@ namespace Microsoft.Dafny var e = (IdentifierSequence)expr;
ResolveIdentifierSequence(e, twoState, codeContext, false);
+ } else if (expr is NegationExpression) {
+ var e = (NegationExpression)expr;
+ var errorCount = ErrorCount;
+ ResolveExpression(e.E, twoState, codeContext);
+ e.Type = e.E.Type;
+ if (errorCount != ErrorCount) {
+ // there were errors resolving the operand; take the quick way out and
+ // just let the (already erronous) subexpression be what the negation expression
+ // will resolve to
+ e.ResolvedExpression = e.E;
+ } else {
+ Expression zero;
+ if (e.E.Type is RealType) {
+ // we know for sure that this is a real-unary-minus
+ zero = new LiteralExpr(e.tok, Basetypes.BigDec.ZERO);
+ } else {
+ // it's may be an integer operand or it may be that we don't know yet; we'll treat
+ // two cases the same way
+ zero = new LiteralExpr(e.tok, 0);
+ }
+ var subtract = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, zero, e.E);
+ // Resolve the subtraction expression. This look like it will resolve e.E once more,
+ // but the recursive calls to the resolver is mindful about DAGs and will check if the
+ // subexpression has already been resolved.
+ ResolveExpression(subtract, twoState, codeContext);
+ e.ResolvedExpression = subtract;
+ }
+
} else if (expr is LiteralExpr) {
LiteralExpr e = (LiteralExpr)expr;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 5297d132..a41cd0cd 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -161,7 +161,7 @@ RealTypes.dfy(19,12): Error: assertion violation Execution trace:
(0,0): anon0
-Dafny program verifier finished with 4 verified, 4 errors
+Dafny program verifier finished with 6 verified, 4 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy index c2d88074..9354bc9d 100644 --- a/Test/dafny0/RealTypes.dfy +++ b/Test/dafny0/RealTypes.dfy @@ -22,6 +22,12 @@ method R3() { // Check that real value in decreases clause doesn't scare Dafny
function R4(x:int, r:real) : int
{
- if x < 0 then 5
- else R4(x - 1, r)
+ if x < 0 then 5
+ else R4(x - 1, r)
+}
+
+method RoundingDirection()
+{
+ assert int(51.500277) == 51;
+ assert int(-0.194771) == -1;
}
|