diff options
Diffstat (limited to 'Source/Dafny/Parser.cs')
| -rw-r--r-- | Source/Dafny/Parser.cs | 3470 |
1 files changed, 3470 insertions, 0 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs new file mode 100644 index 00000000..032b8a10 --- /dev/null +++ b/Source/Dafny/Parser.cs @@ -0,0 +1,3470 @@ +using System.Collections.Generic;
+using System.Numerics;
+using Microsoft.Boogie;
+using System.IO;
+using System.Text;
+
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny {
+
+
+
+public class Parser {
+ public const int _EOF = 0;
+ public const int _ident = 1;
+ public const int _digits = 2;
+ public const int _arrayToken = 3;
+ public const int _string = 4;
+ public const int _colon = 5;
+ public const int _lbrace = 6;
+ public const int _rbrace = 7;
+ public const int maxT = 115;
+
+ const bool T = true;
+ const bool x = false;
+ const int minErrDist = 2;
+
+ public Scanner/*!*/ scanner;
+ public Errors/*!*/ errors;
+
+ public Token/*!*/ t; // last recognized token
+ public Token/*!*/ la; // lookahead token
+ int errDist = minErrDist;
+
+readonly Expression/*!*/ dummyExpr;
+readonly AssignmentRhs/*!*/ dummyRhs;
+readonly FrameExpression/*!*/ dummyFrameExpr;
+readonly Statement/*!*/ dummyStmt;
+readonly Attributes.Argument/*!*/ dummyAttrArg;
+readonly ModuleDecl theModule;
+readonly BuiltIns theBuiltIns;
+int anonymousIds = 0;
+
+struct MemberModifiers {
+ public bool IsGhost;
+ public bool IsStatic;
+}
+// helper routine for parsing call statements
+///<summary>
+/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
+/// and appends them in appropriate form to "module".
+/// Returns the number of parsing errors encountered.
+/// Note: first initialize the Scanner.
+///</summary>
+public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) /* throws System.IO.IOException */ {
+ Contract.Requires(filename != null);
+ Contract.Requires(module != null);
+ string s;
+ if (filename == "stdin.dfy") {
+ s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
+ return Parse(s, filename, module, builtIns);
+ } else {
+ using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
+ s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
+ return Parse(s, filename, module, builtIns);
+ }
+ }
+}
+///<summary>
+/// Parses top-level things (modules, classes, datatypes, class members)
+/// and appends them in appropriate form to "module".
+/// Returns the number of parsing errors encountered.
+/// Note: first initialize the Scanner.
+///</summary>
+public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) {
+ Contract.Requires(s != null);
+ Contract.Requires(filename != null);
+ Contract.Requires(module != null);
+ Errors errors = new Errors();
+ return Parse(s, filename, module, builtIns, errors);
+}
+///<summary>
+/// Parses top-level things (modules, classes, datatypes, class members)
+/// and appends them in appropriate form to "module".
+/// Returns the number of parsing errors encountered.
+/// Note: first initialize the Scanner with the given Errors sink.
+///</summary>
+public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,
+ Errors/*!*/ errors) {
+ Contract.Requires(s != null);
+ Contract.Requires(filename != null);
+ Contract.Requires(module != null);
+ Contract.Requires(errors != null);
+ byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
+ MemoryStream ms = new MemoryStream(buffer,false);
+ Scanner scanner = new Scanner(ms, errors, filename);
+ Parser parser = new Parser(scanner, errors, module, builtIns);
+ parser.Parse();
+ return parser.errors.count;
+}
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns)
+ : this(scanner, errors) // the real work
+{
+ // initialize readonly fields
+ dummyExpr = new LiteralExpr(Token.NoToken);
+ dummyRhs = new ExprRhs(dummyExpr, null);
+ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
+ dummyStmt = new ReturnStmt(Token.NoToken, null);
+ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
+ theModule = module;
+ theBuiltIns = builtIns;
+}
+
+bool IsAttribute() {
+ Token x = scanner.Peek();
+ return la.kind == _lbrace && x.kind == _colon;
+}
+/*--------------------------------------------------------------------------*/
+
+
+ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {
+ this.scanner = scanner;
+ this.errors = errors;
+ Token/*!*/ tok = new Token();
+ tok.val = "";
+ this.la = tok;
+ this.t = new Token(); // just to satisfy its non-null constraint
+ }
+
+ void SynErr (int n) {
+ if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);
+ errDist = 0;
+ }
+
+ public void SemErr (string/*!*/ msg) {
+ Contract.Requires(msg != null);
+ if (errDist >= minErrDist) errors.SemErr(t, msg);
+ errDist = 0;
+ }
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ errors.SemErr(tok, msg);
+ }
+
+ void Get () {
+ for (;;) {
+ t = la;
+ la = scanner.Scan();
+ if (la.kind <= maxT) { ++errDist; break; }
+
+ la = t;
+ }
+ }
+
+ void Expect (int n) {
+ if (la.kind==n) Get(); else { SynErr(n); }
+ }
+
+ bool StartOf (int s) {
+ return set[s, la.kind];
+ }
+
+ void ExpectWeak (int n, int follow) {
+ if (la.kind == n) Get();
+ else {
+ SynErr(n);
+ while (!StartOf(follow)) Get();
+ }
+ }
+
+
+ bool WeakSeparator(int n, int syFol, int repFol) {
+ int kind = la.kind;
+ if (kind == n) {Get(); return true;}
+ else if (StartOf(repFol)) {return false;}
+ else {
+ SynErr(n);
+ while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {
+ Get();
+ kind = la.kind;
+ }
+ return StartOf(syFol);
+ }
+ }
+
+
+ void Dafny() {
+ ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;
+ List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
+ ModuleDecl submodule;
+ // to support multiple files, create a default module only if theModule is null
+ DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
+ // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
+ Contract.Assert(defaultModule != null);
+ bool isGhost;
+
+ while (StartOf(1)) {
+ isGhost = false;
+ if (la.kind == 8) {
+ Get();
+ isGhost = true;
+ }
+ switch (la.kind) {
+ case 9: case 11: {
+ SubModuleDecl(defaultModule, isGhost, out submodule);
+ defaultModule.TopLevelDecls.Add(submodule);
+ 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);
+ 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);
+ 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);
+ 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);
+ break;
+ }
+ default: SynErr(116); break;
+ }
+ }
+ DefaultClassDecl defaultClass = null;
+ foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
+ defaultClass = topleveldecl as DefaultClassDecl;
+ if (defaultClass != null) {
+ defaultClass.Members.AddRange(membersDefaultClass);
+ break;
+ }
+ }
+ if (defaultClass == null) { // create the default class here, because it wasn't found
+ defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);
+ defaultModule.TopLevelDecls.Add(defaultClass);
+ }
+ Expect(0);
+ }
+
+ void SubModuleDecl(ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule) {
+ ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;
+ Attributes attrs = null; IToken/*!*/ id;
+ List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
+ List<IToken> idRefined = null, idPath = null, idAssignment = null;
+ bool isGhost = false;
+ ModuleDefinition module;
+ ModuleDecl sm;
+ submodule = null; // appease compiler
+ bool opened = false;
+
+ if (la.kind == 9) {
+ Get();
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (la.kind == 10) {
+ Get();
+ QualifiedName(out idRefined);
+ }
+ module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false);
+ Expect(6);
+ module.BodyStartTok = t;
+ while (StartOf(1)) {
+ isGhost = false;
+ if (la.kind == 8) {
+ Get();
+ isGhost = true;
+ }
+ switch (la.kind) {
+ case 9: case 11: {
+ SubModuleDecl(module, isGhost, out sm);
+ module.TopLevelDecls.Add(sm);
+ 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);
+ 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);
+ 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);
+ 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);
+ break;
+ }
+ default: SynErr(117); break;
+ }
+ }
+ Expect(7);
+ module.BodyEndTok = t;
+ module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
+ submodule = new LiteralModuleDecl(module, parent);
+ } else if (la.kind == 11) {
+ Get();
+ if (la.kind == 12) {
+ Get();
+ opened = true;
+ }
+ NoUSIdent(out id);
+ if (la.kind == 13) {
+ Get();
+ QualifiedName(out idPath);
+ Expect(14);
+ submodule = new AliasModuleDecl(idPath, id, parent, opened);
+ } else if (la.kind == 14) {
+ Get();
+ idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened);
+ } else if (la.kind == 15) {
+ Get();
+ QualifiedName(out idPath);
+ if (la.kind == 16) {
+ Get();
+ QualifiedName(out idAssignment);
+ }
+ Expect(14);
+ submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened);
+ } else SynErr(118);
+ } else SynErr(119);
+ }
+
+ void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
+ Contract.Requires(module != null);
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null);
+ IToken/*!*/ id;
+ Attributes attrs = null;
+ List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
+ List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
+ IToken bodyStart;
+
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(120); Get();}
+ Expect(18);
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (la.kind == 32) {
+ GenericParameters(typeArgs);
+ }
+ Expect(6);
+ bodyStart = t;
+ while (StartOf(2)) {
+ ClassMemberDecl(members, false, true);
+ }
+ Expect(7);
+ c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
+ c.BodyStartTok = bodyStart;
+ c.BodyEndTok = t;
+
+ }
+
+ void DatatypeDecl(ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt) {
+ Contract.Requires(module != null);
+ Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
+ IToken/*!*/ id;
+ Attributes attrs = null;
+ List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
+ List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
+ IToken bodyStart = Token.NoToken; // dummy assignment
+ bool co = false;
+
+ while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(121); Get();}
+ if (la.kind == 20) {
+ Get();
+ } else if (la.kind == 21) {
+ Get();
+ co = true;
+ } else SynErr(122);
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (la.kind == 32) {
+ GenericParameters(typeArgs);
+ }
+ Expect(13);
+ bodyStart = t;
+ DatatypeMemberDecl(ctors);
+ while (la.kind == 22) {
+ Get();
+ DatatypeMemberDecl(ctors);
+ }
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();}
+ Expect(14);
+ if (co) {
+ dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+ } else {
+ dt = new IndDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+ }
+ dt.BodyStartTok = bodyStart;
+ dt.BodyEndTok = t;
+
+ }
+
+ void ArbitraryTypeDecl(ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at) {
+ IToken/*!*/ id;
+ Attributes attrs = null;
+ var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
+
+ Expect(25);
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (la.kind == 26) {
+ Get();
+ Expect(27);
+ Expect(28);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(124); Get();}
+ Expect(14);
+ }
+
+ void IteratorDecl(ModuleDefinition module, out IteratorDecl/*!*/ iter) {
+ Contract.Ensures(Contract.ValueAtReturn(out iter) != null);
+ IToken/*!*/ id;
+ Attributes attrs = null;
+ List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();
+ IToken openParen;
+ List<Formal/*!*/> ins = new List<Formal/*!*/>();
+ List<Formal/*!*/> outs = new List<Formal/*!*/>();
+ List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
+ List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
+ List<Expression/*!*/> decreases = new List<Expression>();
+ List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();
+ List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();
+ List<MaybeFreeExpression/*!*/> yieldReq = new List<MaybeFreeExpression/*!*/>();
+ List<MaybeFreeExpression/*!*/> yieldEns = new List<MaybeFreeExpression/*!*/>();
+ List<Expression/*!*/> dec = new List<Expression/*!*/>();
+ 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(125); 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(126);
+ 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<FrameExpression>(reads, readsAttrs),
+ new Specification<FrameExpression>(mod, modAttrs),
+ new Specification<Expression>(decreases, decrAttrs),
+ req, ens, yieldReq, yieldEns,
+ body, attrs, signatureOmitted);
+ iter.BodyStartTok = bodyStart;
+ iter.BodyEndTok = bodyEnd;
+
+ }
+
+ void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) {
+ Contract.Requires(cce.NonNullElements(mm));
+ Method/*!*/ m;
+ Function/*!*/ f;
+ MemberModifiers mmod = new MemberModifiers();
+ mmod.IsGhost = isAlreadyGhost;
+
+ while (la.kind == 8 || la.kind == 19) {
+ if (la.kind == 8) {
+ Get();
+ mmod.IsGhost = true;
+ } else {
+ Get();
+ mmod.IsStatic = true;
+ }
+ }
+ if (la.kind == 23) {
+ FieldDecl(mmod, mm);
+ } else if (la.kind == 52 || la.kind == 53 || la.kind == 54) {
+ FunctionDecl(mmod, out f);
+ mm.Add(f);
+ } else if (la.kind == 34 || la.kind == 35) {
+ MethodDecl(mmod, allowConstructors, out m);
+ mm.Add(m);
+ } else SynErr(127);
+ }
+
+ void Attribute(ref Attributes attrs) {
+ Expect(6);
+ AttributeBody(ref attrs);
+ Expect(7);
+ }
+
+ void NoUSIdent(out IToken/*!*/ x) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ Expect(1);
+ x = t;
+ if (x.val.StartsWith("_")) {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+
+ }
+
+ void QualifiedName(out List<IToken> ids) {
+ IToken id; ids = new List<IToken>();
+ Ident(out id);
+ ids.Add(id);
+ while (la.kind == 17) {
+ Get();
+ Ident(out id);
+ ids.Add(id);
+ }
+ }
+
+ void Ident(out IToken/*!*/ x) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ Expect(1);
+ x = t;
+ }
+
+ void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ IToken/*!*/ id;
+ TypeParameter.EqualitySupportValue eqSupport;
+
+ Expect(32);
+ NoUSIdent(out id);
+ eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
+ if (la.kind == 26) {
+ Get();
+ Expect(27);
+ Expect(28);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
+ while (la.kind == 24) {
+ Get();
+ NoUSIdent(out id);
+ eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
+ if (la.kind == 26) {
+ Get();
+ Expect(27);
+ Expect(28);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
+ }
+ Expect(33);
+ }
+
+ void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
+ Contract.Requires(cce.NonNullElements(mm));
+ Attributes attrs = null;
+ IToken/*!*/ id; Type/*!*/ ty;
+
+ while (!(la.kind == 0 || la.kind == 23)) {SynErr(128); Get();}
+ Expect(23);
+ if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
+
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ IdentType(out id, out ty, false);
+ mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
+ while (la.kind == 24) {
+ Get();
+ 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(129); Get();}
+ Expect(14);
+ }
+
+ void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {
+ Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
+ Attributes attrs = null;
+ IToken/*!*/ id = Token.NoToken; // to please compiler
+ List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
+ List<Formal/*!*/> formals = new List<Formal/*!*/>();
+ Type/*!*/ returnType = new BoolType();
+ List<Expression/*!*/> reqs = new List<Expression/*!*/>();
+ List<Expression/*!*/> ens = new List<Expression/*!*/>();
+ List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
+ List<Expression/*!*/> decreases;
+ Expression body = null;
+ bool isPredicate = false; bool isCoPredicate = false;
+ bool isFunctionMethod = false;
+ IToken openParen = null;
+ IToken bodyStart = Token.NoToken;
+ IToken bodyEnd = Token.NoToken;
+ bool signatureOmitted = false;
+
+ if (la.kind == 52) {
+ Get();
+ if (la.kind == 34) {
+ Get();
+ isFunctionMethod = true;
+ }
+ if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
+
+ 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, isFunctionMethod, formals, out openParen);
+ Expect(5);
+ Type(out returnType);
+ } else if (la.kind == 31) {
+ Get();
+ signatureOmitted = true;
+ openParen = Token.NoToken;
+ } else SynErr(130);
+ } else if (la.kind == 53) {
+ Get();
+ isPredicate = true;
+ if (la.kind == 34) {
+ Get();
+ isFunctionMethod = true;
+ }
+ if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
+
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (StartOf(4)) {
+ if (la.kind == 32) {
+ GenericParameters(typeArgs);
+ }
+ if (la.kind == 26) {
+ Formals(true, isFunctionMethod, formals, out openParen);
+ if (la.kind == 5) {
+ Get();
+ SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
+ }
+ }
+ } else if (la.kind == 31) {
+ Get();
+ signatureOmitted = true;
+ openParen = Token.NoToken;
+ } else SynErr(131);
+ } else if (la.kind == 54) {
+ Get();
+ isCoPredicate = true;
+ if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
+
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (StartOf(4)) {
+ if (la.kind == 32) {
+ GenericParameters(typeArgs);
+ }
+ if (la.kind == 26) {
+ Formals(true, isFunctionMethod, formals, out openParen);
+ if (la.kind == 5) {
+ Get();
+ SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool");
+ }
+ }
+ } else if (la.kind == 31) {
+ Get();
+ signatureOmitted = true;
+ openParen = Token.NoToken;
+ } else SynErr(132);
+ } else SynErr(133);
+ decreases = isCoPredicate ? null : new List<Expression/*!*/>();
+ while (StartOf(5)) {
+ FunctionSpec(reqs, reads, ens, decreases);
+ }
+ if (la.kind == 6) {
+ FunctionBody(out body, out bodyStart, out bodyEnd);
+ }
+ if (isPredicate) {
+ f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
+ reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);
+ } else if (isCoPredicate) {
+ f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,
+ reqs, reads, ens, body, attrs, signatureOmitted);
+ } else {
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,
+ reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);
+ }
+ f.BodyStartTok = bodyStart;
+ f.BodyEndTok = bodyEnd;
+
+ }
+
+ void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) {
+ Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
+ IToken/*!*/ id;
+ Attributes attrs = null;
+ List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();
+ IToken openParen;
+ List<Formal/*!*/> ins = new List<Formal/*!*/>();
+ List<Formal/*!*/> outs = new List<Formal/*!*/>();
+ List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();
+ List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
+ List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();
+ List<Expression/*!*/> dec = new List<Expression/*!*/>();
+ Attributes decAttrs = null;
+ Attributes modAttrs = null;
+ BlockStmt body = null;
+ bool isConstructor = false;
+ bool signatureOmitted = false;
+ IToken bodyStart = Token.NoToken;
+ IToken bodyEnd = Token.NoToken;
+
+ while (!(la.kind == 0 || la.kind == 34 || la.kind == 35)) {SynErr(134); Get();}
+ if (la.kind == 34) {
+ Get();
+ } else if (la.kind == 35) {
+ Get();
+ if (allowConstructor) {
+ isConstructor = true;
+ } else {
+ SemErr(t, "constructors are only allowed in classes");
+ }
+
+ } else SynErr(135);
+ if (isConstructor) {
+ if (mmod.IsGhost) {
+ SemErr(t, "constructors cannot be declared 'ghost'");
+ }
+ if (mmod.IsStatic) {
+ SemErr(t, "constructors cannot be declared 'static'");
+ }
+ }
+
+ 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, !mmod.IsGhost, ins, out openParen);
+ 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 == 31) {
+ Get();
+ signatureOmitted = true; openParen = Token.NoToken;
+ } else SynErr(136);
+ while (StartOf(6)) {
+ MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
+ }
+ if (la.kind == 6) {
+ BlockStmt(out body, out bodyStart, out bodyEnd);
+ }
+ if (isConstructor) {
+ m = new Constructor(id, id.val, typeArgs, ins,
+ req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
+ } else {
+ m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
+ req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
+ }
+ m.BodyStartTok = bodyStart;
+ m.BodyEndTok = bodyEnd;
+
+ }
+
+ void DatatypeMemberDecl(List<DatatypeCtor/*!*/>/*!*/ ctors) {
+ Contract.Requires(cce.NonNullElements(ctors));
+ Attributes attrs = null;
+ IToken/*!*/ id;
+ List<Formal/*!*/> formals = new List<Formal/*!*/>();
+
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
+ if (la.kind == 26) {
+ FormalsOptionalIds(formals);
+ }
+ ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
+ }
+
+ void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
+ Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
+ Expect(26);
+ 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) {
+ Get();
+ TypeIdentOptional(out id, out name, out ty, out isGhost);
+ formals.Add(new Formal(id, name, ty, true, isGhost));
+ }
+ }
+ Expect(28);
+ }
+
+ void IdentType(out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId) {
+ Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
+ WildIdent(out id, allowWildcardId);
+ Expect(5);
+ Type(out ty);
+ }
+
+ void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
+ Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
+ Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
+ isGhost = false;
+ if (la.kind == 8) {
+ Get();
+ if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
+ }
+ IdentType(out id, out ty, true);
+ }
+
+ void WildIdent(out IToken/*!*/ x, bool allowWildcardId) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ Expect(1);
+ x = t;
+ if (x.val.StartsWith("_")) {
+ if (allowWildcardId && x.val.Length == 1) {
+ t.val = "_v" + anonymousIds++;
+ } else {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ }
+
+ }
+
+ void Type(out Type/*!*/ ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
+ TypeAndToken(out tok, out ty);
+ }
+
+ void LocalIdentTypeOptional(out VarDecl/*!*/ var, bool isGhost) {
+ IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
+
+ WildIdent(out id, true);
+ if (la.kind == 5) {
+ Get();
+ Type(out ty);
+ optType = ty;
+ }
+ var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost);
+ }
+
+ void IdentTypeOptional(out BoundVar/*!*/ var) {
+ Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
+
+ WildIdent(out id, true);
+ if (la.kind == 5) {
+ Get();
+ Type(out ty);
+ optType = ty;
+ }
+ var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType);
+ }
+
+ void TypeIdentOptional(out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost) {
+ Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
+ Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
+ Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
+ string name = null; isGhost = false;
+ if (la.kind == 8) {
+ Get();
+ isGhost = true;
+ }
+ TypeAndToken(out id, out ty);
+ if (la.kind == 5) {
+ Get();
+ UserDefinedType udt = ty as UserDefinedType;
+ if (udt != null && udt.TypeArgs.Count == 0) {
+ name = udt.Name;
+ } else {
+ SemErr(id, "invalid formal-parameter name in datatype constructor");
+ }
+
+ Type(out ty);
+ }
+ if (name != null) {
+ identName = name;
+ } else {
+ identName = "#" + anonymousIds++;
+ }
+
+ }
+
+ void TypeAndToken(out IToken/*!*/ tok, out Type/*!*/ ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ List<Type/*!*/>/*!*/ gt;
+
+ switch (la.kind) {
+ case 44: {
+ Get();
+ tok = t;
+ break;
+ }
+ case 45: {
+ Get();
+ tok = t; ty = new NatType();
+ break;
+ }
+ case 46: {
+ Get();
+ tok = t; ty = new IntType();
+ break;
+ }
+ case 47: {
+ Get();
+ tok = t; gt = new List<Type/*!*/>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("set type expects exactly one type argument");
+ }
+ ty = new SetType(gt[0]);
+
+ break;
+ }
+ case 48: {
+ Get();
+ tok = t; gt = new List<Type/*!*/>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("multiset type expects exactly one type argument");
+ }
+ ty = new MultiSetType(gt[0]);
+
+ break;
+ }
+ case 49: {
+ Get();
+ tok = t; gt = new List<Type/*!*/>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("seq type expects exactly one type argument");
+ }
+ ty = new SeqType(gt[0]);
+
+ break;
+ }
+ case 50: {
+ Get();
+ tok = t; gt = new List<Type/*!*/>();
+ GenericInstantiation(gt);
+ if (gt.Count != 2) {
+ SemErr("map type expects exactly two type arguments");
+ }
+ else { ty = new MapType(gt[0], gt[1]); }
+
+ break;
+ }
+ case 1: case 3: case 51: {
+ ReferenceType(out tok, out ty);
+ break;
+ }
+ default: SynErr(137); break;
+ }
+ }
+
+ void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {
+ Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
+ Expect(26);
+ openParen = t;
+ if (la.kind == 1 || la.kind == 8) {
+ GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
+ formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
+ while (la.kind == 24) {
+ Get();
+ GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
+ formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
+ }
+ }
+ Expect(28);
+ }
+
+ void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,
+List<MaybeFreeExpression/*!*/>/*!*/ req, List<MaybeFreeExpression/*!*/>/*!*/ ens,
+List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*/ 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(8))) {SynErr(138); 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(139); Get();}
+ Expect(14);
+ } else 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(140); Get();}
+ Expect(14);
+ } else if (StartOf(10)) {
+ if (la.kind == 38) {
+ Get();
+ isFree = true;
+ }
+ if (la.kind == 43) {
+ Get();
+ isYield = true;
+ }
+ if (la.kind == 39) {
+ Get();
+ Expression(out e);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(141); Get();}
+ Expect(14);
+ 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(142); Get();}
+ Expect(14);
+ if (isYield) {
+ yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
+ } else {
+ ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
+ }
+
+ } else SynErr(143);
+ } else if (la.kind == 41) {
+ Get();
+ while (IsAttribute()) {
+ Attribute(ref decrAttrs);
+ }
+ DecreasesList(decreases, false);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(144); Get();}
+ Expect(14);
+ } else SynErr(145);
+ }
+
+ void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
+ Contract.Ensures(Contract.ValueAtReturn(out block) != null);
+ List<Statement/*!*/> body = new List<Statement/*!*/>();
+
+ Expect(6);
+ bodyStart = t;
+ while (StartOf(11)) {
+ Stmt(body);
+ }
+ Expect(7);
+ bodyEnd = t;
+ block = new BlockStmt(bodyStart, body);
+ }
+
+ void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
+List<Expression/*!*/>/*!*/ 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(146); 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(147); 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(148); 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(149); Get();}
+ Expect(14);
+ ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
+ } else SynErr(150);
+ } else if (la.kind == 41) {
+ Get();
+ while (IsAttribute()) {
+ Attribute(ref decAttrs);
+ }
+ DecreasesList(decreases, true);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(151); Get();}
+ Expect(14);
+ } else SynErr(152);
+ }
+
+ void FrameExpression(out FrameExpression/*!*/ fe) {
+ Contract.Ensures(Contract.ValueAtReturn(out fe) != null);
+ Expression/*!*/ e;
+ IToken/*!*/ id;
+ string fieldName = null; IToken feTok = null;
+ fe = null;
+
+ if (StartOf(13)) {
+ Expression(out e);
+ feTok = e.tok;
+ if (la.kind == 56) {
+ Get();
+ Ident(out id);
+ fieldName = id.val; feTok = id;
+ }
+ fe = new FrameExpression(feTok, e, fieldName);
+ } else if (la.kind == 56) {
+ Get();
+ Ident(out id);
+ fieldName = id.val;
+ fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
+ } else SynErr(153);
+ }
+
+ void Expression(out Expression/*!*/ e) {
+ EquivExpression(out e);
+ }
+
+ void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard) {
+ Expression/*!*/ e;
+ PossiblyWildExpression(out e);
+ if (!allowWildcard && e is WildcardExpr) {
+ SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
+ } else {
+ decreases.Add(e);
+ }
+
+ while (la.kind == 24) {
+ Get();
+ PossiblyWildExpression(out e);
+ if (!allowWildcard && e is WildcardExpr) {
+ SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
+ } else {
+ decreases.Add(e);
+ }
+
+ }
+ }
+
+ void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
+ Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
+ Expect(32);
+ Type(out ty);
+ gt.Add(ty);
+ while (la.kind == 24) {
+ Get();
+ Type(out ty);
+ gt.Add(ty);
+ }
+ Expect(33);
+ }
+
+ void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
+ tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ List<Type/*!*/>/*!*/ gt;
+ List<IToken> path;
+
+ if (la.kind == 51) {
+ Get();
+ tok = t; ty = new ObjectType();
+ } else if (la.kind == 3) {
+ Get();
+ tok = t; gt = new List<Type/*!*/>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("array type expects exactly one type argument");
+ }
+ int dims = 1;
+ if (tok.val.Length != 5) {
+ dims = int.Parse(tok.val.Substring(5));
+ }
+ ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
+
+ } else if (la.kind == 1) {
+ Ident(out tok);
+ gt = new List<Type/*!*/>();
+ path = new List<IToken>();
+ while (la.kind == 17) {
+ path.Add(tok);
+ Get();
+ Ident(out tok);
+ }
+ if (la.kind == 32) {
+ GenericInstantiation(gt);
+ }
+ ty = new UserDefinedType(tok, tok.val, gt, path);
+ } else SynErr(154);
+ }
+
+ void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
+ Contract.Requires(cce.NonNullElements(reqs));
+ Contract.Requires(cce.NonNullElements(reads));
+ Contract.Requires(decreases == null || cce.NonNullElements(decreases));
+ Expression/*!*/ e; FrameExpression/*!*/ fe;
+ if (la.kind == 39) {
+ while (!(la.kind == 0 || la.kind == 39)) {SynErr(155); Get();}
+ Get();
+ Expression(out e);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(156); Get();}
+ Expect(14);
+ reqs.Add(e);
+ } else if (la.kind == 42) {
+ Get();
+ if (StartOf(14)) {
+ PossiblyWildFrameExpression(out fe);
+ reads.Add(fe);
+ while (la.kind == 24) {
+ Get();
+ PossiblyWildFrameExpression(out fe);
+ reads.Add(fe);
+ }
+ }
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(157); Get();}
+ Expect(14);
+ } else if (la.kind == 40) {
+ Get();
+ Expression(out e);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(158); Get();}
+ Expect(14);
+ ens.Add(e);
+ } else if (la.kind == 41) {
+ Get();
+ if (decreases == null) {
+ SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
+ decreases = new List<Expression/*!*/>();
+ }
+
+ DecreasesList(decreases, false);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(159); Get();}
+ Expect(14);
+ } else SynErr(160);
+ }
+
+ void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
+ Expect(6);
+ bodyStart = t;
+ Expression(out e);
+ Expect(7);
+ bodyEnd = t;
+ }
+
+ void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
+ Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
+ if (la.kind == 55) {
+ Get();
+ fe = new FrameExpression(t, new WildcardExpr(t), null);
+ } else if (StartOf(9)) {
+ FrameExpression(out fe);
+ } else SynErr(161);
+ }
+
+ void PossiblyWildExpression(out Expression/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
+ e = dummyExpr;
+ if (la.kind == 55) {
+ Get();
+ e = new WildcardExpr(t);
+ } else if (StartOf(13)) {
+ Expression(out e);
+ } else SynErr(162);
+ }
+
+ void Stmt(List<Statement/*!*/>/*!*/ ss) {
+ Statement/*!*/ s;
+
+ OneStmt(out s);
+ ss.Add(s);
+ }
+
+ void OneStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
+ s = dummyStmt; /* to please the compiler */
+ BlockStmt bs;
+ IToken bodyStart, bodyEnd;
+ int breakCount;
+
+ while (!(StartOf(15))) {SynErr(163); Get();}
+ switch (la.kind) {
+ case 6: {
+ BlockStmt(out bs, out bodyStart, out bodyEnd);
+ s = bs;
+ break;
+ }
+ case 75: {
+ AssertStmt(out s);
+ break;
+ }
+ case 63: {
+ AssumeStmt(out s);
+ break;
+ }
+ case 76: {
+ PrintStmt(out s);
+ break;
+ }
+ case 1: case 2: case 22: case 26: case 101: case 102: case 103: case 104: case 105: case 106: {
+ UpdateStmt(out s);
+ break;
+ }
+ case 8: case 23: {
+ VarDeclStatement(out s);
+ break;
+ }
+ case 68: {
+ IfStmt(out s);
+ break;
+ }
+ case 72: {
+ WhileStmt(out s);
+ break;
+ }
+ case 74: {
+ MatchStmt(out s);
+ break;
+ }
+ case 77: {
+ ParallelStmt(out s);
+ break;
+ }
+ case 78: {
+ CalcStmt(out s);
+ break;
+ }
+ case 57: {
+ Get();
+ x = t;
+ NoUSIdent(out id);
+ Expect(5);
+ OneStmt(out s);
+ s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
+ break;
+ }
+ case 58: {
+ Get();
+ x = t; breakCount = 1; label = null;
+ if (la.kind == 1) {
+ NoUSIdent(out id);
+ label = id.val;
+ } else if (la.kind == 14 || la.kind == 58) {
+ while (la.kind == 58) {
+ Get();
+ breakCount++;
+ }
+ } else SynErr(164);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(165); Get();}
+ Expect(14);
+ s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
+ break;
+ }
+ case 43: case 61: {
+ ReturnStmt(out s);
+ break;
+ }
+ case 31: {
+ SkeletonStmt(out s);
+ Expect(14);
+ break;
+ }
+ default: SynErr(166); break;
+ }
+ }
+
+ void AssertStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+
+ Expect(75);
+ x = t;
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ if (StartOf(13)) {
+ Expression(out e);
+ } else if (la.kind == 31) {
+ Get();
+ } else SynErr(167);
+ Expect(14);
+ if (e == null) {
+ s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssertStmt(x, e, attrs);
+ }
+
+ }
+
+ void AssumeStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+
+ Expect(63);
+ x = t;
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ if (StartOf(13)) {
+ Expression(out e);
+ } else if (la.kind == 31) {
+ Get();
+ } else SynErr(168);
+ if (e == null) {
+ s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssumeStmt(x, e, attrs);
+ }
+
+ Expect(14);
+ }
+
+ void PrintStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
+ List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
+
+ Expect(76);
+ x = t;
+ AttributeArg(out arg);
+ args.Add(arg);
+ while (la.kind == 24) {
+ Get();
+ AttributeArg(out arg);
+ args.Add(arg);
+ }
+ Expect(14);
+ s = new PrintStmt(x, args);
+ }
+
+ void UpdateStmt(out Statement/*!*/ s) {
+ List<Expression> lhss = new List<Expression>();
+ List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+ Expression e; AssignmentRhs r;
+ Expression lhs0;
+ IToken x;
+ Attributes attrs = null;
+ IToken suchThatAssume = null;
+ Expression suchThat = null;
+
+ Lhs(out e);
+ x = e.tok;
+ if (la.kind == 6 || la.kind == 14) {
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ Expect(14);
+ rhss.Add(new ExprRhs(e, attrs));
+ } else if (la.kind == 24 || la.kind == 60 || la.kind == 62) {
+ lhss.Add(e); lhs0 = e;
+ while (la.kind == 24) {
+ Get();
+ Lhs(out e);
+ lhss.Add(e);
+ }
+ if (la.kind == 60) {
+ Get();
+ x = t;
+ Rhs(out r, lhs0);
+ rhss.Add(r);
+ while (la.kind == 24) {
+ Get();
+ Rhs(out r, lhs0);
+ rhss.Add(r);
+ }
+ } else if (la.kind == 62) {
+ Get();
+ x = t;
+ if (la.kind == 63) {
+ Get();
+ suchThatAssume = t;
+ }
+ Expression(out suchThat);
+ } else SynErr(169);
+ Expect(14);
+ } else if (la.kind == 5) {
+ Get();
+ SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
+ } else SynErr(170);
+ if (suchThat != null) {
+ s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
+ } else {
+ if (lhss.Count == 0 && rhss.Count == 0) {
+ s = new BlockStmt(x, new List<Statement>()); // error, give empty statement
+ } else {
+ s = new UpdateStmt(x, lhss, rhss);
+ }
+ }
+
+ }
+
+ void VarDeclStatement(out Statement/*!*/ s) {
+ IToken x = null, assignTok = null; bool isGhost = false;
+ VarDecl/*!*/ d;
+ AssignmentRhs r; IdentifierExpr lhs0;
+ List<VarDecl> lhss = new List<VarDecl>();
+ List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+ IToken suchThatAssume = null;
+ Expression suchThat = null;
+
+ if (la.kind == 8) {
+ Get();
+ isGhost = true; x = t;
+ }
+ Expect(23);
+ if (!isGhost) { x = t; }
+ LocalIdentTypeOptional(out d, isGhost);
+ lhss.Add(d);
+ while (la.kind == 24) {
+ Get();
+ LocalIdentTypeOptional(out d, isGhost);
+ lhss.Add(d);
+ }
+ if (la.kind == 60 || la.kind == 62) {
+ if (la.kind == 60) {
+ Get();
+ assignTok = t;
+ lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
+ lhs0.Var = lhss[0]; lhs0.Type = lhss[0].OptionalType; // resolve here
+
+ Rhs(out r, lhs0);
+ rhss.Add(r);
+ while (la.kind == 24) {
+ Get();
+ Rhs(out r, lhs0);
+ rhss.Add(r);
+ }
+ } else {
+ Get();
+ assignTok = t;
+ if (la.kind == 63) {
+ Get();
+ suchThatAssume = t;
+ }
+ Expression(out suchThat);
+ }
+ }
+ Expect(14);
+ 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);
+ } else if (rhss.Count == 0) {
+ update = null;
+ } else {
+ var ies = new List<Expression>();
+ foreach (var lhs in lhss) {
+ ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
+ }
+ update = new UpdateStmt(assignTok, ies, rhss);
+ }
+ s = new VarDeclStmt(x, lhss, update);
+
+ }
+
+ void IfStmt(out Statement/*!*/ ifStmt) {
+ Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
+ Expression guard = null; bool guardOmitted = false;
+ BlockStmt/*!*/ thn;
+ BlockStmt/*!*/ bs;
+ Statement/*!*/ s;
+ Statement els = null;
+ IToken bodyStart, bodyEnd;
+ List<GuardedAlternative> alternatives;
+ ifStmt = dummyStmt; // to please the compiler
+
+ Expect(68);
+ x = t;
+ if (la.kind == 26 || la.kind == 31) {
+ if (la.kind == 26) {
+ Guard(out guard);
+ } else {
+ Get();
+ guardOmitted = true;
+ }
+ BlockStmt(out thn, out bodyStart, out bodyEnd);
+ if (la.kind == 69) {
+ Get();
+ if (la.kind == 68) {
+ IfStmt(out s);
+ els = s;
+ } else if (la.kind == 6) {
+ BlockStmt(out bs, out bodyStart, out bodyEnd);
+ els = bs;
+ } else SynErr(171);
+ }
+ if (guardOmitted) {
+ ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
+ } else {
+ ifStmt = new IfStmt(x, guard, thn, els);
+ }
+
+ } else if (la.kind == 6) {
+ AlternativeBlock(out alternatives);
+ ifStmt = new AlternativeStmt(x, alternatives);
+ } else SynErr(172);
+ }
+
+ void WhileStmt(out Statement/*!*/ stmt) {
+ Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
+ Expression guard = null; bool guardOmitted = false;
+ List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
+ List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ Attributes decAttrs = null;
+ Attributes modAttrs = null;
+ List<FrameExpression/*!*/> mod = null;
+ BlockStmt/*!*/ body = null; bool bodyOmitted = false;
+ IToken bodyStart = null, bodyEnd = null;
+ List<GuardedAlternative> alternatives;
+ stmt = dummyStmt; // to please the compiler
+
+ Expect(72);
+ x = t;
+ if (la.kind == 26 || la.kind == 31) {
+ if (la.kind == 26) {
+ Guard(out guard);
+ Contract.Assume(guard == null || cce.Owner.None(guard));
+ } else {
+ Get();
+ guardOmitted = true;
+ }
+ LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
+ if (la.kind == 6) {
+ BlockStmt(out body, out bodyStart, out bodyEnd);
+ } else if (la.kind == 31) {
+ Get();
+ bodyOmitted = true;
+ } else SynErr(173);
+ if (guardOmitted || bodyOmitted) {
+ if (mod != null) {
+ SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
+ }
+ if (body == null) {
+ body = new BlockStmt(x, new List<Statement>());
+ }
+ stmt = new WhileStmt(x, 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);
+ }
+
+ } else if (StartOf(16)) {
+ 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);
+ } else SynErr(174);
+ }
+
+ void MatchStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null);
+ Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
+ List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
+ Expect(74);
+ x = t;
+ Expression(out e);
+ Expect(6);
+ while (la.kind == 70) {
+ CaseStatement(out c);
+ cases.Add(c);
+ }
+ Expect(7);
+ s = new MatchStmt(x, e, cases);
+ }
+
+ void ParallelStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null);
+ IToken/*!*/ x;
+ List<BoundVar/*!*/> bvars = null;
+ Attributes attrs = null;
+ Expression range = null;
+ var ens = new List<MaybeFreeExpression/*!*/>();
+ bool isFree;
+ Expression/*!*/ e;
+ BlockStmt/*!*/ block;
+ IToken bodyStart, bodyEnd;
+
+ Expect(77);
+ x = t;
+ Expect(26);
+ if (la.kind == 1) {
+ List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX;
+ QuantifierDomain(out bvarsX, out attrsX, out rangeX);
+ bvars = bvarsX; attrs = attrsX; range = rangeX;
+
+ }
+ if (bvars == null) { bvars = new List<BoundVar>(); }
+ if (range == null) { range = new LiteralExpr(x, true); }
+
+ Expect(28);
+ while (la.kind == 38 || la.kind == 40) {
+ isFree = false;
+ if (la.kind == 38) {
+ Get();
+ isFree = true;
+ }
+ Expect(40);
+ Expression(out e);
+ Expect(14);
+ ens.Add(new MaybeFreeExpression(e, isFree));
+ }
+ BlockStmt(out block, out bodyStart, out bodyEnd);
+ s = new ParallelStmt(x, bvars, attrs, range, ens, block);
+ }
+
+ void CalcStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null);
+ Token x;
+ BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;
+ var lines = new List<Expression/*!*/>();
+ var hints = new List<BlockStmt/*!*/>();
+ var customOps = new List<BinaryExpr.Opcode?>();
+ BinaryExpr.Opcode? maybeOp;
+ Expression/*!*/ e;
+ BlockStmt/*!*/ h;
+ IToken opTok;
+
+ Expect(78);
+ x = t;
+ if (StartOf(17)) {
+ CalcOp(out opTok, out calcOp);
+ maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(calcOp, calcOp); // guard against non-trasitive calcOp (like !=)
+ if (maybeOp == null) {
+ SemErr(opTok, "the main operator of a calculation must be transitive");
+ }
+ resOp = calcOp;
+
+ }
+ Expect(6);
+ if (StartOf(13)) {
+ Expression(out e);
+ lines.Add(e);
+ Expect(14);
+ while (StartOf(18)) {
+ Hint(out h);
+ hints.Add(h);
+ if (StartOf(17)) {
+ CalcOp(out opTok, out op);
+ maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
+ if (maybeOp == null) {
+ customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor
+ SemErr(opTok, "this operator cannot continue this calculation");
+ } else {
+ customOps.Add(op);
+ resOp = (BinaryExpr.Opcode)maybeOp;
+ }
+
+ } else if (StartOf(13)) {
+ customOps.Add(null);
+ } else SynErr(175);
+ Expression(out e);
+ lines.Add(e);
+ Expect(14);
+ }
+ }
+ Expect(7);
+ s = new CalcStmt(x, calcOp, lines, hints, customOps);
+ }
+
+ void ReturnStmt(out Statement/*!*/ s) {
+ IToken returnTok = null;
+ List<AssignmentRhs> rhss = null;
+ AssignmentRhs r;
+ bool isYield = false;
+
+ if (la.kind == 61) {
+ Get();
+ returnTok = t;
+ } else if (la.kind == 43) {
+ Get();
+ returnTok = t; isYield = true;
+ } else SynErr(176);
+ if (StartOf(19)) {
+ Rhs(out r, null);
+ rhss = new List<AssignmentRhs>(); rhss.Add(r);
+ while (la.kind == 24) {
+ Get();
+ Rhs(out r, null);
+ rhss.Add(r);
+ }
+ }
+ Expect(14);
+ if (isYield) {
+ s = new YieldStmt(returnTok, rhss);
+ } else {
+ s = new ReturnStmt(returnTok, rhss);
+ }
+
+ }
+
+ void SkeletonStmt(out Statement s) {
+ List<IToken> names = null;
+ List<Expression> exprs = null;
+ IToken tok, dotdotdot, whereTok;
+ Expression e;
+ Expect(31);
+ dotdotdot = t;
+ if (la.kind == 59) {
+ Get();
+ names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
+ Ident(out tok);
+ names.Add(tok);
+ while (la.kind == 24) {
+ Get();
+ Ident(out tok);
+ names.Add(tok);
+ }
+ Expect(60);
+ Expression(out e);
+ exprs.Add(e);
+ while (la.kind == 24) {
+ Get();
+ Expression(out e);
+ exprs.Add(e);
+ }
+ if (exprs.Count != names.Count) {
+ SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");
+ names = null; exprs = null;
+ }
+
+ }
+ s = new SkeletonStatement(dotdotdot, names, exprs);
+ }
+
+ void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {
+ Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);
+ IToken/*!*/ x, newToken; Expression/*!*/ e;
+ List<Expression> ee = null;
+ Type ty = null;
+ CallStmt initCall = null;
+ List<Expression> args;
+ r = dummyRhs; // to please compiler
+ Attributes attrs = null;
+
+ if (la.kind == 64) {
+ Get();
+ newToken = t;
+ TypeAndToken(out x, out ty);
+ if (la.kind == 17 || la.kind == 26 || la.kind == 65) {
+ if (la.kind == 65) {
+ Get();
+ ee = new List<Expression>();
+ Expressions(ee);
+ Expect(66);
+ UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
+
+ } else if (la.kind == 17) {
+ Get();
+ Ident(out x);
+ Expect(26);
+ args = new List<Expression/*!*/>();
+ if (StartOf(13)) {
+ Expressions(args);
+ }
+ Expect(28);
+ initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
+ } else {
+ Get();
+ var udf = ty as UserDefinedType;
+ if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {
+ // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as
+ // the name of the constructor that's being invoked.
+ x = udf.tok;
+ ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));
+ } else {
+ SemErr(t, "expected '.'");
+ x = null;
+ }
+ args = new List<Expression/*!*/>();
+ if (StartOf(13)) {
+ Expressions(args);
+ }
+ Expect(28);
+ if (x != null) {
+ initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
+ }
+
+ }
+ }
+ if (ee != null) {
+ r = new TypeRhs(newToken, ty, ee);
+ } else {
+ r = new TypeRhs(newToken, ty, initCall);
+ }
+
+ } else if (la.kind == 67) {
+ Get();
+ x = t;
+ Expression(out e);
+ r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
+ } else if (la.kind == 55) {
+ Get();
+ r = new HavocRhs(t);
+ } else if (StartOf(13)) {
+ Expression(out e);
+ r = new ExprRhs(e);
+ } else SynErr(177);
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ r.Attributes = attrs;
+ }
+
+ void Lhs(out Expression e) {
+ e = dummyExpr; // the assignment is to please the compiler, the dummy value to satisfy contracts in the event of a parse error
+
+ if (la.kind == 1) {
+ DottedIdentifiersAndFunction(out e);
+ while (la.kind == 17 || la.kind == 65) {
+ Suffix(ref e);
+ }
+ } else if (StartOf(20)) {
+ ConstAtomExpression(out e);
+ Suffix(ref e);
+ while (la.kind == 17 || la.kind == 65) {
+ Suffix(ref e);
+ }
+ } else SynErr(178);
+ }
+
+ void Expressions(List<Expression/*!*/>/*!*/ args) {
+ Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
+ Expression(out e);
+ args.Add(e);
+ while (la.kind == 24) {
+ Get();
+ Expression(out e);
+ args.Add(e);
+ }
+ }
+
+ void Guard(out Expression e) {
+ Expression/*!*/ ee; e = null;
+ Expect(26);
+ if (la.kind == 55) {
+ Get();
+ e = null;
+ } else if (StartOf(13)) {
+ Expression(out ee);
+ e = ee;
+ } else SynErr(179);
+ Expect(28);
+ }
+
+ void AlternativeBlock(out List<GuardedAlternative> alternatives) {
+ alternatives = new List<GuardedAlternative>();
+ IToken x;
+ Expression e;
+ List<Statement> body;
+
+ Expect(6);
+ while (la.kind == 70) {
+ Get();
+ x = t;
+ Expression(out e);
+ Expect(71);
+ body = new List<Statement>();
+ while (StartOf(11)) {
+ Stmt(body);
+ }
+ alternatives.Add(new GuardedAlternative(x, e, body));
+ }
+ Expect(7);
+ }
+
+ void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
+ FrameExpression/*!*/ fe;
+ invariants = new List<MaybeFreeExpression/*!*/>();
+ MaybeFreeExpression invariant = null;
+ decreases = new List<Expression/*!*/>();
+ mod = null;
+
+ while (StartOf(21)) {
+ if (la.kind == 38 || la.kind == 73) {
+ Invariant(out invariant);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(180); Get();}
+ Expect(14);
+ invariants.Add(invariant);
+ } else if (la.kind == 41) {
+ while (!(la.kind == 0 || la.kind == 41)) {SynErr(181); Get();}
+ Get();
+ while (IsAttribute()) {
+ Attribute(ref decAttrs);
+ }
+ DecreasesList(decreases, true);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(182); Get();}
+ Expect(14);
+ } else {
+ while (!(la.kind == 0 || la.kind == 37)) {SynErr(183); Get();}
+ Get();
+ while (IsAttribute()) {
+ Attribute(ref modAttrs);
+ }
+ mod = mod ?? new List<FrameExpression>();
+ 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(184); Get();}
+ Expect(14);
+ }
+ }
+ }
+
+ void Invariant(out MaybeFreeExpression/*!*/ invariant) {
+ bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
+ while (!(la.kind == 0 || la.kind == 38 || la.kind == 73)) {SynErr(185); Get();}
+ if (la.kind == 38) {
+ Get();
+ isFree = true;
+ }
+ Expect(73);
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ Expression(out e);
+ invariant = new MaybeFreeExpression(e, isFree, attrs);
+ }
+
+ void CaseStatement(out MatchCaseStmt/*!*/ c) {
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null);
+ IToken/*!*/ x, id;
+ List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
+ List<Statement/*!*/> body = new List<Statement/*!*/>();
+
+ Expect(70);
+ x = t;
+ Ident(out id);
+ if (la.kind == 26) {
+ Get();
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
+ while (la.kind == 24) {
+ Get();
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
+ }
+ Expect(28);
+ }
+ Expect(71);
+ while (StartOf(11)) {
+ Stmt(body);
+ }
+ c = new MatchCaseStmt(x, id.val, arguments, body);
+ }
+
+ void AttributeArg(out Attributes.Argument/*!*/ arg) {
+ Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg;
+ if (la.kind == 4) {
+ Get();
+ arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2));
+ } else if (StartOf(13)) {
+ Expression(out e);
+ arg = new Attributes.Argument(t, e);
+ } else SynErr(186);
+ }
+
+ void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
+ bvars = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
+ attrs = null;
+ range = null;
+
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ while (la.kind == 24) {
+ Get();
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ }
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ if (la.kind == 22) {
+ Get();
+ Expression(out range);
+ }
+ }
+
+ void CalcOp(out IToken x, out BinaryExpr.Opcode/*!*/ op) {
+ Contract.Ensures(Microsoft.Dafny.CalcStmt.ValidOp(Contract.ValueAtReturn(out op)));
+ op = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
+ x = null;
+
+ switch (la.kind) {
+ case 27: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Eq;
+ break;
+ }
+ case 32: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Lt;
+ break;
+ }
+ case 33: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Gt;
+ break;
+ }
+ case 79: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Le;
+ break;
+ }
+ case 80: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Ge;
+ break;
+ }
+ case 81: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Neq;
+ break;
+ }
+ case 82: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Neq;
+ break;
+ }
+ case 83: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Le;
+ break;
+ }
+ case 84: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Ge;
+ break;
+ }
+ case 85: case 86: {
+ EquivOp();
+ x = t; op = BinaryExpr.Opcode.Iff;
+ break;
+ }
+ case 87: case 88: {
+ ImpliesOp();
+ x = t; op = BinaryExpr.Opcode.Imp;
+ break;
+ }
+ default: SynErr(187); break;
+ }
+ }
+
+ void Hint(out BlockStmt s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
+ var subhints = new List<Statement/*!*/>();
+ IToken bodyStart, bodyEnd;
+ BlockStmt/*!*/ block;
+ Statement/*!*/ calc;
+ Token x = la;
+
+ while (la.kind == 6 || la.kind == 78) {
+ if (la.kind == 6) {
+ BlockStmt(out block, out bodyStart, out bodyEnd);
+ subhints.Add(block);
+ } else {
+ CalcStmt(out calc);
+ 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
+
+ }
+
+ void EquivOp() {
+ if (la.kind == 85) {
+ Get();
+ } else if (la.kind == 86) {
+ Get();
+ } else SynErr(188);
+ }
+
+ void ImpliesOp() {
+ if (la.kind == 87) {
+ Get();
+ } else if (la.kind == 88) {
+ Get();
+ } else SynErr(189);
+ }
+
+ void EquivExpression(out Expression/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
+ ImpliesExpression(out e0);
+ while (la.kind == 85 || la.kind == 86) {
+ EquivOp();
+ x = t;
+ ImpliesExpression(out e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1);
+ }
+ }
+
+ void ImpliesExpression(out Expression/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
+ LogicalExpression(out e0);
+ if (la.kind == 87 || la.kind == 88) {
+ ImpliesOp();
+ x = t;
+ ImpliesExpression(out e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1);
+ }
+ }
+
+ void LogicalExpression(out Expression/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
+ RelationalExpression(out e0);
+ if (StartOf(22)) {
+ if (la.kind == 89 || la.kind == 90) {
+ AndOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
+ while (la.kind == 89 || la.kind == 90) {
+ AndOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
+ }
+ } else {
+ OrOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
+ while (la.kind == 91 || la.kind == 92) {
+ OrOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
+ }
+ }
+ }
+ }
+
+ void RelationalExpression(out Expression/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
+ List<Expression> chain = null;
+ List<BinaryExpr.Opcode> ops = null;
+ int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
+ // 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
+ // 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
+ // 3 ("illegal") indicates illegal chain
+ // 4 ("disjoint") indicates chain of disjoint set operators
+ bool hasSeenNeq = false;
+
+ Term(out e0);
+ e = e0;
+ if (StartOf(23)) {
+ RelOp(out x, out op);
+ firstOpTok = x;
+ Term(out e1);
+ e = new BinaryExpr(x, op, e0, e1);
+ if (op == BinaryExpr.Opcode.Disjoint)
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
+
+ while (StartOf(23)) {
+ if (chain == null) {
+ chain = new List<Expression>();
+ ops = new List<BinaryExpr.Opcode>();
+ chain.Add(e0); ops.Add(op); chain.Add(e1);
+ switch (op) {
+ case BinaryExpr.Opcode.Eq:
+ kind = 0; break;
+ case BinaryExpr.Opcode.Neq:
+ kind = 0; hasSeenNeq = true; break;
+ case BinaryExpr.Opcode.Lt:
+ case BinaryExpr.Opcode.Le:
+ kind = 1; break;
+ case BinaryExpr.Opcode.Gt:
+ case BinaryExpr.Opcode.Ge:
+ kind = 2; break;
+ case BinaryExpr.Opcode.Disjoint:
+ kind = 4; break;
+ default:
+ kind = 3; break;
+ }
+ }
+ e0 = e1;
+
+ RelOp(out x, out op);
+ switch (op) {
+ case BinaryExpr.Opcode.Eq:
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }
+ break;
+ case BinaryExpr.Opcode.Neq:
+ if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
+ hasSeenNeq = true; break;
+ case BinaryExpr.Opcode.Lt:
+ case BinaryExpr.Opcode.Le:
+ if (kind == 0) { kind = 1; }
+ else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
+ break;
+ case BinaryExpr.Opcode.Gt:
+ case BinaryExpr.Opcode.Ge:
+ if (kind == 0) { kind = 2; }
+ else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
+ break;
+ case BinaryExpr.Opcode.Disjoint:
+ if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
+ break;
+ default:
+ SemErr(x, "this operator cannot be part of a chain");
+ kind = 3; break;
+ }
+
+ Term(out e1);
+ ops.Add(op); chain.Add(e1);
+ if (op == BinaryExpr.Opcode.Disjoint) {
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
+ }
+ else
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+
+ }
+ }
+ if (chain != null) {
+ e = new ChainingExpression(firstOpTok, chain, ops, e);
+ }
+
+ }
+
+ void AndOp() {
+ if (la.kind == 89) {
+ Get();
+ } else if (la.kind == 90) {
+ Get();
+ } else SynErr(190);
+ }
+
+ void OrOp() {
+ if (la.kind == 91) {
+ Get();
+ } else if (la.kind == 92) {
+ Get();
+ } else SynErr(191);
+ }
+
+ void Term(out Expression/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
+ Factor(out e0);
+ while (la.kind == 96 || la.kind == 97) {
+ AddOp(out x, out op);
+ Factor(out e1);
+ e0 = new BinaryExpr(x, op, e0, e1);
+ }
+ }
+
+ void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
+ IToken y;
+
+ switch (la.kind) {
+ case 27: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Eq;
+ break;
+ }
+ case 32: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Lt;
+ break;
+ }
+ case 33: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Gt;
+ break;
+ }
+ case 79: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Le;
+ break;
+ }
+ case 80: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Ge;
+ break;
+ }
+ case 81: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Neq;
+ break;
+ }
+ case 93: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Disjoint;
+ break;
+ }
+ case 94: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.In;
+ break;
+ }
+ case 95: {
+ Get();
+ x = t; y = Token.NoToken;
+ if (la.kind == 94) {
+ Get();
+ y = t;
+ }
+ if (y == Token.NoToken) {
+ SemErr(x, "invalid RelOp");
+ } else if (y.pos != x.pos + 1) {
+ SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");
+ } else {
+ x.val = "!in";
+ op = BinaryExpr.Opcode.NotIn;
+ }
+
+ break;
+ }
+ case 82: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Neq;
+ break;
+ }
+ case 83: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Le;
+ break;
+ }
+ case 84: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Ge;
+ break;
+ }
+ default: SynErr(192); break;
+ }
+ }
+
+ void Factor(out Expression/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
+ UnaryExpression(out e0);
+ while (la.kind == 55 || la.kind == 98 || la.kind == 99) {
+ MulOp(out x, out op);
+ UnaryExpression(out e1);
+ e0 = new BinaryExpr(x, op, e0, e1);
+ }
+ }
+
+ void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
+ if (la.kind == 96) {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Add;
+ } else if (la.kind == 97) {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Sub;
+ } else SynErr(193);
+ }
+
+ void UnaryExpression(out Expression/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
+ switch (la.kind) {
+ case 97: {
+ Get();
+ x = t;
+ UnaryExpression(out e);
+ e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
+ break;
+ }
+ case 95: case 100: {
+ NegOp();
+ x = t;
+ UnaryExpression(out e);
+ e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
+ break;
+ }
+ case 23: case 47: case 57: case 63: case 68: case 74: case 75: case 109: case 110: case 111: case 112: {
+ EndlessExpression(out e);
+ break;
+ }
+ case 1: {
+ DottedIdentifiersAndFunction(out e);
+ while (la.kind == 17 || la.kind == 65) {
+ Suffix(ref e);
+ }
+ break;
+ }
+ case 6: case 65: {
+ DisplayExpr(out e);
+ while (la.kind == 17 || la.kind == 65) {
+ Suffix(ref e);
+ }
+ break;
+ }
+ case 48: {
+ MultiSetExpr(out e);
+ while (la.kind == 17 || la.kind == 65) {
+ Suffix(ref e);
+ }
+ break;
+ }
+ case 50: {
+ Get();
+ x = t;
+ if (la.kind == 65) {
+ MapDisplayExpr(x, out e);
+ while (la.kind == 17 || la.kind == 65) {
+ Suffix(ref e);
+ }
+ } else if (la.kind == 1) {
+ MapComprehensionExpr(x, out e);
+ } else if (StartOf(24)) {
+ SemErr("map must be followed by literal in brackets or comprehension.");
+ } else SynErr(194);
+ break;
+ }
+ case 2: case 22: case 26: case 101: case 102: case 103: case 104: case 105: case 106: {
+ ConstAtomExpression(out e);
+ while (la.kind == 17 || la.kind == 65) {
+ Suffix(ref e);
+ }
+ break;
+ }
+ default: SynErr(195); break;
+ }
+ }
+
+ void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
+ if (la.kind == 55) {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Mul;
+ } else if (la.kind == 98) {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Div;
+ } else if (la.kind == 99) {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Mod;
+ } else SynErr(196);
+ }
+
+ void NegOp() {
+ if (la.kind == 95) {
+ Get();
+ } else if (la.kind == 100) {
+ Get();
+ } else SynErr(197);
+ }
+
+ void EndlessExpression(out Expression e) {
+ IToken/*!*/ x;
+ Expression e0, e1;
+ e = dummyExpr;
+
+ switch (la.kind) {
+ case 68: {
+ Get();
+ x = t;
+ Expression(out e);
+ Expect(107);
+ Expression(out e0);
+ Expect(69);
+ Expression(out e1);
+ e = new ITEExpr(x, e, e0, e1);
+ break;
+ }
+ case 74: {
+ MatchExpression(out e);
+ break;
+ }
+ case 109: case 110: case 111: case 112: {
+ QuantifierGuts(out e);
+ break;
+ }
+ case 47: {
+ ComprehensionExpr(out e);
+ break;
+ }
+ case 75: {
+ Get();
+ x = t;
+ Expression(out e0);
+ Expect(14);
+ Expression(out e1);
+ e = new AssertExpr(x, e0, e1);
+ break;
+ }
+ case 63: {
+ Get();
+ x = t;
+ Expression(out e0);
+ Expect(14);
+ Expression(out e1);
+ e = new AssumeExpr(x, e0, e1);
+ break;
+ }
+ case 23: {
+ LetExpr(out e);
+ break;
+ }
+ case 57: {
+ NamedExpr(out e);
+ break;
+ }
+ default: SynErr(198); break;
+ }
+ }
+
+ void DottedIdentifiersAndFunction(out Expression e) {
+ IToken id; IToken openParen = null;
+ List<Expression> args = null;
+ List<IToken> idents = new List<IToken>();
+
+ Ident(out id);
+ idents.Add(id);
+ while (la.kind == 17) {
+ Get();
+ Ident(out id);
+ idents.Add(id);
+ }
+ if (la.kind == 26) {
+ Get();
+ openParen = t; args = new List<Expression>();
+ if (StartOf(13)) {
+ Expressions(args);
+ }
+ Expect(28);
+ }
+ e = new IdentifierSequence(idents, openParen, args);
+ }
+
+ void Suffix(ref Expression/*!*/ e) {
+ Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List<Expression/*!*/>/*!*/ args;
+ Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
+ List<Expression> multipleIndices = null;
+ bool func = false;
+
+ if (la.kind == 17) {
+ Get();
+ Ident(out id);
+ if (la.kind == 26) {
+ Get();
+ IToken openParen = t; args = new List<Expression/*!*/>(); func = true;
+ if (StartOf(13)) {
+ Expressions(args);
+ }
+ Expect(28);
+ e = new FunctionCallExpr(id, id.val, e, openParen, args);
+ }
+ if (!func) { e = new ExprDotName(id, e, id.val); }
+ } else if (la.kind == 65) {
+ Get();
+ x = t;
+ if (StartOf(13)) {
+ Expression(out ee);
+ e0 = ee;
+ if (la.kind == 108) {
+ Get();
+ anyDots = true;
+ if (StartOf(13)) {
+ Expression(out ee);
+ e1 = ee;
+ }
+ } else if (la.kind == 60) {
+ Get();
+ Expression(out ee);
+ e1 = ee;
+ } else if (la.kind == 24 || la.kind == 66) {
+ while (la.kind == 24) {
+ Get();
+ Expression(out ee);
+ if (multipleIndices == null) {
+ multipleIndices = new List<Expression>();
+ multipleIndices.Add(e0);
+ }
+ multipleIndices.Add(ee);
+
+ }
+ } else SynErr(199);
+ } else if (la.kind == 108) {
+ Get();
+ anyDots = true;
+ if (StartOf(13)) {
+ Expression(out ee);
+ e1 = ee;
+ }
+ } else SynErr(200);
+ if (multipleIndices != null) {
+ e = new MultiSelectExpr(x, e, multipleIndices);
+ // make sure an array class with this dimensionality exists
+ UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);
+ } else {
+ if (!anyDots && e0 == null) {
+ /* a parsing error occurred */
+ e0 = dummyExpr;
+ }
+ Contract.Assert(anyDots || e0 != null);
+ if (anyDots) {
+ //Contract.Assert(e0 != null || e1 != null);
+ e = new SeqSelectExpr(x, false, e, e0, e1);
+ } else if (e1 == null) {
+ Contract.Assert(e0 != null);
+ e = new SeqSelectExpr(x, true, e, e0, null);
+ } else {
+ Contract.Assert(e0 != null);
+ e = new SeqUpdateExpr(x, e, e0, e1);
+ }
+ }
+
+ Expect(66);
+ } else SynErr(201);
+ }
+
+ void DisplayExpr(out Expression e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
+ e = dummyExpr;
+
+ if (la.kind == 6) {
+ Get();
+ x = t; elements = new List<Expression/*!*/>();
+ if (StartOf(13)) {
+ Expressions(elements);
+ }
+ e = new SetDisplayExpr(x, elements);
+ Expect(7);
+ } else if (la.kind == 65) {
+ Get();
+ x = t; elements = new List<Expression/*!*/>();
+ if (StartOf(13)) {
+ Expressions(elements);
+ }
+ e = new SeqDisplayExpr(x, elements);
+ Expect(66);
+ } else SynErr(202);
+ }
+
+ void MultiSetExpr(out Expression e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
+ e = dummyExpr;
+
+ Expect(48);
+ x = t;
+ if (la.kind == 6) {
+ Get();
+ elements = new List<Expression/*!*/>();
+ if (StartOf(13)) {
+ Expressions(elements);
+ }
+ e = new MultiSetDisplayExpr(x, elements);
+ Expect(7);
+ } else if (la.kind == 26) {
+ Get();
+ x = t; elements = new List<Expression/*!*/>();
+ Expression(out e);
+ e = new MultiSetFormingExpr(x, e);
+ Expect(28);
+ } else if (StartOf(25)) {
+ SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
+ } else SynErr(203);
+ }
+
+ void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
+ e = dummyExpr;
+
+ Expect(65);
+ if (StartOf(13)) {
+ MapLiteralExpressions(out elements);
+ }
+ e = new MapDisplayExpr(mapToken, elements);
+ Expect(66);
+ }
+
+ void MapComprehensionExpr(IToken/*!*/ mapToken, out Expression e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ Expression range = null;
+ Expression body;
+
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ if (la.kind == 22) {
+ Get();
+ Expression(out range);
+ }
+ QSep();
+ Expression(out body);
+ e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body);
+
+ }
+
+ void ConstAtomExpression(out Expression/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x; BigInteger n;
+ e = dummyExpr;
+
+ switch (la.kind) {
+ case 101: {
+ Get();
+ e = new LiteralExpr(t, false);
+ break;
+ }
+ case 102: {
+ Get();
+ e = new LiteralExpr(t, true);
+ break;
+ }
+ case 103: {
+ Get();
+ e = new LiteralExpr(t);
+ break;
+ }
+ case 2: {
+ Nat(out n);
+ e = new LiteralExpr(t, n);
+ break;
+ }
+ case 104: {
+ Get();
+ e = new ThisExpr(t);
+ break;
+ }
+ case 105: {
+ Get();
+ x = t;
+ Expect(26);
+ Expression(out e);
+ Expect(28);
+ e = new FreshExpr(x, e);
+ break;
+ }
+ case 106: {
+ Get();
+ x = t;
+ Expect(26);
+ Expression(out e);
+ Expect(28);
+ e = new OldExpr(x, e);
+ break;
+ }
+ case 22: {
+ Get();
+ x = t;
+ Expression(out e);
+ e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
+ Expect(22);
+ break;
+ }
+ case 26: {
+ Get();
+ x = t;
+ Expression(out e);
+ e = new ParensExpression(x, e);
+ Expect(28);
+ break;
+ }
+ default: SynErr(204); break;
+ }
+ }
+
+ void Nat(out BigInteger n) {
+ Expect(2);
+ try {
+ n = BigInteger.Parse(t.val);
+ } catch (System.FormatException) {
+ SemErr("incorrectly formatted number");
+ n = BigInteger.Zero;
+ }
+
+ }
+
+ void MapLiteralExpressions(out List<ExpressionPair> elements) {
+ Expression/*!*/ d, r;
+ elements = new List<ExpressionPair/*!*/>();
+ Expression(out d);
+ Expect(60);
+ Expression(out r);
+ elements.Add(new ExpressionPair(d,r));
+ while (la.kind == 24) {
+ Get();
+ Expression(out d);
+ Expect(60);
+ Expression(out r);
+ elements.Add(new ExpressionPair(d,r));
+ }
+ }
+
+ void QSep() {
+ if (la.kind == 113) {
+ Get();
+ } else if (la.kind == 114) {
+ Get();
+ } else SynErr(205);
+ }
+
+ void MatchExpression(out Expression/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
+ List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
+
+ Expect(74);
+ x = t;
+ Expression(out e);
+ while (la.kind == 70) {
+ CaseExpression(out c);
+ cases.Add(c);
+ }
+ e = new MatchExpr(x, e, cases);
+ }
+
+ void QuantifierGuts(out Expression/*!*/ q) {
+ Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
+ bool univ = false;
+ List<BoundVar/*!*/> bvars;
+ Attributes attrs;
+ Expression range;
+ Expression/*!*/ body;
+
+ if (la.kind == 109 || la.kind == 110) {
+ Forall();
+ x = t; univ = true;
+ } else if (la.kind == 111 || la.kind == 112) {
+ Exists();
+ x = t;
+ } else SynErr(206);
+ QuantifierDomain(out bvars, out attrs, out range);
+ QSep();
+ Expression(out body);
+ if (univ) {
+ q = new ForallExpr(x, bvars, range, body, attrs);
+ } else {
+ q = new ExistsExpr(x, bvars, range, body, attrs);
+ }
+
+ }
+
+ void ComprehensionExpr(out Expression/*!*/ q) {
+ Contract.Ensures(Contract.ValueAtReturn(out q) != null);
+ IToken/*!*/ x = Token.NoToken;
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ Expression/*!*/ range;
+ Expression body = null;
+
+ Expect(47);
+ x = t;
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ while (la.kind == 24) {
+ Get();
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ }
+ Expect(22);
+ Expression(out range);
+ if (la.kind == 113 || la.kind == 114) {
+ QSep();
+ Expression(out body);
+ }
+ if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
+ q = new SetComprehension(x, bvars, range, body);
+
+ }
+
+ void LetExpr(out Expression e) {
+ IToken/*!*/ x;
+ e = dummyExpr;
+ BoundVar d;
+ List<BoundVar> letVars; List<Expression> letRHSs;
+
+ Expect(23);
+ x = t;
+ letVars = new List<BoundVar>();
+ letRHSs = new List<Expression>();
+ IdentTypeOptional(out d);
+ letVars.Add(d);
+ while (la.kind == 24) {
+ Get();
+ IdentTypeOptional(out d);
+ letVars.Add(d);
+ }
+ Expect(60);
+ Expression(out e);
+ letRHSs.Add(e);
+ while (la.kind == 24) {
+ Get();
+ Expression(out e);
+ letRHSs.Add(e);
+ }
+ Expect(14);
+ Expression(out e);
+ e = new LetExpr(x, letVars, letRHSs, e);
+ }
+
+ void NamedExpr(out Expression e) {
+ IToken/*!*/ x, d;
+ e = dummyExpr;
+ Expression expr;
+
+ Expect(57);
+ x = t;
+ NoUSIdent(out d);
+ Expect(5);
+ Expression(out e);
+ expr = e;
+ e = new NamedExpr(x, d.val, expr);
+ }
+
+ void CaseExpression(out MatchCaseExpr/*!*/ c) {
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
+ List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
+ Expression/*!*/ body;
+
+ Expect(70);
+ x = t;
+ Ident(out id);
+ if (la.kind == 26) {
+ Get();
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
+ while (la.kind == 24) {
+ Get();
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
+ }
+ Expect(28);
+ }
+ Expect(71);
+ Expression(out body);
+ c = new MatchCaseExpr(x, id.val, arguments, body);
+ }
+
+ void Forall() {
+ if (la.kind == 109) {
+ Get();
+ } else if (la.kind == 110) {
+ Get();
+ } else SynErr(207);
+ }
+
+ void Exists() {
+ if (la.kind == 111) {
+ Get();
+ } else if (la.kind == 112) {
+ Get();
+ } else SynErr(208);
+ }
+
+ void AttributeBody(ref Attributes attrs) {
+ string aName;
+ List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
+ Attributes.Argument/*!*/ aArg;
+
+ Expect(5);
+ Expect(1);
+ aName = t.val;
+ if (StartOf(26)) {
+ AttributeArg(out aArg);
+ aArgs.Add(aArg);
+ while (la.kind == 24) {
+ Get();
+ AttributeArg(out aArg);
+ aArgs.Add(aArg);
+ }
+ }
+ attrs = new Attributes(aName, aArgs, attrs);
+ }
+
+
+
+ public void Parse() {
+ la = new Token();
+ la.val = "";
+ Get();
+ Dafny();
+ Expect(0);
+
+ Expect(0);
+ }
+
+ static readonly bool[,]/*!*/ set = {
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, x,x,T,x, x,T,x,T, x,x,T,T, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,T, x,x,x,x, T,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,T,x, x,T,x,x, T,x,T,T, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, T,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, x,T,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, T,x,x,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,T,x, T,x,x,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,T,x, x,T,T,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
+
+ };
+} // end Parser
+
+
+public class Errors {
+ public int count = 0; // number of errors detected
+ public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
+ public void SynErr(string filename, int line, int col, int n) {
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+
+ public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ count++;
+ }
+
+ string GetSyntaxErrorString(int n) {
+ string s;
+ switch (n) {
+ case 0: s = "EOF expected"; break;
+ case 1: s = "ident expected"; break;
+ case 2: s = "digits expected"; break;
+ case 3: s = "arrayToken expected"; break;
+ case 4: s = "string expected"; break;
+ case 5: s = "colon expected"; break;
+ case 6: s = "lbrace expected"; break;
+ case 7: s = "rbrace expected"; break;
+ case 8: s = "\"ghost\" expected"; break;
+ case 9: s = "\"module\" expected"; break;
+ case 10: s = "\"refines\" expected"; break;
+ case 11: s = "\"import\" expected"; break;
+ case 12: s = "\"opened\" expected"; break;
+ case 13: s = "\"=\" expected"; break;
+ case 14: s = "\";\" expected"; break;
+ case 15: s = "\"as\" expected"; break;
+ case 16: s = "\"default\" expected"; break;
+ case 17: s = "\".\" expected"; break;
+ case 18: s = "\"class\" expected"; break;
+ case 19: s = "\"static\" expected"; break;
+ case 20: s = "\"datatype\" expected"; break;
+ case 21: s = "\"codatatype\" expected"; break;
+ case 22: s = "\"|\" expected"; break;
+ case 23: s = "\"var\" expected"; break;
+ case 24: s = "\",\" expected"; break;
+ case 25: s = "\"type\" expected"; break;
+ case 26: s = "\"(\" expected"; break;
+ case 27: s = "\"==\" expected"; break;
+ case 28: s = "\")\" expected"; break;
+ case 29: s = "\"iterator\" expected"; break;
+ case 30: s = "\"yields\" expected"; break;
+ case 31: s = "\"...\" expected"; break;
+ case 32: s = "\"<\" expected"; break;
+ case 33: s = "\">\" expected"; break;
+ case 34: s = "\"method\" expected"; break;
+ case 35: s = "\"constructor\" expected"; break;
+ case 36: s = "\"returns\" expected"; break;
+ case 37: s = "\"modifies\" expected"; break;
+ case 38: s = "\"free\" expected"; break;
+ case 39: s = "\"requires\" expected"; break;
+ case 40: s = "\"ensures\" expected"; break;
+ case 41: s = "\"decreases\" expected"; break;
+ case 42: s = "\"reads\" expected"; break;
+ case 43: s = "\"yield\" expected"; break;
+ case 44: s = "\"bool\" expected"; break;
+ case 45: s = "\"nat\" expected"; break;
+ case 46: s = "\"int\" expected"; break;
+ case 47: s = "\"set\" expected"; break;
+ case 48: s = "\"multiset\" expected"; break;
+ case 49: s = "\"seq\" expected"; break;
+ case 50: s = "\"map\" expected"; break;
+ case 51: s = "\"object\" expected"; break;
+ case 52: s = "\"function\" expected"; break;
+ case 53: s = "\"predicate\" expected"; break;
+ case 54: s = "\"copredicate\" expected"; break;
+ case 55: s = "\"*\" expected"; break;
+ case 56: s = "\"`\" expected"; break;
+ case 57: s = "\"label\" expected"; break;
+ case 58: s = "\"break\" expected"; break;
+ case 59: s = "\"where\" expected"; break;
+ case 60: s = "\":=\" expected"; break;
+ case 61: s = "\"return\" expected"; break;
+ case 62: s = "\":|\" expected"; break;
+ case 63: s = "\"assume\" expected"; break;
+ case 64: s = "\"new\" expected"; break;
+ case 65: s = "\"[\" expected"; break;
+ case 66: s = "\"]\" expected"; break;
+ case 67: s = "\"choose\" expected"; break;
+ case 68: s = "\"if\" expected"; break;
+ case 69: s = "\"else\" expected"; break;
+ case 70: s = "\"case\" expected"; break;
+ case 71: s = "\"=>\" expected"; break;
+ case 72: s = "\"while\" expected"; break;
+ case 73: s = "\"invariant\" expected"; break;
+ case 74: s = "\"match\" expected"; break;
+ case 75: s = "\"assert\" expected"; break;
+ case 76: s = "\"print\" expected"; break;
+ case 77: s = "\"parallel\" expected"; break;
+ case 78: s = "\"calc\" expected"; break;
+ case 79: s = "\"<=\" expected"; break;
+ case 80: s = "\">=\" expected"; break;
+ case 81: s = "\"!=\" expected"; break;
+ case 82: s = "\"\\u2260\" expected"; break;
+ case 83: s = "\"\\u2264\" expected"; break;
+ case 84: s = "\"\\u2265\" expected"; break;
+ case 85: s = "\"<==>\" expected"; break;
+ case 86: s = "\"\\u21d4\" expected"; break;
+ case 87: s = "\"==>\" expected"; break;
+ case 88: s = "\"\\u21d2\" expected"; break;
+ case 89: s = "\"&&\" expected"; break;
+ case 90: s = "\"\\u2227\" expected"; break;
+ case 91: s = "\"||\" expected"; break;
+ case 92: s = "\"\\u2228\" expected"; break;
+ case 93: s = "\"!!\" expected"; break;
+ case 94: s = "\"in\" expected"; break;
+ case 95: s = "\"!\" expected"; break;
+ case 96: s = "\"+\" expected"; break;
+ case 97: s = "\"-\" expected"; break;
+ case 98: s = "\"/\" expected"; break;
+ case 99: s = "\"%\" expected"; break;
+ case 100: s = "\"\\u00ac\" expected"; break;
+ case 101: s = "\"false\" expected"; break;
+ case 102: s = "\"true\" expected"; break;
+ case 103: s = "\"null\" expected"; break;
+ case 104: s = "\"this\" expected"; break;
+ case 105: s = "\"fresh\" expected"; break;
+ case 106: s = "\"old\" expected"; break;
+ case 107: s = "\"then\" expected"; break;
+ case 108: s = "\"..\" expected"; break;
+ case 109: s = "\"forall\" expected"; break;
+ case 110: s = "\"\\u2200\" expected"; break;
+ case 111: s = "\"exists\" expected"; break;
+ case 112: s = "\"\\u2203\" expected"; break;
+ case 113: s = "\"::\" expected"; break;
+ case 114: s = "\"\\u2022\" expected"; break;
+ case 115: s = "??? expected"; break;
+ case 116: s = "invalid Dafny"; break;
+ case 117: s = "invalid SubModuleDecl"; break;
+ case 118: s = "invalid SubModuleDecl"; break;
+ case 119: s = "invalid SubModuleDecl"; break;
+ case 120: s = "this symbol not expected in ClassDecl"; break;
+ case 121: s = "this symbol not expected in DatatypeDecl"; break;
+ case 122: s = "invalid DatatypeDecl"; break;
+ case 123: s = "this symbol not expected in DatatypeDecl"; break;
+ case 124: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 125: s = "this symbol not expected in IteratorDecl"; break;
+ case 126: s = "invalid IteratorDecl"; break;
+ case 127: s = "invalid ClassMemberDecl"; break;
+ case 128: s = "this symbol not expected in FieldDecl"; break;
+ case 129: s = "this symbol not expected in FieldDecl"; break;
+ case 130: s = "invalid FunctionDecl"; break;
+ case 131: s = "invalid FunctionDecl"; break;
+ case 132: s = "invalid FunctionDecl"; break;
+ case 133: s = "invalid FunctionDecl"; break;
+ case 134: s = "this symbol not expected in MethodDecl"; break;
+ case 135: s = "invalid MethodDecl"; break;
+ case 136: s = "invalid MethodDecl"; break;
+ case 137: s = "invalid TypeAndToken"; break;
+ case 138: s = "this symbol not expected in IteratorSpec"; break;
+ case 139: s = "this symbol not expected in IteratorSpec"; break;
+ case 140: s = "this symbol not expected in IteratorSpec"; break;
+ case 141: s = "this symbol not expected in IteratorSpec"; break;
+ case 142: s = "this symbol not expected in IteratorSpec"; break;
+ case 143: s = "invalid IteratorSpec"; break;
+ case 144: s = "this symbol not expected in IteratorSpec"; break;
+ case 145: s = "invalid IteratorSpec"; break;
+ case 146: s = "this symbol not expected in MethodSpec"; break;
+ case 147: s = "this symbol not expected in MethodSpec"; break;
+ case 148: s = "this symbol not expected in MethodSpec"; break;
+ case 149: s = "this symbol not expected in MethodSpec"; break;
+ case 150: s = "invalid MethodSpec"; break;
+ case 151: s = "this symbol not expected in MethodSpec"; break;
+ case 152: s = "invalid MethodSpec"; break;
+ case 153: s = "invalid FrameExpression"; break;
+ case 154: s = "invalid ReferenceType"; break;
+ case 155: s = "this symbol not expected in FunctionSpec"; break;
+ case 156: s = "this symbol not expected in FunctionSpec"; break;
+ case 157: s = "this symbol not expected in FunctionSpec"; break;
+ case 158: s = "this symbol not expected in FunctionSpec"; break;
+ case 159: s = "this symbol not expected in FunctionSpec"; break;
+ case 160: s = "invalid FunctionSpec"; break;
+ case 161: s = "invalid PossiblyWildFrameExpression"; break;
+ case 162: s = "invalid PossiblyWildExpression"; break;
+ case 163: s = "this symbol not expected in OneStmt"; break;
+ case 164: s = "invalid OneStmt"; break;
+ case 165: s = "this symbol not expected in OneStmt"; break;
+ case 166: s = "invalid OneStmt"; break;
+ case 167: s = "invalid AssertStmt"; break;
+ case 168: s = "invalid AssumeStmt"; break;
+ case 169: s = "invalid UpdateStmt"; break;
+ case 170: s = "invalid UpdateStmt"; break;
+ case 171: s = "invalid IfStmt"; break;
+ case 172: s = "invalid IfStmt"; break;
+ case 173: s = "invalid WhileStmt"; break;
+ case 174: s = "invalid WhileStmt"; break;
+ case 175: s = "invalid CalcStmt"; break;
+ case 176: s = "invalid ReturnStmt"; break;
+ case 177: s = "invalid Rhs"; break;
+ case 178: s = "invalid Lhs"; break;
+ case 179: s = "invalid Guard"; break;
+ case 180: s = "this symbol not expected in LoopSpec"; break;
+ case 181: s = "this symbol not expected in LoopSpec"; break;
+ case 182: s = "this symbol not expected in LoopSpec"; break;
+ case 183: s = "this symbol not expected in LoopSpec"; break;
+ case 184: s = "this symbol not expected in LoopSpec"; break;
+ case 185: s = "this symbol not expected in Invariant"; break;
+ case 186: s = "invalid AttributeArg"; break;
+ case 187: s = "invalid CalcOp"; break;
+ case 188: s = "invalid EquivOp"; break;
+ case 189: s = "invalid ImpliesOp"; break;
+ case 190: s = "invalid AndOp"; break;
+ case 191: s = "invalid OrOp"; break;
+ case 192: s = "invalid RelOp"; break;
+ case 193: s = "invalid AddOp"; break;
+ case 194: s = "invalid UnaryExpression"; break;
+ case 195: s = "invalid UnaryExpression"; break;
+ case 196: s = "invalid MulOp"; break;
+ case 197: s = "invalid NegOp"; break;
+ case 198: s = "invalid EndlessExpression"; break;
+ case 199: s = "invalid Suffix"; break;
+ case 200: s = "invalid Suffix"; break;
+ case 201: s = "invalid Suffix"; break;
+ case 202: s = "invalid DisplayExpr"; break;
+ case 203: s = "invalid MultiSetExpr"; break;
+ case 204: s = "invalid ConstAtomExpression"; break;
+ case 205: s = "invalid QSep"; break;
+ case 206: s = "invalid QuantifierGuts"; break;
+ case 207: s = "invalid Forall"; break;
+ case 208: s = "invalid Exists"; break;
+
+ default: s = "error " + n; break;
+ }
+ return s;
+ }
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ SemErr(tok.filename, tok.line, tok.col, msg);
+ }
+
+ public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ count++;
+ }
+
+ public virtual void Warning(string filename, int line, int col, string msg) {
+ Contract.Requires(msg != null);
+ errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);
+ }
+} // Errors
+
+
+public class FatalError: Exception {
+ public FatalError(string m): base(m) {}
+}
+
+
+}
\ No newline at end of file |