diff options
| author |  leino <unknown> | 2014-08-20 20:21:47 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-20 20:21:47 -0700 |
| commit | 61d55705cdf6a710f1a21ddb2ae2caaa314ca7f6 (patch) | |
| tree | eb71616351742e3e1e5b56b334065df860a904af /Source/Dafny/RefinementTransformer.cs | |
| parent | 3b51d9251d78bd3de763c951102677eecd764984 (diff) | |
Start of derived types (aka "new types")
Fixed bug in type checking for integer division.
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index a7989cba..88d3fd24 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -159,10 +159,15 @@ namespace Microsoft.Dafny }
} else if (dDemandsEqualitySupport) {
if (nw is ClassDecl) {
- // fine, as long as "nw" does not take any type parameters
+ // fine, as long as "nw" takes the right number of type parameters
if (nw.TypeArgs.Count != d.TypeArgs.Count) {
reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
}
+ } else if (nw is DerivedTypeDecl) {
+ // fine, as long as "nw" does not take any type parameters
+ if (nw.TypeArgs.Count != 0) {
+ reporter.Error(nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a derived type, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");
+ }
} else if (nw is CoDatatypeDecl) {
reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
} else {
|