From 2541e9de002267359897bf967755172fcc726512 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 22 Oct 2012 02:18:51 -0700 Subject: renamed "abstract module" to "module facade" renamed "ghost module" to "abstract module", adding a keyword "abstract" --- Source/Dafny/Cloner.cs | 8 +- Source/Dafny/Compiler.cs | 4 +- Source/Dafny/Dafny.atg | 57 +- Source/Dafny/DafnyAst.cs | 12 +- Source/Dafny/Parser.cs | 1271 ++++++++++----------- Source/Dafny/Printer.cs | 11 +- Source/Dafny/RefinementTransformer.cs | 12 +- Source/Dafny/Resolver.cs | 32 +- Source/Dafny/Scanner.cs | 215 ++-- Source/Dafny/Translator.cs | 2 +- Source/DafnyExtension/TokenTagger.cs | 1 + Test/dafny0/Compilation.dfy | 4 +- Test/dafny0/RefinementModificationChecking.dfy | 4 +- Test/dafny1/SchorrWaite-stages.dfy | 6 +- Test/dafny2/StoreAndRetrieve.dfy | 2 +- Test/dafny3/CachedContainer.dfy | 6 +- Util/Emacs/dafny-mode.el | 2 +- Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 +- Util/latex/dafny.sty | 2 +- Util/vim/syntax/dafny.vim | 2 +- 20 files changed, 813 insertions(+), 843 deletions(-) diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index ceb3748c..00389ad0 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -14,7 +14,7 @@ namespace Microsoft.Dafny if (m is DefaultModuleDecl) { nw = new DefaultModuleDecl(); } else { - nw = new ModuleDefinition(Tok(m.tok), name, m.IsGhost, m.IsAbstract, m.RefinementBaseName, CloneAttributes(m.Attributes), true); + nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.RefinementBaseName, CloneAttributes(m.Attributes), true); } foreach (var d in m.TopLevelDecls) { nw.TopLevelDecls.Add(CloneDeclaration(d, nw)); @@ -85,9 +85,9 @@ namespace Microsoft.Dafny alias.ModuleReference = a.ModuleReference; alias.Signature = a.Signature; return alias; - } else if (d is AbstractModuleDecl) { - var a = (AbstractModuleDecl)d; - var abs = new AbstractModuleDecl(a.Path, a.tok, m, a.CompilePath, a.Opened); + } else if (d is ModuleFacadeDecl) { + var a = (ModuleFacadeDecl)d; + var abs = new ModuleFacadeDecl(a.Path, a.tok, m, a.CompilePath, a.Opened); abs.Signature = a.Signature; abs.OriginalSignature = a.OriginalSignature; return abs; diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index dd50c4eb..4b59682f 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -68,8 +68,8 @@ namespace Microsoft.Dafny { CompileBuiltIns(program.BuiltIns); foreach (ModuleDefinition m in program.CompileModules) { - if (m.IsGhost) { - // the purpose of a ghost module is to skip compilation + if (m.IsAbstract) { + // the purpose of an abstract module is to skip compilation continue; } int indent = 0; diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 774d800a..d7bf11c4 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -146,23 +146,13 @@ Dafny DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef; // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl) Contract.Assert(defaultModule != null); - bool isGhost; .) - { (. isGhost = false; .) - [ "ghost" (. isGhost = true; .) ] - - ( SubModuleDecl - (. defaultModule.TopLevelDecls.Add(submodule); .) - | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .) - ClassDecl (. defaultModule.TopLevelDecls.Add(c); .) - | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .) - DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .) - | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .) - ArbitraryTypeDecl (. defaultModule.TopLevelDecls.Add(at); .) - | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .) - IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) - | ClassMemberDecl - ) + { SubModuleDecl (. defaultModule.TopLevelDecls.Add(submodule); .) + | ClassDecl (. defaultModule.TopLevelDecls.Add(c); .) + | DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .) + | ArbitraryTypeDecl (. defaultModule.TopLevelDecls.Add(at); .) + | IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) + | ClassMemberDecl } (. // find the default class in the default module, then append membersDefaultClass to its member list DefaultClassDecl defaultClass = null; @@ -179,36 +169,30 @@ Dafny } .) EOF . -SubModuleDecl +SubModuleDecl = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter; Attributes attrs = null; IToken/*!*/ id; List namedModuleDefaultClassMembers = new List();; List idRefined = null, idPath = null, idAssignment = null; - bool isGhost = false; ModuleDefinition module; ModuleDecl sm; submodule = null; // appease compiler + bool isAbstract = false; bool opened = false; .) - ( "module" + ( [ "abstract" (. isAbstract = true; .) ] + "module" { Attribute } NoUSIdent - [ "refines" QualifiedName ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); .) + [ "refines" QualifiedName ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, attrs, false); .) "{" (. module.BodyStartTok = t; .) - { (. isGhost = false; .) - [ "ghost" (. isGhost = true; .) ] - ( SubModuleDecl (. module.TopLevelDecls.Add(sm); .) - | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .) - ClassDecl (. module.TopLevelDecls.Add(c); .) - | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .) - DatatypeDecl (. module.TopLevelDecls.Add(dt); .) - | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .) - ArbitraryTypeDecl (. module.TopLevelDecls.Add(at); .) - | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .) - IteratorDecl (. module.TopLevelDecls.Add(iter); .) - | ClassMemberDecl - ) + { SubModuleDecl (. module.TopLevelDecls.Add(sm); .) + | ClassDecl (. module.TopLevelDecls.Add(c); .) + | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) + | ArbitraryTypeDecl (. module.TopLevelDecls.Add(at); .) + | IteratorDecl (. module.TopLevelDecls.Add(iter); .) + | ClassMemberDecl } "}" (. module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); @@ -220,7 +204,7 @@ SubModuleDecl(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened); .) | "as" QualifiedName ["default" QualifiedName ] ";" - (.submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened); .) + (.submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .) ) ) ) @@ -248,7 +232,7 @@ ClassDecl NoUSIdent [ GenericParameters ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); @@ -256,12 +240,11 @@ ClassDecl c.BodyEndTok = t; .) . -ClassMemberDecl<.List/*!*/ mm, bool isAlreadyGhost, bool allowConstructors.> +ClassMemberDecl<.List/*!*/ mm, bool allowConstructors.> = (. Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; MemberModifiers mmod = new MemberModifiers(); - mmod.IsGhost = isAlreadyGhost; .) { "ghost" (. mmod.IsGhost = true; .) | "static" (. mmod.IsStatic = true; .) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0f06ec55..45367e90 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -845,7 +845,7 @@ namespace Microsoft.Dafny { } } // Represents "module name as path [ = compilePath];", where name is a identifier and path is a possibly qualified name. - public class AbstractModuleDecl : ModuleDecl + public class ModuleFacadeDecl : ModuleDecl { public ModuleDecl Root; public readonly List Path; @@ -853,7 +853,7 @@ namespace Microsoft.Dafny { public readonly List CompilePath; public ModuleSignature OriginalSignature; - public AbstractModuleDecl(List path, IToken name, ModuleDefinition parent, List compilePath, bool opened) + public ModuleFacadeDecl(List path, IToken name, ModuleDefinition parent, List compilePath, bool opened) : base(name, name.val, parent, opened) { Path = path; Root = null; @@ -894,8 +894,8 @@ namespace Microsoft.Dafny { public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that public readonly Graph CallGraph = new Graph(); // filled in during resolution public int Height; // height in the topological sorting of modules; filled in during resolution - public readonly bool IsGhost; - public readonly bool IsAbstract; // True iff this module represents an abstract interface + public readonly bool IsAbstract; + public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. [ContractInvariantMethod] void ObjectInvariant() { @@ -903,13 +903,13 @@ namespace Microsoft.Dafny { Contract.Invariant(CallGraph != null); } - public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List refinementBase, Attributes attributes, bool isBuiltinName) + public ModuleDefinition(IToken tok, string name, bool isAbstract, bool isFacade, List refinementBase, Attributes attributes, bool isBuiltinName) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); RefinementBaseName = refinementBase; - IsGhost = isGhost; IsAbstract = isAbstract; + IsFacade = isFacade; RefinementBaseRoot = null; RefinementBase = null; IsBuiltinName = isBuiltinName; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 8982750d..b4d64827 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -21,7 +21,7 @@ public class Parser { public const int _colon = 5; public const int _lbrace = 6; public const int _rbrace = 7; - public const int maxT = 116; + public const int maxT = 117; const bool T = true; const bool x = false; @@ -196,49 +196,38 @@ bool IsAttribute() { 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); + case 8: case 9: case 11: { + SubModuleDecl(defaultModule, 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'"); } + case 21: case 22: { 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'"); } + case 26: { 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'"); } + case 30: { IteratorDecl(defaultModule, out iter); defaultModule.TopLevelDecls.Add(iter); break; } - case 8: case 19: case 23: case 34: case 35: case 36: case 53: case 54: case 55: { - ClassMemberDecl(membersDefaultClass, isGhost, false); + case 19: case 20: case 24: case 35: case 36: case 37: case 54: case 55: case 56: { + ClassMemberDecl(membersDefaultClass, false); break; } - default: SynErr(117); break; } } DefaultClassDecl defaultClass = null; @@ -256,19 +245,23 @@ bool IsAttribute() { Expect(0); } - void SubModuleDecl(ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule) { + void SubModuleDecl(ModuleDefinition parent, out ModuleDecl submodule) { ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter; Attributes attrs = null; IToken/*!*/ id; List namedModuleDefaultClassMembers = new List();; List idRefined = null, idPath = null, idAssignment = null; - bool isGhost = false; ModuleDefinition module; ModuleDecl sm; submodule = null; // appease compiler + bool isAbstract = false; bool opened = false; - if (la.kind == 9) { - Get(); + if (la.kind == 8 || la.kind == 9) { + if (la.kind == 8) { + Get(); + isAbstract = true; + } + Expect(9); while (la.kind == 6) { Attribute(ref attrs); } @@ -277,50 +270,40 @@ bool IsAttribute() { Get(); QualifiedName(out idRefined); } - module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); + module = new ModuleDefinition(id, id.val, isAbstract, 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); + case 8: case 9: case 11: { + SubModuleDecl(module, 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'"); } + case 21: case 22: { 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'"); } + case 26: { 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'"); } + case 30: { IteratorDecl(module, out iter); module.TopLevelDecls.Add(iter); break; } - case 8: case 19: case 23: case 34: case 35: case 36: case 53: case 54: case 55: { - ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false); + case 19: case 20: case 24: case 35: case 36: case 37: case 54: case 55: case 56: { + ClassMemberDecl(namedModuleDefaultClassMembers, false); break; } - default: SynErr(118); break; } } Expect(7); @@ -350,9 +333,9 @@ bool IsAttribute() { QualifiedName(out idAssignment); } Expect(14); - submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened); - } else SynErr(119); - } else SynErr(120); + submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); + } else SynErr(118); + } else SynErr(119); } void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { @@ -364,19 +347,19 @@ bool IsAttribute() { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 18)) {SynErr(121); Get();} + 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) { + if (la.kind == 33) { GenericParameters(typeArgs); } Expect(6); bodyStart = t; while (StartOf(2)) { - ClassMemberDecl(members, false, true); + ClassMemberDecl(members, true); } Expect(7); c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); @@ -395,28 +378,28 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; - while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(122); Get();} - if (la.kind == 20) { + while (!(la.kind == 0 || la.kind == 21 || la.kind == 22)) {SynErr(121); Get();} + if (la.kind == 21) { Get(); - } else if (la.kind == 21) { + } else if (la.kind == 22) { Get(); co = true; - } else SynErr(123); + } else SynErr(122); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 32) { + if (la.kind == 33) { GenericParameters(typeArgs); } Expect(13); bodyStart = t; DatatypeMemberDecl(ctors); - while (la.kind == 22) { + while (la.kind == 23) { Get(); DatatypeMemberDecl(ctors); } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(124); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();} Expect(14); if (co) { dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); @@ -433,19 +416,19 @@ bool IsAttribute() { Attributes attrs = null; var eqSupport = TypeParameter.EqualitySupportValue.Unspecified; - Expect(25); + Expect(26); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 26) { + if (la.kind == 27) { Get(); - Expect(27); Expect(28); + Expect(29); eqSupport = TypeParameter.EqualitySupportValue.Required; } at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(125); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(124); Get();} Expect(14); } @@ -473,25 +456,25 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 29)) {SynErr(126); Get();} - Expect(29); + while (!(la.kind == 0 || la.kind == 30)) {SynErr(125); Get();} + Expect(30); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 26 || la.kind == 32) { - if (la.kind == 32) { + if (la.kind == 27 || la.kind == 33) { + if (la.kind == 33) { GenericParameters(typeArgs); } Formals(true, true, ins, out openParen); - if (la.kind == 30) { + if (la.kind == 31) { Get(); Formals(false, true, outs, out openParen); } - } else if (la.kind == 31) { + } else if (la.kind == 32) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(127); + } else SynErr(126); while (StartOf(3)) { IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); } @@ -509,15 +492,14 @@ bool IsAttribute() { } - void ClassMemberDecl(List/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) { + void ClassMemberDecl(List/*!*/ mm, 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) { + while (la.kind == 19 || la.kind == 20) { + if (la.kind == 19) { Get(); mmod.IsGhost = true; } else { @@ -525,15 +507,15 @@ bool IsAttribute() { mmod.IsStatic = true; } } - if (la.kind == 23) { + if (la.kind == 24) { FieldDecl(mmod, mm); - } else if (la.kind == 53 || la.kind == 54 || la.kind == 55) { + } else if (la.kind == 54 || la.kind == 55 || la.kind == 56) { FunctionDecl(mmod, out f); mm.Add(f); - } else if (la.kind == 34 || la.kind == 35 || la.kind == 36) { + } else if (la.kind == 35 || la.kind == 36 || la.kind == 37) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(128); + } else SynErr(127); } void Attribute(ref Attributes attrs) { @@ -574,29 +556,29 @@ bool IsAttribute() { IToken/*!*/ id; TypeParameter.EqualitySupportValue eqSupport; - Expect(32); + Expect(33); NoUSIdent(out id); eqSupport = TypeParameter.EqualitySupportValue.Unspecified; - if (la.kind == 26) { + if (la.kind == 27) { Get(); - Expect(27); Expect(28); + Expect(29); eqSupport = TypeParameter.EqualitySupportValue.Required; } typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); - while (la.kind == 24) { + while (la.kind == 25) { Get(); NoUSIdent(out id); eqSupport = TypeParameter.EqualitySupportValue.Unspecified; - if (la.kind == 26) { + if (la.kind == 27) { Get(); - Expect(27); Expect(28); + Expect(29); eqSupport = TypeParameter.EqualitySupportValue.Required; } typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); } - Expect(33); + Expect(34); } void FieldDecl(MemberModifiers mmod, List/*!*/ mm) { @@ -604,8 +586,8 @@ bool IsAttribute() { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 23)) {SynErr(129); Get();} - Expect(23); + while (!(la.kind == 0 || la.kind == 24)) {SynErr(128); Get();} + Expect(24); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } while (la.kind == 6) { @@ -613,12 +595,12 @@ bool IsAttribute() { } IdentType(out id, out ty, false); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); - while (la.kind == 24) { + while (la.kind == 25) { 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(130); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(129); Get();} Expect(14); } @@ -641,9 +623,9 @@ bool IsAttribute() { IToken bodyEnd = Token.NoToken; bool signatureOmitted = false; - if (la.kind == 53) { + if (la.kind == 54) { Get(); - if (la.kind == 34) { + if (la.kind == 35) { Get(); isFunctionMethod = true; } @@ -653,22 +635,22 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 26 || la.kind == 32) { - if (la.kind == 32) { + if (la.kind == 27 || la.kind == 33) { + if (la.kind == 33) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals, out openParen); Expect(5); Type(out returnType); - } else if (la.kind == 31) { + } else if (la.kind == 32) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(131); - } else if (la.kind == 54) { + } else SynErr(130); + } else if (la.kind == 55) { Get(); isPredicate = true; - if (la.kind == 34) { + if (la.kind == 35) { Get(); isFunctionMethod = true; } @@ -679,22 +661,22 @@ bool IsAttribute() { } NoUSIdent(out id); if (StartOf(4)) { - if (la.kind == 32) { + if (la.kind == 33) { GenericParameters(typeArgs); } - if (la.kind == 26) { + if (la.kind == 27) { 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) { + } else if (la.kind == 32) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(132); - } else if (la.kind == 55) { + } else SynErr(131); + } else if (la.kind == 56) { Get(); isCoPredicate = true; if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); } @@ -704,22 +686,22 @@ bool IsAttribute() { } NoUSIdent(out id); if (StartOf(4)) { - if (la.kind == 32) { + if (la.kind == 33) { GenericParameters(typeArgs); } - if (la.kind == 26) { + if (la.kind == 27) { 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) { + } else if (la.kind == 32) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(133); - } else SynErr(134); + } else SynErr(132); + } else SynErr(133); decreases = isCoPredicate ? null : new List(); while (StartOf(5)) { FunctionSpec(reqs, reads, ens, decreases); @@ -764,13 +746,13 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(StartOf(6))) {SynErr(135); Get();} - if (la.kind == 34) { + while (!(StartOf(6))) {SynErr(134); Get();} + if (la.kind == 35) { Get(); - } else if (la.kind == 35) { + } else if (la.kind == 36) { Get(); isCoMethod = true; - } else if (la.kind == 36) { + } else if (la.kind == 37) { Get(); if (allowConstructor) { isConstructor = true; @@ -778,7 +760,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes"); } - } else SynErr(136); + } else SynErr(135); keywordToken = t; if (isConstructor) { if (mmod.IsGhost) { @@ -807,20 +789,20 @@ bool IsAttribute() { } } - if (la.kind == 26 || la.kind == 32) { - if (la.kind == 32) { + if (la.kind == 27 || la.kind == 33) { + if (la.kind == 33) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins, out openParen); - if (la.kind == 37) { + if (la.kind == 38) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs, out openParen); } - } else if (la.kind == 31) { + } else if (la.kind == 32) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(137); + } else SynErr(136); while (StartOf(7)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } @@ -852,7 +834,7 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 26) { + if (la.kind == 27) { FormalsOptionalIds(formals); } ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); @@ -860,17 +842,17 @@ bool IsAttribute() { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; - Expect(26); + Expect(27); if (StartOf(8)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); - while (la.kind == 24) { + while (la.kind == 25) { Get(); TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); } } - Expect(28); + Expect(29); } void IdentType(out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId) { @@ -884,7 +866,7 @@ bool IsAttribute() { Contract.Ensures(Contract.ValueAtReturn(out id)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); isGhost = false; - if (la.kind == 8) { + if (la.kind == 19) { Get(); if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } } @@ -939,7 +921,7 @@ bool IsAttribute() { Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); Contract.Ensures(Contract.ValueAtReturn(out identName)!=null); string name = null; isGhost = false; - if (la.kind == 8) { + if (la.kind == 19) { Get(); isGhost = true; } @@ -968,22 +950,22 @@ bool IsAttribute() { List/*!*/ gt; switch (la.kind) { - case 45: { + case 46: { Get(); tok = t; break; } - case 46: { + case 47: { Get(); tok = t; ty = new NatType(); break; } - case 47: { + case 48: { Get(); tok = t; ty = new IntType(); break; } - case 48: { + case 49: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -994,7 +976,7 @@ bool IsAttribute() { break; } - case 49: { + case 50: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -1005,7 +987,7 @@ bool IsAttribute() { break; } - case 50: { + case 51: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -1016,7 +998,7 @@ bool IsAttribute() { break; } - case 51: { + case 52: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -1027,28 +1009,28 @@ bool IsAttribute() { break; } - case 1: case 3: case 52: { + case 1: case 3: case 53: { ReferenceType(out tok, out ty); break; } - default: SynErr(138); break; + default: SynErr(137); break; } } void Formals(bool incoming, bool allowGhostKeyword, List/*!*/ formals, out IToken openParen) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; - Expect(26); + Expect(27); openParen = t; - if (la.kind == 1 || la.kind == 8) { + if (la.kind == 1 || la.kind == 19) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); - while (la.kind == 24) { + while (la.kind == 25) { Get(); GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); } } - Expect(28); + Expect(29); } void IteratorSpec(List/*!*/ reads, List/*!*/ mod, List decreases, @@ -1057,8 +1039,8 @@ List/*!*/ yieldReq, List/*!* ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; - while (!(StartOf(9))) {SynErr(139); Get();} - if (la.kind == 43) { + while (!(StartOf(9))) {SynErr(138); Get();} + if (la.kind == 44) { Get(); while (IsAttribute()) { Attribute(ref readsAttrs); @@ -1066,15 +1048,15 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (StartOf(10)) { FrameExpression(out fe); reads.Add(fe); - while (la.kind == 24) { + while (la.kind == 25) { Get(); FrameExpression(out fe); reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(140); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(139); Get();} Expect(14); - } else if (la.kind == 38) { + } else if (la.kind == 39) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1082,27 +1064,27 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (StartOf(10)) { FrameExpression(out fe); mod.Add(fe); - while (la.kind == 24) { + while (la.kind == 25) { Get(); FrameExpression(out fe); mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(141); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(140); Get();} Expect(14); } else if (StartOf(11)) { - if (la.kind == 39) { + if (la.kind == 40) { Get(); isFree = true; } - if (la.kind == 44) { + if (la.kind == 45) { Get(); isYield = true; } - if (la.kind == 40) { + if (la.kind == 41) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(141); Get();} Expect(14); if (isYield) { yieldReq.Add(new MaybeFreeExpression(e, isFree)); @@ -1110,13 +1092,13 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { req.Add(new MaybeFreeExpression(e, isFree)); } - } else if (la.kind == 41) { + } else if (la.kind == 42) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(143); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();} Expect(14); if (isYield) { yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); @@ -1124,16 +1106,16 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } - } else SynErr(144); - } else if (la.kind == 42) { + } else SynErr(143); + } else if (la.kind == 43) { Get(); while (IsAttribute()) { Attribute(ref decrAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(145); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(144); Get();} Expect(14); - } else SynErr(146); + } else SynErr(145); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -1155,8 +1137,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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(13))) {SynErr(147); Get();} - if (la.kind == 38) { + while (!(StartOf(13))) {SynErr(146); Get();} + if (la.kind == 39) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1164,44 +1146,44 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(10)) { FrameExpression(out fe); mod.Add(fe); - while (la.kind == 24) { + while (la.kind == 25) { Get(); FrameExpression(out fe); mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(148); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(147); Get();} Expect(14); - } else if (la.kind == 39 || la.kind == 40 || la.kind == 41) { - if (la.kind == 39) { + } else if (la.kind == 40 || la.kind == 41 || la.kind == 42) { + if (la.kind == 40) { Get(); isFree = true; } - if (la.kind == 40) { + if (la.kind == 41) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(149); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(148); Get();} Expect(14); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 41) { + } else if (la.kind == 42) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(150); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(149); Get();} Expect(14); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(151); - } else if (la.kind == 42) { + } else SynErr(150); + } else if (la.kind == 43) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(152); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(151); Get();} Expect(14); - } else SynErr(153); + } else SynErr(152); } void FrameExpression(out FrameExpression/*!*/ fe) { @@ -1214,18 +1196,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(14)) { Expression(out e); feTok = e.tok; - if (la.kind == 57) { + if (la.kind == 58) { Get(); Ident(out id); fieldName = id.val; feTok = id; } fe = new FrameExpression(feTok, e, fieldName); - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); Ident(out id); fieldName = id.val; fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); - } else SynErr(154); + } else SynErr(153); } void Expression(out Expression/*!*/ e) { @@ -1241,7 +1223,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases.Add(e); } - while (la.kind == 24) { + while (la.kind == 25) { Get(); PossiblyWildExpression(out e); if (!allowWildcard && e is WildcardExpr) { @@ -1255,15 +1237,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(32); + Expect(33); Type(out ty); gt.Add(ty); - while (la.kind == 24) { + while (la.kind == 25) { Get(); Type(out ty); gt.Add(ty); } - Expect(33); + Expect(34); } void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) { @@ -1272,7 +1254,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List/*!*/ gt; List path; - if (la.kind == 52) { + if (la.kind == 53) { Get(); tok = t; ty = new ObjectType(); } else if (la.kind == 3) { @@ -1297,11 +1279,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); Ident(out tok); } - if (la.kind == 32) { + if (la.kind == 33) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt, path); - } else SynErr(155); + } else SynErr(154); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases) { @@ -1309,33 +1291,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - if (la.kind == 40) { - while (!(la.kind == 0 || la.kind == 40)) {SynErr(156); Get();} + if (la.kind == 41) { + while (!(la.kind == 0 || la.kind == 41)) {SynErr(155); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(157); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(156); Get();} Expect(14); reqs.Add(e); - } else if (la.kind == 43) { + } else if (la.kind == 44) { Get(); if (StartOf(15)) { PossiblyWildFrameExpression(out fe); reads.Add(fe); - while (la.kind == 24) { + while (la.kind == 25) { Get(); PossiblyWildFrameExpression(out fe); reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 14)) {SynErr(158); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(157); Get();} Expect(14); - } else if (la.kind == 41) { + } else if (la.kind == 42) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(159); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(158); Get();} Expect(14); ens.Add(e); - } else if (la.kind == 42) { + } else if (la.kind == 43) { Get(); if (decreases == null) { SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed"); @@ -1343,9 +1325,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 14)) {SynErr(160); Get();} + while (!(la.kind == 0 || la.kind == 14)) {SynErr(159); Get();} Expect(14); - } else SynErr(161); + } else SynErr(160); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -1359,23 +1341,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; - if (la.kind == 56) { + if (la.kind == 57) { Get(); fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(10)) { FrameExpression(out fe); - } else SynErr(162); + } else SynErr(161); } void PossiblyWildExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; - if (la.kind == 56) { + if (la.kind == 57) { Get(); e = new WildcardExpr(t); } else if (StartOf(14)) { Expression(out e); - } else SynErr(163); + } else SynErr(162); } void Stmt(List/*!*/ ss) { @@ -1392,54 +1374,54 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(16))) {SynErr(164); Get();} + while (!(StartOf(16))) {SynErr(163); Get();} switch (la.kind) { case 6: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; } - case 76: { + case 77: { AssertStmt(out s); break; } - case 64: { + case 65: { AssumeStmt(out s); break; } - case 77: { + case 78: { PrintStmt(out s); break; } - case 1: case 2: case 22: case 26: case 102: case 103: case 104: case 105: case 106: case 107: { + case 1: case 2: case 23: case 27: case 103: case 104: case 105: case 106: case 107: case 108: { UpdateStmt(out s); break; } - case 8: case 23: { + case 19: case 24: { VarDeclStatement(out s); break; } - case 69: { + case 70: { IfStmt(out s); break; } - case 73: { + case 74: { WhileStmt(out s); break; } - case 75: { + case 76: { MatchStmt(out s); break; } - case 78: { + case 79: { ParallelStmt(out s); break; } - case 79: { + case 80: { CalcStmt(out s); break; } - case 58: { + case 59: { Get(); x = t; NoUSIdent(out id); @@ -1448,33 +1430,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList