diff options
| author |  qunyanm <unknown> | 2015-04-20 13:07:23 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-20 13:07:23 -0700 |
| commit | 9c230b0c9037c30879e865aa5b6d994fee5820ff (patch) | |
| tree | 18346dc55e7170c5b2b1663639adfa3444ab2fc0 /Source | |
| parent | d248da33b7763b8c3b2ef75ece9612a45182e7b0 (diff) | |
Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Translator.cs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index aa3e1854..eac28b05 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -11061,14 +11061,15 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.InMap: {
bool finite = e.E1.Type.AsMapType.Finite;
var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;
- return Bpl.Expr.Select(translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
+ return Bpl.Expr.SelectTok(expr.tok, translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
BoxIfNecessary(expr.tok, e0, e.E0.Type));
}
case BinaryExpr.ResolvedOpcode.NotInMap: {
bool finite = e.E1.Type.AsMapType.Finite;
var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;
- return Bpl.Expr.Not(Bpl.Expr.Select(translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
- BoxIfNecessary(expr.tok, e0, e.E0.Type)));
+ Bpl.Expr inMap = Bpl.Expr.SelectTok(expr.tok, translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),
+ BoxIfNecessary(expr.tok, e0, e.E0.Type));
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, inMap);
}
case BinaryExpr.ResolvedOpcode.MapDisjoint: {
return translator.FunctionCall(expr.tok, BuiltinFunction.MapDisjoint, null, e0, e1);
|