diff options
Diffstat (limited to 'Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Dafny/RefinementTransformer.cs | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index e0f12246..6af14b14 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -473,21 +473,26 @@ namespace Microsoft.Dafny }
Expression body;
+ Predicate.BodyOriginKind bodyOrigin;
if (replacementBody != null) {
body = replacementBody;
+ bodyOrigin = Predicate.BodyOriginKind.DelayedDefinition;
} else if (moreBody != null) {
if (f.Body == null) {
body = moreBody;
+ bodyOrigin = Predicate.BodyOriginKind.DelayedDefinition;
} else {
body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, refinementCloner.CloneExpr(f.Body), moreBody);
+ bodyOrigin = Predicate.BodyOriginKind.Extension;
}
} else {
body = refinementCloner.CloneExpr(f.Body);
+ bodyOrigin = Predicate.BodyOriginKind.OriginalOrInherited;
}
if (f is Predicate) {
return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
- req, reads, ens, decreases, body, moreBody != null, null, false);
+ req, reads, ens, decreases, body, bodyOrigin, null, false);
} else if (f is CoPredicate) {
return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,
req, reads, ens, body, null, false);
@@ -497,14 +502,14 @@ namespace Microsoft.Dafny }
}
- Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, BlockStmt replacementBody) {
+ Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, Specification<Expression> decreases, BlockStmt replacementBody) {
Contract.Requires(m != null);
+ Contract.Requires(decreases != null);
var tps = m.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam);
var ins = m.Ins.ConvertAll(refinementCloner.CloneFormal);
var req = m.Req.ConvertAll(refinementCloner.CloneMayBeFreeExpr);
var mod = refinementCloner.CloneSpecFrameExpr(m.Mod);
- var decreases = refinementCloner.CloneSpecExpr(m.Decreases);
List<MaybeFreeExpression> ens;
if (replacementBody != null)
@@ -592,10 +597,10 @@ namespace Microsoft.Dafny Expression moreBody = null;
Expression replacementBody = null;
- if (isPredicate) {
- moreBody = f.Body;
- } else if (prevFunction.Body == null) {
+ if (prevFunction.Body == null) {
replacementBody = f.Body;
+ } else if (isPredicate) {
+ moreBody = f.Body;
} else if (f.Body != null) {
reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");
}
@@ -614,10 +619,15 @@ namespace Microsoft.Dafny if (m.Mod.Expressions.Count != 0) {
reporter.Error(m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause");
}
- if (m.Decreases.Expressions.Count != 0) {
- reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported");
+ Specification<Expression> decreases;
+ if (Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) {
+ decreases = m.Decreases;
+ } else {
+ if (m.Decreases.Expressions.Count != 0) {
+ reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported, unless the refined method was specified with 'decreases *'");
+ }
+ decreases = refinementCloner.CloneSpecExpr(prevMethod.Decreases);
}
-
if (prevMethod.IsStatic != m.IsStatic) {
reporter.Error(m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name);
}
@@ -644,7 +654,7 @@ namespace Microsoft.Dafny replacementBody = MergeBlockStmt(replacementBody, prevMethod.Body);
}
}
- nw.Members[index] = CloneMethod(prevMethod, m.Ens, replacementBody);
+ nw.Members[index] = CloneMethod(prevMethod, m.Ens, decreases, replacementBody);
}
}
}
@@ -1263,7 +1273,7 @@ namespace Microsoft.Dafny var e = (FunctionCallExpr)expr;
if (e.Function.EnclosingClass.Module == m) {
var p = e.Function as Predicate;
- if (p != null && p.BodyIsExtended) {
+ if (p != null && p.BodyOrigin == Predicate.BodyOriginKind.Extension) {
return true;
}
}
@@ -1283,7 +1293,7 @@ namespace Microsoft.Dafny public RefinementCloner(ModuleDefinition m) {
moduleUnderConstruction = m;
}
- override public IToken Tok(IToken tok) {
+ public override IToken Tok(IToken tok) {
return new RefinementToken(tok, moduleUnderConstruction);
}
}
|