diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 50 |
1 files changed, 45 insertions, 5 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 197a603e..19a0da05 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -897,6 +897,8 @@ namespace Microsoft.Dafny { return b is ObjectType;
} else if (a is SetType) {
return b is SetType && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg);
+ } else if (a is MultiSetType) {
+ return b is MultiSetType && UnifyTypes(((MultiSetType)a).Arg, ((MultiSetType)b).Arg);
} else if (a is SeqType) {
return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg);
} else if (a is UserDefinedType) {
@@ -994,7 +996,7 @@ namespace Microsoft.Dafny { } else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
- if (t is IntType || t is SetType || (opProxy.AllowSeq && t is SeqType)) {
+ if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
// this is the expected case
} else {
return false;
@@ -2097,6 +2099,8 @@ namespace Microsoft.Dafny { return type;
} else if (type is SetType) {
return new SetType(arg);
+ } else if (type is MultiSetType) {
+ return new MultiSetType(arg);
} else if (type is SeqType) {
return new SeqType(arg);
} else {
@@ -2301,6 +2305,8 @@ namespace Microsoft.Dafny { }
if (expr is SetDisplayExpr) {
expr.Type = new SetType(elementType);
+ } else if (expr is MultiSetDisplayExpr) {
+ expr.Type = new MultiSetType(elementType);
} else {
expr.Type = new SeqType(elementType);
}
@@ -2477,12 +2483,13 @@ namespace Microsoft.Dafny { break;
case BinaryExpr.Opcode.Disjoint:
- if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy()))) {
- Error(expr, "arguments must be of a set type (got {0})", e.E0.Type);
- }
+ // TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.
if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
}
+ if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy())) && !UnifyTypes(e.E0.Type, new MultiSetType(new InferredTypeProxy()))) {
+ Error(expr, "arguments must be of a [multi]set type (got {0})", e.E0.Type);
+ }
expr.Type = Type.Bool;
break;
@@ -3137,6 +3144,12 @@ namespace Microsoft.Dafny { goto CHECK_NEXT_BOUND_VARIABLE;
}
break;
+ case BinaryExpr.ResolvedOpcode.InMultiSet:
+ if (whereIsBv == 0) {
+ bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
+ goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
case BinaryExpr.ResolvedOpcode.InSeq:
if (whereIsBv == 0) {
bounds.Add(new QuantifierExpr.SeqBoundedPool(e1));
@@ -3553,6 +3566,8 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Eq:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.SetEq;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetEq;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.SeqEq;
} else {
@@ -3561,17 +3576,26 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Neq:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.SetNeq;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetNeq;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.SeqNeq;
} else {
return BinaryExpr.ResolvedOpcode.NeqCommon;
}
- case BinaryExpr.Opcode.Disjoint: return BinaryExpr.ResolvedOpcode.Disjoint;
+ case BinaryExpr.Opcode.Disjoint:
+ if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetDisjoint;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Disjoint;
+ }
case BinaryExpr.Opcode.Lt:
if (operandType.IsDatatype) {
return BinaryExpr.ResolvedOpcode.RankLt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSubset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.ProperMultiSubset;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.ProperPrefix;
} else {
@@ -3580,6 +3604,8 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Le:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Subset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSubset;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.Prefix;
} else {
@@ -3588,6 +3614,8 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Add:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Union;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetUnion;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.Concat;
} else {
@@ -3596,12 +3624,16 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Sub:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.SetDifference;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetDifference;
} else {
return BinaryExpr.ResolvedOpcode.Sub;
}
case BinaryExpr.Opcode.Mul:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Intersection;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetIntersection;
} else {
return BinaryExpr.ResolvedOpcode.Mul;
}
@@ -3610,24 +3642,32 @@ namespace Microsoft.Dafny { return BinaryExpr.ResolvedOpcode.RankGt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSuperset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.ProperMultiSuperset;
} else {
return BinaryExpr.ResolvedOpcode.Gt;
}
case BinaryExpr.Opcode.Ge:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Superset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSuperset;
} else {
return BinaryExpr.ResolvedOpcode.Ge;
}
case BinaryExpr.Opcode.In:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.InSet;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.InMultiSet;
} else {
return BinaryExpr.ResolvedOpcode.InSeq;
}
case BinaryExpr.Opcode.NotIn:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.NotInSet;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.NotInMultiSet;
} else {
return BinaryExpr.ResolvedOpcode.NotInSeq;
}
|