diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-30 16:29:33 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-30 16:29:33 -0700 |
| commit | dcc10fd61f7056542bc61c096a851aa76f6d688f (patch) | |
| tree | b0e0de635fe5ca887f94cd4e5b928515e66d0365 /Source/Dafny/RefinementTransformer.cs | |
| parent | 40d21f0057a4d0ce9fc184aae375e2404f00f51e (diff) | |
Dafny: for refinements, don't consider a newly provided predicate body to be an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index e0f12246..28387f16 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/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);
@@ -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");
}
@@ -1263,7 +1268,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 +1288,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);
}
}
|