Dafny and Boogie: get rid of 'static' fields in parser

1 files changed, 23 insertions, 15 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 1629fe51..5280521f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -14,14 +14,15 @@ using System.IO;
 using System.Text;

 COMPILER Dafny

 /*--------------------------------------------------------------------------*/

-static ModuleDecl theModule;

-static BuiltIns theBuiltIns;

-static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

-static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);

-static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);

-static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

-static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");

-static int anonymousIds = 0;

+readonly Expression/*!*/ dummyExpr;

+readonly AssignmentRhs/*!*/ dummyRhs;

+readonly FrameExpression/*!*/ dummyFrameExpr;

+readonly Statement/*!*/ dummyStmt;

+readonly Attributes.Argument/*!*/ dummyAttrArg;

+readonly ModuleDecl theModule;

+readonly BuiltIns theBuiltIns;

+int anonymousIds = 0;

+

 struct MemberModifiers {

   public bool IsGhost;

   public bool IsStatic;

@@ -72,19 +73,26 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module,
   Contract.Requires(filename != null);

   Contract.Requires(module != null);

   Contract.Requires(errors != null);

-  var oldModule = theModule;

-  theModule = module;

-  BuiltIns oldBuiltIns = builtIns;

-  theBuiltIns = builtIns;

   byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

   Scanner scanner = new Scanner(ms, errors, filename);

-  Parser parser = new Parser(scanner, errors);

+  Parser parser = new Parser(scanner, errors, module, builtIns);

   parser.Parse();

-  theModule = oldModule;

-  theBuiltIns = oldBuiltIns;

   return parser.errors.count;

 }

+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns) 

+  : this(scanner, errors)  // the real work

+{

+  // initialize readonly fields

+  dummyExpr = new LiteralExpr(Token.NoToken);

+  dummyRhs = new ExprRhs(dummyExpr, null);

+  dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);

+  dummyStmt = new ReturnStmt(Token.NoToken, null);

+  dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");

+  theModule = module;

+  theBuiltIns = builtIns;

+}

+

 bool IsAttribute() {

   Token x = scanner.Peek();

   return la.kind == _lbrace && x.kind == _colon;