From b09206df1a298d56fca3bec95baab41b7f670731 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 7 Jan 2015 23:02:42 -0800
Subject: Added command-line switch /allowGlobals to simplify transition from
 language changes introduced in changeset c56031307ac1

---
 Source/Dafny/Dafny.atg       |  4 ++--
 Source/Dafny/DafnyAst.cs     |  2 +-
 Source/Dafny/DafnyOptions.cs | 11 +++++++++++
 Source/Dafny/Parser.cs       |  4 ++--
 4 files changed, 16 insertions(+), 5 deletions(-)

(limited to 'Source')

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;
 				}
 				}
-- 
cgit v1.2.3