From 8f024b5cf0cf19bc75a4526d957770b6fcf8749a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 25 Sep 2012 15:06:54 -0700 Subject: Dafny: added iterators; for now, only parsing and resolving (and printing and refining), no compilation or verification --- Dafny/Cloner.cs | 22 + Dafny/Compiler.cs | 4 + Dafny/Dafny.atg | 115 +- Dafny/DafnyAst.cs | 165 ++- Dafny/Parser.cs | 1266 ++++++++++++-------- Dafny/Printer.cs | 82 +- Dafny/RefinementTransformer.cs | 87 +- Dafny/Resolver.cs | 457 +++++-- Dafny/Scanner.cs | 181 +-- Dafny/Translator.cs | 4 + Test/dafny0/Answer | 6 +- Util/Emacs/dafny-mode.el | 6 +- Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 10 +- .../DafnyExtension/IdentifierTagger.cs | 20 +- .../DafnyExtension/DafnyExtension/TokenTagger.cs | 3 + Util/latex/dafny.sty | 8 +- Util/vim/syntax/dafny.vim | 7 +- 17 files changed, 1667 insertions(+), 776 deletions(-) diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs index 6d99ce9b..408e9797 100644 --- a/Dafny/Cloner.cs +++ b/Dafny/Cloner.cs @@ -42,6 +42,24 @@ namespace Microsoft.Dafny var ctors = dd.Ctors.ConvertAll(CloneCtor); var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes)); return dt; + } else if (d is IteratorDecl) { + var dd = (IteratorDecl)d; + var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); + var ins = dd.Ins.ConvertAll(CloneFormal); + var outs = dd.Outs.ConvertAll(CloneFormal); + var reads = CloneSpecFrameExpr(dd.Reads); + var mod = CloneSpecFrameExpr(dd.Modifies); + var decr = CloneSpecExpr(dd.Decreases); + var req = dd.Requires.ConvertAll(CloneMayBeFreeExpr); + var yreq = dd.YieldRequires.ConvertAll(CloneMayBeFreeExpr); + var ens = dd.Ensures.ConvertAll(CloneMayBeFreeExpr); + var yens = dd.YieldEnsures.ConvertAll(CloneMayBeFreeExpr); + var body = CloneBlockStmt(dd.Body); + 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); + return iter; } else if (d is ClassDecl) { if (d is DefaultClassDecl) { var dd = (ClassDecl)d; @@ -387,6 +405,10 @@ namespace Microsoft.Dafny var s = (ReturnStmt)stmt; r = new ReturnStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS)); + } else if (stmt is YieldStmt) { + var s = (YieldStmt)stmt; + r = new YieldStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS)); + } else if (stmt is AssignStmt) { var s = (AssignStmt)stmt; r = new AssignStmt(Tok(s.Tok), CloneExpr(s.Lhs), CloneRHS(s.Rhs)); diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index a138f4d9..a6e05c22 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -92,6 +92,8 @@ namespace Microsoft.Dafny { wr.WriteLine(" { }"); CompileDatatypeConstructors(dt, indent); CompileDatatypeStruct(dt, indent); + } else if (d is IteratorDecl) { + throw new NotImplementedException(); // TODO } else if (d is ClassDecl) { ClassDecl cl = (ClassDecl)d; Indent(indent); @@ -942,6 +944,8 @@ namespace Microsoft.Dafny { if (s.hiddenUpdate != null) TrStmt(s.hiddenUpdate, indent); Indent(indent); wr.WriteLine("return;"); + } else if (stmt is YieldStmt) { + throw new NotImplementedException(); // TODO } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; var resolved = s.ResolvedStatements; diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 3afdc061..dcc9a3ca 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -139,7 +139,7 @@ IGNORE cr + lf + tab /*------------------------------------------------------------------------*/ PRODUCTIONS Dafny -= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; += (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter; List membersDefaultClass = new List(); ModuleDecl submodule; // to support multiple files, create a default module only if theModule is null @@ -159,6 +159,8 @@ Dafny DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .) | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .) ArbitraryTypeDecl (. defaultModule.TopLevelDecls.Add(at); .) + | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .) + IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) | ClassMemberDecl ) } @@ -178,7 +180,7 @@ Dafny EOF . SubModuleDecl -= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; += (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter; Attributes attrs = null; IToken/*!*/ id; List namedModuleDefaultClassMembers = new List();; List idRefined = null, idPath = null, idAssignment = null; @@ -196,13 +198,15 @@ SubModuleDecl (. module.TopLevelDecls.Add(sm); .) + ( SubModuleDecl (. module.TopLevelDecls.Add(sm); .) | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .) - ClassDecl (. module.TopLevelDecls.Add(c); .) + ClassDecl (. module.TopLevelDecls.Add(c); .) | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .) - DatatypeDecl (. module.TopLevelDecls.Add(dt); .) + DatatypeDecl (. module.TopLevelDecls.Add(dt); .) | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .) - ArbitraryTypeDecl (. module.TopLevelDecls.Add(at); .) + ArbitraryTypeDecl (. module.TopLevelDecls.Add(at); .) + | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .) + IteratorDecl (. module.TopLevelDecls.Add(iter); .) | ClassMemberDecl ) } @@ -393,6 +397,55 @@ TypeIdentOptional += (. Contract.Ensures(Contract.ValueAtReturn(out iter) != null); + IToken/*!*/ id; + Attributes attrs = null; + List/*!*/ typeArgs = new List(); + IToken openParen; + List ins = new List(); + List outs = new List(); + List reads = new List(); + List mod = new List(); + List decreases = new List(); + List req = new List(); + List ens = new List(); + List yieldReq = new List(); + List yieldEns = new List(); + List dec = new List(); + Attributes readsAttrs = null; + Attributes modAttrs = null; + Attributes decrAttrs = null; + BlockStmt body = null; + bool signatureOmitted = false; + IToken bodyStart = Token.NoToken; + IToken bodyEnd = Token.NoToken; + .) + SYNC + "iterator" + { Attribute } + NoUSIdent + ( + [ GenericParameters ] + Formals + [ "yields" + Formals + ] + | "..." (. signatureOmitted = true; openParen = Token.NoToken; .) + ) + { IteratorSpec } + [ BlockStmt + ] + (. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs, + new Specification(mod, modAttrs), new Specification(reads, readsAttrs), + new Specification(decreases, decrAttrs), + req, ens, yieldReq, yieldEns, + body, attrs, signatureOmitted); + iter.BodyStartTok = bodyStart; + iter.BodyEndTok = bodyEnd; + .) + . +/*------------------------------------------------------------------------*/ GenericParameters<.List/*!*/ typeArgs.> = (. Contract.Requires(cce.NonNullElements(typeArgs)); IToken/*!*/ id; @@ -490,6 +543,44 @@ MethodSpec<.List/*!*/ req, List/ | "decreases" { IF(IsAttribute()) Attribute } DecreasesList SYNC ";" ) . +IteratorSpec<.List/*!*/ reads, List/*!*/ mod, List decreases, + List/*!*/ req, List/*!*/ ens, + List/*!*/ yieldReq, List/*!*/ yieldEns, + ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs.> += (. Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; + .) + SYNC + ( "reads" { IF(IsAttribute()) Attribute } + [ FrameExpression (. reads.Add(fe); .) + { "," FrameExpression (. reads.Add(fe); .) + } + ] SYNC ";" + | "modifies" { IF(IsAttribute()) Attribute } + [ FrameExpression (. mod.Add(fe); .) + { "," FrameExpression (. mod.Add(fe); .) + } + ] SYNC ";" + | [ "free" (. isFree = true; .) + ] + [ "yield" (. isYield = true; .) + ] + ( "requires" Expression SYNC ";" (. if (isYield) { + yieldReq.Add(new MaybeFreeExpression(e, isFree)); + } else { + req.Add(new MaybeFreeExpression(e, isFree)); + } + .) + | "ensures" { IF(IsAttribute()) Attribute } + Expression SYNC ";" (. if (isYield) { + yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); + } else { + ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); + } + .) + ) + | "decreases" { IF(IsAttribute()) Attribute } DecreasesList SYNC ";" + ) + . Formals<.bool incoming, bool allowGhostKeyword, List/*!*/ formals, out IToken openParen.> = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .) "(" (. openParen = t; .) @@ -814,14 +905,22 @@ ReturnStmt IToken returnTok = null; List rhss = null; AssignmentRhs r; + bool isYield = false; .) - "return" (. returnTok = t; .) + ( "return" (. returnTok = t; .) + | "yield" (. returnTok = t; isYield = true; .) + ) [ Rhs (. rhss = new List(); rhss.Add(r); .) { "," Rhs (. rhss.Add(r); .) } ] - ";" (. s = new ReturnStmt(returnTok, rhss); .) + ";" (. if (isYield) { + s = new YieldStmt(returnTok, rhss); + } else { + s = new ReturnStmt(returnTok, rhss); + } + .) . UpdateStmt = (. List lhss = new List(); diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index c8c61c55..71e48fdf 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -287,6 +287,16 @@ namespace Microsoft.Dafny { return IsCoDatatype; // TODO: should really check structure of the type recursively } } + public IteratorDecl AsIteratorType { + get { + UserDefinedType udt = this as UserDefinedType; + if (udt == null) { + return null; + } else { + return udt.ResolvedClass as IteratorDecl; + } + } + } public bool IsTypeParameter { get { return AsTypeParameter != null; @@ -465,7 +475,7 @@ namespace Microsoft.Dafny { } } - public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype + public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype/iterator and TypeArgs match the type parameters of that class/datatype/iterator public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List/*!*/ typeArgs, List moduleName) { @@ -481,7 +491,7 @@ namespace Microsoft.Dafny { } /// - /// This constructor constructs a resolved class type + /// This constructor constructs a resolved class/datatype/iterator type /// public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, TopLevelDecl/*!*/ cd, [Captured] List/*!*/ typeArgs) { Contract.Requires(tok != null); @@ -577,6 +587,8 @@ namespace Microsoft.Dafny { i++; } return true; + } else if (ResolvedClass is IteratorDecl) { + return false; } else if (ResolvedParam != null) { return ResolvedParam.MustSupportEquality; } @@ -898,7 +910,7 @@ namespace Microsoft.Dafny { public ModuleDefinition RefinementBase; // filled in during resolution (null if no refinement base) public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that - public readonly Graph CallGraph = new Graph(); // filled in during resolution + public readonly Graph CallGraph = new Graph(); // filled in during resolution public int Height; // height in the topological sorting of modules; filled in during resolution public readonly bool IsGhost; public readonly bool IsAbstract; // True iff this module represents an abstract interface @@ -1146,6 +1158,85 @@ namespace Microsoft.Dafny { } } + public interface ICodeContext : ICallable + { + bool IsGhost { get; } + bool IsStatic { get; } + List TypeArgs { get; } + List Ins { get ; } + List Outs { get; } + ModuleDefinition EnclosingModule { get; } // to be called only after signature-resolution is complete + } + + public class IteratorDecl : TopLevelDecl, ICodeContext + { + public readonly List Ins; + public readonly List Outs; + public readonly List OutsHistory; // these are the 'xs' variables + public readonly Specification Reads; + public readonly Specification Modifies; + public readonly Specification Decreases; + public readonly List Requires; + public readonly List Ensures; + public readonly List YieldRequires; + public readonly List YieldEnsures; + public readonly BlockStmt Body; + public readonly bool SignatureIsOmitted; + public Dictionary ImplicitlyDefinedMembers; // filled in during resolution + public IteratorDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, + List ins, List outs, + Specification reads, Specification mod, Specification decreases, + List requires, + List ensures, + List yieldRequires, + List yieldEnsures, + BlockStmt body, Attributes attributes, bool signatureIsOmitted) + : base(tok, name, module, typeArgs, attributes) + { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(typeArgs != null); + Contract.Requires(ins != null); + Contract.Requires(outs != null); + Contract.Requires(reads != null); + Contract.Requires(mod != null); + Contract.Requires(decreases != null); + Contract.Requires(requires != null); + Contract.Requires(ensures != null); + Contract.Requires(yieldRequires != null); + Contract.Requires(yieldEnsures != null); + Ins = ins; + Outs = outs; + Reads = reads; + Modifies = mod; + Decreases = decreases; + Requires = requires; + Ensures = ensures; + YieldRequires = yieldRequires; + YieldEnsures = yieldEnsures; + Body = body; + SignatureIsOmitted = signatureIsOmitted; + + OutsHistory = new List(); + foreach (var p in Outs) { + OutsHistory.Add(new Formal(p.tok, p.Name + "s", new SeqType(p.Type), false, true)); + } + } + + bool ICodeContext.IsGhost { get { return false; } } + bool ICodeContext.IsStatic { get { return true; } } + List ICodeContext.TypeArgs { get { return this.TypeArgs; } } + List ICodeContext.Ins { get { return this.Ins; } } + List ICodeContext.Outs { get { return this.Outs; } } + ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } } + } + + /// + /// An "ICallable" is a function, method, or iterator. + /// + public interface ICallable { } + public abstract class MemberDecl : Declaration { public readonly bool IsStatic; public readonly bool IsGhost; @@ -1303,31 +1394,31 @@ namespace Microsoft.Dafny { public string Name { get { Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } public string DisplayName { get { Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } public string UniqueName { get { Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } public string CompileName { get { Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } public Type Type { get { Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } public bool IsMutable { @@ -1502,7 +1593,7 @@ namespace Microsoft.Dafny { } } - public class Function : MemberDecl, TypeParameter.ParentType { + public class Function : MemberDecl, TypeParameter.ParentType, ICallable { public bool IsRecursive; // filled in during resolution public readonly List/*!*/ TypeArgs; public readonly IToken OpenParen; // can be null (for predicates), if there are no formals @@ -1588,7 +1679,7 @@ namespace Microsoft.Dafny { } } - public class Method : MemberDecl, TypeParameter.ParentType + public class Method : MemberDecl, TypeParameter.ParentType, ICodeContext { public readonly bool SignatureIsOmitted; public bool MustReverify; @@ -1643,6 +1734,18 @@ namespace Microsoft.Dafny { this.SignatureIsOmitted = signatureOmitted; MustReverify = false; } + + bool ICodeContext.IsGhost { get { return this.IsGhost; } } + bool ICodeContext.IsStatic { get { return this.IsStatic; } } + List ICodeContext.TypeArgs { get { return this.TypeArgs; } } + List ICodeContext.Ins { get { return this.Ins; } } + List ICodeContext.Outs { get { return this.Outs; } } + ModuleDefinition ICodeContext.EnclosingModule { + get { + Contract.Assert(this.EnclosingClass != null); // this getter is supposed to be called only after signature-resolution is complete + return this.EnclosingClass.Module; + } + } } public class Constructor : Method @@ -1854,10 +1957,11 @@ namespace Microsoft.Dafny { } } - public class ReturnStmt : Statement { + public abstract class ProduceStmt : Statement + { public List rhss; public UpdateStmt hiddenUpdate; - public ReturnStmt(IToken tok, List rhss) + public ProduceStmt(IToken tok, List rhss) : base(tok) { Contract.Requires(tok != null); this.rhss = rhss; @@ -1876,7 +1980,24 @@ namespace Microsoft.Dafny { } } - public abstract class AssignmentRhs { + public class ReturnStmt : ProduceStmt + { + public ReturnStmt(IToken tok, List rhss) + : base(tok, rhss) { + Contract.Requires(tok != null); + } + } + + public class YieldStmt : ProduceStmt + { + public YieldStmt(IToken tok, List rhss) + : base(tok, rhss) { + Contract.Requires(tok != null); + } + } + + public abstract class AssignmentRhs + { public readonly IToken Tok; private Attributes attributes; @@ -2900,15 +3021,27 @@ namespace Microsoft.Dafny { public class StaticReceiverExpr : LiteralExpr { public StaticReceiverExpr(IToken tok, ClassDecl cl) - : base(tok) // constructs a LiteralExpr representing the 'null' literal + : this(cl, tok) // constructs a LiteralExpr representing the 'null' literal { Contract.Requires(tok != null); Contract.Requires(cl != null); + } + public StaticReceiverExpr(IToken tok, IteratorDecl iter) + : this(iter, tok) // constructs a LiteralExpr representing the 'null' literal + { + Contract.Requires(tok != null); + Contract.Requires(iter != null); + } + private StaticReceiverExpr(TopLevelDecl decl, IToken tok) // switch the order of the parameters, just to disambiguate calls + : base(tok) // constructs a LiteralExpr representing the 'null' literal + { + Contract.Requires(tok != null); + Contract.Requires(decl != null); var typeArgs = new List(); - foreach (var ta in cl.TypeArgs) { + foreach (var ta in decl.TypeArgs) { typeArgs.Add(new InferredTypeProxy()); } - Type = new UserDefinedType(tok, cl.Name, cl, typeArgs); + Type = new UserDefinedType(tok, decl.Name, decl, typeArgs); } } diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 69d13347..6b4be0eb 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -21,7 +21,7 @@ public class Parser { public const int _colon = 5; public const int _lbrace = 6; public const int _rbrace = 7; - public const int maxT = 111; + public const int maxT = 114; const bool T = true; const bool x = false; @@ -189,7 +189,7 @@ bool IsAttribute() { void Dafny() { - ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; + ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter; List membersDefaultClass = new List(); ModuleDecl submodule; // to support multiple files, create a default module only if theModule is null @@ -204,24 +204,42 @@ bool IsAttribute() { Get(); isGhost = true; } - if (la.kind == 9 || la.kind == 11) { + switch (la.kind) { + case 9: case 11: { SubModuleDecl(defaultModule, isGhost, out submodule); defaultModule.TopLevelDecls.Add(submodule); - } else if (la.kind == 18) { + break; + } + case 18: { if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } ClassDecl(defaultModule, out c); defaultModule.TopLevelDecls.Add(c); - } else if (la.kind == 20 || la.kind == 21) { + break; + } + case 20: case 21: { if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } DatatypeDecl(defaultModule, out dt); defaultModule.TopLevelDecls.Add(dt); - } else if (la.kind == 25) { + break; + } + case 25: { if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } ArbitraryTypeDecl(defaultModule, out at); defaultModule.TopLevelDecls.Add(at); - } else if (StartOf(2)) { + break; + } + case 29: { + if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } + IteratorDecl(defaultModule, out iter); + defaultModule.TopLevelDecls.Add(iter); + break; + } + case 8: case 19: case 23: case 34: case 35: case 52: case 53: case 54: { ClassMemberDecl(membersDefaultClass, isGhost, false); - } else SynErr(112); + break; + } + default: SynErr(115); break; + } } DefaultClassDecl defaultClass = null; foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { @@ -239,7 +257,7 @@ bool IsAttribute() { } void SubModuleDecl(ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule) { - ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; + ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter; Attributes attrs = null; IToken/*!*/ id; List namedModuleDefaultClassMembers = new List();; List idRefined = null, idPath = null, idAssignment = null; @@ -268,24 +286,42 @@ bool IsAttribute() { Get(); isGhost = true; } - if (la.kind == 9 || la.kind == 11) { + switch (la.kind) { + case 9: case 11: { SubModuleDecl(module, isGhost, out sm); module.TopLevelDecls.Add(sm); - } else if (la.kind == 18) { + break; + } + case 18: { if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } ClassDecl(module, out c); module.TopLevelDecls.Add(c); - } else if (la.kind == 20 || la.kind == 21) { + break; + } + case 20: case 21: { if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } DatatypeDecl(module, out dt); module.TopLevelDecls.Add(dt); - } else if (la.kind == 25) { + break; + } + case 25: { if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } ArbitraryTypeDecl(module, out at); module.TopLevelDecls.Add(at); - } else if (StartOf(2)) { + break; + } + case 29: { + if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } + IteratorDecl(module, out iter); + module.TopLevelDecls.Add(iter); + break; + } + case 8: case 19: case 23: case 34: case 35: case 52: case 53: case 54: { ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false); - } else SynErr(113); + break; + } + default: SynErr(116); break; + } } Expect(7); module.BodyEndTok = t; @@ -315,8 +351,8 @@ bool IsAttribute() { } Expect(14); submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened); - } else SynErr(114); - } else SynErr(115); + } else SynErr(117); + } else SynErr(118); } void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { @@ -328,13 +364,13 @@ bool IsAttribute() { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 18)) {SynErr(116); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(119); Get();} Expect(18); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 29) { + if (la.kind == 32) { GenericParameters(typeArgs); } Expect(6); @@ -359,18 +395,18 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; - while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(117); Get();} + while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(120); Get();} if (la.kind == 20) { Get(); } else if (la.kind == 21) { Get(); co = true; - } else SynErr(118); + } else SynErr(121); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 29) { + if (la.kind == 32) { GenericParameters(typeArgs); } Expect(13); @@ -380,7 +416,7 @@ bool IsAttribute() { Get(); DatatypeMemberDecl(ctors); } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(119); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(122); Get();} Expect(14); if (co) { dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); @@ -409,10 +445,69 @@ bool IsAttribute() { eqSupport = TypeParameter.EqualitySupportValue.Required; } at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(120); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();} Expect(14); } + void IteratorDecl(ModuleDefinition module, out IteratorDecl/*!*/ iter) { + Contract.Ensures(Contract.ValueAtReturn(out iter) != null); + IToken/*!*/ id; + Attributes attrs = null; + List/*!*/ typeArgs = new List(); + IToken openParen; + List ins = new List(); + List outs = new List(); + List reads = new List(); + List mod = new List(); + List decreases = new List(); + List req = new List(); + List ens = new List(); + List yieldReq = new List(); + List yieldEns = new List(); + List dec = new List(); + Attributes readsAttrs = null; + Attributes modAttrs = null; + Attributes decrAttrs = null; + BlockStmt body = null; + bool signatureOmitted = false; + IToken bodyStart = Token.NoToken; + IToken bodyEnd = Token.NoToken; + + while (!(la.kind == 0 || la.kind == 29)) {SynErr(124); Get();} + Expect(29); + while (la.kind == 6) { + Attribute(ref attrs); + } + NoUSIdent(out id); + if (la.kind == 26 || la.kind == 32) { + if (la.kind == 32) { + GenericParameters(typeArgs); + } + Formals(true, true, ins, out openParen); + if (la.kind == 30) { + Get(); + Formals(false, true, outs, out openParen); + } + } else if (la.kind == 31) { + Get(); + signatureOmitted = true; openParen = Token.NoToken; + } else SynErr(125); + while (StartOf(3)) { + IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); + } + if (la.kind == 6) { + BlockStmt(out body, out bodyStart, out bodyEnd); + } + iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs, + new Specification(mod, modAttrs), new Specification(reads, readsAttrs), + new Specification(decreases, decrAttrs), + req, ens, yieldReq, yieldEns, + body, attrs, signatureOmitted); + iter.BodyStartTok = bodyStart; + iter.BodyEndTok = bodyEnd; + + } + void ClassMemberDecl(List/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) { Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; @@ -431,13 +526,13 @@ bool IsAttribute() { } if (la.kind == 23) { FieldDecl(mmod, mm); - } else if (la.kind == 48 || la.kind == 49 || la.kind == 50) { + } else if (la.kind == 52 || la.kind == 53 || la.kind == 54) { FunctionDecl(mmod, out f); mm.Add(f); - } else if (la.kind == 31 || la.kind == 32) { + } else if (la.kind == 34 || la.kind == 35) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(121); + } else SynErr(126); } void Attribute(ref Attributes attrs) { @@ -478,7 +573,7 @@ bool IsAttribute() { IToken/*!*/ id; TypeParameter.EqualitySupportValue eqSupport; - Expect(29); + Expect(32); NoUSIdent(out id); eqSupport = TypeParameter.EqualitySupportValue.Unspecified; if (la.kind == 26) { @@ -500,7 +595,7 @@ bool IsAttribute() { } typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); } - Expect(30); + Expect(33); } void FieldDecl(MemberModifiers mmod, List/*!*/ mm) { @@ -508,7 +603,7 @@ bool IsAttribute() { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 23)) {SynErr(122); Get();} + while (!(la.kind == 0 || la.kind == 23)) {SynErr(127); Get();} Expect(23); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } @@ -522,7 +617,7 @@ bool IsAttribute() { IdentType(out id, out ty, false); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(128); Get();} Expect(14); } @@ -545,9 +640,9 @@ bool IsAttribute() { IToken bodyEnd = Token.NoToken; bool signatureOmitted = false; - if (la.kind == 48) { + if (la.kind == 52) { Get(); - if (la.kind == 31) { + if (la.kind == 34) { Get(); isFunctionMethod = true; } @@ -557,22 +652,22 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 26 || la.kind == 29) { - if (la.kind == 29) { + if (la.kind == 26 || la.kind == 32) { + if (la.kind == 32) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals, out openParen); Expect(5); Type(out returnType); - } else if (la.kind == 34) { + } else if (la.kind == 31) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(124); - } else if (la.kind == 49) { + } else SynErr(129); + } else if (la.kind == 53) { Get(); isPredicate = true; - if (la.kind == 31) { + if (la.kind == 34) { Get(); isFunctionMethod = true; } @@ -582,8 +677,8 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (StartOf(3)) { - if (la.kind == 29) { + if (StartOf(4)) { + if (la.kind == 32) { GenericParameters(typeArgs); } if (la.kind == 26) { @@ -593,12 +688,12 @@ bool IsAttribute() { SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); } } - } else if (la.kind == 34) { + } else if (la.kind == 31) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(125); - } else if (la.kind == 50) { + } else SynErr(130); + } else if (la.kind == 54) { Get(); isCoPredicate = true; if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); } @@ -607,8 +702,8 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (StartOf(3)) { - if (la.kind == 29) { + if (StartOf(4)) { + if (la.kind == 32) { GenericParameters(typeArgs); } if (la.kind == 26) { @@ -618,14 +713,14 @@ bool IsAttribute() { SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); } } - } else if (la.kind == 34) { + } else if (la.kind == 31) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(126); - } else SynErr(127); + } else SynErr(131); + } else SynErr(132); decreases = isCoPredicate ? null : new List(); - while (StartOf(4)) { + while (StartOf(5)) { FunctionSpec(reqs, reads, ens, decreases); } if (la.kind == 6) { @@ -666,10 +761,10 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 31 || la.kind == 32)) {SynErr(128); Get();} - if (la.kind == 31) { + while (!(la.kind == 0 || la.kind == 34 || la.kind == 35)) {SynErr(133); Get();} + if (la.kind == 34) { Get(); - } else if (la.kind == 32) { + } else if (la.kind == 35) { Get(); if (allowConstructor) { isConstructor = true; @@ -677,7 +772,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes"); } - } else SynErr(129); + } else SynErr(134); if (isConstructor) { if (mmod.IsGhost) { SemErr(t, "constructors cannot be declared 'ghost'"); @@ -691,21 +786,21 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 26 || la.kind == 29) { - if (la.kind == 29) { + if (la.kind == 26 || la.kind == 32) { + if (la.kind == 32) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins, out openParen); - if (la.kind == 33) { + if (la.kind == 36) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs, out openParen); } - } else if (la.kind == 34) { + } else if (la.kind == 31) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(130); - while (StartOf(5)) { + } else SynErr(135); + while (StartOf(6)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } if (la.kind == 6) { @@ -742,7 +837,7 @@ bool IsAttribute() { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; Expect(26); - if (StartOf(6)) { + if (StartOf(7)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); while (la.kind == 24) { @@ -849,22 +944,22 @@ bool IsAttribute() { List/*!*/ gt; switch (la.kind) { - case 40: { + case 44: { Get(); tok = t; break; } - case 41: { + case 45: { Get(); tok = t; ty = new NatType(); break; } - case 42: { + case 46: { Get(); tok = t; ty = new IntType(); break; } - case 43: { + case 47: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -875,7 +970,7 @@ bool IsAttribute() { break; } - case 44: { + case 48: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -886,7 +981,7 @@ bool IsAttribute() { break; } - case 45: { + case 49: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -897,7 +992,7 @@ bool IsAttribute() { break; } - case 46: { + case 50: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -908,11 +1003,11 @@ bool IsAttribute() { break; } - case 1: case 3: case 47: { + case 1: case 3: case 51: { ReferenceType(out tok, out ty); break; } - default: SynErr(131); break; + default: SynErr(136); break; } } @@ -932,18 +1027,35 @@ bool IsAttribute() { Expect(28); } - void MethodSpec(List/*!*/ req, List/*!*/ mod, List/*!*/ ens, -List/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs) { - Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); - Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; + void IteratorSpec(List/*!*/ reads, List/*!*/ mod, List decreases, +List/*!*/ req, List/*!*/ ens, +List/*!*/ yieldReq, List/*!*/ yieldEns, +ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { + Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; - while (!(StartOf(7))) {SynErr(132); Get();} - if (la.kind == 35) { + while (!(StartOf(8))) {SynErr(137); Get();} + if (la.kind == 42) { + Get(); + while (IsAttribute()) { + Attribute(ref readsAttrs); + } + if (StartOf(9)) { + FrameExpression(out fe); + reads.Add(fe); + while (la.kind == 24) { + Get(); + FrameExpression(out fe); + reads.Add(fe); + } + } + while (!(la.kind == 0 || la.kind == 14)) {SynErr(138); Get();} + Expect(14); + } else if (la.kind == 37) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); } - if (StartOf(8)) { + if (StartOf(9)) { FrameExpression(out fe); mod.Add(fe); while (la.kind == 24) { @@ -952,38 +1064,52 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(133); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(139); Get();} Expect(14); - } else if (la.kind == 36 || la.kind == 37 || la.kind == 38) { - if (la.kind == 36) { + } else if (StartOf(10)) { + if (la.kind == 38) { Get(); isFree = true; } - if (la.kind == 37) { + if (la.kind == 43) { + Get(); + isYield = true; + } + if (la.kind == 39) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(134); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(140); Get();} Expect(14); - req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 38) { + if (isYield) { + yieldReq.Add(new MaybeFreeExpression(e, isFree)); + } else { + req.Add(new MaybeFreeExpression(e, isFree)); + } + + } else if (la.kind == 40) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(135); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(141); Get();} Expect(14); - ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(136); - } else if (la.kind == 39) { + if (isYield) { + yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); + } else { + ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); + } + + } else SynErr(142); + } else if (la.kind == 41) { Get(); while (IsAttribute()) { - Attribute(ref decAttrs); + Attribute(ref decrAttrs); } - DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(137); Get();} + DecreasesList(decreases, false); + while (!(la.kind == 0 || la.kind == 14)) {SynErr(143); Get();} Expect(14); - } else SynErr(138); + } else SynErr(144); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -992,7 +1118,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(6); bodyStart = t; - while (StartOf(9)) { + while (StartOf(11)) { Stmt(body); } Expect(7); @@ -1000,6 +1126,60 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo block = new BlockStmt(bodyStart, body); } + void MethodSpec(List/*!*/ req, List/*!*/ mod, List/*!*/ ens, +List/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs) { + Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); + Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; + + while (!(StartOf(12))) {SynErr(145); Get();} + if (la.kind == 37) { + Get(); + while (IsAttribute()) { + Attribute(ref modAttrs); + } + if (StartOf(9)) { + FrameExpression(out fe); + mod.Add(fe); + while (la.kind == 24) { + Get(); + FrameExpression(out fe); + mod.Add(fe); + } + } + while (!(la.kind == 0 || la.kind == 14)) {SynErr(146); Get();} + Expect(14); + } else if (la.kind == 38 || la.kind == 39 || la.kind == 40) { + if (la.kind == 38) { + Get(); + isFree = true; + } + if (la.kind == 39) { + Get(); + Expression(out e); + while (!(la.kind == 0 || la.kind == 14)) {SynErr(147); Get();} + Expect(14); + req.Add(new MaybeFreeExpression(e, isFree)); + } else if (la.kind == 40) { + Get(); + while (IsAttribute()) { + Attribute(ref ensAttrs); + } + Expression(out e); + while (!(la.kind == 0 || la.kind == 14)) {SynErr(148); Get();} + Expect(14); + ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); + } else SynErr(149); + } else if (la.kind == 41) { + Get(); + while (IsAttribute()) { + Attribute(ref decAttrs); + } + DecreasesList(decreases, true); + while (!(la.kind == 0 || la.kind == 14)) {SynErr(150); Get();} + Expect(14); + } else SynErr(151); + } + void FrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; @@ -1007,21 +1187,21 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo string fieldName = null; IToken feTok = null; fe = null; - if (StartOf(10)) { + if (StartOf(13)) { Expression(out e); feTok = e.tok; - if (la.kind == 53) { + if (la.kind == 56) { Get(); Ident(out id); fieldName = id.val; feTok = id; } fe = new FrameExpression(feTok, e, fieldName); - } else if (la.kind == 53) { + } else if (la.kind == 56) { Get(); Ident(out id); fieldName = id.val; fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); - } else SynErr(139); + } else SynErr(152); } void Expression(out Expression/*!*/ e) { @@ -1051,7 +1231,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(29); + Expect(32); Type(out ty); gt.Add(ty); while (la.kind == 24) { @@ -1059,7 +1239,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Type(out ty); gt.Add(ty); } - Expect(30); + Expect(33); } void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) { @@ -1068,7 +1248,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List/*!*/ gt; List path; - if (la.kind == 47) { + if (la.kind == 51) { Get(); tok = t; ty = new ObjectType(); } else if (la.kind == 3) { @@ -1093,11 +1273,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); Ident(out tok); } - if (la.kind == 29) { + if (la.kind == 32) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt, path); - } else SynErr(140); + } else SynErr(153); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases) { @@ -1105,16 +1285,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - if (la.kind == 37) { - while (!(la.kind == 0 || la.kind == 37)) {SynErr(141); Get();} + if (la.kind == 39) { + while (!(la.kind == 0 || la.kind == 39)) {SynErr(154); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(155); Get();} Expect(14); reqs.Add(e); - } else if (la.kind == 51) { + } else if (la.kind == 42) { Get(); - if (StartOf(11)) { + if (StartOf(14)) { PossiblyWildFrameExpression(out fe); reads.Add(fe); while (la.kind == 24) { @@ -1123,15 +1303,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(143); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(156); Get();} Expect(14); - } else if (la.kind == 38) { + } else if (la.kind == 40) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(144); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(157); Get();} Expect(14); ens.Add(e); - } else if (la.kind == 39) { + } else if (la.kind == 41) { Get(); if (decreases == null) { SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed"); @@ -1139,9 +1319,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(145); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(158); Get();} Expect(14); - } else SynErr(146); + } else SynErr(159); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -1155,23 +1335,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; - if (la.kind == 52) { + if (la.kind == 55) { Get(); fe = new FrameExpression(t, new WildcardExpr(t), null); - } else if (StartOf(8)) { + } else if (StartOf(9)) { FrameExpression(out fe); - } else SynErr(147); + } else SynErr(160); } void PossiblyWildExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; - if (la.kind == 52) { + if (la.kind == 55) { Get(); e = new WildcardExpr(t); - } else if (StartOf(10)) { + } else if (StartOf(13)) { Expression(out e); - } else SynErr(148); + } else SynErr(161); } void Stmt(List/*!*/ ss) { @@ -1188,26 +1368,26 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(12))) {SynErr(149); Get();} + while (!(StartOf(15))) {SynErr(162); Get();} switch (la.kind) { case 6: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; } - case 72: { + case 75: { AssertStmt(out s); break; } - case 60: { + case 63: { AssumeStmt(out s); break; } - case 73: { + case 76: { PrintStmt(out s); break; } - case 1: case 2: case 22: case 26: case 97: case 98: case 99: case 100: case 101: case 102: { + case 1: case 2: case 22: case 26: case 100: case 101: case 102: case 103: case 104: case 105: { UpdateStmt(out s); break; } @@ -1215,23 +1395,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s); break; } - case 65: { + case 68: { IfStmt(out s); break; } - case 69: { + case 72: { WhileStmt(out s); break; } - case 71: { + case 74: { MatchStmt(out s); break; } - case 74: { + case 77: { ParallelStmt(out s); break; } - case 54: { + case 57: { Get(); x = t; NoUSIdent(out id); @@ -1240,33 +1420,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList