diff options
| author |  chrishaw <unknown> | 2015-04-02 19:59:14 -0700 |
|---|---|---|
| committer | chrishaw <unknown> | 2015-04-02 19:59:14 -0700 |
| commit | 4d502277ed355fc739cf0c1856044c30645fcd13 (patch) | |
| tree | 67d4b59eb4b1735e18119c87a8ce7b793f0d8ad3 | |
| parent | 8a332057c2c9fc76e5fb112d430404d1aa47ea0d (diff) | |
Eliminate redundant checks of newtype and opaque function well-formedness from included files
| -rw-r--r-- | Source/Dafny/Dafny.atg | 4 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 5 |
4 files changed, 10 insertions, 5 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a9653439..56d8a431 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -737,8 +737,8 @@ NewtypeDecl<ModuleDefinition module, out TopLevelDecl td> NoUSIdent<out bvId>
[ ":" Type<out baseType> ] (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } .)
"|"
- Expression<out wh, false, true> (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
- | Type<out baseType> (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)
+ Expression<out wh, false, true> (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
+ | Type<out baseType> (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .)
)
.
OtherTypeDecl<ModuleDefinition module, out TopLevelDecl td>
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 6342e9c7..3085c975 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -795,10 +795,10 @@ bool IsType(ref IToken pt) { if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); }
Expect(22);
Expression(out wh, false, true);
- td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs);
+ td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs);
} else if (StartOf(3)) {
Type(out baseType);
- td = new NewtypeDecl(id, id.val, module, baseType, attrs);
+ td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs);
} else SynErr(142);
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 4cda8fd8..091ee24a 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -492,7 +492,7 @@ namespace Microsoft.Dafny newToken._val = fWithBody.Name;
newToken._kind = f.tok.kind;
newToken._pos = f.tok.pos;
- fWithBody.tok = newToken;
+ fWithBody.tok = (f.tok is IncludeToken) ? new IncludeToken(newToken) : (Boogie.IToken)newToken;
// Annotate the new function so we remember that we introduced it
fWithBody.Attributes = new Attributes("opaque_full", new List<Expression>(), fWithBody.Attributes);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 96405daf..9160248c 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4154,6 +4154,11 @@ namespace Microsoft.Dafny { Contract.Requires(currentModule == null && codeContext == null);
Contract.Ensures(currentModule == null && codeContext == null);
+ if (decl.tok is IncludeToken) {
+ // Checked in other file
+ return;
+ }
+
// If there's no constraint, there's nothing to do
if (decl.Var == null) {
return;
|