diff options
| author |  leino <unknown> | 2015-01-23 16:17:23 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-01-23 16:17:23 -0800 |
| commit | 227fa997dd25a41c8bfc86d919635b6677df2c5f (patch) | |
| tree | 4ac05f6efa2a3d51ff46118c61567f3b1f52d120 /Source/Dafny/RefinementTransformer.cs | |
| parent | 97e7528b3cd3e9b9e21b75abf817d6e0ed3b9df7 (diff) | |
Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, so use the new name resolution machinery that handles modules and type parameters
Included some inadvertently left-out test cases in dafny0/Modules0.dfy
Fixed comparable-types tests
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 8234846e..6067ed50 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -332,10 +332,7 @@ namespace Microsoft.Dafny if (newMem is Function) {
CheckFunctionsAreRefinements((Function)newMem, (Function)m);
} else {
- bool isPredicate = m is Predicate;
- bool isCoPredicate = m is CoPredicate;
- string s = isPredicate ? "predicate" : isCoPredicate ? "copredicate" : "function";
- reporter.Error(newMem, "{0} must be refined by a {0}", s);
+ reporter.Error(newMem, "{0} must be refined by a {0}", m.WhatKind);
}
}
} else {
@@ -690,19 +687,18 @@ namespace Microsoft.Dafny var f = (Function)nwMember;
bool isPredicate = f is Predicate;
bool isCoPredicate = f is CoPredicate;
- string s = isPredicate ? "predicate" : isCoPredicate ? "copredicate" : "function";
if (!(member is Function) || (isPredicate && !(member is Predicate)) || (isCoPredicate && !(member is CoPredicate))) {
- reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", s, nwMember.Name);
+ reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", f.WhatKind, nwMember.Name);
} else {
var prevFunction = (Function)member;
if (f.Req.Count != 0) {
- reporter.Error(f.Req[0].tok, "a refining {0} is not allowed to add preconditions", s);
+ reporter.Error(f.Req[0].tok, "a refining {0} is not allowed to add preconditions", f.WhatKind);
}
if (f.Reads.Count != 0) {
- reporter.Error(f.Reads[0].E.tok, "a refining {0} is not allowed to extend the reads clause", s);
+ reporter.Error(f.Reads[0].E.tok, "a refining {0} is not allowed to extend the reads clause", f.WhatKind);
}
if (f.Decreases.Expressions.Count != 0) {
- reporter.Error(f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", s);
+ reporter.Error(f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", f.WhatKind);
}
if (prevFunction.HasStaticKeyword != f.HasStaticKeyword) {
|