diff options
| author |  rustanleino <unknown> | 2009-11-05 01:24:43 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-05 01:24:43 +0000 |
| commit | ddede5ad5f9236d8ee4e1e75ba3ecfd7077d9296 (patch) | |
| tree | b2c7adc1e94b67d774aec3520d9c285662f94b60 /Source/Dafny/Resolver.ssc | |
| parent | b5a942353fc4cf0b6a6c3df853860171e421a26a (diff) | |
Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "!(x in S)".
Changed Dafny test files to use the new operator.
Included the file b8.dfy into the VSI-Benchmarks test harness.
Diffstat (limited to 'Source/Dafny/Resolver.ssc')
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 66cdabe1..2159d3dc 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -1201,6 +1201,7 @@ namespace Microsoft.Dafny { break;
case BinaryExpr.Opcode.In:
+ case BinaryExpr.Opcode.NotIn:
if (!UnifyTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type))) {
Error(expr, "second argument to {0} must be a set or sequence of type {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
}
@@ -1355,6 +1356,12 @@ namespace Microsoft.Dafny { } else {
return BinaryExpr.ResolvedOpcode.InSeq;
}
+ case BinaryExpr.Opcode.NotIn:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.NotInSet;
+ } else {
+ return BinaryExpr.ResolvedOpcode.NotInSeq;
+ }
case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div;
case BinaryExpr.Opcode.Mod: return BinaryExpr.ResolvedOpcode.Mod;
default:
|