diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 5 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 3 |
6 files changed, 8 insertions, 15 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 5226c6ca..b6da3dd4 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -55,7 +55,7 @@ namespace Microsoft.Dafny var ens = dd.Ensures.ConvertAll(CloneMayBeFreeExpr);
var yens = dd.YieldEnsures.ConvertAll(CloneMayBeFreeExpr);
var body = CloneBlockStmt(dd.Body);
- var iter = new IteratorDecl(Tok(dd.IteratorKeywordTok), Tok(dd.tok), dd.Name, dd.Module,
+ var iter = new IteratorDecl(Tok(dd.tok), dd.Name, dd.Module,
tps, ins, outs, reads, mod, decr,
req, ens, yreq, yens,
body, CloneAttributes(dd.Attributes), dd.SignatureIsOmitted);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a0a8e699..09b71e59 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -487,10 +487,9 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter> bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- IToken iteratorKeywordTok;
.)
SYNC
- "iterator" (. iteratorKeywordTok = t; .)
+ "iterator"
{ Attribute<ref attrs> }
NoUSIdent<out id>
(
@@ -506,7 +505,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(iteratorKeywordTok, id, id.val, module, typeArgs, ins, outs,
+ (. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
new Specification<FrameExpression>(reads, readsAttrs),
new Specification<FrameExpression>(mod, modAttrs),
new Specification<Expression>(decreases, decrAttrs),
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 988b6717..a0ea57b7 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1396,7 +1396,6 @@ namespace Microsoft.Dafny { public class IteratorDecl : ClassDecl, IMethodCodeContext
{
- public readonly IToken IteratorKeywordTok;
public readonly List<Formal> Ins;
public readonly List<Formal> Outs;
public readonly Specification<FrameExpression> Reads;
@@ -1418,7 +1417,7 @@ namespace Microsoft.Dafny { public Predicate Member_Valid; // created during registration phase of resolution; its specification is filled in during resolution
public Method Member_MoveNext; // created during registration phase of resolution; its specification is filled in during resolution
public readonly VarDecl YieldCountVariable;
- public IteratorDecl(IToken iteratorKeywordTok, IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,
+ public IteratorDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,
List<Formal> ins, List<Formal> outs,
Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,
List<MaybeFreeExpression> requires,
@@ -1428,7 +1427,6 @@ namespace Microsoft.Dafny { BlockStmt body, Attributes attributes, bool signatureIsOmitted)
: base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes)
{
- Contract.Requires(iteratorKeywordTok != null);
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
@@ -1442,7 +1440,6 @@ namespace Microsoft.Dafny { Contract.Requires(ensures != null);
Contract.Requires(yieldRequires != null);
Contract.Requires(yieldEnsures != null);
- IteratorKeywordTok = iteratorKeywordTok;
Ins = ins;
Outs = outs;
Reads = reads;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index b1531a65..afb7291a 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -513,11 +513,9 @@ bool SemiFollowsCall(Expression e) { bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- IToken iteratorKeywordTok;
while (!(la.kind == 0 || la.kind == 34)) {SynErr(131); Get();}
Expect(34);
- iteratorKeywordTok = t;
while (la.kind == 8) {
Attribute(ref attrs);
}
@@ -546,7 +544,7 @@ bool SemiFollowsCall(Expression e) { if (la.kind == 8) {
BlockStmt(out body, out bodyStart, out bodyEnd);
}
- iter = new IteratorDecl(iteratorKeywordTok, id, id.val, module, typeArgs, ins, outs,
+ iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
new Specification<FrameExpression>(reads, readsAttrs),
new Specification<FrameExpression>(mod, modAttrs),
new Specification<Expression>(decreases, decrAttrs),
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index c410d56d..3b04e017 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -608,8 +608,8 @@ namespace Microsoft.Dafny var yens = prev.YieldEnsures.ConvertAll(rawCloner.CloneMayBeFreeExpr);
yens.AddRange(nw.YieldEnsures);
- return new IteratorDecl(new RefinementToken(nw.IteratorKeywordTok, moduleUnderConstruction),
- new RefinementToken(nw.tok, moduleUnderConstruction), nw.Name, moduleUnderConstruction,
+ return new IteratorDecl(new RefinementToken(nw.tok, moduleUnderConstruction),
+ nw.Name, moduleUnderConstruction,
nw.SignatureIsOmitted ? prev.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam) : nw.TypeArgs,
nw.SignatureIsOmitted ? prev.Ins.ConvertAll(refinementCloner.CloneFormal) : nw.Ins,
nw.SignatureIsOmitted ? prev.Outs.ConvertAll(refinementCloner.CloneFormal) : nw.Outs,
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index be48e23a..b659811d 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -323,8 +323,7 @@ namespace Microsoft.Dafny }
foreach (var module in prog.Modules) {
foreach (var iter in ModuleDefinition.AllIteratorDecls(module.TopLevelDecls)) {
- var tok = iter.IteratorKeywordTok;
- ReportAdditionalInformation(tok, Printer.IteratorClassToString(iter), tok.val.Length);
+ ReportAdditionalInformation(iter.tok, Printer.IteratorClassToString(iter), iter.Name.Length);
}
}
}
|