Added command-line switch /allowGlobals to simplify transition from language changes introduced in changeset c56031307ac1

4 files changed, 16 insertions, 5 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index e474f3aa..d6799290 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -486,7 +486,7 @@ Dafny
   | OtherTypeDecl<defaultModule, out td>        (. defaultModule.TopLevelDecls.Add(td); .)

   | IteratorDecl<defaultModule, out iter>       (. defaultModule.TopLevelDecls.Add(iter); .)

   | TraitDecl<defaultModule, out trait>    (. defaultModule.TopLevelDecls.Add(trait); .)

-  | ClassMemberDecl<membersDefaultClass, false, true>

+  | ClassMemberDecl<membersDefaultClass, false, !DafnyOptions.O.AllowGlobals>

   }

   (. // find the default class in the default module, then append membersDefaultClass to its member list

      DefaultClassDecl defaultClass = null;

@@ -529,7 +529,7 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
         | NewtypeDecl<module, out td>                  (. module.TopLevelDecls.Add(td); .)

         | OtherTypeDecl<module, out td>                (. module.TopLevelDecls.Add(td); .)

         | IteratorDecl<module, out iter>               (. module.TopLevelDecls.Add(iter); .)

-        | ClassMemberDecl<namedModuleDefaultClassMembers, false, true>

+        | ClassMemberDecl<namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals>

         }

       "}"                                  (. module.BodyEndTok = t;

                                               module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0b845c23..0742ee43 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2183,7 +2183,7 @@ namespace Microsoft.Dafny {
     public readonly bool HasStaticKeyword;

     public bool IsStatic {

       get {

-        return HasStaticKeyword || (EnclosingClass is ClassDecl && ((ClassDecl)EnclosingClass).IsDefaultClass);

+        return HasStaticKeyword || (!DafnyOptions.O.AllowGlobals && EnclosingClass is ClassDecl && ((ClassDecl)EnclosingClass).IsDefaultClass);

       }

     }

     public readonly bool IsGhost;

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 8c36ece9..1690455f 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -48,6 +48,7 @@ namespace Microsoft.Dafny
     public bool DisableNLarith = false;

     public string AutoReqPrintFile = null;

     public bool ignoreAutoReq = false;

+    public bool AllowGlobals = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -161,6 +162,10 @@ namespace Microsoft.Dafny
           ignoreAutoReq = true;

           return true;

 

+        case "allowGlobals":

+          AllowGlobals = true;

+          return true;

+

         default:

           break;

       }

@@ -240,6 +245,12 @@ namespace Microsoft.Dafny
   /autoReqPrint:<file>

                 Print out requirements that were automatically generated by autoReq.

   /noAutoReq    Ignore autoReq attributes

+  /allowGlobals Allow the implicit class '_default' to contain fields, instance functions,

+                and instance methods.  These class members are declared at the module scope,

+                outside of explicit classes.  This command-line option is provided to simply

+                a transition from the behavior in the language prior to version 1.9.3, from

+                which point onward all functions and methods declared at the module scope are

+                implicitly static and fields declarations are not allowed at the module scope.

 ");

       base.Usage();  // also print the Boogie options

     }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 15137923..12fc3c34 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -547,7 +547,7 @@ bool IsType(ref IToken pt) {
 				break;

 			}

 			case 64: case 65: case 68: case 74: case 75: case 76: case 77: case 78: case 82: case 83: case 84: {

-				ClassMemberDecl(membersDefaultClass, false, true);

+				ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals);

 				break;

 			}

 			}

@@ -634,7 +634,7 @@ bool IsType(ref IToken pt) {
 					break;

 				}

 				case 64: case 65: case 68: case 74: case 75: case 76: case 77: case 78: case 82: case 83: case 84: {

-					ClassMemberDecl(namedModuleDefaultClassMembers, false, true);

+					ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals);

 					break;

 				}

 				}