From 85d4456ccf1e1d8c456dffa012d3f3d724f50a4a Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Thu, 2 Jul 2015 15:00:52 -0700 Subject: multiple changes... - fix for requirement inheritance in refinement. - minimimally viable implementation of exclusive refinement feature. --- Source/Dafny/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Source/Dafny/Makefile') diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index 4c01c780..e8c0f5e0 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -4,8 +4,8 @@ # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to # point to whatever directory you install that into. # ############################################################################### -COCO_EXE_DIR = ..\..\..\boogiepartners\CocoRdownload -FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified +COCO_EXE_DIR = ..\..\..\boogie-partners\CocoRdownload +FRAME_DIR = ..\..\..\boogie-partners\CocoR\Modified COCO = $(COCO_EXE_DIR)\Coco.exe # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they -- cgit v1.2.3 From d5eb6e9e4c8e4f71e3bb48e0a40fc412e9a5e65e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 27 Jul 2015 18:59:02 -0700 Subject: Updated parser generation to work with latest update in boogiepartners. Note that Coco.exe is now included in boogiepartners. --- Source/Dafny/Makefile | 2 +- Source/Dafny/Parser.cs | 29 ++++++++++++++--------------- 2 files changed, 15 insertions(+), 16 deletions(-) (limited to 'Source/Dafny/Makefile') diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index e8c0f5e0..68ab7a2d 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -4,7 +4,7 @@ # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to # point to whatever directory you install that into. # ############################################################################### -COCO_EXE_DIR = ..\..\..\boogie-partners\CocoRdownload +COCO_EXE_DIR = ..\..\..\boogie-partners\CocoR\bin FRAME_DIR = ..\..\..\boogie-partners\CocoR\Modified COCO = $(COCO_EXE_DIR)\Coco.exe diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index dae1b95e..b4f45159 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -78,11 +78,11 @@ public class Parser { const bool _x = false; const int minErrDist = 2; - public Scanner/*!*/ scanner; - public Errors/*!*/ errors; + public Scanner scanner; + public Errors errors; - public Token/*!*/ t; // last recognized token - public Token/*!*/ la; // lookahead token + public Token t; // last recognized token + public Token la; // lookahead token int errDist = minErrDist; readonly Expression/*!*/ dummyExpr; @@ -454,10 +454,10 @@ bool IsType(ref IToken pt) { /*--------------------------------------------------------------------------*/ - public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) { + public Parser(Scanner scanner, Errors errors) { this.scanner = scanner; this.errors = errors; - Token/*!*/ tok = new Token(); + Token tok = new Token(); tok.val = ""; this.la = tok; this.t = new Token(); // just to satisfy its non-null constraint @@ -468,13 +468,13 @@ bool IsType(ref IToken pt) { errDist = 0; } - public void SemErr (string/*!*/ msg) { + 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) { + public void SemErr(IToken tok, string msg) { Contract.Requires(tok != null); Contract.Requires(msg != null); errors.SemErr(tok, msg); @@ -4385,10 +4385,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Dafny(); Expect(0); - Expect(0); } - static readonly bool[,]/*!*/ set = { + static readonly bool[,] set = { {_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_T, _x,_x,_T,_T, _T,_x,_x,_T, _T,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_x,_T, _T,_T,_x,_x, _T,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_x,_T, _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,_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,_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,_x, _T,_x,_x,_x, _x,_T,_x,_T, _T,_T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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, _T,_T,_T,_x, _x,_T,_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}, @@ -4428,7 +4427,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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 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 @@ -4436,7 +4435,7 @@ public class Errors { SynErr(filename, line, col, GetSyntaxErrorString(n)); } - public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) { + public virtual void SynErr(string filename, int line, int col, string msg) { Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg); count++; @@ -4693,19 +4692,19 @@ public class Errors { return s; } - public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors + 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) { + public virtual void SemErr(string filename, int line, int col, string msg) { Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg); count++; } - public void Warning(IToken/*!*/ tok, string/*!*/ msg) { // warnings + public void Warning(IToken tok, string msg) { // warnings Contract.Requires(tok != null); Contract.Requires(msg != null); Warning(tok.filename, tok.line, tok.col, msg); -- cgit v1.2.3 From 17405efd598d2a8a2dac304ee9a7f7d9bd30a558 Mon Sep 17 00:00:00 2001 From: "Richard L. Ford" Date: Wed, 27 Jan 2016 14:09:16 -0800 Subject: Implement 'extern' declaration modifier. The 'extern' declaration modifier provides a more convenient way of interfacing Dafny code with C# source files and .Net DLLs. We support an 'extern' keyword on a module, class, function method, or method (cannot extern ghost). We check the CompileNames of all modules to make sure there are no duplicate names. Every Dafny-generated C# class is marked partial, so it can potentially be extended. The extern keyword could be accompanied by an optional string naming the corresponding C# method/class to connect to. If not given the name of the method/class is used. An 'extern' keyword implies an {:axiom} attribute for functions and methods, so their ensures clauses are assumed to be true without proof. In addition to the .dfy files, the user may supply C# files (.cs) and dynamic linked libraries (.dll) on command line. These will be passed onto the C# compiler, the .cs files as sources, and the .dll files as references. As part of this change the grammar was refactored some. New productions are - TopDecls - a list of top-level declarations. - TopDecl - a single top-level declaration - DeclModifiers - a list of declaration modifiers which are either 'abstract', 'ghost', 'static', 'protected', or 'extern'. They can be in any order and we diagnose duplicates. In addition, since they are not all allowed in all contexts, we check and give diagnostics if an DeclModifier appears where it is not allowed. --- Source/Dafny/Compiler.cs | 2 +- Source/Dafny/Dafny.atg | 356 +++++--- Source/Dafny/DafnyAst.cs | 31 +- Source/Dafny/Makefile | 4 +- Source/Dafny/Parser.cs | 1534 ++++++++++++++++++--------------- Source/Dafny/Resolver.cs | 29 + Source/Dafny/Scanner.cs | 169 ++-- Source/DafnyDriver/DafnyDriver.cs | 121 ++- Source/DafnyExtension/DafnyDriver.cs | 6 +- Test/dafny0/Extern.dfy | 27 + Test/dafny0/Extern.dfy.expect | 4 + Test/dafny0/Extern2.cs | 14 + Test/dafny0/ExternHelloLibrary.cs | 15 + Test/dafny0/ExternHelloLibrary.dll | Bin 0 -> 3072 bytes Test/dafny0/ExternNegative.dfy | 26 + Test/dafny0/ExternNegative.dfy.expect | 3 + Test/dafny0/ExternNegative2.dfy | 26 + 17 files changed, 1407 insertions(+), 960 deletions(-) create mode 100644 Test/dafny0/Extern.dfy create mode 100644 Test/dafny0/Extern.dfy.expect create mode 100644 Test/dafny0/Extern2.cs create mode 100644 Test/dafny0/ExternHelloLibrary.cs create mode 100644 Test/dafny0/ExternHelloLibrary.dll create mode 100644 Test/dafny0/ExternNegative.dfy create mode 100644 Test/dafny0/ExternNegative.dfy.expect create mode 100644 Test/dafny0/ExternNegative2.dfy (limited to 'Source/Dafny/Makefile') diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 1a99a8af..f5f95bd2 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -254,7 +254,7 @@ namespace Microsoft.Dafny { else if (d is ClassDecl) { var cl = (ClassDecl)d; Indent(indent, wr); - wr.Write("public class @{0}", cl.CompileName); + wr.Write("public partial class @{0}", cl.CompileName); if (cl.TypeArgs.Count != 0) { wr.Write("<{0}>", TypeParameters(cl.TypeArgs)); } diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 08c22db4..87e75541 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -23,10 +23,113 @@ readonly BuiltIns theBuiltIns; readonly bool theVerifyThisFile; int anonymousIds = 0; -struct MemberModifiers { +/// +/// Holds the modifiers given for a declaration +/// +/// Not all modifiers are applicable to all kinds of declarations. +/// Errors are given when a modify does not apply. +/// We also record the tokens for the specified modifiers so that +/// they can be used in error messages. +/// +struct DeclModifierData { + public bool IsAbstract; + public IToken AbstractToken; public bool IsGhost; + public IToken GhostToken; public bool IsStatic; + public IToken StaticToken; public bool IsProtected; + public IToken ProtectedToken; + public bool IsExtern; + public IToken ExternToken; + public StringLiteralExpr ExternName; + +} + +// Check that token has not been set, then set it. +public void CheckAndSetToken(ref IToken token) +{ + if (token != null) { + SemErr(t, "Duplicate declaration modifier: " + t.val); + } + token = t; +} + +/// +// A flags type used to tell what declaration modifiers are allowed for a declaration. +/// +[Flags] +enum AllowedDeclModifiers { + None = 0, + Abstract = 1, + Ghost = 2, + + // Means ghost not allowed because already implicitly ghost. + AlreadyGhost = 4, + Static = 8, + Protected = 16, + Extern = 32 +}; + +/// +/// Check the declaration modifiers against those that are allowed. +/// +/// The 'allowed' parameter specifies which declaratio modifiers are allowed. +/// The 'declCaption' parameter should be a string describing the kind of declaration. +/// It is used in error messages. +/// Any declaration modifiers that are present but not allowed are cleared. +/// +void CheckDeclModifiers(DeclModifierData dmod, string declCaption, AllowedDeclModifiers allowed) +{ + if (dmod.IsAbstract && ((allowed & AllowedDeclModifiers.Abstract) == 0)) { + SemErr(dmod.AbstractToken, declCaption + " cannot be declared 'abstract'."); + dmod.IsAbstract = false; + } + if (dmod.IsGhost) { + if ((allowed & AllowedDeclModifiers.AlreadyGhost) != 0) { + SemErr(dmod.GhostToken, declCaption + " cannot be declared ghost (they are 'ghost' by default)."); + dmod.IsGhost = false; + } else if ((allowed & AllowedDeclModifiers.Ghost) == 0) { + SemErr(dmod.GhostToken, declCaption + " cannot be declared 'ghost'."); + dmod.IsGhost = false; + } + } + if (dmod.IsStatic && ((allowed & AllowedDeclModifiers.Static) == 0)) { + SemErr(dmod.StaticToken, declCaption + " cannot be declared 'static'."); + dmod.IsStatic = false; + } + if (dmod.IsProtected && ((allowed & AllowedDeclModifiers.Protected) == 0)) { + SemErr(dmod.ProtectedToken, declCaption + " cannot be declared 'protected'."); + dmod.IsProtected = false; + } + if (dmod.IsExtern && ((allowed & AllowedDeclModifiers.Extern) == 0)) { + SemErr(dmod.ExternToken, declCaption + " cannot be declared 'extern'."); + dmod.IsExtern = false; + } +} + +/// +/// Encode an 'extern' declaration modifier as an {:extern name} attribute. +/// +/// We also include an {:axiom} attribute since the specification of an +/// external entity is assumed to hold, but only for methods or functions. +/// +static void EncodeExternAsAttribute(DeclModifierData dmod, ref Attributes attrs, IToken/*!*/ id, bool needAxiom) { + if (dmod.IsExtern) { + StringLiteralExpr name = dmod.ExternName; + if (name == null) { + bool isVerbatimString = false; + name = new StringLiteralExpr(id, id.val, isVerbatimString); + } + var args = new List(); + args.Add(name); + attrs = new Attributes("extern", args, attrs); + + // Also 'extern' implies 'axiom' for methods or functions. + if (needAxiom) { + attrs = new Attributes("axiom", new List(), attrs); + } + } } /// @@ -516,13 +619,10 @@ IGNORE cr + lf + tab /*------------------------------------------------------------------------*/ PRODUCTIONS Dafny -= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; - List membersDefaultClass = new List(); - ModuleDecl submodule; += (. List membersDefaultClass = new List(); // 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) - TraitDecl/*!*/ trait; Contract.Assert(defaultModule != null); .) { "include" stringToken (. { @@ -540,15 +640,7 @@ Dafny } .) } - { SubModuleDecl (. defaultModule.TopLevelDecls.Add(submodule); .) - | ClassDecl (. defaultModule.TopLevelDecls.Add(c); .) - | DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .) - | NewtypeDecl (. defaultModule.TopLevelDecls.Add(td); .) - | OtherTypeDecl (. defaultModule.TopLevelDecls.Add(td); .) - | IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) - | TraitDecl (. defaultModule.TopLevelDecls.Add(trait); .) - | ClassMemberDecl - } + TopDecls (. // find the default class in the default module, then append membersDefaultClass to its member list DefaultClassDecl defaultClass = null; foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { @@ -564,43 +656,71 @@ Dafny } .) EOF . -SubModuleDecl -= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; - Attributes attrs = null; IToken/*!*/ id; - TraitDecl/*!*/ trait; - List namedModuleDefaultClassMembers = new List();; + +TopDecls<. ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract .> += { TopDecl } + . + +DeclModifiers += (. dmod = new DeclModifierData(); .) + { "abstract" (. dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); .) + | "ghost" (. dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); .) + | "static" (. dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); .) + | "protected" (. dmod.IsProtected = true; CheckAndSetToken(ref dmod.ProtectedToken); .) + | "extern" (. dmod.IsExtern = true; CheckAndSetToken(ref dmod.ExternToken); .) + [ stringToken (. bool isVerbatimString; + string s = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString); + dmod.ExternName = new StringLiteralExpr(t, s, isVerbatimString); + .) + ] + } + . + +TopDecl<. ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract .> += (. DeclModifierData dmod; ModuleDecl submodule; + ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; + TraitDecl/*!*/ trait; + .) + DeclModifiers + ( SubModuleDecl (. module.TopLevelDecls.Add(submodule); .) + | ClassDecl (. module.TopLevelDecls.Add(c); .) + | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) + | NewtypeDecl (. module.TopLevelDecls.Add(td); .) + | OtherTypeDecl (. module.TopLevelDecls.Add(td); .) + | IteratorDecl (. module.TopLevelDecls.Add(iter); .) + | TraitDecl (. module.TopLevelDecls.Add(trait); .) + | ClassMemberDecl + ) . + +SubModuleDecl += (. Attributes attrs = null; IToken/*!*/ id; + List namedModuleDefaultClassMembers = new List();; List idRefined = null, idPath = null, idAssignment = null; ModuleDefinition module; - ModuleDecl sm; submodule = null; // appease compiler - bool isAbstract = false; + bool isAbstract = dmod.IsAbstract; bool isExclusively = false; bool opened = false; + CheckDeclModifiers(dmod, "Modules", AllowedDeclModifiers.Abstract | AllowedDeclModifiers.Extern); .) - ( [ "abstract" (. isAbstract = true; .) ] - "module" + ( "module" { Attribute } NoUSIdent + (. EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ false); .) [ "exclusively" "refines" QualifiedModuleName (. isExclusively = true; .) | "refines" QualifiedModuleName (. isExclusively = false; .) ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, isExclusively, idRefined == null ? null : idRefined, parent, attrs, false, this); .) "{" (. module.BodyStartTok = t; .) - { SubModuleDecl (. module.TopLevelDecls.Add(sm); .) - | ClassDecl (. module.TopLevelDecls.Add(c); .) - | TraitDecl (. module.TopLevelDecls.Add(trait); .) - | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) - | NewtypeDecl (. module.TopLevelDecls.Add(td); .) - | OtherTypeDecl (. module.TopLevelDecls.Add(td); .) - | IteratorDecl (. module.TopLevelDecls.Add(iter); .) - | ClassMemberDecl - } - "}" (. module.BodyEndTok = t; + TopDecls + "}" (. module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); submodule = new LiteralModuleDecl(module, parent); .) | "import" ["opened" (.opened = true;.)] NoUSIdent + (. EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ false); .) [ "=" QualifiedModuleName (. submodule = new AliasModuleDecl(idPath, id, parent, opened); .) | "as" QualifiedModuleName ["default" QualifiedModuleName ] @@ -629,7 +749,7 @@ QualifiedModuleName<.out List ids.> } . -ClassDecl +ClassDecl = (. Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ id; @@ -639,18 +759,21 @@ ClassDecl List typeArgs = new List(); List members = new List(); IToken bodyStart; + CheckDeclModifiers(dmodClass, "Classes", AllowedDeclModifiers.Extern); + DeclModifierData dmod; .) SYNC "class" { Attribute } NoUSIdent + (. EncodeExternAsAttribute(dmodClass, ref attrs, id, /* needAxiom */ false); .) [ GenericParameters ] ["extends" Type (. traits.Add(trait); .) {"," Type (. traits.Add(trait); .) } ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { DeclModifiers ClassMemberDecl } "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -659,14 +782,16 @@ ClassDecl .) . - TraitDecl - = (. Contract.Requires(module != null); +TraitDecl + = (. Contract.Requires(module != null); + CheckDeclModifiers(dmodIn, "Traits", AllowedDeclModifiers.None); Contract.Ensures(Contract.ValueAtReturn(out trait) != null); IToken/*!*/ id; Attributes attrs = null; List typeArgs = new List(); //traits should not support type parameters at the moment List members = new List(); IToken bodyStart; + DeclModifierData dmod; .) SYNC "trait" @@ -674,7 +799,7 @@ ClassDecl NoUSIdent [ GenericParameters ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { DeclModifiers ClassMemberDecl } "}" (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -683,44 +808,33 @@ ClassDecl .) . -ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl, bool isWithinAbstractModule.> +ClassMemberDecl<. DeclModifierData dmod, List mm, bool allowConstructors, bool moduleLevelDecl, bool isWithinAbstractModule.> = (. Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; - MemberModifiers mmod = new MemberModifiers(); - IToken staticToken = null, protectedToken = null; .) - { "ghost" (. mmod.IsGhost = true; .) - | "static" (. mmod.IsStatic = true; staticToken = t; .) - | "protected" (. mmod.IsProtected = true; protectedToken = t; .) - } ( (. if (moduleLevelDecl) { SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration"); - mmod.IsStatic = false; - mmod.IsProtected = false; + dmod.IsStatic = false; } .) - FieldDecl + FieldDecl | IF(IsFunctionDecl()) - (. if (moduleLevelDecl && staticToken != null) { - errors.Warning(staticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here"); - mmod.IsStatic = false; + (. if (moduleLevelDecl && dmod.StaticToken != null) { + errors.Warning(dmod.StaticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here"); + dmod.IsStatic = false; } .) - FunctionDecl (. mm.Add(f); .) - | (. if (moduleLevelDecl && staticToken != null) { - errors.Warning(staticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here"); - mmod.IsStatic = false; - } - if (protectedToken != null) { - SemErr(protectedToken, "only functions, not methods, can be declared 'protected'"); - mmod.IsProtected = false; + FunctionDecl (. mm.Add(f); .) + | (. if (moduleLevelDecl && dmod.StaticToken != null) { + errors.Warning(dmod.StaticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here"); + dmod.IsStatic = false; } .) - MethodDecl (. mm.Add(m); .) + MethodDecl (. mm.Add(m); .) ) . -DatatypeDecl +DatatypeDecl = (. Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out dt)!=null); IToken/*!*/ id; @@ -729,6 +843,7 @@ DatatypeDecl List ctors = new List(); IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; + CheckDeclModifiers(dmod, "Datatypes or codatatypes", AllowedDeclModifiers.None); .) SYNC ( "datatype" @@ -766,27 +881,27 @@ DatatypeMemberDecl<.List/*!*/ ctors.> [ FormalsOptionalIds ] (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .) . -FieldDecl<.MemberModifiers mmod, List/*!*/ mm.> +FieldDecl<.DeclModifierData dmod, List/*!*/ mm.> = (. Contract.Requires(cce.NonNullElements(mm)); Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; + CheckDeclModifiers(dmod, "Fields", AllowedDeclModifiers.Ghost); .) SYNC "var" - (. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } - .) { Attribute } - FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) - { "," FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) + FIdentType (. mm.Add(new Field(id, id.val, dmod.IsGhost, ty, attrs)); .) + { "," FIdentType (. mm.Add(new Field(id, id.val, dmod.IsGhost, ty, attrs)); .) } OldSemi . -NewtypeDecl +NewtypeDecl = (. IToken id, bvId; Attributes attrs = null; td = null; Type baseType = null; Expression wh; + CheckDeclModifiers(dmod, "Newtypes", AllowedDeclModifiers.None); .) "newtype" { Attribute } @@ -800,13 +915,14 @@ NewtypeDecl | Type (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .) ) . -OtherTypeDecl +OtherTypeDecl = (. IToken id; Attributes attrs = null; var eqSupport = TypeParameter.EqualitySupportValue.Unspecified; var typeArgs = new List(); td = null; Type ty; + CheckDeclModifiers(dmod, "Type aliases", AllowedDeclModifiers.None); .) "type" { Attribute } @@ -902,7 +1018,7 @@ TypeIdentOptional +IteratorDecl = (. Contract.Ensures(Contract.ValueAtReturn(out iter) != null); IToken/*!*/ id; Attributes attrs = null; @@ -924,6 +1040,7 @@ IteratorDecl IToken signatureEllipsis = null; IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; + CheckDeclModifiers(dmod, "Iterators", AllowedDeclModifiers.None); .) SYNC "iterator" @@ -969,7 +1086,7 @@ GenericParameters<.List/*!*/ typeArgs.> ">" . /*------------------------------------------------------------------------*/ -MethodDecl +MethodDecl = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -991,43 +1108,36 @@ MethodDecl } [ NoUSIdent (. hasName = true; .) ] @@ -1037,12 +1147,13 @@ MethodDecl ] - Formals + Formals [ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .) - Formals + Formals ] | "..." (. signatureEllipsis = t; .) ) @@ -1059,16 +1170,16 @@ MethodDecl(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isIndLemma) { - m = new InductiveLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs, + m = new InductiveLemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isCoLemma) { - m = new CoLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs, + m = new CoLemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isLemma) { - m = new Lemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs, + m = new Lemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else { - m = new Method(tok, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, + m = new Method(tok, id.val, dmod.IsStatic, dmod.IsGhost, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } m.BodyStartTok = bodyStart; @@ -1273,7 +1384,7 @@ GenericInstantiation<.List/*!*/ gt.> ">" . /*------------------------------------------------------------------------*/ -FunctionDecl +FunctionDecl = (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null); Attributes attrs = null; IToken/*!*/ id = Token.NoToken; // to please compiler @@ -1296,7 +1407,13 @@ FunctionDecl } NoUSIdent @@ -1312,7 +1429,13 @@ FunctionDecl } NoUSIdent @@ -1327,7 +1450,8 @@ FunctionDecl } NoUSIdent @@ -1341,7 +1465,8 @@ FunctionDecl } NoUSIdent @@ -1358,22 +1483,23 @@ FunctionDecl } [ FunctionBody ] - (. if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) { + (. if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && + !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) { SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute"); } - + EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ true); IToken tok = theVerifyThisFile ? id : new IncludeToken(id); if (isPredicate) { - f = new Predicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals, + f = new Predicate(tok, id.val, dmod.IsStatic, dmod.IsProtected, !isFunctionMethod, typeArgs, formals, reqs, reads, ens, new Specification(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis); } else if (isIndPredicate) { - f = new InductivePredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals, + f = new InductivePredicate(tok, id.val, dmod.IsStatic, dmod.IsProtected, typeArgs, formals, reqs, reads, ens, body, attrs, signatureEllipsis); } else if (isCoPredicate) { - f = new CoPredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals, + f = new CoPredicate(tok, id.val, dmod.IsStatic, dmod.IsProtected, typeArgs, formals, reqs, reads, ens, body, attrs, signatureEllipsis); } else { - f = new Function(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals, returnType, + f = new Function(tok, id.val, dmod.IsStatic, dmod.IsProtected, !isFunctionMethod, typeArgs, formals, returnType, reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis); } f.BodyStartTok = bodyStart; diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 4c1e2bd7..a51e30de 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1059,7 +1059,7 @@ namespace Microsoft.Dafny { public virtual string FullCompileName { get { if (ResolvedClass != null && !ResolvedClass.Module.IsDefaultModule) { - return ResolvedClass.Module.CompileName + ".@" + CompileName; + return ResolvedClass.Module.CompileName + ".@" + ResolvedClass.CompileName; } else { return CompileName; } @@ -1536,7 +1536,17 @@ namespace Microsoft.Dafny { public virtual string CompileName { get { if (compileName == null) { - compileName = NonglobalVariable.CompilerizeName(Name); + object externValue = ""; + string errorMessage = ""; + bool isExternal = Attributes.ContainsMatchingValue(this.Attributes, "extern", ref externValue, + new Attributes.MatchingValueOption[] { Attributes.MatchingValueOption.String }, + err => errorMessage = err); + if (isExternal) { + compileName = (string)externValue; + } + else { + compileName = NonglobalVariable.CompilerizeName(Name); + } } return compileName; } @@ -1835,10 +1845,19 @@ namespace Microsoft.Dafny { public string CompileName { get { if (compileName == null) { - if (IsBuiltinName) - compileName = Name; - else - compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name); + object externValue = ""; + string errorMessage = ""; + bool isExternal = Attributes.ContainsMatchingValue(this.Attributes, "extern", ref externValue, + new Attributes.MatchingValueOption[] { Attributes.MatchingValueOption.String }, + err => errorMessage = err); + if (isExternal) { + compileName = (string)externValue; + } else { + if (IsBuiltinName) + compileName = Name; + else + compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name); + } } return compileName; } diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index 68ab7a2d..a61539b0 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -4,8 +4,8 @@ # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to # point to whatever directory you install that into. # ############################################################################### -COCO_EXE_DIR = ..\..\..\boogie-partners\CocoR\bin -FRAME_DIR = ..\..\..\boogie-partners\CocoR\Modified +COCO_EXE_DIR = ..\..\..\coco +FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified COCO = $(COCO_EXE_DIR)\Coco.exe # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 922aad75..dc661fc5 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -73,7 +73,7 @@ public class Parser { public const int _star = 57; public const int _notIn = 58; public const int _ellipsis = 59; - public const int maxT = 138; + public const int maxT = 139; const bool _T = true; const bool _x = false; @@ -95,10 +95,113 @@ readonly BuiltIns theBuiltIns; readonly bool theVerifyThisFile; int anonymousIds = 0; -struct MemberModifiers { +/// +/// Holds the modifiers given for a declaration +/// +/// Not all modifiers are applicable to all kinds of declarations. +/// Errors are given when a modify does not apply. +/// We also record the tokens for the specified modifiers so that +/// they can be used in error messages. +/// +struct DeclModifierData { + public bool IsAbstract; + public IToken AbstractToken; public bool IsGhost; + public IToken GhostToken; public bool IsStatic; + public IToken StaticToken; public bool IsProtected; + public IToken ProtectedToken; + public bool IsExtern; + public IToken ExternToken; + public StringLiteralExpr ExternName; + +} + +// Check that token has not been set, then set it. +public void CheckAndSetToken(ref IToken token) +{ + if (token != null) { + SemErr(t, "Duplicate declaration modifier: " + t.val); + } + token = t; +} + +/// +// A flags type used to tell what declaration modifiers are allowed for a declaration. +/// +[Flags] +enum AllowedDeclModifiers { + None = 0, + Abstract = 1, + Ghost = 2, + + // Means ghost not allowed because already implicitly ghost. + AlreadyGhost = 4, + Static = 8, + Protected = 16, + Extern = 32 +}; + +/// +/// Check the declaration modifiers against those that are allowed. +/// +/// The 'allowed' parameter specifies which declaratio modifiers are allowed. +/// The 'declCaption' parameter should be a string describing the kind of declaration. +/// It is used in error messages. +/// Any declaration modifiers that are present but not allowed are cleared. +/// +void CheckDeclModifiers(DeclModifierData dmod, string declCaption, AllowedDeclModifiers allowed) +{ + if (dmod.IsAbstract && ((allowed & AllowedDeclModifiers.Abstract) == 0)) { + SemErr(dmod.AbstractToken, declCaption + " cannot be declared 'abstract'."); + dmod.IsAbstract = false; + } + if (dmod.IsGhost) { + if ((allowed & AllowedDeclModifiers.AlreadyGhost) != 0) { + SemErr(dmod.GhostToken, declCaption + " cannot be declared ghost (they are 'ghost' by default)."); + dmod.IsGhost = false; + } else if ((allowed & AllowedDeclModifiers.Ghost) == 0) { + SemErr(dmod.GhostToken, declCaption + " cannot be declared 'ghost'."); + dmod.IsGhost = false; + } + } + if (dmod.IsStatic && ((allowed & AllowedDeclModifiers.Static) == 0)) { + SemErr(dmod.StaticToken, declCaption + " cannot be declared 'static'."); + dmod.IsStatic = false; + } + if (dmod.IsProtected && ((allowed & AllowedDeclModifiers.Protected) == 0)) { + SemErr(dmod.ProtectedToken, declCaption + " cannot be declared 'protected'."); + dmod.IsProtected = false; + } + if (dmod.IsExtern && ((allowed & AllowedDeclModifiers.Extern) == 0)) { + SemErr(dmod.ExternToken, declCaption + " cannot be declared 'extern'."); + dmod.IsExtern = false; + } +} + +/// +/// Encode an 'extern' declaration modifier as an {:extern name} attribute. +/// +/// We also include an {:axiom} attribute since the specification of an +/// external entity is assumed to hold, but only for methods or functions. +/// +static void EncodeExternAsAttribute(DeclModifierData dmod, ref Attributes attrs, IToken/*!*/ id, bool needAxiom) { + if (dmod.IsExtern) { + StringLiteralExpr name = dmod.ExternName; + if (name == null) { + bool isVerbatimString = false; + name = new StringLiteralExpr(id, id.val, isVerbatimString); + } + var args = new List(); + args.Add(name); + attrs = new Attributes("extern", args, attrs); + + // Also 'extern' implies 'axiom' for methods or functions. + if (needAxiom) { + attrs = new Attributes("axiom", new List(), attrs); + } + } } /// @@ -543,13 +646,10 @@ bool IsType(ref IToken pt) { void Dafny() { - ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; List membersDefaultClass = new List(); - 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) - TraitDecl/*!*/ trait; Contract.Assert(defaultModule != null); while (la.kind == 60) { @@ -570,49 +670,7 @@ bool IsType(ref IToken pt) { } } - while (StartOf(1)) { - switch (la.kind) { - case 61: case 62: case 65: { - SubModuleDecl(defaultModule, out submodule); - defaultModule.TopLevelDecls.Add(submodule); - break; - } - case 70: { - ClassDecl(defaultModule, out c); - defaultModule.TopLevelDecls.Add(c); - break; - } - case 76: case 77: { - DatatypeDecl(defaultModule, out dt); - defaultModule.TopLevelDecls.Add(dt); - break; - } - case 79: { - NewtypeDecl(defaultModule, out td); - defaultModule.TopLevelDecls.Add(td); - break; - } - case 80: { - OtherTypeDecl(defaultModule, out td); - defaultModule.TopLevelDecls.Add(td); - break; - } - case 81: { - IteratorDecl(defaultModule, out iter); - defaultModule.TopLevelDecls.Add(iter); - break; - } - case 72: { - TraitDecl(defaultModule, out trait); - defaultModule.TopLevelDecls.Add(trait); - break; - } - case 38: case 39: case 40: case 41: case 42: case 73: case 74: case 75: case 78: case 84: case 85: case 86: case 87: { - ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, false); - break; - } - } - } + TopDecls(defaultModule, membersDefaultClass, /* isTopLevel */ true, /* isAbstract */ false); DefaultClassDecl defaultClass = null; foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { defaultClass = topleveldecl as DefaultClassDecl; @@ -628,33 +686,114 @@ bool IsType(ref IToken pt) { Expect(0); } - void SubModuleDecl(ModuleDefinition parent, out ModuleDecl submodule) { + void TopDecls(ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract ) { + while (StartOf(1)) { + TopDecl(module, membersDefaultClass, isTopLevel, isAbstract); + } + } + + void TopDecl(ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract ) { + DeclModifierData dmod; ModuleDecl submodule; ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; - Attributes attrs = null; IToken/*!*/ id; TraitDecl/*!*/ trait; + + DeclModifiers(out dmod); + switch (la.kind) { + case 66: case 69: { + SubModuleDecl(dmod, module, out submodule); + module.TopLevelDecls.Add(submodule); + break; + } + case 74: { + ClassDecl(dmod, module, out c); + module.TopLevelDecls.Add(c); + break; + } + case 77: case 78: { + DatatypeDecl(dmod, module, out dt); + module.TopLevelDecls.Add(dt); + break; + } + case 80: { + NewtypeDecl(dmod, module, out td); + module.TopLevelDecls.Add(td); + break; + } + case 81: { + OtherTypeDecl(dmod, module, out td); + module.TopLevelDecls.Add(td); + break; + } + case 82: { + IteratorDecl(dmod, module, out iter); + module.TopLevelDecls.Add(iter); + break; + } + case 76: { + TraitDecl(dmod, module, out trait); + module.TopLevelDecls.Add(trait); + break; + } + case 38: case 39: case 40: case 41: case 42: case 79: case 85: case 86: case 87: case 88: { + ClassMemberDecl(dmod, membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, +!isTopLevel && DafnyOptions.O.IronDafny && isAbstract); + break; + } + default: SynErr(140); break; + } + } + + void DeclModifiers(out DeclModifierData dmod) { + dmod = new DeclModifierData(); + while (StartOf(2)) { + if (la.kind == 61) { + Get(); + dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); + } else if (la.kind == 62) { + Get(); + dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); + } else if (la.kind == 63) { + Get(); + dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); + } else if (la.kind == 64) { + Get(); + dmod.IsProtected = true; CheckAndSetToken(ref dmod.ProtectedToken); + } else { + Get(); + dmod.IsExtern = true; CheckAndSetToken(ref dmod.ExternToken); + if (la.kind == 20) { + Get(); + bool isVerbatimString; + string s = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString); + dmod.ExternName = new StringLiteralExpr(t, s, isVerbatimString); + + } + } + } + } + + void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDecl submodule) { + Attributes attrs = null; IToken/*!*/ id; List namedModuleDefaultClassMembers = new List();; List idRefined = null, idPath = null, idAssignment = null; ModuleDefinition module; - ModuleDecl sm; submodule = null; // appease compiler - bool isAbstract = false; + bool isAbstract = dmod.IsAbstract; bool isExclusively = false; bool opened = false; + CheckDeclModifiers(dmod, "Modules", AllowedDeclModifiers.Abstract | AllowedDeclModifiers.Extern); - if (la.kind == 61 || la.kind == 62) { - if (la.kind == 61) { - Get(); - isAbstract = true; - } - Expect(62); + if (la.kind == 66) { + Get(); while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 63 || la.kind == 64) { - if (la.kind == 63) { + EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ false); + if (la.kind == 67 || la.kind == 68) { + if (la.kind == 67) { Get(); - Expect(64); + Expect(68); QualifiedModuleName(out idRefined); isExclusively = true; } else { @@ -666,69 +805,28 @@ bool IsType(ref IToken pt) { module = new ModuleDefinition(id, id.val, isAbstract, false, isExclusively, idRefined == null ? null : idRefined, parent, attrs, false, this); Expect(46); module.BodyStartTok = t; - while (StartOf(1)) { - switch (la.kind) { - case 61: case 62: case 65: { - SubModuleDecl(module, out sm); - module.TopLevelDecls.Add(sm); - break; - } - case 70: { - ClassDecl(module, out c); - module.TopLevelDecls.Add(c); - break; - } - case 72: { - TraitDecl(module, out trait); - module.TopLevelDecls.Add(trait); - break; - } - case 76: case 77: { - DatatypeDecl(module, out dt); - module.TopLevelDecls.Add(dt); - break; - } - case 79: { - NewtypeDecl(module, out td); - module.TopLevelDecls.Add(td); - break; - } - case 80: { - OtherTypeDecl(module, out td); - module.TopLevelDecls.Add(td); - break; - } - case 81: { - IteratorDecl(module, out iter); - module.TopLevelDecls.Add(iter); - break; - } - case 38: case 39: case 40: case 41: case 42: case 73: case 74: case 75: case 78: case 84: case 85: case 86: case 87: { - ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, DafnyOptions.O.IronDafny && isAbstract); - break; - } - } - } + TopDecls(module, namedModuleDefaultClassMembers, /* isTopLevel */ false, isAbstract); Expect(47); module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); submodule = new LiteralModuleDecl(module, parent); - } else if (la.kind == 65) { + } else if (la.kind == 69) { Get(); - if (la.kind == 66) { + if (la.kind == 70) { Get(); opened = true; } NoUSIdent(out id); - if (la.kind == 67 || la.kind == 68) { - if (la.kind == 67) { + EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ false); + if (la.kind == 71 || la.kind == 72) { + if (la.kind == 71) { Get(); QualifiedModuleName(out idPath); submodule = new AliasModuleDecl(idPath, id, parent, opened); } else { Get(); QualifiedModuleName(out idPath); - if (la.kind == 69) { + if (la.kind == 73) { Get(); QualifiedModuleName(out idAssignment); } @@ -736,7 +834,7 @@ bool IsType(ref IToken pt) { } } if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(139); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(141); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -746,10 +844,10 @@ bool IsType(ref IToken pt) { submodule = new AliasModuleDecl(idPath, id, parent, opened); } - } else SynErr(140); + } else SynErr(142); } - void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { + void ClassDecl(DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ id; @@ -759,17 +857,20 @@ bool IsType(ref IToken pt) { List typeArgs = new List(); List members = new List(); IToken bodyStart; + CheckDeclModifiers(dmodClass, "Classes", AllowedDeclModifiers.Extern); + DeclModifierData dmod; - while (!(la.kind == 0 || la.kind == 70)) {SynErr(141); Get();} - Expect(70); + while (!(la.kind == 0 || la.kind == 74)) {SynErr(143); Get();} + Expect(74); while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); + EncodeExternAsAttribute(dmodClass, ref attrs, id, /* needAxiom */ false); if (la.kind == 52) { GenericParameters(typeArgs); } - if (la.kind == 71) { + if (la.kind == 75) { Get(); Type(out trait); traits.Add(trait); @@ -781,8 +882,9 @@ bool IsType(ref IToken pt) { } Expect(46); bodyStart = t; - while (StartOf(2)) { - ClassMemberDecl(members, true, false, false); + while (StartOf(3)) { + DeclModifiers(out dmod); + ClassMemberDecl(dmod, members, true, false, false); } Expect(47); c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -791,7 +893,7 @@ bool IsType(ref IToken pt) { } - void DatatypeDecl(ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt) { + void DatatypeDecl(DeclModifierData dmod, ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt) { Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out dt)!=null); IToken/*!*/ id; @@ -800,14 +902,15 @@ bool IsType(ref IToken pt) { List ctors = new List(); IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; + CheckDeclModifiers(dmod, "Datatypes or codatatypes", AllowedDeclModifiers.None); - while (!(la.kind == 0 || la.kind == 76 || la.kind == 77)) {SynErr(142); Get();} - if (la.kind == 76) { + while (!(la.kind == 0 || la.kind == 77 || la.kind == 78)) {SynErr(144); Get();} + if (la.kind == 77) { Get(); - } else if (la.kind == 77) { + } else if (la.kind == 78) { Get(); co = true; - } else SynErr(143); + } else SynErr(145); while (la.kind == 46) { Attribute(ref attrs); } @@ -815,7 +918,7 @@ bool IsType(ref IToken pt) { if (la.kind == 52) { GenericParameters(typeArgs); } - Expect(67); + Expect(71); bodyStart = t; DatatypeMemberDecl(ctors); while (la.kind == 23) { @@ -823,7 +926,7 @@ bool IsType(ref IToken pt) { DatatypeMemberDecl(ctors); } if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(144); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(146); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -837,19 +940,20 @@ bool IsType(ref IToken pt) { } - void NewtypeDecl(ModuleDefinition module, out TopLevelDecl td) { + void NewtypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td) { IToken id, bvId; Attributes attrs = null; td = null; Type baseType = null; Expression wh; + CheckDeclModifiers(dmod, "Newtypes", AllowedDeclModifiers.None); - Expect(79); + Expect(80); while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - Expect(67); + Expect(71); if (IsIdentColonOrBar()) { NoUSIdent(out bvId); if (la.kind == 21) { @@ -860,21 +964,22 @@ bool IsType(ref IToken pt) { Expect(23); Expression(out wh, false, true); td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); - } else if (StartOf(3)) { + } else if (StartOf(4)) { Type(out baseType); td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); - } else SynErr(145); + } else SynErr(147); } - void OtherTypeDecl(ModuleDefinition module, out TopLevelDecl td) { + void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td) { IToken id; Attributes attrs = null; var eqSupport = TypeParameter.EqualitySupportValue.Unspecified; var typeArgs = new List(); td = null; Type ty; + CheckDeclModifiers(dmod, "Type aliases", AllowedDeclModifiers.None); - Expect(80); + Expect(81); while (la.kind == 46) { Attribute(ref attrs); } @@ -887,28 +992,28 @@ bool IsType(ref IToken pt) { if (la.kind == 52) { GenericParameters(typeArgs); } - } else if (StartOf(4)) { + } else if (StartOf(5)) { if (la.kind == 52) { GenericParameters(typeArgs); } - if (la.kind == 67) { + if (la.kind == 71) { Get(); Type(out ty); td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); } - } else SynErr(146); + } else SynErr(148); if (td == null) { td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs); } if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(147); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(149); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } } - void IteratorDecl(ModuleDefinition module, out IteratorDecl/*!*/ iter) { + void IteratorDecl(DeclModifierData dmod, ModuleDefinition module, out IteratorDecl/*!*/ iter) { Contract.Ensures(Contract.ValueAtReturn(out iter) != null); IToken/*!*/ id; Attributes attrs = null; @@ -930,9 +1035,10 @@ bool IsType(ref IToken pt) { IToken signatureEllipsis = null; IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; + CheckDeclModifiers(dmod, "Iterators", AllowedDeclModifiers.None); - while (!(la.kind == 0 || la.kind == 81)) {SynErr(148); Get();} - Expect(81); + while (!(la.kind == 0 || la.kind == 82)) {SynErr(150); Get();} + Expect(82); while (la.kind == 46) { Attribute(ref attrs); } @@ -942,8 +1048,8 @@ bool IsType(ref IToken pt) { GenericParameters(typeArgs); } Formals(true, true, ins); - if (la.kind == 82 || la.kind == 83) { - if (la.kind == 82) { + if (la.kind == 83 || la.kind == 84) { + if (la.kind == 83) { Get(); } else { Get(); @@ -954,8 +1060,8 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(149); - while (StartOf(5)) { + } else SynErr(151); + while (StartOf(6)) { IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); } if (la.kind == 46) { @@ -972,17 +1078,19 @@ bool IsType(ref IToken pt) { } - void TraitDecl(ModuleDefinition/*!*/ module, out TraitDecl/*!*/ trait) { - Contract.Requires(module != null); + void TraitDecl(DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitDecl/*!*/ trait) { + Contract.Requires(module != null); + CheckDeclModifiers(dmodIn, "Traits", AllowedDeclModifiers.None); Contract.Ensures(Contract.ValueAtReturn(out trait) != null); IToken/*!*/ id; Attributes attrs = null; List typeArgs = new List(); //traits should not support type parameters at the moment List members = new List(); IToken bodyStart; + DeclModifierData dmod; - while (!(la.kind == 0 || la.kind == 72)) {SynErr(150); Get();} - Expect(72); + while (!(la.kind == 0 || la.kind == 76)) {SynErr(152); Get();} + Expect(76); while (la.kind == 46) { Attribute(ref attrs); } @@ -992,8 +1100,9 @@ bool IsType(ref IToken pt) { } Expect(46); bodyStart = t; - while (StartOf(2)) { - ClassMemberDecl(members, true, false, false); + while (StartOf(3)) { + DeclModifiers(out dmod); + ClassMemberDecl(dmod, members, true, false, false); } Expect(47); trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -1002,54 +1111,35 @@ bool IsType(ref IToken pt) { } - void ClassMemberDecl(List mm, bool allowConstructors, bool moduleLevelDecl, bool isWithinAbstractModule) { + void ClassMemberDecl(DeclModifierData dmod, List mm, bool allowConstructors, bool moduleLevelDecl, bool isWithinAbstractModule) { Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; - MemberModifiers mmod = new MemberModifiers(); - IToken staticToken = null, protectedToken = null; - while (la.kind == 73 || la.kind == 74 || la.kind == 75) { - if (la.kind == 73) { - Get(); - mmod.IsGhost = true; - } else if (la.kind == 74) { - Get(); - mmod.IsStatic = true; staticToken = t; - } else { - Get(); - mmod.IsProtected = true; protectedToken = t; - } - } - if (la.kind == 78) { + if (la.kind == 79) { if (moduleLevelDecl) { SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration"); - mmod.IsStatic = false; - mmod.IsProtected = false; + dmod.IsStatic = false; } - FieldDecl(mmod, mm); + FieldDecl(dmod, mm); } else if (IsFunctionDecl()) { - if (moduleLevelDecl && staticToken != null) { - errors.Warning(staticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here"); - mmod.IsStatic = false; + if (moduleLevelDecl && dmod.StaticToken != null) { + errors.Warning(dmod.StaticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here"); + dmod.IsStatic = false; } - FunctionDecl(mmod, isWithinAbstractModule, out f); + FunctionDecl(dmod, isWithinAbstractModule, out f); mm.Add(f); - } else if (StartOf(6)) { - if (moduleLevelDecl && staticToken != null) { - errors.Warning(staticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here"); - mmod.IsStatic = false; - } - if (protectedToken != null) { - SemErr(protectedToken, "only functions, not methods, can be declared 'protected'"); - mmod.IsProtected = false; + } else if (StartOf(7)) { + if (moduleLevelDecl && dmod.StaticToken != null) { + errors.Warning(dmod.StaticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here"); + dmod.IsStatic = false; } - MethodDecl(mmod, allowConstructors, isWithinAbstractModule, out m); + MethodDecl(dmod, allowConstructors, isWithinAbstractModule, out m); mm.Add(m); - } else SynErr(151); + } else SynErr(153); } void Attribute(ref Attributes attrs) { @@ -1060,7 +1150,7 @@ bool IsType(ref IToken pt) { Expect(21); NoUSIdent(out x); name = x.val; - if (StartOf(7)) { + if (StartOf(8)) { Expressions(args); } Expect(47); @@ -1129,29 +1219,28 @@ bool IsType(ref IToken pt) { TypeAndToken(out tok, out ty); } - void FieldDecl(MemberModifiers mmod, List/*!*/ mm) { + void FieldDecl(DeclModifierData dmod, List/*!*/ mm) { Contract.Requires(cce.NonNullElements(mm)); Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; + CheckDeclModifiers(dmod, "Fields", AllowedDeclModifiers.Ghost); - while (!(la.kind == 0 || la.kind == 78)) {SynErr(152); Get();} - Expect(78); - if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } - + while (!(la.kind == 0 || la.kind == 79)) {SynErr(154); Get();} + Expect(79); while (la.kind == 46) { Attribute(ref attrs); } FIdentType(out id, out ty); - mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); + mm.Add(new Field(id, id.val, dmod.IsGhost, ty, attrs)); while (la.kind == 22) { Get(); FIdentType(out id, out ty); - mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); + mm.Add(new Field(id, id.val, dmod.IsGhost, ty, attrs)); } OldSemi(); } - void FunctionDecl(MemberModifiers mmod, bool isWithinAbstractModule, out Function/*!*/ f) { + void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Function/*!*/ f) { Contract.Ensures(Contract.ValueAtReturn(out f)!=null); Attributes attrs = null; IToken/*!*/ id = Token.NoToken; // to please compiler @@ -1172,11 +1261,17 @@ bool IsType(ref IToken pt) { if (la.kind == 38) { Get(); - if (la.kind == 84) { + if (la.kind == 85) { Get(); isFunctionMethod = true; } - if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); } + AllowedDeclModifiers allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static | AllowedDeclModifiers.Protected; + string caption = "Functions"; + if (isFunctionMethod) { + allowed |= AllowedDeclModifiers.Extern; + caption = "Function methods"; + } + CheckDeclModifiers(dmod, caption, allowed); while (la.kind == 46) { Attribute(ref attrs); @@ -1192,21 +1287,27 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(153); + } else SynErr(155); } else if (la.kind == 39) { Get(); isPredicate = true; - if (la.kind == 84) { + if (la.kind == 85) { Get(); isFunctionMethod = true; } - if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); } + AllowedDeclModifiers allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static | AllowedDeclModifiers.Protected; + string caption = "Predicates"; + if (isFunctionMethod) { + allowed |= AllowedDeclModifiers.Extern; + caption = "Predicate methods"; + } + CheckDeclModifiers(dmod, caption, allowed); while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (StartOf(8)) { + if (StartOf(9)) { if (la.kind == 52) { GenericParameters(typeArgs); } @@ -1223,12 +1324,13 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(154); + } else SynErr(156); } else if (la.kind == 40) { Get(); Expect(39); isIndPredicate = true; - if (mmod.IsGhost) { SemErr(t, "inductive predicates cannot be declared 'ghost' (they are ghost by default)"); } + CheckDeclModifiers(dmod, "Inductive predicates", + AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static | AllowedDeclModifiers.Protected); while (la.kind == 46) { Attribute(ref attrs); @@ -1246,11 +1348,12 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(155); + } else SynErr(157); } else if (la.kind == 42) { Get(); isCoPredicate = true; - if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); } + CheckDeclModifiers(dmod, "Copredicates", + AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static | AllowedDeclModifiers.Protected); while (la.kind == 46) { Attribute(ref attrs); @@ -1268,31 +1371,32 @@ bool IsType(ref IToken pt) { } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(156); - } else SynErr(157); + } else SynErr(158); + } else SynErr(159); decreases = isIndPredicate || isCoPredicate ? null : new List(); - while (StartOf(9)) { + while (StartOf(10)) { FunctionSpec(reqs, reads, ens, decreases); } if (la.kind == 46) { FunctionBody(out body, out bodyStart, out bodyEnd); } - if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) { + if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && + !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) { SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute"); } - + EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ true); IToken tok = theVerifyThisFile ? id : new IncludeToken(id); if (isPredicate) { - f = new Predicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals, + f = new Predicate(tok, id.val, dmod.IsStatic, dmod.IsProtected, !isFunctionMethod, typeArgs, formals, reqs, reads, ens, new Specification(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis); } else if (isIndPredicate) { - f = new InductivePredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals, + f = new InductivePredicate(tok, id.val, dmod.IsStatic, dmod.IsProtected, typeArgs, formals, reqs, reads, ens, body, attrs, signatureEllipsis); } else if (isCoPredicate) { - f = new CoPredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals, + f = new CoPredicate(tok, id.val, dmod.IsStatic, dmod.IsProtected, typeArgs, formals, reqs, reads, ens, body, attrs, signatureEllipsis); } else { - f = new Function(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals, returnType, + f = new Function(tok, id.val, dmod.IsStatic, dmod.IsProtected, !isFunctionMethod, typeArgs, formals, returnType, reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis); } f.BodyStartTok = bodyStart; @@ -1305,7 +1409,7 @@ bool IsType(ref IToken pt) { } - void MethodDecl(MemberModifiers mmod, bool allowConstructor, bool isWithinAbstractModule, out Method/*!*/ m) { + void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstractModule, out Method/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -1327,26 +1431,37 @@ bool IsType(ref IToken pt) { IToken signatureEllipsis = null; IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; + AllowedDeclModifiers allowed = AllowedDeclModifiers.None; + string caption = ""; - while (!(StartOf(10))) {SynErr(158); Get();} + while (!(StartOf(11))) {SynErr(160); Get();} switch (la.kind) { - case 84: { + case 85: { Get(); + caption = "Methods"; + allowed = AllowedDeclModifiers.Ghost | AllowedDeclModifiers.Static + | AllowedDeclModifiers.Extern; break; } case 41: { Get(); - isLemma = true; + isLemma = true; caption = "Lemmas"; + allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static + | AllowedDeclModifiers.Protected; break; } - case 85: { + case 86: { Get(); - isCoLemma = true; + isCoLemma = true; caption = "Colemmas"; + allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static + | AllowedDeclModifiers.Protected; break; } - case 86: { + case 87: { Get(); - isCoLemma = true; + isCoLemma = true; caption = "Comethods"; + allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static + | AllowedDeclModifiers.Protected; errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'"); break; @@ -1354,43 +1469,26 @@ bool IsType(ref IToken pt) { case 40: { Get(); Expect(41); - isIndLemma = true; + isIndLemma = true; caption = "Inductive lemmas"; + allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static; break; } - case 87: { + case 88: { Get(); if (allowConstructor) { isConstructor = true; } else { SemErr(t, "constructors are allowed only in classes"); - } + } + caption = "Constructors"; + allowed = AllowedDeclModifiers.None; break; } - default: SynErr(159); break; + default: SynErr(161); break; } keywordToken = t; - if (isLemma) { - if (mmod.IsGhost) { - SemErr(t, "lemmas cannot be declared 'ghost' (they are automatically 'ghost')"); - } - } else if (isConstructor) { - if (mmod.IsGhost) { - SemErr(t, "constructors cannot be declared 'ghost'"); - } - if (mmod.IsStatic) { - SemErr(t, "constructors cannot be declared 'static'"); - } - } else if (isIndLemma) { - if (mmod.IsGhost) { - SemErr(t, "inductive lemmas cannot be declared 'ghost' (they are automatically 'ghost')"); - } - } else if (isCoLemma) { - if (mmod.IsGhost) { - SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')"); - } - } - + CheckDeclModifiers(dmod, caption, allowed); while (la.kind == 46) { Attribute(ref attrs); } @@ -1404,22 +1502,23 @@ bool IsType(ref IToken pt) { SemErr(la, "a method must be given a name (expecting identifier)"); } } + EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ true); if (la.kind == 50 || la.kind == 52) { if (la.kind == 52) { GenericParameters(typeArgs); } - Formals(true, !mmod.IsGhost, ins); - if (la.kind == 83) { + Formals(true, !dmod.IsGhost, ins); + if (la.kind == 84) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } - Formals(false, !mmod.IsGhost, outs); + Formals(false, !dmod.IsGhost, outs); } } else if (la.kind == 59) { Get(); signatureEllipsis = t; - } else SynErr(160); - while (StartOf(11)) { + } else SynErr(162); + while (StartOf(12)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } if (la.kind == 46) { @@ -1434,16 +1533,16 @@ bool IsType(ref IToken pt) { m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isIndLemma) { - m = new InductiveLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs, + m = new InductiveLemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isCoLemma) { - m = new CoLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs, + m = new CoLemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isLemma) { - m = new Lemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs, + m = new Lemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else { - m = new Method(tok, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, + m = new Method(tok, id.val, dmod.IsStatic, dmod.IsGhost, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } m.BodyStartTok = bodyStart; @@ -1470,7 +1569,7 @@ bool IsType(ref IToken pt) { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; Expect(50); - if (StartOf(12)) { + if (StartOf(13)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); while (la.kind == 22) { @@ -1491,14 +1590,14 @@ bool IsType(ref IToken pt) { } else if (la.kind == 2) { Get(); id = t; - } else SynErr(161); + } else SynErr(163); Expect(21); Type(out ty); } void OldSemi() { if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(162); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(164); Get();} Get(); } } @@ -1521,7 +1620,7 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out id)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); isGhost = false; - if (la.kind == 73) { + if (la.kind == 62) { Get(); if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } } @@ -1573,11 +1672,11 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); Contract.Ensures(Contract.ValueAtReturn(out identName)!=null); string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; - if (la.kind == 73) { + if (la.kind == 62) { Get(); isGhost = true; } - if (StartOf(3)) { + if (StartOf(4)) { TypeAndToken(out id, out ty); if (la.kind == 21) { Get(); @@ -1595,7 +1694,7 @@ bool IsType(ref IToken pt) { id = t; name = id.val; Expect(21); Type(out ty); - } else SynErr(163); + } else SynErr(165); if (name != null) { identName = name; } else { @@ -1746,7 +1845,7 @@ bool IsType(ref IToken pt) { case 50: { Get(); tok = t; tupleArgTypes = new List(); - if (StartOf(3)) { + if (StartOf(4)) { Type(out ty); tupleArgTypes.Add(ty); while (la.kind == 22) { @@ -1783,7 +1882,7 @@ bool IsType(ref IToken pt) { ty = new UserDefinedType(e.tok, e); break; } - default: SynErr(164); break; + default: SynErr(166); break; } if (la.kind == 30) { Type t2; @@ -1804,7 +1903,7 @@ bool IsType(ref IToken pt) { void Formals(bool incoming, bool allowGhostKeyword, List formals) { Contract.Requires(cce.NonNullElements(formals)); IToken id; Type ty; bool isGhost; Expect(50); - if (la.kind == 1 || la.kind == 73) { + if (la.kind == 1 || la.kind == 62) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); while (la.kind == 22) { @@ -1822,7 +1921,7 @@ 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(13))) {SynErr(165); Get();} + while (!(StartOf(14))) {SynErr(167); Get();} if (la.kind == 44) { Get(); while (IsAttribute()) { @@ -1849,14 +1948,14 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { mod.Add(fe); } OldSemi(); - } else if (StartOf(14)) { - if (la.kind == 88) { + } else if (StartOf(15)) { + if (la.kind == 89) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); } - if (la.kind == 90) { + if (la.kind == 91) { Get(); isYield = true; } @@ -1870,7 +1969,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { req.Add(new MaybeFreeExpression(e, isFree)); } - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1883,7 +1982,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } - } else SynErr(166); + } else SynErr(168); } else if (la.kind == 36) { Get(); while (IsAttribute()) { @@ -1891,7 +1990,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(167); + } else SynErr(169); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -1900,7 +1999,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expect(46); bodyStart = t; - while (StartOf(15)) { + while (StartOf(16)) { Stmt(body); } Expect(47); @@ -1913,7 +2012,7 @@ 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(16))) {SynErr(168); Get();} + while (!(StartOf(17))) {SynErr(170); Get();} if (la.kind == 43) { Get(); while (IsAttribute()) { @@ -1927,8 +2026,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } OldSemi(); - } else if (la.kind == 45 || la.kind == 88 || la.kind == 89) { - if (la.kind == 88) { + } else if (la.kind == 45 || la.kind == 89 || la.kind == 90) { + if (la.kind == 89) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); @@ -1939,7 +2038,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false, false); OldSemi(); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1947,7 +2046,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false, false); OldSemi(); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(169); + } else SynErr(171); } else if (la.kind == 36) { Get(); while (IsAttribute()) { @@ -1955,7 +2054,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, true, false); OldSemi(); - } else SynErr(170); + } else SynErr(172); } void FrameExpression(out FrameExpression fe, bool allowSemi, bool allowLambda) { @@ -1965,21 +2064,21 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo string fieldName = null; IToken feTok = null; fe = null; - if (StartOf(7)) { + if (StartOf(8)) { Expression(out e, allowSemi, allowLambda); feTok = e.tok; - if (la.kind == 91) { + if (la.kind == 92) { Get(); Ident(out id); fieldName = id.val; feTok = id; } fe = new FrameExpression(feTok, e, fieldName); - } else if (la.kind == 91) { + } else if (la.kind == 92) { Get(); Ident(out id); fieldName = id.val; fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); - } else SynErr(171); + } else SynErr(173); } void DecreasesList(List decreases, bool allowWildcard, bool allowLambda) { @@ -2034,7 +2133,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - while (!(StartOf(17))) {SynErr(172); Get();} + while (!(StartOf(18))) {SynErr(174); Get();} if (la.kind == 45) { Get(); Expression(out e, false, false); @@ -2050,7 +2149,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } OldSemi(); - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); Expression(out e, false, false); OldSemi(); @@ -2064,7 +2163,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(173); + } else SynErr(175); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -2081,9 +2180,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 57) { Get(); fe = new FrameExpression(t, new WildcardExpr(t), null); - } else if (StartOf(18)) { + } else if (StartOf(19)) { FrameExpression(out fe, allowSemi, false); - } else SynErr(174); + } else SynErr(176); } void PossiblyWildExpression(out Expression e, bool allowLambda) { @@ -2092,9 +2191,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 57) { Get(); e = new WildcardExpr(t); - } else if (StartOf(7)) { + } else if (StartOf(8)) { Expression(out e, false, allowLambda); - } else SynErr(175); + } else SynErr(177); } void Stmt(List/*!*/ ss) { @@ -2111,14 +2210,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(19))) {SynErr(176); Get();} + while (!(StartOf(20))) {SynErr(178); Get();} switch (la.kind) { case 46: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; } - case 101: { + case 102: { AssertStmt(out s); break; } @@ -2126,31 +2225,31 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); break; } - case 102: { + case 103: { PrintStmt(out s); break; } - case 1: case 2: case 3: case 4: case 8: case 10: case 19: case 20: case 23: case 50: case 131: case 132: case 133: case 134: case 135: case 136: { + case 1: case 2: case 3: case 4: case 8: case 10: case 19: case 20: case 23: case 50: case 132: case 133: case 134: case 135: case 136: case 137: { UpdateStmt(out s); break; } - case 73: case 78: { + case 62: case 79: { VarDeclStatement(out s); break; } - case 98: { + case 99: { IfStmt(out s); break; } - case 99: { + case 100: { WhileStmt(out s); break; } - case 100: { + case 101: { MatchStmt(out s); break; } - case 103: case 104: { + case 104: case 105: { ForallStmt(out s); break; } @@ -2158,11 +2257,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CalcStmt(out s); break; } - case 105: { + case 106: { ModifyStmt(out s); break; } - case 92: { + case 93: { Get(); x = t; NoUSIdent(out id); @@ -2171,24 +2270,24 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList