summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-07-08 13:46:45 -0700
committerGravatar Rustan Leino <unknown>2014-07-08 13:46:45 -0700
commit1844457f6a4a51592103c67de5f67a8785d8c92f (patch)
tree1c1b762f60486131e758154090e824bfd485ae15 /Source
parentde0ad2057984cc066d4a9dc0fcf701abe23b47fc (diff)
Implemented compilation of the int<->real conversions, and changed the resolution and verification implementations of these.
Changed FreshExpr to be a UnaryExpr, and also introduced the UnaryOpExpr subclass.
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Cloner.cs12
-rw-r--r--Source/Dafny/Compiler.cs56
-rw-r--r--Source/Dafny/Dafny.atg30
-rw-r--r--Source/Dafny/DafnyAst.cs64
-rw-r--r--Source/Dafny/Parser.cs46
-rw-r--r--Source/Dafny/Printer.cs26
-rw-r--r--Source/Dafny/Resolver.cs163
-rw-r--r--Source/Dafny/Rewriter.cs9
-rw-r--r--Source/Dafny/Translator.cs131
9 files changed, 265 insertions, 272 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 5b8f8cc5..72721fc5 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -280,13 +280,13 @@ namespace Microsoft.Dafny
var e = (MultiSetFormingExpr)expr;
return new MultiSetFormingExpr(Tok(e.tok), CloneExpr(e.E));
- } else if (expr is FreshExpr) {
- var e = (FreshExpr)expr;
- return new FreshExpr(Tok(e.tok), CloneExpr(e.E));
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
+ return new UnaryOpExpr(Tok(e.tok), e.Op, CloneExpr(e.E));
- } else if (expr is UnaryExpr) {
- var e = (UnaryExpr)expr;
- return new UnaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E));
+ } else if (expr is ConversionExpr) {
+ var e = (ConversionExpr)expr;
+ return new ConversionExpr(Tok(e.tok), CloneExpr(e.E), CloneType(e.ToType));
} else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index fcf8a2ca..1e5ba1ba 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -983,7 +983,7 @@ namespace Microsoft.Dafny {
if (type is BoolType) {
return "false";
} else if (type is IntType) {
- return "new BigInteger(0)";
+ return "BigInteger.Zero";
} else if (type is RealType) {
return "Dafny.BigRational.ZERO";
} else if (type.IsRefType) {
@@ -2200,17 +2200,14 @@ namespace Microsoft.Dafny {
} else if (expr is OldExpr) {
Contract.Assert(false); throw new cce.UnreachableException(); // 'old' is always a ghost (right?)
- } else if (expr is FreshExpr) {
- Contract.Assert(false); throw new cce.UnreachableException(); // 'fresh' is always a ghost
-
- } else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
switch (e.Op) {
- case UnaryExpr.Opcode.Not:
+ case UnaryOpExpr.Opcode.Not:
wr.Write("!");
TrParenExpr(e.E);
break;
- case UnaryExpr.Opcode.SeqLength:
+ case UnaryOpExpr.Opcode.Cardinality:
if (cce.NonNull(e.E.Type).IsArrayType) {
wr.Write("new BigInteger(");
TrParenExpr(e.E);
@@ -2224,6 +2221,21 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
}
+ } else if (expr is ConversionExpr) {
+ var e = (ConversionExpr)expr;
+ if (e.ToType is IntType) {
+ Contract.Assert(e.E.Type is RealType);
+ TrParenExpr(e.E);
+ wr.Write(".ToBigInteger()");
+ } else if (e.ToType is RealType) {
+ Contract.Assert(e.E.Type is IntType);
+ wr.Write("new Dafny.BigRational(");
+ TrExpr(e.E);
+ wr.Write(", BigInteger.One)");
+ } else {
+ Contract.Assert(false); // unexpected ConversionExpr to-type
+ }
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
string opString = null;
@@ -2285,18 +2297,26 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.Mul:
opString = "*"; break;
case BinaryExpr.ResolvedOpcode.Div:
- wr.Write("Dafny.Helpers.EuclideanDivision(");
- TrParenExpr(e.E0);
- wr.Write(", ");
- TrExpr(e.E1);
- wr.Write(")");
+ if (expr.Type is IntType) {
+ wr.Write("Dafny.Helpers.EuclideanDivision(");
+ TrParenExpr(e.E0);
+ wr.Write(", ");
+ TrExpr(e.E1);
+ wr.Write(")");
+ } else {
+ opString = "/"; // for reals
+ }
break;
case BinaryExpr.ResolvedOpcode.Mod:
- wr.Write("Dafny.Helpers.EuclideanModulus(");
- TrParenExpr(e.E0);
- wr.Write(", ");
- TrExpr(e.E1);
- wr.Write(")");
+ if (expr.Type is IntType) {
+ wr.Write("Dafny.Helpers.EuclideanModulus(");
+ TrParenExpr(e.E0);
+ wr.Write(", ");
+ TrExpr(e.E1);
+ wr.Write(")");
+ } else {
+ opString = "%"; // for reals
+ }
break;
case BinaryExpr.ResolvedOpcode.SetEq:
case BinaryExpr.ResolvedOpcode.MultiSetEq:
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 5c1148c6..ff1c8a16 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -814,7 +814,7 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
{ (. path.Add(tok); .)
"." Ident<out tok>
}
- [ GenericInstantiation<gt> ] (. ty = (tok.val == "real") ? (Type)Microsoft.Dafny.Type.Real : new UserDefinedType(tok, tok.val, gt, path); .)
+ [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt, path); .)
)
.
GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
@@ -1840,7 +1840,7 @@ UnaryExpression<out Expression e, bool allowSemi>
( "-" (. x = t; .)
UnaryExpression<out e, allowSemi> (. e = new NegationExpression(x, e); .)
| NegOp (. x = t; .)
- UnaryExpression<out e, allowSemi> (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
+ UnaryExpression<out e, allowSemi> (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e); .)
| EndlessExpression<out e, allowSemi> /* these have no further suffix */
| DottedIdentifiersAndFunction<out e>
{ Suffix<ref e> }
@@ -1876,7 +1876,7 @@ NegOp = "!" | '\u00ac'.
ConstAtomExpression<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
IToken/*!*/ x; BigInteger n; Basetypes.BigDec d;
- e = dummyExpr;
+ e = dummyExpr; Type toType = null;
.)
( "false" (. e = new LiteralExpr(t, false); .)
| "true" (. e = new LiteralExpr(t, true); .)
@@ -1885,29 +1885,17 @@ ConstAtomExpression<out Expression e>
| Dec<out d> (. e = new LiteralExpr(t, d); .)
| "this" (. e = new ThisExpr(t); .)
| "fresh" (. x = t; .)
- "(" Expression<out e, true> ")" (. e = new FreshExpr(x, e); .)
+ "(" Expression<out e, true> ")" (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e); .)
| "old" (. x = t; .)
"(" Expression<out e, true> ")" (. e = new OldExpr(x, e); .)
| "|" (. x = t; .)
- Expression<out e, true> (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
+ Expression<out e, true> (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Cardinality, e); .)
"|"
+ | ( "int" (. x = t; toType = new IntType(); .)
+ | "real" (. x = t; toType = new RealType(); .)
+ )
+ "(" Expression<out e, true> ")" (. e = new ConversionExpr(x, e, toType); .)
| ParensExpression<out e>
- | "real" (. x = t; .)
- "(" (. IToken openParen = t; .)
- Expression<out e, true>
- ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
- IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
- e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
- .)
- | "int" (. x = t; .)
- "(" (. IToken openParen = t; .)
- Expression<out e, true>
- ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
- IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
- e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
- .)
)
.
ParensExpression<out Expression e>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 55dc973f..e8f4948b 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -90,9 +90,6 @@ namespace Microsoft.Dafny {
Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();
Dictionary<int, TupleTypeDecl> tupleTypeDecls = new Dictionary<int, TupleTypeDecl>();
public readonly ClassDecl ObjectDecl;
- public readonly ClassDecl RealClass;
- //public readonly Function RealToInt;
- //public readonly Function IntToReal;
public BuiltIns() {
// create class 'object'
ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile());
@@ -100,22 +97,6 @@ namespace Microsoft.Dafny {
// add one-dimensional arrays, since they may arise during type checking
// Arrays of other dimensions may be added during parsing as the parser detects the need for these
UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
- // add real number functions
- Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List<TypeParameter>(), Token.NoToken,
- new List<Formal> { new Formal(Token.NoToken, "x", Type.Real, true, true) }, Type.Int, new List<Expression>(),
- new List<FrameExpression>(), new List<Expression>(), new Specification<Expression>(new List<Expression>(), null),
- null, null, Token.NoToken);
- Function IntToReal = new Function(Token.NoToken, "IntToReal", true, true, new List<TypeParameter>(), Token.NoToken,
- new List<Formal> { new Formal(Token.NoToken, "x", Type.Int, true, true) }, Type.Real, new List<Expression>(),
- new List<FrameExpression>(), new List<Expression>(), new Specification<Expression>(new List<Expression>(), null),
- null, null, Token.NoToken);
- RealClass = new ClassDecl(Token.NoToken, "Real", SystemModule, new List<TypeParameter>(),
- new List<MemberDecl>() { RealToInt, IntToReal }, DontCompile());
- RealToInt.EnclosingClass = RealClass;
- IntToReal.EnclosingClass = RealClass;
- RealToInt.IsBuiltin = true;
- IntToReal.IsBuiltin = true;
- SystemModule.TopLevelDecls.Add(RealClass);
// Note, in addition to these types, the _System module contains tuple types. These tuple types are added to SystemModule
// by the parser as the parser detects the need for these.
}
@@ -4299,7 +4280,7 @@ namespace Microsoft.Dafny {
public static Expression CreateNot(IToken tok, Expression e) {
Contract.Requires(tok != null);
Contract.Requires(e.Type is BoolType);
- var un = new UnaryExpr(tok, UnaryExpr.Opcode.Not, e);
+ var un = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Not, e);
un.Type = Type.Bool; // resolve here
return un;
}
@@ -4957,18 +4938,20 @@ namespace Microsoft.Dafny {
get { yield return E; }
}
}
- public class FreshExpr : Expression {
+
+ public abstract class UnaryExpr : Expression
+ {
public readonly Expression E;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(E != null);
}
- public FreshExpr(IToken tok, Expression expr)
+ public UnaryExpr(IToken tok, Expression e)
: base(tok) {
Contract.Requires(tok != null);
- Contract.Requires(expr != null);
- E = expr;
+ Contract.Requires(e != null);
+ this.E = e;
}
public override IEnumerable<Expression> SubExpressions {
@@ -4976,35 +4959,38 @@ namespace Microsoft.Dafny {
}
}
- public class UnaryExpr : Expression
+ public class UnaryOpExpr : UnaryExpr
{
public enum Opcode {
- Lit,
Not,
- SeqLength
+ Cardinality,
+ Fresh,
+ Lit, // there is no syntax for this operator, but it is sometimes introduced during translation
}
public readonly Opcode Op;
- public readonly Expression E;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(E != null);
- }
- public UnaryExpr(IToken tok, Opcode op, Expression e)
- : base(tok) {
+ public UnaryOpExpr(IToken tok, Opcode op, Expression e)
+ : base(tok, e) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
this.Op = op;
- this.E = e;
-
}
+ }
- public override IEnumerable<Expression> SubExpressions {
- get { yield return E; }
+ public class ConversionExpr : UnaryExpr
+ {
+ public readonly Type ToType;
+ public ConversionExpr(IToken tok, Expression expr, Type toType)
+ : base(tok, expr) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
+ Contract.Requires(toType != null);
+ ToType = toType;
}
}
- public class BinaryExpr : Expression {
+ public class BinaryExpr : Expression
+ {
public enum Opcode {
Iff,
Imp,
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index a7f058db..55c5e8d5 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1503,7 +1503,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 38) {
GenericInstantiation(gt);
}
- ty = (tok.val == "real") ? (Type)Microsoft.Dafny.Type.Real : new UserDefinedType(tok, tok.val, gt, path);
+ ty = new UserDefinedType(tok, tok.val, gt, path);
} else SynErr(166);
}
@@ -2946,7 +2946,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
NegOp();
x = t;
UnaryExpression(out e, allowSemi);
- e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
+ e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e);
break;
}
case 25: case 30: case 56: case 66: case 72: case 76: case 82: case 83: case 85: case 88: case 121: case 122: case 123: {
@@ -3317,7 +3317,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void ConstAtomExpression(out Expression e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
IToken/*!*/ x; BigInteger n; Basetypes.BigDec d;
- e = dummyExpr;
+ e = dummyExpr; Type toType = null;
switch (la.kind) {
case 113: {
@@ -3356,7 +3356,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(11);
Expression(out e, true);
Expect(12);
- e = new FreshExpr(x, e);
+ e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e);
break;
}
case 118: {
@@ -3372,40 +3372,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
x = t;
Expression(out e, true);
- e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
+ e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Cardinality, e);
Expect(29);
break;
}
- case 11: {
- ParensExpression(out e);
- break;
- }
- case 55: {
- Get();
- x = t;
+ case 54: case 55: {
+ if (la.kind == 54) {
+ Get();
+ x = t; toType = new IntType();
+ } else {
+ Get();
+ x = t; toType = new RealType();
+ }
Expect(11);
- IToken openParen = t;
Expression(out e, true);
Expect(12);
- IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
- IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
- e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
-
+ e = new ConversionExpr(x, e, toType);
break;
}
- case 54: {
- Get();
- x = t;
- Expect(11);
- IToken openParen = t;
- Expression(out e, true);
- Expect(12);
- IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
- IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
- e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
-
+ case 11: {
+ ParensExpression(out e);
break;
}
default: SynErr(221); break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 5be5614d..c6f7126d 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1347,24 +1347,23 @@ namespace Microsoft.Dafny {
PrintExpression(((MultiSetFormingExpr)expr).E, false);
wr.Write(")");
- } else if (expr is FreshExpr) {
- wr.Write("fresh(");
- PrintExpression(((FreshExpr)expr).E, false);
- wr.Write(")");
-
- } else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
- if (e.Op == UnaryExpr.Opcode.SeqLength) {
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
+ if (e.Op == UnaryOpExpr.Opcode.Cardinality) {
wr.Write("|");
PrintExpression(e.E, false);
wr.Write("|");
+ } else if (e.Op == UnaryOpExpr.Opcode.Fresh) {
+ wr.Write("fresh(");
+ PrintExpression(e.E, false);
+ wr.Write(")");
} else {
// Prefix operator.
// determine if parens are needed
string op;
int opBindingStrength;
switch (e.Op) {
- case UnaryExpr.Opcode.Not:
+ case UnaryOpExpr.Opcode.Not:
op = "!"; opBindingStrength = 0x60; break;
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary opcode
@@ -1374,7 +1373,7 @@ namespace Microsoft.Dafny {
bool containsNestedNot = e.E is ParensExpression &&
((ParensExpression)e.E).E is UnaryExpr &&
- ((UnaryExpr)((ParensExpression)e.E).E).Op == UnaryExpr.Opcode.Not;
+ ((UnaryOpExpr)((ParensExpression)e.E).E).Op == UnaryOpExpr.Opcode.Not;
if (parensNeeded) { wr.Write("("); }
wr.Write(op);
@@ -1382,6 +1381,13 @@ namespace Microsoft.Dafny {
if (parensNeeded) { wr.Write(")"); }
}
+ } else if (expr is ConversionExpr) {
+ var e = (ConversionExpr)expr;
+ PrintType(e.ToType);
+ wr.Write("(");
+ PrintExpression(e.E, false);
+ wr.Write(")");
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
// determine if parens are needed
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 73925aef..974fb676 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1266,13 +1266,13 @@ namespace Microsoft.Dafny
var e = (MultiSetFormingExpr)expr;
return new MultiSetFormingExpr(e.tok, CloneExpr(e.E));
- } else if (expr is FreshExpr) {
- var e = (FreshExpr)expr;
- return new FreshExpr(e.tok, CloneExpr(e.E));
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
+ return new UnaryOpExpr(e.tok, e.Op, CloneExpr(e.E));
- } else if (expr is UnaryExpr) {
- var e = (UnaryExpr)expr;
- return new UnaryExpr(e.tok, e.Op, CloneExpr(e.E));
+ } else if (expr is ConversionExpr) {
+ var e = (ConversionExpr)expr;
+ return new ConversionExpr(e.tok, CloneExpr(e.E), CloneType(e.ToType));
} else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
@@ -2173,9 +2173,9 @@ namespace Microsoft.Dafny
}
}
// fall through to do the subexpressions (with cp := Neither)
- } else if (expr is UnaryExpr) {
- var e = (UnaryExpr)expr;
- if (e.Op == UnaryExpr.Opcode.Not) {
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
+ if (e.Op == UnaryOpExpr.Opcode.Not) {
// for the sub-parts, use Invert(cp)
cp = Invert(cp);
return true;
@@ -3455,7 +3455,7 @@ namespace Microsoft.Dafny
mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null));
// ensures fresh(_new - old(_new));
ens = iter.Member_MoveNext.Ens;
- ens.Add(new MaybeFreeExpression(new FreshExpr(iter.tok,
+ ens.Add(new MaybeFreeExpression(new UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Fresh,
new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub,
new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));
@@ -3485,7 +3485,7 @@ namespace Microsoft.Dafny
// ensures !more ==> Ensures;
foreach (var e in iter.Ensures) {
ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,
- new UnaryExpr(iter.tok, UnaryExpr.Opcode.Not, new IdentifierExpr(iter.tok, "more")),
+ new UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Not, new IdentifierExpr(iter.tok, "more")),
e.E),
e.IsFree));
}
@@ -5999,58 +5999,41 @@ namespace Microsoft.Dafny
}
expr.Type = e.Seq.Type;
- }
- else if (e.Seq.Type is UserDefinedType && ((UserDefinedType)e.Seq.Type).IsDatatype)
- {
+ } else if (e.Seq.Type is UserDefinedType && ((UserDefinedType)e.Seq.Type).IsDatatype) {
DatatypeDecl dt = ((UserDefinedType)e.Seq.Type).AsDatatype;
- if (!(e.Index is IdentifierSequence || (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger)))
- {
+ if (!(e.Index is IdentifierSequence || (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger))) {
Error(expr, "datatype updates must be to datatype destructors");
} else {
string destructor_str = null;
- if (e.Index is IdentifierSequence)
- {
+ if (e.Index is IdentifierSequence) {
IdentifierSequence iseq = (IdentifierSequence)e.Index;
- if (iseq.Tokens.Count() != 1)
- {
+ if (iseq.Tokens.Count() != 1) {
Error(expr, "datatype updates must name a single datatype destructor");
- }
- else
- {
+ } else {
destructor_str = iseq.Tokens.First().val;
}
- }
- else
- {
+ } else {
Contract.Assert(e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger);
destructor_str = ((LiteralExpr)e.Index).tok.val;
}
- if (destructor_str != null)
- {
+ if (destructor_str != null) {
MemberDecl member;
- if (!datatypeMembers[dt].TryGetValue(destructor_str, out member))
- {
+ if (!datatypeMembers[dt].TryGetValue(destructor_str, out member)) {
Error(expr, "member {0} does not exist in datatype {1}", destructor_str, dt.Name);
- }
- else
- {
+ } else {
// Rewrite an update of the form "dt[dtor := E]" to be "dtCtr(E, dt.dtor2, dt.dtor3,...)"
DatatypeDestructor destructor = (DatatypeDestructor)member;
DatatypeCtor ctor = destructor.EnclosingCtor;
List<Expression> ctor_args = new List<Expression>();
- foreach (Formal d in ctor.Formals)
- {
- if (d.Name == destructor.Name)
- {
+ foreach (Formal d in ctor.Formals) {
+ if (d.Name == destructor.Name) {
ctor_args.Add(e.Value);
- }
- else
- {
+ } else {
ctor_args.Add(new ExprDotName(expr.tok, e.Seq, d.Name));
}
}
@@ -6063,13 +6046,10 @@ namespace Microsoft.Dafny
}
}
}
- }
- else
- {
+ } else {
Error(expr, "update requires a sequence, map, or datatype (got {0})", e.Seq.Type);
}
-
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
ResolveFunctionCallExpr(e, twoState, codeContext, false);
@@ -6089,50 +6069,66 @@ namespace Microsoft.Dafny
Error(e.tok, "can only form a multiset from a seq or set.");
}
expr.Type = new MultiSetType(((CollectionType)e.E.Type).Arg);
- } else if (expr is FreshExpr) {
- FreshExpr e = (FreshExpr)expr;
- if (!twoState) {
- Error(expr, "fresh expressions are not allowed in this context");
- }
- ResolveExpression(e.E, twoState, codeContext);
- // the type of e.E must be either an object or a collection of objects
- Type t = e.E.Type;
- Contract.Assert(t != null); // follows from postcondition of ResolveExpression
- if (t is CollectionType) {
- t = ((CollectionType)t).Arg;
- }
- if (t is ObjectType) {
- // fine
- } else if (UserDefinedType.DenotesClass(t) != null) {
- // fine
- } else if (t.IsDatatype) {
- // fine, treat this as the datatype itself.
- } else {
- Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type);
- }
- expr.Type = Type.Bool;
- } else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
ResolveExpression(e.E, twoState, codeContext);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
switch (e.Op) {
- case UnaryExpr.Opcode.Not:
+ case UnaryOpExpr.Opcode.Not:
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(expr, "logical negation expects a boolean argument (instead got {0})", e.E.Type);
}
expr.Type = Type.Bool;
break;
- case UnaryExpr.Opcode.SeqLength:
+ case UnaryOpExpr.Opcode.Cardinality:
if (!UnifyTypes(e.E.Type, new CollectionTypeProxy(new InferredTypeProxy()))) {
Error(expr, "size operator expects a collection argument (instead got {0})", e.E.Type);
}
expr.Type = Type.Int;
break;
+ case UnaryOpExpr.Opcode.Fresh:
+ if (!twoState) {
+ Error(expr, "fresh expressions are not allowed in this context");
+ }
+ // the type of e.E must be either an object or a collection of objects
+ Type t = e.E.Type;
+ Contract.Assert(t != null); // follows from postcondition of ResolveExpression
+ if (t is CollectionType) {
+ t = ((CollectionType)t).Arg;
+ }
+ if (t is ObjectType) {
+ // fine
+ } else if (UserDefinedType.DenotesClass(t) != null) {
+ // fine
+ } else if (t.IsDatatype) {
+ // fine, treat this as the datatype itself.
+ } else {
+ Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type);
+ }
+ expr.Type = Type.Bool;
+ break;
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator
}
+ } else if (expr is ConversionExpr) {
+ var e = (ConversionExpr)expr;
+ ResolveType(e.tok, e.ToType, ResolveTypeOption.DontInfer, null);
+ ResolveExpression(e.E, twoState, codeContext);
+ if (e.ToType is IntType) {
+ if (!(e.E.Type is RealType)) {
+ Error(expr, "type conversion to int is allowed only from real (got {0})", e.E.Type);
+ }
+ } else if (e.ToType is RealType) {
+ if (!(e.E.Type is IntType)) {
+ Error(expr, "type conversion to real is allowed only from int (got {0})", e.E.Type);
+ }
+ } else {
+ Error(expr, "type conversions are not supported to this type (got {0})", e.ToType);
+ }
+ e.Type = e.ToType;
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
ResolveExpression(e.E0, twoState, codeContext);
@@ -6837,9 +6833,12 @@ namespace Microsoft.Dafny
Error(expr, "old expressions are allowed only in specification and ghost contexts");
return;
- } else if (expr is FreshExpr) {
- Error(expr, "fresh expressions are allowed only in specification and ghost contexts");
- return;
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
+ if (e.Op == UnaryOpExpr.Opcode.Fresh) {
+ Error(expr, "fresh expressions are allowed only in specification and ghost contexts");
+ return;
+ }
} else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
@@ -7646,8 +7645,8 @@ namespace Microsoft.Dafny
}
// Unary expression
- var u = expr as UnaryExpr;
- if (u != null && u.Op == UnaryExpr.Opcode.Not) {
+ var u = expr as UnaryOpExpr;
+ if (u != null && u.Op == UnaryOpExpr.Opcode.Not) {
foreach (var c in NormalizedConjuncts(u.E, !polarity)) {
yield return c;
}
@@ -7706,7 +7705,7 @@ namespace Microsoft.Dafny
if (polarity) {
yield return expr;
} else {
- expr = new UnaryExpr(expr.tok, UnaryExpr.Opcode.Not, expr);
+ expr = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr);
expr.Type = Type.Bool;
yield return expr;
}
@@ -8017,10 +8016,12 @@ namespace Microsoft.Dafny
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
return UsesSpecFeatures(e.E);
- } else if (expr is FreshExpr) {
- return true;
} else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
+ var e = (UnaryExpr)expr;
+ var unaryOpExpr = e as UnaryOpExpr;
+ if (unaryOpExpr != null && unaryOpExpr.Op == UnaryOpExpr.Opcode.Fresh) {
+ return true;
+ }
return UsesSpecFeatures(e.E);
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
@@ -8102,8 +8103,8 @@ namespace Microsoft.Dafny
CheckCoLemmaConclusions(e.Body, position, coConclusions);
} else if (expr is UnaryExpr) {
- var e = (UnaryExpr)expr;
- if (e.Op == UnaryExpr.Opcode.Not) {
+ var e = (UnaryOpExpr)expr;
+ if (e.Op == UnaryOpExpr.Opcode.Not) {
CheckCoLemmaConclusions(e.E, !position, coConclusions);
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 83623399..a46d98a8 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -112,7 +112,7 @@ namespace Microsoft.Dafny
// ensures Valid();
ctor.Ens.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List<Expression>())));
// ensures fresh(Repr - {this});
- var freshness = new FreshExpr(tok, new BinaryExpr(tok, BinaryExpr.Opcode.Sub,
+ var freshness = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Fresh, new BinaryExpr(tok, BinaryExpr.Opcode.Sub,
new FieldSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"),
new SetDisplayExpr(tok, new List<Expression>() { new ThisExpr(tok) })));
ctor.Ens.Insert(1, new MaybeFreeExpression(freshness));
@@ -265,7 +265,7 @@ namespace Microsoft.Dafny
var e1 = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, Repr, e0);
e1.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference;
e1.Type = Repr.Type;
- var freshness = new FreshExpr(tok, e1);
+ var freshness = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Fresh, e1);
freshness.Type = Type.Bool;
m.Ens.Insert(1, new MaybeFreeExpression(freshness));
}
@@ -345,7 +345,9 @@ namespace Microsoft.Dafny
/// </summary>
static bool MentionsOldState(Expression expr) {
Contract.Requires(expr != null);
- if (expr is OldExpr || expr is FreshExpr) {
+ if (expr is OldExpr) {
+ return true;
+ } else if (expr is UnaryOpExpr && ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh) {
return true;
}
foreach (var ee in expr.SubExpressions) {
@@ -803,7 +805,6 @@ namespace Microsoft.Dafny
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
reqs.AddRange(generateAutoReqs(e.E));
- } else if (expr is FreshExpr) {
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
Expression arg = e.E;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3680d4dc..827d712a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1329,7 +1329,7 @@ namespace Microsoft.Dafny {
old_nw.Type = nw.Type; // resolve here
var setDiff = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub, nw, old_nw);
setDiff.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference; setDiff.Type = nw.Type; // resolve here
- Expression cond = new FreshExpr(iter.tok, setDiff);
+ Expression cond = new UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Fresh, setDiff);
cond.Type = Type.Bool; // resolve here
builder.Add(new Bpl.AssumeCmd(iter.tok, yeEtran.TrExpr(cond)));
@@ -1800,7 +1800,7 @@ namespace Microsoft.Dafny {
args.Add(Lit(formal));
var ie = new IdentifierExpr(p.tok, p.AssignUniqueName(f));
ie.Var = p; ie.Type = ie.Var.Type;
- var l = new UnaryExpr(p.tok, UnaryExpr.Opcode.Lit, ie);
+ var l = new UnaryOpExpr(p.tok, UnaryOpExpr.Opcode.Lit, ie);
l.Type = ie.Var.Type;
substMap.Add(p, l);
} else {
@@ -3156,13 +3156,9 @@ namespace Microsoft.Dafny {
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
return CanCallAssumption(e.E, etran);
- } else if (expr is FreshExpr) {
- FreshExpr e = (FreshExpr)expr;
- return CanCallAssumption(e.E, etran);
} else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
- Bpl.Expr t = CanCallAssumption(e.E, etran);
- return t;
+ var e = (UnaryExpr)expr;
+ return CanCallAssumption(e.E, etran);
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
Bpl.Expr t0 = CanCallAssumption(e.E0, etran);
@@ -3718,9 +3714,6 @@ namespace Microsoft.Dafny {
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
CheckWellformed(e.E, options, locals, builder, etran);
- } else if (expr is FreshExpr) {
- FreshExpr e = (FreshExpr)expr;
- CheckWellformed(e.E, options, locals, builder, etran);
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
CheckWellformed(e.E, options, locals, builder, etran);
@@ -8547,50 +8540,15 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException();
}
-
- } else if (expr is FreshExpr) {
- FreshExpr e = (FreshExpr)expr;
- if (e.E.Type is SetType) {
- // generate: (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])
- // TODO: trigger?
- Bpl.Variable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));
- Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
- Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
- Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);
- Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o));
- Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);
- return new Bpl.ForallExpr(expr.tok, new List<Variable> { oVar }, body);
- } else if (e.E.Type is SeqType) {
- // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Unbox(Seq#Index(X,$i)),alloc])
- // TODO: trigger?
- Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
- Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);
- Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);
- Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);
- XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI);
- Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, XsubI));
- Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(XsubI, predef.Null);
- Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);
- return new Bpl.ForallExpr(expr.tok, new List<Variable> { iVar }, body);
- } else if (e.E.Type.IsDatatype) {
- Bpl.Expr alloc = translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);
- return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, alloc);
- } else {
- // generate: x != null && !old($Heap)[x]
- Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null);
- Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));
- return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And, oNull, oIsFresh);
- }
-
- } else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
Bpl.Expr arg = TrExpr(e.E);
switch (e.Op) {
- case UnaryExpr.Opcode.Lit:
+ case UnaryOpExpr.Opcode.Lit:
return translator.Lit(arg);
- case UnaryExpr.Opcode.Not:
+ case UnaryOpExpr.Opcode.Not:
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
- case UnaryExpr.Opcode.SeqLength:
+ case UnaryOpExpr.Opcode.Cardinality:
if (e.E.Type is SeqType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
} else if (e.E.Type is SetType) {
@@ -8602,10 +8560,55 @@ namespace Microsoft.Dafny {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected sized type
}
+ case UnaryOpExpr.Opcode.Fresh:
+ if (e.E.Type is SetType) {
+ // generate: (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])
+ // TODO: trigger?
+ Bpl.Variable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));
+ Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
+ Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
+ Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);
+ Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o));
+ Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);
+ return new Bpl.ForallExpr(expr.tok, new List<Variable> { oVar }, body);
+ } else if (e.E.Type is SeqType) {
+ // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Unbox(Seq#Index(X,$i)),alloc])
+ // TODO: trigger?
+ Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
+ Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);
+ Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);
+ Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);
+ XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI);
+ Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, XsubI));
+ Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(XsubI, predef.Null);
+ Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);
+ return new Bpl.ForallExpr(expr.tok, new List<Variable> { iVar }, body);
+ } else if (e.E.Type.IsDatatype) {
+ Bpl.Expr alloc = translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, alloc);
+ } else {
+ // generate: x != null && !old($Heap)[x]
+ Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null);
+ Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And, oNull, oIsFresh);
+ }
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
}
+ } else if (expr is ConversionExpr) {
+ var e = (ConversionExpr)expr;
+ Bpl.ArithmeticCoercion.CoercionType ct;
+ if (e.ToType is IntType) {
+ ct = Bpl.ArithmeticCoercion.CoercionType.ToInt;
+ } else if (e.ToType is RealType) {
+ ct = Bpl.ArithmeticCoercion.CoercionType.ToReal;
+ } else {
+ Contract.Assert(false); // unexpected ConversionExpr to-type
+ ct = Bpl.ArithmeticCoercion.CoercionType.ToInt; // please compiler
+ }
+ return new Bpl.NAryExpr(e.tok, new ArithmeticCoercion(e.tok, ct), new List<Expr> { TrExpr(e.E) });
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
bool isReal = e.E0.Type is RealType;
@@ -9921,9 +9924,9 @@ namespace Microsoft.Dafny {
return TrSplitExpr(d, splits, position, heightLimit, etran);
}
- } else if (expr is UnaryExpr) {
- var e = (UnaryExpr)expr;
- if (e.Op == UnaryExpr.Opcode.Not) {
+ } else if (expr is UnaryOpExpr) {
+ var e = (UnaryOpExpr)expr;
+ if (e.Op == UnaryOpExpr.Opcode.Not) {
var ss = new List<SplitExprInfo>();
if (TrSplitExpr(e.E, ss, !position, heightLimit, etran)) {
foreach (var s in ss) {
@@ -10651,7 +10654,7 @@ namespace Microsoft.Dafny {
usesHeap = true;
} else if (expr is FunctionCallExpr) {
usesHeap = true;
- } else if (expr is FreshExpr) {
+ } else if (expr is UnaryOpExpr && ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh) {
usesOldHeap = true;
}
@@ -10886,12 +10889,6 @@ namespace Microsoft.Dafny {
if (se != e.E) {
newExpr = new OldExpr(expr.tok, se);
}
- } else if (expr is FreshExpr) {
- FreshExpr e = (FreshExpr)expr;
- Expression se = Substitute(e.E);
- if (se != e.E) {
- newExpr = new FreshExpr(expr.tok, se);
- }
} else if (expr is MultiSetFormingExpr) {
var e = (MultiSetFormingExpr)expr;
var se = Substitute(e.E);
@@ -10905,10 +10902,18 @@ namespace Microsoft.Dafny {
newExpr = new BoxingCastExpr(se, e.FromType, e.ToType);
}
} else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
+ var e = (UnaryExpr)expr;
Expression se = Substitute(e.E);
if (se != e.E) {
- newExpr = new UnaryExpr(expr.tok, e.Op, se);
+ if (e is UnaryOpExpr) {
+ var ee = (UnaryOpExpr)e;
+ newExpr = new UnaryOpExpr(expr.tok, ee.Op, se);
+ } else if (e is ConversionExpr) {
+ var ee = (ConversionExpr)e;
+ newExpr = new ConversionExpr(expr.tok, se, ee.ToType);
+ } else {
+ Contract.Assert(false); // unexpected UnaryExpr subtype
+ }
}
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 21:03:19 +0000