Move changes made in Parser.cs to Dafny.atg

When fix issue #16, there are changed made to Parser.cs, which is
auto-generated from Dafny.atg. Therefore, the change should be moved to
Dafny.atg instead.

Source/Dafny/Dafny.atg

@@ -18,6 +18,7 @@ readonly Expression/*!*/ dummyExpr;
 readonly AssignmentRhs/*!*/ dummyRhs;
 readonly FrameExpression/*!*/ dummyFrameExpr; 
 readonly Statement/*!*/ dummyStmt;
+readonly Include theInclude;
 readonly ModuleDecl theModule;
 readonly BuiltIns theBuiltIns;
 readonly bool theVerifyThisFile;
@@ -138,17 +139,17 @@ static void EncodeExternAsAttribute(DeclModifierData dmod, ref Attributes attrs,
 /// Returns the number of parsing errors encountered.
 /// Note: first initialize the Scanner.
 ///</summary>
-public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ {
+public static int Parse (string/*!*/ filename, Include include, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ {
  Contract.Requires(filename != null);
  Contract.Requires(module != null);
  string s;
  if (filename == "stdin.dfy") {
  s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
- return Parse(s, filename, filename, module, builtIns, errors, verifyThisFile);
+ return Parse(s, filename, filename, include, module, builtIns, errors, verifyThisFile);
  } else {
  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
  s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
- return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);
+ return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, include, module, builtIns, errors, verifyThisFile);
  }
  }
 }
@@ -163,15 +164,15 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi
  Contract.Requires(filename != null);
  Contract.Requires(module != null);
  Errors errors = new Errors(reporter);
- return Parse(s, fullFilename, filename, module, builtIns, errors, verifyThisFile);
+ return Parse(s, fullFilename, filename, null, module, builtIns, errors, verifyThisFile);
 }
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members)
 /// and appends them in appropriate form to "module".
 /// Returns the number of parsing errors encountered.
 /// Note: first initialize the Scanner with the given Errors sink.
 ///</summary>
-public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module,
+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, Include include, ModuleDecl module,
  BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) {
  Contract.Requires(s != null);
  Contract.Requires(filename != null);
@@ -180,18 +181,19 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi
  byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
  MemoryStream ms = new MemoryStream(buffer,false);
  Scanner scanner = new Scanner(ms, errors, fullFilename, filename);
- Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile);
+ Parser parser = new Parser(scanner, errors, include, module, builtIns, verifyThisFile);
  parser.Parse();
  return parser.errors.ErrorCount;
 }
-public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, Include include, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
  : 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, Token.NoToken, null);
+ theInclude = include; // the "include" that includes this file
  theModule = module;
  theBuiltIns = builtIns;
  theVerifyThisFile = verifyThisFile;
@@ -1083,8 +1085,8 @@ NewtypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
  NoUSIdent<out bvId>
  [ ":" Type<out baseType> ] (. if (baseType == null) { baseType = new InferredTypeProxy(); } .)
  "|"
- Expression<out wh, false, true> (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
- | Type<out baseType> (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .)
+ Expression<out wh, false, true> (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
+ | Type<out baseType> (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)
  )
  .
 OtherTypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
@@ -1110,7 +1112,7 @@ OtherTypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl t
  [ ":" Type<out ty> ] (. if (ty == null) { ty = new InferredTypeProxy(); } .)
  "|"
  Expression<out constraint, false, true>
- (. td = new SubsetTypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs);
+ (. td = new SubsetTypeDecl(id, id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs);
  kind = "Subset type";
  .)
  |
@@ -1358,7 +1360,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, bool isWithinAbstractMo
  SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");
  }
 
- IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
+ IToken tok = id;
  if (isConstructor) {
  m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
  req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
@@ -1720,7 +1722,7 @@ FunctionDecl<DeclModifierData dmod, bool isWithinAbstractModule, out Function/*!
  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);
+ IToken tok = id;
  if (isTwoState && isPredicate) {
  f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals,
  reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);
@@ -2261,7 +2263,7 @@ ExistentialGuard<out Expression e, bool allowLambda>
  .
 MatchStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
+ IToken x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
  List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
  bool usesOptionalBraces = false;
  .)
@@ -2455,7 +2457,7 @@ ModifyStmt<out Statement s>
 
 CalcStmt<out Statement s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- Token x;
+ IToken x;
  Attributes attrs = null;
  CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
  var lines = new List<Expression>();