diff options
| author |  Rustan Leino <unknown> | 2013-12-19 18:32:23 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-19 18:32:23 -0800 |
| commit | bf57c570f53037e225af26378c9e90cf8f85e08b (patch) | |
| tree | 8ea159d4634bf99c7416dd0f7cc0dc45bbf13038 /Source/Dafny/Dafny.atg | |
| parent | 72dba23b3ec67244cdf7c598a953bf4fdf32a001 (diff) | |
Added an .EndTok for every statement. (Note, in some places, especially in VarDecl statements, there's often no good .EndTok information.)
Used the .EndTok in CaptureState information. In other words, move the blue dots in the IDE to after the statement just executed.
Removed /*!*/ comments in some parts of the source code -- CodeContracts reveal this information.
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 112 |
1 files changed, 58 insertions, 54 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 9432b54d..a0a8e699 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -88,7 +88,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyExpr = new LiteralExpr(Token.NoToken);
dummyRhs = new ExprRhs(dummyExpr, null);
dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
- dummyStmt = new ReturnStmt(Token.NoToken, null);
+ dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null);
dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
theModule = module;
theBuiltIns = builtIns;
@@ -423,7 +423,7 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost> WildIdent<out id, true>
[ ":" Type<out ty> (. optType = ty; .)
]
- (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
+ (. var = new VarDecl(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
.
IdentTypeOptional<out BoundVar/*!*/ var>
= (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
@@ -487,9 +487,10 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter> bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
+ IToken iteratorKeywordTok;
.)
SYNC
- "iterator"
+ "iterator" (. iteratorKeywordTok = t; .)
{ Attribute<ref attrs> }
NoUSIdent<out id>
(
@@ -505,7 +506,7 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter> { IteratorSpec<reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs> }
[ BlockStmt<out body, out bodyStart, out bodyEnd>
]
- (. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
+ (. iter = new IteratorDecl(iteratorKeywordTok, id, id.val, module, typeArgs, ins, outs,
new Specification<FrameExpression>(reads, readsAttrs),
new Specification<FrameExpression>(mod, modAttrs),
new Specification<Expression>(decreases, decrAttrs),
@@ -967,7 +968,7 @@ BlockStmt<out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd> { Stmt<body>
}
"}" (. bodyEnd = t;
- block = new BlockStmt(bodyStart, body); .)
+ block = new BlockStmt(bodyStart, bodyEnd, body); .)
.
Stmt<.List<Statement/*!*/>/*!*/ ss.>
= (. Statement/*!*/ s;
@@ -1002,10 +1003,9 @@ OneStmt<out Statement/*!*/ s> }
)
SYNC
- ";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
+ ";" (. s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount); .)
| ReturnStmt<out s>
| SkeletonStmt<out s>
- ";"
)
.
@@ -1029,7 +1029,8 @@ SkeletonStmt<out Statement s> }
.)
]
- (. s = new SkeletonStatement(dotdotdot, names, exprs); .)
+ ";"
+ (. s = new SkeletonStatement(dotdotdot, t, names, exprs); .)
.
ReturnStmt<out Statement/*!*/ s>
= (.
@@ -1047,9 +1048,9 @@ ReturnStmt<out Statement/*!*/ s> }
]
";" (. if (isYield) {
- s = new YieldStmt(returnTok, rhss);
+ s = new YieldStmt(returnTok, t, rhss);
} else {
- s = new ReturnStmt(returnTok, rhss);
+ s = new ReturnStmt(returnTok, t, rhss);
}
.)
.
@@ -1058,14 +1059,14 @@ UpdateStmt<out Statement/*!*/ s> List<AssignmentRhs> rhss = new List<AssignmentRhs>();
Expression e; AssignmentRhs r;
Expression lhs0;
- IToken x;
+ IToken x, endTok = Token.NoToken;
Attributes attrs = null;
IToken suchThatAssume = null;
Expression suchThat = null;
.)
Lhs<out e> (. x = e.tok; .)
( { Attribute<ref attrs> }
- ";" (. rhss.Add(new ExprRhs(e, attrs)); .)
+ ";" (. endTok = t; rhss.Add(new ExprRhs(e, attrs)); .)
| (. lhss.Add(e); lhs0 = e; .)
{ "," Lhs<out e> (. lhss.Add(e); .)
}
@@ -1078,16 +1079,16 @@ UpdateStmt<out Statement/*!*/ s> ]
Expression<out suchThat>
)
- ";"
+ ";" (. endTok = t; .)
| ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
)
(. if (suchThat != null) {
- s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
+ s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
if (lhss.Count == 0 && rhss.Count == 0) {
- s = new BlockStmt(x, new List<Statement>()); // error, give empty statement
+ s = new BlockStmt(x, endTok, new List<Statement>()); // error, give empty statement
} else {
- s = new UpdateStmt(x, lhss, rhss);
+ s = new UpdateStmt(x, endTok, lhss, rhss);
}
}
.)
@@ -1136,6 +1137,7 @@ VarDeclStatement<.out Statement/*!*/ s.> IToken suchThatAssume = null;
Expression suchThat = null;
Attributes attrs = null;
+ IToken endTok;
.)
[ "ghost" (. isGhost = true; x = t; .)
]
@@ -1158,14 +1160,14 @@ VarDeclStatement<.out Statement/*!*/ s.> ]
Expression<out suchThat>
]
- ";"
+ ";" (. endTok = t; .)
(. ConcreteUpdateStatement update;
if (suchThat != null) {
var ies = new List<Expression>();
foreach (var lhs in lhss) {
ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
}
- update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);
+ update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume);
} else if (rhss.Count == 0) {
update = null;
} else {
@@ -1173,9 +1175,9 @@ VarDeclStatement<.out Statement/*!*/ s.> foreach (var lhs in lhss) {
ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
}
- update = new UpdateStmt(assignTok, ies, rhss);
+ update = new UpdateStmt(assignTok, endTok, ies, rhss);
}
- s = new VarDeclStmt(x, lhss, update);
+ s = new VarDeclStmt(x, endTok, lhss, update);
.)
.
IfStmt<out Statement/*!*/ ifStmt>
@@ -1185,34 +1187,34 @@ IfStmt<out Statement/*!*/ ifStmt> BlockStmt/*!*/ bs;
Statement/*!*/ s;
Statement els = null;
- IToken bodyStart, bodyEnd;
+ IToken bodyStart, bodyEnd, endTok;
List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
.)
"if" (. x = t; .)
(
IF(IsAlternative())
- AlternativeBlock<out alternatives>
- (. ifStmt = new AlternativeStmt(x, alternatives); .)
+ AlternativeBlock<out alternatives, out endTok>
+ (. ifStmt = new AlternativeStmt(x, endTok, alternatives); .)
|
( Guard<out guard>
| "..." (. guardOmitted = true; .)
)
- BlockStmt<out thn, out bodyStart, out bodyEnd>
+ BlockStmt<out thn, out bodyStart, out bodyEnd> (. endTok = thn.EndTok; .)
[ "else"
- ( IfStmt<out s> (. els = s; .)
- | BlockStmt<out bs, out bodyStart, out bodyEnd> (. els = bs; .)
+ ( IfStmt<out s> (. els = s; endTok = s.EndTok; .)
+ | BlockStmt<out bs, out bodyStart, out bodyEnd> (. els = bs; endTok = bs.EndTok; .)
)
]
(. if (guardOmitted) {
- ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
+ ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), true, false);
} else {
- ifStmt = new IfStmt(x, guard, thn, els);
+ ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
.)
)
.
-AlternativeBlock<.out List<GuardedAlternative> alternatives.>
+AlternativeBlock<.out List<GuardedAlternative> alternatives, out IToken endTok.>
= (. alternatives = new List<GuardedAlternative>();
IToken x;
Expression e;
@@ -1226,7 +1228,7 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.> { Stmt<body> }
(. alternatives.Add(new GuardedAlternative(x, e, body)); .)
}
- "}"
+ "}" (. endTok = t; .)
.
WhileStmt<out Statement/*!*/ stmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
@@ -1237,7 +1239,7 @@ WhileStmt<out Statement/*!*/ stmt> Attributes modAttrs = null;
List<FrameExpression/*!*/> mod = null;
BlockStmt/*!*/ body = null; bool bodyOmitted = false;
- IToken bodyStart = null, bodyEnd = null;
+ IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken;
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
.)
@@ -1245,15 +1247,15 @@ WhileStmt<out Statement/*!*/ stmt> (
IF(IsLoopSpecOrAlternative())
LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
- AlternativeBlock<out alternatives>
- (. stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); .)
+ AlternativeBlock<out alternatives, out endTok>
+ (. stmt = new AlternativeLoopStmt(x, endTok, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); .)
|
( Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
| "..." (. guardOmitted = true; .)
)
LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
- ( BlockStmt<out body, out bodyStart, out bodyEnd>
- | "..." (. bodyOmitted = true; .)
+ ( BlockStmt<out body, out bodyStart, out bodyEnd> (. endTok = body.EndTok; .)
+ | "..." (. bodyOmitted = true; endTok = t; .)
)
(.
if (guardOmitted || bodyOmitted) {
@@ -1261,14 +1263,14 @@ WhileStmt<out Statement/*!*/ stmt> SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
}
if (body == null) {
- body = new BlockStmt(x, new List<Statement>());
+ body = new BlockStmt(x, endTok, new List<Statement>());
}
- stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);
+ stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);
stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);
} else {
// The following statement protects against crashes in case of parsing errors
- body = body ?? new BlockStmt(x, new List<Statement>());
- stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
+ body = body ?? new BlockStmt(x, endTok, new List<Statement>());
+ stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
.)
)
@@ -1333,7 +1335,7 @@ MatchStmt<out Statement/*!*/ s> { CaseStatement<out c> (. cases.Add(c); .)
}
"}"
- (. s = new MatchStmt(x, e, cases); .)
+ (. s = new MatchStmt(x, t, e, cases); .)
.
CaseStatement<out MatchCaseStmt/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
@@ -1365,9 +1367,9 @@ AssertStmt<out Statement/*!*/ s> )
";"
(. if (e == null) {
- s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), true, false);
} else {
- s = new AssertStmt(x, e, attrs);
+ s = new AssertStmt(x, t, e, attrs);
}
.)
.
@@ -1380,13 +1382,13 @@ AssumeStmt<out Statement/*!*/ s> ( Expression<out e>
| "..."
)
+ ";"
(. if (e == null) {
- s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), true, false);
} else {
- s = new AssumeStmt(x, e, attrs);
+ s = new AssumeStmt(x, t, e, attrs);
}
.)
- ";"
.
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
@@ -1396,7 +1398,7 @@ PrintStmt<out Statement/*!*/ s> AttributeArg<out arg> (. args.Add(arg); .)
{ "," AttributeArg<out arg> (. args.Add(arg); .)
}
- ";" (. s = new PrintStmt(x, args); .)
+ ";" (. s = new PrintStmt(x, t, args); .)
.
ForallStmt<out Statement/*!*/ s>
@@ -1436,7 +1438,7 @@ ForallStmt<out Statement/*!*/ s> "ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
}
BlockStmt<out block, out bodyStart, out bodyEnd>
- (. s = new ForallStmt(x, bvars, attrs, range, ens, block); .)
+ (. s = new ForallStmt(x, block.EndTok, bvars, attrs, range, ens, block); .)
.
CalcStmt<out Statement/*!*/ s>
@@ -1487,7 +1489,7 @@ CalcStmt<out Statement/*!*/ s> // Repeat the last line to create a dummy line for the dangling hint
lines.Add(lines[lines.Count - 1]);
}
- s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp);
+ s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);
.)
.
CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
@@ -1524,21 +1526,23 @@ Hint<out BlockStmt s> BlockStmt/*!*/ block;
Statement/*!*/ calc;
Token x = la;
+ IToken endTok = x;
.)
- { BlockStmt<out block, out bodyStart, out bodyEnd> (. subhints.Add(block); .)
- | CalcStmt<out calc> (. subhints.Add(calc); .)
+ { BlockStmt<out block, out bodyStart, out bodyEnd> (. endTok = block.EndTok; subhints.Add(block); .)
+ | CalcStmt<out calc> (. endTok = calc.EndTok; subhints.Add(calc); .)
}
- (. s = new BlockStmt(x, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
+ (. s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
.)
.
/*------------------------------------------------------------------------*/
ExpressionX<out Expression/*!*/ e>
-= (. Expression e0; .)
+= (. Expression e0; IToken endTok; .)
Expression<out e>
[ IF(SemiFollowsCall(e))
- ";" ExpressionX<out e0>
+ ";" (. endTok = t; .)
+ ExpressionX<out e0>
(. e = new StmtExpr(e.tok,
- new UpdateStmt(e.tok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),
+ new UpdateStmt(e.tok, endTok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),
e0);
.)
]
|