diff options
Diffstat (limited to 'Dafny/RefinementTransformer.cs')
-rw-r--r-- | Dafny/RefinementTransformer.cs | 69 |
1 files changed, 37 insertions, 32 deletions
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index c97f47aa..6954ee87 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -19,13 +19,14 @@ using System.Diagnostics.Contracts; using IToken = Microsoft.Boogie.IToken;
namespace Microsoft.Dafny {
- public class RefinementToken : IToken
+ public class RefinementToken : TokenWrapper
{
- readonly IToken tok;
public readonly ModuleDecl InheritingModule;
public RefinementToken(IToken tok, ModuleDecl m)
+ : base(tok)
{
- this.tok = tok;
+ Contract.Requires(tok != null);
+ Contract.Requires(m != null);
this.InheritingModule = m;
}
@@ -43,34 +44,10 @@ namespace Microsoft.Dafny { var rtok = tok as RefinementToken;
return rtok != null && rtok.InheritingModule == m;
}
-
- public int kind {
- get { return tok.kind; }
- set { throw new NotSupportedException(); }
- }
- public string filename {
- get { return tok.filename + "[" + InheritingModule.Name + "]"; }
- set { throw new NotSupportedException(); }
- }
- public int pos {
- get { return tok.pos; }
- set { throw new NotSupportedException(); }
- }
- public int col {
- get { return tok.col; }
- set { throw new NotSupportedException(); }
- }
- public int line {
- get { return tok.line; }
+ public override string filename {
+ get { return WrappedToken.filename + "[" + InheritingModule.Name + "]"; }
set { throw new NotSupportedException(); }
}
- public string/*!*/ val {
- get { return tok.val; }
- set { throw new NotSupportedException(); }
- }
- public bool IsValid {
- get { return tok.IsValid; }
- }
}
public class RefinementTransformer
@@ -548,12 +525,16 @@ namespace Microsoft.Dafny { var decreases = CloneSpecExpr(f.Decreases);
var body = CloneExpr(f.Body);
if (moreBody != null) {
- body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, body, moreBody);
+ if (body == null) {
+ body = moreBody;
+ } else {
+ body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, body, moreBody);
+ }
}
if (f is Predicate) {
return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.OpenParen, formals,
- req, reads, ens, decreases, body, null);
+ req, reads, ens, decreases, body, moreBody != null, null);
} else {
return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.OpenParen, formals, CloneType(f.ResultType),
req, reads, ens, decreases, body, null);
@@ -604,7 +585,7 @@ namespace Microsoft.Dafny { reporter.Error(nwMember, "a refining function is not allowed to provided a body");
newBody = null;
}
- nw.Members[index] = CloneFunction((Function)member, f.Ens, f.Body);
+ nw.Members[index] = CloneFunction((Function)member, f.Ens, newBody);
}
} else {
@@ -637,5 +618,29 @@ namespace Microsoft.Dafny { return nw;
}
+
+ // ---------------------- additional methods -----------------------------------------------------------------------------
+
+ public static bool ContainsChange(Expression expr, ModuleDecl m) {
+ Contract.Requires(expr != null);
+ Contract.Requires(m != null);
+
+ if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ if (e.Function.EnclosingClass.Module == m) {
+ var p = e.Function as Predicate;
+ if (p != null && p.BodyIsExtended) {
+ return true;
+ }
+ }
+ }
+
+ foreach (var ee in expr.SubExpressions) {
+ if (ContainsChange(ee, m)) {
+ return true;
+ }
+ }
+ return false;
+ }
}
}
|