Updated the frame files to work with the latest Coco/R. This entails *not* having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories.

Lots of code changes to compensate for the new frame files.

11 files changed, 1528 insertions, 1496 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 7affe087..ca02d3cf 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -12,6 +12,8 @@
 using System.Collections.Generic;

 using System.Numerics;

 using Microsoft.Boogie;

+using System.IO;

+using System.Text;

 

 

 COMPILER Dafny

@@ -64,15 +66,14 @@ private static Expression! ConvertToLocal(Expression! e)
 /// Note: first initialize the Scanner.

 ///</summary>

 public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws System.IO.IOException */ {

+  string s;

   if (filename == "stdin.dfy") {

-    BoogiePL.Buffer.Fill(System.Console.In);

-    Scanner.Init(filename);

-    return Parse(modules);

+    s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string!>());

+    return Parse(s, modules);

   } else {

     using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

-      BoogiePL.Buffer.Fill(reader);

-      Scanner.Init(filename);

-      return Parse(modules);

+      s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string!>());

+      return Parse(s, filename, modules);

     }

   }

 }

@@ -83,12 +84,17 @@ public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (List<ModuleDecl!>! modules) {

+public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules) {

   List<ModuleDecl!> oldModules = theModules;

   theModules = modules;

-  Parse();

+  byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s);

+  MemoryStream ms = new MemoryStream(buffer,false);

+  Errors errors = new Errors();

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

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

+  parser.Parse();

   theModules = oldModules;

-  return Errors.count;

+  return parser.errors.count;

 }

 

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

@@ -126,7 +132,7 @@ PRODUCTIONS
 

 Dafny

 = (. ClassDecl! c; DatatypeDecl! dt;

-     Attributes attrs;  Token! id;  List<string!> theImports;

+     Attributes attrs;  IToken! id;  List<string!> theImports;

 

      List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();

      ModuleDecl module;

@@ -174,7 +180,7 @@ Dafny
   .

 

 ClassDecl<ModuleDecl! module, out ClassDecl! c>

-= (. Token! id;

+= (. IToken! id;

      Attributes attrs = null;

      List<TypeParameter!> typeArgs = new List<TypeParameter!>();

      List<MemberDecl!> members = new List<MemberDecl!>();

@@ -189,7 +195,7 @@ ClassDecl<ModuleDecl! module, out ClassDecl! c>
   "}"                                      (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); .)

   .

 

-ClassMemberDecl<List<MemberDecl!\>! mm>

+ClassMemberDecl<.List<MemberDecl!>! mm.>

 = (. Method! m;

      Function! f;

      MemberModifiers mmod = new MemberModifiers();

@@ -205,7 +211,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm>
   .

 

 DatatypeDecl<ModuleDecl! module, out DatatypeDecl! dt>

-= (. Token! id;

+= (. IToken! id;

      Attributes attrs = null;

      List<TypeParameter!> typeArgs = new List<TypeParameter!>();

      List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();

@@ -220,9 +226,9 @@ DatatypeDecl<ModuleDecl! module, out DatatypeDecl! dt>
   "}"                                      (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); .)

   .

 

-DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>

+DatatypeMemberDecl<.List<DatatypeCtor!>! ctors.>

 = (. Attributes attrs = null;

-     Token! id;

+     IToken! id;

      List<TypeParameter!> typeArgs = new List<TypeParameter!>();

      List<Formal!> formals = new List<Formal!>();

   .)

@@ -237,13 +243,13 @@ DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>
   ";"

   .

 

-FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>

+FieldDecl<.MemberModifiers mmod, List<MemberDecl!>! mm.>

 = (. Attributes attrs = null;

-     Token! id;  Type! ty;

+     IToken! id;  Type! ty;

   .)

   "var"

-  (. if (mmod.IsUnlimited) { SemErr(token, "fields cannot be declared 'unlimited'"); }

-     if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }

+  (. if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }

+     if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

   .)

   { Attribute<ref attrs> }

   IdentType<out id, out ty>                         (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)

@@ -252,22 +258,22 @@ FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>
   ";"

   .

 

-GIdentType<bool allowGhost, out Token! id, out Type! ty, out bool isGhost>

+GIdentType<bool allowGhost, out IToken! id, out Type! ty, out bool isGhost>

 /* isGhost always returns as false if allowGhost is false */

 = (. isGhost = false; .)

-  [ "ghost"                    (. if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); } .)

+  [ "ghost"                    (. if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)

   ]

   IdentType<out id, out ty>

   .

 

-IdentType<out Token! id, out Type! ty>

+IdentType<out IToken! id, out Type! ty>

 = Ident<out id>

   ":"

   Type<out ty>

   .

 

 IdentTypeOptional<out BoundVar! var>

-= (. Token! id;  Type! ty;  Type optType = null;

+= (. IToken! id;  Type! ty;  Type optType = null;

   .)

   Ident<out id>

   [ ":" Type<out ty>             (. optType = ty; .)

@@ -275,7 +281,7 @@ IdentTypeOptional<out BoundVar! var>
   (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)

   .

 

-TypeIdentOptional<out Token! id, out string! identName, out Type! ty, out bool isGhost>

+TypeIdentOptional<out IToken! id, out string! identName, out Type! ty, out bool isGhost>

 = (. string name = null;  isGhost = false; .)

   [ "ghost"                            (. isGhost = true; .)

   ]

@@ -301,8 +307,8 @@ TypeIdentOptional<out Token! id, out string! identName, out Type! ty, out bool i
 

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

 

-GenericParameters<List<TypeParameter!\>! typeArgs>

-= (. Token! id; .)

+GenericParameters<.List<TypeParameter!>! typeArgs.>

+= (. IToken! id; .)

   "<"

   Ident<out id>                       (. typeArgs.Add(new TypeParameter(id, id.val)); .)

   { "," Ident<out id>                 (. typeArgs.Add(new TypeParameter(id, id.val)); .)

@@ -313,7 +319,7 @@ GenericParameters<List<TypeParameter!\>! typeArgs>
 /*------------------------------------------------------------------------*/

 

 MethodDecl<MemberModifiers mmod, out Method! m>

-= (. Token! id;

+= (. IToken! id;

      Attributes attrs = null;

      List<TypeParameter!>! typeArgs = new List<TypeParameter!>();

      List<Formal!> ins = new List<Formal!>();

@@ -325,7 +331,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
      Statement! bb;  BlockStmt body = null;

   .)

   "method"

-  (. if (mmod.IsUnlimited) { SemErr(token, "methods cannot be declared 'unlimited'"); }

+  (. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

   .)

   { Attribute<ref attrs> }

   Ident<out id>

@@ -345,8 +351,8 @@ MethodDecl<MemberModifiers mmod, out Method! m>
   .)

   .

 

-MethodSpec<List<MaybeFreeExpression!\>! req, List<FrameExpression!\>! mod, List<MaybeFreeExpression!\>! ens,

-           List<Expression!\>! decreases>

+MethodSpec<.List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,

+           List<Expression!>! decreases.>

 = (. Expression! e;  FrameExpression! fe;  bool isFree = false;

   .)

   ( "modifies" [ FrameExpression<out fe>                     (. mod.Add(fe); .)

@@ -362,8 +368,8 @@ MethodSpec<List<MaybeFreeExpression!\>! req, List<FrameExpression!\>! mod, List<
   )

   .

 

-Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals> 

-= (. Token! id;  Type! ty;  bool isGhost; .)

+Formals<.bool incoming, bool allowGhosts, List<Formal!>! formals.> 

+= (. IToken! id;  Type! ty;  bool isGhost; .)

   "("

   [

     GIdentType<allowGhosts, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); .)

@@ -373,8 +379,8 @@ Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals>
   ")"

   .

 

-FormalsOptionalIds<List<Formal!\>! formals> 

-= (. Token! id;  Type! ty;  string! name;  bool isGhost; .)

+FormalsOptionalIds<.List<Formal!>! formals.> 

+= (. IToken! id;  Type! ty;  string! name;  bool isGhost; .)

   "("

   [

     TypeIdentOptional<out id, out name, out ty, out isGhost>        (. formals.Add(new Formal(id, name, ty, true, isGhost));  parseVarScope.Push(name, name); .)

@@ -387,24 +393,24 @@ FormalsOptionalIds<List<Formal!\>! formals>
 /*------------------------------------------------------------------------*/

 

 Type<out Type! ty>

-= (. Token! tok; .)

+= (. IToken! tok; .)

   TypeAndToken<out tok, out ty>

   .

 

-TypeAndToken<out Token! tok, out Type! ty>

+TypeAndToken<out IToken! tok, out Type! ty>

 = (. tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

      List<Type!>! gt;

   .)

-  ( "bool"                          (. tok = token; .)

-  | "int"                           (. tok = token;  ty = new IntType(); .)

-  | "set"                           (. tok = token;  gt = new List<Type!>(); .)

+  ( "bool"                          (. tok = t; .)

+  | "int"                           (. tok = t;  ty = new IntType(); .)

+  | "set"                           (. tok = t;  gt = new List<Type!>(); .)

     GenericInstantiation<gt>        (. if (gt.Count != 1) {

                                          SemErr("set type expects exactly one type argument");

                                        }

                                        ty = new SetType(gt[0]);

                                     .)

     

-  | "seq"                           (. tok = token;  gt = new List<Type!>(); .)

+  | "seq"                           (. tok = t;  gt = new List<Type!>(); .)

     GenericInstantiation<gt>        (. if (gt.Count != 1) {

                                          SemErr("seq type expects exactly one type argument");

                                        }

@@ -414,12 +420,12 @@ TypeAndToken<out Token! tok, out Type! ty>
   )

   .

 

-ReferenceType<out Token! tok, out Type! ty>

+ReferenceType<out IToken! tok, out Type! ty>

 = (. tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

      List<Type!>! gt;

   .)

-  ( "object"                        (. tok = token;  ty = new ObjectType(); .)

-  | "array"                         (. tok = token;  gt = new List<Type!>(); .)

+  ( "object"                        (. tok = t;  ty = new ObjectType(); .)

+  | "array"                         (. tok = t;  gt = new List<Type!>(); .)

     GenericInstantiation<gt>        (. if (gt.Count != 1) {

                                          SemErr("array type expects exactly one type argument");

                                        }

@@ -430,7 +436,7 @@ ReferenceType<out Token! tok, out Type! ty>
   )

   .

 

-GenericInstantiation<List<Type!\>! gt>

+GenericInstantiation<.List<Type!>! gt.>

 = (. Type! ty; .)

   "<"

     Type<out ty>                     (. gt.Add(ty); .)

@@ -443,7 +449,7 @@ GenericInstantiation<List<Type!\>! gt>
 

 FunctionDecl<MemberModifiers mmod, out Function! f>

 = (. Attributes attrs = null;

-     Token! id;

+     IToken! id;

      List<TypeParameter!> typeArgs = new List<TypeParameter!>();

      List<Formal!> formals = new List<Formal!>();

      Type! returnType;

@@ -456,7 +462,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f>
   "function"

   [ "method"                 (. isFunctionMethod = true; .)

   ]

-  (. if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); }

+  (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }

   .)

   { Attribute<ref attrs> }

   Ident<out id> 

@@ -475,7 +481,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f>
   .)

   .

 

-FunctionSpec<List<Expression!\>! reqs, List<FrameExpression!\>! reads, List<Expression!\>! decreases>

+FunctionSpec<.List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases.>

 = (. Expression! e;  FrameExpression! fe; .)

   ( "requires" Expression<out e> ";"      (. reqs.Add(e); .)

   | "reads" [ PossiblyWildFrameExpression<out fe>              (. reads.Add(fe); .)

@@ -491,7 +497,7 @@ PossiblyWildExpression<out Expression! e>
   /* A decreases clause on a loop asks that no termination check be performed.

    * Use of this feature is sound only with respect to partial correctness.

    */

-  ( "*"                        (. e = new WildcardExpr(token); .)

+  ( "*"                        (. e = new WildcardExpr(t); .)

   | Expression<out e>

   )

   .

@@ -504,13 +510,13 @@ PossiblyWildFrameExpression<out FrameExpression! fe>
    * any use of the function.  Nevertheless, as an experimental feature, the

    * language allows it (and it is sound).

    */

-  ( "*"                        (. fe = new FrameExpression(new WildcardExpr(token), null); .)

+  ( "*"                        (. fe = new FrameExpression(new WildcardExpr(t), null); .)

   | FrameExpression<out fe>

   )

   .

 

 FrameExpression<out FrameExpression! fe>

-= (. Expression! e;  Token! id;  string fieldName = null; .)

+= (. Expression! e;  IToken! id;  string fieldName = null; .)

   Expression<out e>

   [ "`" Ident<out id>        (. fieldName = id.val; .)

   ]

@@ -527,10 +533,10 @@ FunctionBody<out Expression! e>
   .

   

 MatchExpression<out Expression! e>

-= (. Token! x;  MatchCaseExpr! c;

+= (. IToken! x;  MatchCaseExpr! c;

      List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();

   .)

-  "match"                     (. x = token; .)

+  "match"                     (. x = t; .)

   Expression<out e>

   { CaseExpression<out c>     (. cases.Add(c); .)

   }

@@ -538,11 +544,11 @@ MatchExpression<out Expression! e>
   .

 

 CaseExpression<out MatchCaseExpr! c>

-= (. Token! x, id, arg;

+= (. IToken! x, id, arg;

      List<BoundVar!> arguments = new List<BoundVar!>();

      Expression! body;

   .)

-  "case"                      (. x = token;  parseVarScope.PushMarker(); .)

+  "case"                      (. x = t;  parseVarScope.PushMarker(); .)

   Ident<out id>

   [ "("

     Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

@@ -559,19 +565,19 @@ CaseExpression<out MatchCaseExpr! c>
 /*------------------------------------------------------------------------*/

 

 BlockStmt<out Statement! block>

-= (. Token! x;

+= (. IToken! x;

      List<Statement!> body = new List<Statement!>();

      Statement! s;

   .)

   (. parseVarScope.PushMarker(); .)

-  "{"                                  (. x = token; .)

+  "{"                                  (. x = t; .)

   { Stmt<body>

   }

   "}"                                  (. block = new BlockStmt(x, body); .)

   (. parseVarScope.PopMarker(); .)

   .

 

-Stmt<List<Statement!\>! ss>

+Stmt<.List<Statement!>! ss.>

 = (. Statement! s; .)

   /* By first reading a sequence of block statements, we avoid problems in the generated parser, despite

      the ambiguity in the grammar.  See Note in ConstAtomExpression production.

@@ -584,7 +590,7 @@ Stmt<List<Statement!\>! ss>
   .

 

 OneStmt<out Statement! s>

-= (. Token! x;  Token! id;  string label = null;

+= (. IToken! x;  IToken! id;  string label = null;

      s = dummyStmt;  /* to please the compiler */

   .)

   /* This list does not contain BlockStmt, see comment above in Stmt production. */

@@ -599,25 +605,25 @@ OneStmt<out Statement! s>
   | WhileStmt<out s>

   | MatchStmt<out s>

   | ForeachStmt<out s>

-  | "label"                            (. x = token; .)

+  | "label"                            (. x = t; .)

     Ident<out id> ":"                  (. s = new LabelStmt(x, id.val); .)

-  | "break"                            (. x = token; .)

+  | "break"                            (. x = t; .)

     [ Ident<out id>                    (. label = id.val; .)

     ] ";"                              (. s = new BreakStmt(x, label); .)

-  | "return"                           (. x = token; .)

+  | "return"                           (. x = t; .)

     ";"                                (. s = new ReturnStmt(x); .)

   )

   .

 

 AssignStmt<out Statement! s>

-= (. Token! x;

+= (. IToken! x;

      Expression! lhs;

      Expression rhs;

      Type ty;

      s = dummyStmt;

   .)

   LhsExpr<out lhs>

-  ":="                                 (. x = token; .)

+  ":="                                 (. x = t; .)

   AssignRhs<out rhs, out ty>           (. if (ty == null) {

                                             assert rhs != null;

                                             s = new AssignStmt(x, lhs, rhs);

@@ -632,7 +638,7 @@ AssignStmt<out Statement! s>
 

 AssignRhs<out Expression e, out Type ty>

 /* ensures e != null || ty != null; */

-= (. Token! x;  Expression! ee;  Type! tt;

+= (. IToken! x;  Expression! ee;  Type! tt;

      e = null;  ty = null;

   .)

   ( "new" TypeAndToken<out x, out tt>  (. ty = tt; .)

@@ -643,8 +649,8 @@ AssignRhs<out Expression e, out Type ty>
   .

 

 HavocStmt<out Statement! s>

-= (. Token! x;  Expression! lhs; .)

-  "havoc"                              (. x = token; .)

+= (. IToken! x;  Expression! lhs; .)

+  "havoc"                              (. x = t; .)

   LhsExpr<out lhs> ";"                 (. s = new AssignStmt(x, lhs); .)

   .

 

@@ -652,7 +658,7 @@ LhsExpr<out Expression! e>
 = SelectExpression<out e>

   .

 

-VarDeclStmts<List<Statement!\>! ss>

+VarDeclStmts<.List<Statement!>! ss.>

 = (. VarDecl! d;  bool isGhost = false; .)

   [ "ghost"                            (. isGhost = true; .)

   ]

@@ -664,7 +670,7 @@ VarDeclStmts<List<Statement!\>! ss>
   .

 

 IdentTypeRhs<out VarDecl! d, bool isGhost>

-= (. Token! id;  Type! ty;  Expression! e;

+= (. IToken! id;  Type! ty;  Expression! e;

      Expression rhs = null;  Type newType = null;

      Type optionalType = null;  DeterminedAssignmentRhs optionalRhs = null;

   .)

@@ -690,13 +696,13 @@ IdentTypeRhs<out VarDecl! d, bool isGhost>
   .

 

 IfStmt<out Statement! ifStmt>

-= (. Token! x;

+= (. IToken! x;

      Expression guard;

      Statement! thn;

      Statement! s;

      Statement els = null;

   .)

-  "if"                       (. x = token; .)

+  "if"                       (. x = t; .)

   Guard<out guard>

   BlockStmt<out thn>

   [ "else"

@@ -708,14 +714,14 @@ IfStmt<out Statement! ifStmt>
   .

 

 WhileStmt<out Statement! stmt>

-= (. Token! x;

+= (. IToken! x;

      Expression guard;

      bool isFree;  Expression! e;

      List<MaybeFreeExpression!> invariants = new List<MaybeFreeExpression!>();

      List<Expression!> decreases = new List<Expression!>();

      Statement! body;

   .)

-  "while"                    (. x = token; .)

+  "while"                    (. x = t; .)

   Guard<out guard>           (. assume guard == null || Owner.None(guard); .)

   {                          (. isFree = false; .)

      [ "free"                (. isFree = true; .)

@@ -744,7 +750,7 @@ Guard<out Expression e>   /* null represents demonic-choice */
 MatchStmt<out Statement! s>

 = (. Token x;  Expression! e;  MatchCaseStmt! c;

      List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>(); .)

-  "match"                     (. x = token; .)

+  "match"                     (. x = t; .)

   Expression<out e>

   "{"

   { CaseStatement<out c>     (. cases.Add(c); .)

@@ -754,11 +760,11 @@ MatchStmt<out Statement! s>
   .

 

 CaseStatement<out MatchCaseStmt! c>

-= (. Token! x, id, arg;

+= (. IToken! x, id, arg;

      List<BoundVar!> arguments = new List<BoundVar!>();

      List<Statement!> body = new List<Statement!>();

   .)

-  "case"                      (. x = token;  parseVarScope.PushMarker(); .)

+  "case"                      (. x = t;  parseVarScope.PushMarker(); .)

   Ident<out id>

   [ "("

     Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

@@ -776,12 +782,12 @@ CaseStatement<out MatchCaseStmt! c>
   .

 

 CallStmt<out Statement! s>

-= (. Token! x, id;

+= (. IToken! x, id;

      Expression! e;

      List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

      List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();

   .)

-  "call"                       (. x = token; .)

+  "call"                       (. x = t; .)

   CallStmtSubExpr<out e>

   

   [ ","                        /* call a,b,c,... := ... */

@@ -829,7 +835,7 @@ CallStmt<out Statement! s>
 /*------------------------------------------------------------------------*/

 

 ForeachStmt<out Statement! s>

-= (. Token! x, boundVar;

+= (. IToken! x, boundVar;

      Type! ty;

      Expression! collection;

      Expression! range;

@@ -837,7 +843,7 @@ ForeachStmt<out Statement! s>
      AssignStmt bodyAssign = null;

   .)

   (. parseVarScope.PushMarker(); .)

-  "foreach"                                    (. x = token;

+  "foreach"                                    (. x = t;

                                                   range = new LiteralExpr(x, true);

                                                   ty = new InferredTypeProxy();

                                                .)

@@ -865,28 +871,28 @@ ForeachStmt<out Statement! s>
   .

 

 AssertStmt<out Statement! s>

-= (. Token! x;  Expression! e; .)

-  "assert"                                     (. x = token; .)

+= (. IToken! x;  Expression! e; .)

+  "assert"                                     (. x = t; .)

   Expression<out e> ";"                        (. s = new AssertStmt(x, e); .)

   .

 

 AssumeStmt<out Statement! s>

-= (. Token! x;  Expression! e; .)

-  "assume"                                     (. x = token; .)

+= (. IToken! x;  Expression! e; .)

+  "assume"                                     (. x = t; .)

   Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)

   .

 

 UseStmt<out Statement! s>

-= (. Token! x;  Expression! e; .)

-  "use"                                        (. x = token; .)

+= (. IToken! x;  Expression! e; .)

+  "use"                                        (. x = t; .)

   Expression<out e> ";"                        (. s = new UseStmt(x, e); .)

   .

 

 PrintStmt<out Statement! s>

-= (. Token! x;  Attributes.Argument! arg;

+= (. IToken! x;  Attributes.Argument! arg;

      List<Attributes.Argument!> args = new List<Attributes.Argument!>();

   .)

-  "print"                                      (. x = token; .)

+  "print"                                      (. x = t; .)

   AttributeArg<out arg>                        (. args.Add(arg); .)

   { "," AttributeArg<out arg>                  (. args.Add(arg); .)

   }

@@ -895,10 +901,10 @@ PrintStmt<out Statement! s>
 

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

 Expression<out Expression! e>

-= (. Token! x;  Expression! e0;  Expression! e1 = dummyExpr;

+= (. IToken! x;  Expression! e0;  Expression! e1 = dummyExpr;

      e = dummyExpr;

   .)

-  ( "if"                               (. x = token; .)

+  ( "if"                               (. x = t; .)

     Expression<out e>

     "then" Expression<out e0>

     "else" Expression<out e1>          (. e = new ITEExpr(x, e, e0, e1); .)

@@ -908,9 +914,9 @@ Expression<out Expression! e>
 

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

 EquivExpression<out Expression! e0>

-= (. Token! x;  Expression! e1; .)

+= (. IToken! x;  Expression! e1; .)

   ImpliesExpression<out e0>

-  { EquivOp                                    (. x = token; .)

+  { EquivOp                                    (. x = t; .)

     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)

   }

   .

@@ -919,9 +925,9 @@ EquivOp = "<==>" | '\u21d4'.
 

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

 ImpliesExpression<out Expression! e0>

-= (. Token! x;  Expression! e1; .)

+= (. IToken! x;  Expression! e1; .)

   LogicalExpression<out e0>

-  [ ImpliesOp                                  (. x = token; .)

+  [ ImpliesOp                                  (. x = t; .)

     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

   ]

   .

@@ -930,16 +936,16 @@ ImpliesOp = "==>" | '\u21d2'.
 

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

 LogicalExpression<out Expression! e0>

-= (. Token! x;  Expression! e1; .)

+= (. IToken! x;  Expression! e1; .)

   RelationalExpression<out e0>

-  [ AndOp                                      (. x = token; .)

+  [ AndOp                                      (. x = t; .)

     RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)

-    { AndOp                                    (. x = token; .)

+    { AndOp                                    (. x = t; .)

       RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)

     }

-  | OrOp                                       (. x = token; .)

+  | OrOp                                       (. x = t; .)

     RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)

-    { OrOp                                     (. x = token; .)

+    { OrOp                                     (. x = t; .)

       RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)

     }

   ]

@@ -950,69 +956,69 @@ OrOp = "||" | '\u2228'.
 

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

 RelationalExpression<out Expression! e0>

-= (. Token! x;  Expression! e1;  BinaryExpr.Opcode op; .)

+= (. IToken! x;  Expression! e1;  BinaryExpr.Opcode op; .)

   Term<out e0>

   [ RelOp<out x, out op>

     Term<out e1>                               (. e0 = new BinaryExpr(x, op, e0, e1); .)

   ]

   .

 

-RelOp<out Token! x, out BinaryExpr.Opcode op>

+RelOp<out IToken! x, out BinaryExpr.Opcode op>

 =                  (. x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)

-  ( "=="           (. x = token;  op = BinaryExpr.Opcode.Eq; .)

-  | "<"            (. x = token;  op = BinaryExpr.Opcode.Lt; .)

-  | ">"            (. x = token;  op = BinaryExpr.Opcode.Gt; .)

-  | "<="           (. x = token;  op = BinaryExpr.Opcode.Le; .)

-  | ">="           (. x = token;  op = BinaryExpr.Opcode.Ge; .)

-  | "!="           (. x = token;  op = BinaryExpr.Opcode.Neq; .)

-  | "!!"           (. x = token;  op = BinaryExpr.Opcode.Disjoint; .)

-  | "in"           (. x = token;  op = BinaryExpr.Opcode.In; .)

-  | "!in"          (. x = token;  op = BinaryExpr.Opcode.NotIn; .)

-  | '\u2260'       (. x = token;  op = BinaryExpr.Opcode.Neq; .)

-  | '\u2264'       (. x = token;  op = BinaryExpr.Opcode.Le; .)

-  | '\u2265'       (. x = token;  op = BinaryExpr.Opcode.Ge; .)

+  ( "=="           (. x = t;  op = BinaryExpr.Opcode.Eq; .)

+  | "<"            (. x = t;  op = BinaryExpr.Opcode.Lt; .)

+  | ">"            (. x = t;  op = BinaryExpr.Opcode.Gt; .)

+  | "<="           (. x = t;  op = BinaryExpr.Opcode.Le; .)

+  | ">="           (. x = t;  op = BinaryExpr.Opcode.Ge; .)

+  | "!="           (. x = t;  op = BinaryExpr.Opcode.Neq; .)

+  | "!!"           (. x = t;  op = BinaryExpr.Opcode.Disjoint; .)

+  | "in"           (. x = t;  op = BinaryExpr.Opcode.In; .)

+  | "!in"          (. x = t;  op = BinaryExpr.Opcode.NotIn; .)

+  | '\u2260'       (. x = t;  op = BinaryExpr.Opcode.Neq; .)

+  | '\u2264'       (. x = t;  op = BinaryExpr.Opcode.Le; .)

+  | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)

   )

   .

 

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

 Term<out Expression! e0>

-= (. Token! x;  Expression! e1;  BinaryExpr.Opcode op; .)

+= (. IToken! x;  Expression! e1;  BinaryExpr.Opcode op; .)

   Factor<out e0>

   { AddOp<out x, out op>

     Factor<out e1>                             (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

 

-AddOp<out Token! x, out BinaryExpr.Opcode op>

+AddOp<out IToken! x, out BinaryExpr.Opcode op>

 =                  (. x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; .)

-  ( "+"            (. x = token;  op = BinaryExpr.Opcode.Add; .)

-  | "-"            (. x = token;  op = BinaryExpr.Opcode.Sub; .)

+  ( "+"            (. x = t;  op = BinaryExpr.Opcode.Add; .)

+  | "-"            (. x = t;  op = BinaryExpr.Opcode.Sub; .)

   )

   .

 

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

 Factor<out Expression! e0>

-= (. Token! x;  Expression! e1;  BinaryExpr.Opcode op; .)

+= (. IToken! x;  Expression! e1;  BinaryExpr.Opcode op; .)

   UnaryExpression<out e0>

   { MulOp<out x, out op>

     UnaryExpression<out e1>                    (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

 

-MulOp<out Token! x, out BinaryExpr.Opcode op>

+MulOp<out IToken! x, out BinaryExpr.Opcode op>

 =                  (. x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)

-  ( "*"            (. x = token;  op = BinaryExpr.Opcode.Mul; .)

-  | "/"            (. x = token;  op = BinaryExpr.Opcode.Div; .)

-  | "%"            (. x = token;  op = BinaryExpr.Opcode.Mod; .)

+  ( "*"            (. x = t;  op = BinaryExpr.Opcode.Mul; .)

+  | "/"            (. x = t;  op = BinaryExpr.Opcode.Div; .)

+  | "%"            (. x = t;  op = BinaryExpr.Opcode.Mod; .)

   )

   .

 

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

 UnaryExpression<out Expression! e>

-= (. Token! x;  e = dummyExpr; .)

-  ( "-"                                        (. x = token; .)

+= (. IToken! x;  e = dummyExpr; .)

+  ( "-"                                        (. x = t; .)

     UnaryExpression<out e>                     (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)

-  | NegOp                                      (. x = token; .)

+  | NegOp                                      (. x = t; .)

     UnaryExpression<out e>                     (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)

   | SelectExpression<out e>

   | ConstAtomExpression<out e>

@@ -1022,29 +1028,29 @@ UnaryExpression<out Expression! e>
 NegOp = "!" | '\u00ac'.

 

 ConstAtomExpression<out Expression! e>            

-= (. Token! x, dtName, id;  BigInteger n;  List<Expression!>! elements;

+= (. IToken! x, dtName, id;  BigInteger n;  List<Expression!>! elements;

      e = dummyExpr;  

   .)

-  ( "false"                                    (. e = new LiteralExpr(token, false); .)

-  | "true"                                     (. e = new LiteralExpr(token, true); .)

-  | "null"                                     (. e = new LiteralExpr(token); .)

-  | Nat<out n>                                 (. e = new LiteralExpr(token, n); .)

-  | "#"                                        (. x = token; .)

+  ( "false"                                    (. e = new LiteralExpr(t, false); .)

+  | "true"                                     (. e = new LiteralExpr(t, true); .)

+  | "null"                                     (. e = new LiteralExpr(t); .)

+  | Nat<out n>                                 (. e = new LiteralExpr(t, n); .)

+  | "#"                                        (. x = t; .)

     Ident<out dtName>

     "."

     Ident<out id>                              (. elements = new List<Expression!>(); .)

     [ "("

       [ Expressions<elements> ]

-    ")" ]                                      (. e = new DatatypeValue(token, dtName.val, id.val, elements); .)

-  | "fresh"                                    (. x = token; .)

+    ")" ]                                      (. e = new DatatypeValue(t, dtName.val, id.val, elements); .)

+  | "fresh"                                    (. x = t; .)

     "(" Expression<out e> ")"                  (. e = new FreshExpr(x, e); .)

-  | "|"                                        (. x = token; .)

+  | "|"                                        (. x = t; .)

       Expression<out e>                        (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

     "|"

-  | "{"                                        (. x = token;  elements = new List<Expression!>(); .)

+  | "{"                                        (. x = t;  elements = new List<Expression!>(); .)

       [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, elements); .)

     "}"

-  | "["                                        (. x = token;  elements = new List<Expression!>(); .)

+  | "["                                        (. x = t;  elements = new List<Expression!>(); .)

       [ Expressions<elements> ]                (. e = new SeqDisplayExpr(x, elements); .)

     "]"

   )

@@ -1067,7 +1073,7 @@ CallStmtSubExpr<out Expression! e>
   .

 

 SelectExpression<out Expression! e>

-= (. Token! id;  e = dummyExpr; .)

+= (. IToken! id;  e = dummyExpr; .)

   ( IdentOrFuncExpression<out e>

   | ObjectExpression<out e>

   )

@@ -1075,7 +1081,7 @@ SelectExpression<out Expression! e>
   .

 

 IdentOrFuncExpression<out Expression! e>

-= (. Token! id;  e = dummyExpr;  List<Expression!>! args; .)

+= (. IToken! id;  e = dummyExpr;  List<Expression!>! args; .)

   Ident<out id>

   [ "("                                      (. args = new List<Expression!>(); .)

       [ Expressions<args> ]

@@ -1091,7 +1097,7 @@ IdentOrFuncExpression<out Expression! e>
   .

 

 SelectOrCallSuffix<ref Expression! e>

-= (. Token! id, x;  List<Expression!>! args;

+= (. IToken! id, x;  List<Expression!>! args;

      Expression e0 = null;  Expression e1 = null;  Expression! ee;  bool anyDots = false;

      bool func = false;

   .)

@@ -1102,7 +1108,7 @@ SelectOrCallSuffix<ref Expression! e>
       ")"                                      (. e = new FunctionCallExpr(id, id.val, e, args); .)

     ]                                          (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)

     

-  | "["                                        (. x = token; .)

+  | "["                                        (. x = t; .)

       ( Expression<out ee>                     (. e0 = ee; .)

         [ ".."                                 (. anyDots = true; .)

           [ Expression<out ee>                 (. e1 = ee; .)

@@ -1136,9 +1142,9 @@ SelectOrCallSuffix<ref Expression! e>
    parsed here.  The expression returned is never an lvalue.

 */

 ObjectExpression<out Expression! e>

-= (. Token! x;  e = dummyExpr; .)

-  ( "this"                                     (. e = new ThisExpr(token); .)

-  | "old"                                      (. x = token; .)

+= (. IToken! x;  e = dummyExpr; .)

+  ( "this"                                     (. e = new ThisExpr(t); .)

+  | "old"                                      (. x = t; .)

     "("

       Expression<out e>

     ")"                                        (. e = new OldExpr(x, e); .)

@@ -1152,17 +1158,17 @@ ObjectExpression<out Expression! e>
 /*------------------------------------------------------------------------*/

 

 QuantifierGuts<out Expression! q>

-= (. Token! x = Token.NoToken;

+= (. IToken! x = Token.NoToken;

      bool univ = false;

      BoundVar! bv;

      List<BoundVar!> bvars = new List<BoundVar!>();

-     Token! tok;  Expr! e;  ExprSeq! es;

+     IToken! tok;  Expr! e;  ExprSeq! es;

      Attributes attrs = null;

      Triggers trigs = null;

      Expression! body;

   .)

-  ( Forall                                     (. x = token;  univ = true; .)

-  | Exists                                     (. x = token; .)

+  ( Forall                                     (. x = t;  univ = true; .)

+  | Exists                                     (. x = t; .)

   )

   (. parseVarScope.PushMarker(); .)

   IdentTypeOptional<out bv>                    (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)

@@ -1185,7 +1191,7 @@ Forall = "forall" | '\u2200'.
 Exists = "exists" | '\u2203'.

 QSep = "::" | '\u2022'.

 

-Expressions<List<Expression!\>! args>

+Expressions<.List<Expression!>! args.>

 = (. Expression! e; .)

   Expression<out e>                            (. args.Add(e); .)

   { "," Expression<out e>                      (. args.Add(e); .)

@@ -1205,7 +1211,7 @@ AttributeBody<ref Attributes attrs>
      List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();

      Attributes.Argument! aArg;

   .)

-  ":" ident                            (. aName = token.val; .)

+  ":" ident                            (. aName = t.val; .)

   [ AttributeArg<out aArg>             (. aArgs.Add(aArg); .)

     { "," AttributeArg<out aArg>       (. aArgs.Add(aArg); .)

     }

@@ -1214,7 +1220,7 @@ AttributeBody<ref Attributes attrs>
 

 AttributeArg<out Attributes.Argument! arg>

 = (. Expression! e;  arg = dummyAttrArg; .)

-  ( string                             (. arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2)); .)

+  ( string                             (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)

   | Expression<out e>                  (. arg = new Attributes.Argument(e); .)

   )

   .

@@ -1232,23 +1238,23 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
 

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

 

-Idents<List<string!\>! ids>

-= (. Token! id; .)

+Idents<.List<string!>! ids.>

+= (. IToken! id; .)

   Ident<out id>                            (. ids.Add(id.val); .)

   { "," Ident<out id>                      (. ids.Add(id.val); .)

   }

   .

 

-Ident<out Token! x>

+Ident<out IToken! x>

 =

-  ident            (. x = token; .)

+  ident            (. x = t; .)

   .                                  

 

 Nat<out BigInteger n>

 =

   digits

   (. try {

-       n = BigInteger.Parse(token.val);

+       n = BigInteger.Parse(t.val);

      } catch (System.FormatException) {

        SemErr("incorrectly formatted number");

        n = BigInteger.Zero;

diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc
index a8a93067..1d9dfd1c 100644
--- a/Dafny/DafnyAst.ssc
+++ b/Dafny/DafnyAst.ssc
@@ -7,6 +7,7 @@ using System;
 using System.Collections.Generic;

 using Microsoft.Contracts;

 using System.Numerics;

+using Microsoft.Boogie;

 

 namespace Microsoft.Dafny

 {

@@ -148,14 +149,14 @@ namespace Microsoft.Dafny
   }

   

   public class UserDefinedType : Type {

-    public readonly Token! tok;

+    public readonly IToken! tok;

     public readonly string! Name;

     [Rep] public readonly List<Type!>! TypeArgs;

     

     public TopLevelDecl ResolvedClass;  // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype

     public TypeParameter ResolvedParam;  // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list

 

-    public static UserDefinedType! ArrayType(Token! tok, Type! arg) {

+    public static UserDefinedType! ArrayType(IToken! tok, Type! arg) {

       List<Type!> typeArgs = new List<Type!>();

       typeArgs.Add(arg);

       UserDefinedType udt = new UserDefinedType(tok, "array", typeArgs);

@@ -171,7 +172,7 @@ namespace Microsoft.Dafny
     }

 

     

-    public UserDefinedType(Token! tok, string! name, [Captured] List<Type!>! typeArgs) {

+    public UserDefinedType(IToken! tok, string! name, [Captured] List<Type!>! typeArgs) {

       this.tok = tok;

       this.Name = name;

       this.TypeArgs = typeArgs;

@@ -180,7 +181,7 @@ namespace Microsoft.Dafny
     /// <summary>

     /// This constructor constructs a resolved class type

     /// </summary>

-    public UserDefinedType(Token! tok, string! name, TopLevelDecl! cd, [Captured] List<Type!>! typeArgs) {

+    public UserDefinedType(IToken! tok, string! name, TopLevelDecl! cd, [Captured] List<Type!>! typeArgs) {

       this.tok = tok;

       this.Name = name;

       this.TypeArgs = typeArgs;

@@ -190,7 +191,7 @@ namespace Microsoft.Dafny
     /// <summary>

     /// This constructor constructs a resolved type parameter

     /// </summary>

-    public UserDefinedType(Token! tok, string! name, TypeParameter! tp) {

+    public UserDefinedType(IToken! tok, string! name, TypeParameter! tp) {

       this.tok = tok;

       this.Name = name;

       this.TypeArgs = new List<Type!>();

@@ -350,11 +351,11 @@ namespace Microsoft.Dafny
   // ------------------------------------------------------------------------------------------------------

   

   public abstract class Declaration {

-    public Token! tok;

+    public IToken! tok;

     public readonly string! Name;

     public readonly Attributes Attributes;

     

-    public Declaration(Token! tok, string! name, Attributes attributes) {

+    public Declaration(IToken! tok, string! name, Attributes attributes) {

       this.tok = tok;

       this.Name = name;

       this.Attributes = attributes;

@@ -386,7 +387,7 @@ namespace Microsoft.Dafny
         parent = value;

       }

     }

-    public TypeParameter(Token! tok, string! name) {

+    public TypeParameter(IToken! tok, string! name) {

       base(tok, name, null);

     }

   }

@@ -396,7 +397,7 @@ namespace Microsoft.Dafny
     public readonly List<TopLevelDecl!>! TopLevelDecls = new List<TopLevelDecl!>();  // filled in by the parser; readonly after that

     public readonly Graph<MemberDecl!>! CallGraph = new Graph<MemberDecl!>();  // filled in during resolution

     public int Height;  // height in the topological sorting of modules; filled in during resolution

-    public ModuleDecl(Token! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {

+    public ModuleDecl(IToken! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {

       Imports = imports;

       base(tok, name, attributes);

     }

@@ -418,7 +419,7 @@ namespace Microsoft.Dafny
     public readonly ModuleDecl! Module;

     public readonly List<TypeParameter!>! TypeArgs;

     

-    public TopLevelDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, Attributes attributes) {

+    public TopLevelDecl(IToken! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, Attributes attributes) {

       Module = module;

       TypeArgs = typeArgs;

       base(tok, name, attributes);

@@ -428,7 +429,7 @@ namespace Microsoft.Dafny
   public class ClassDecl : TopLevelDecl {

     public readonly List<MemberDecl!>! Members;

 

-    public ClassDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {

+    public ClassDecl(IToken! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {

       Members = members;

       base(tok, name, module, typeArgs, attributes);

     }

@@ -450,7 +451,7 @@ namespace Microsoft.Dafny
     public readonly List<DatatypeCtor!>! Ctors;

     public DatatypeCtor DefaultCtor;  // set during resolution

     

-    public DatatypeDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {

+    public DatatypeDecl(IToken! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {

       Ctors = ctors;

       base(tok, name, module, typeArgs, attributes);

     }

@@ -462,7 +463,7 @@ namespace Microsoft.Dafny
     // Todo: One could imagine having a precondition on datatype constructors

     public DatatypeDecl EnclosingDatatype;  // filled in during resolution

     

-    public DatatypeCtor(Token! tok, string! name, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals,

+    public DatatypeCtor(IToken! tok, string! name, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals,

                         Attributes attributes) {

       this.TypeArgs = typeArgs;

       this.Formals = formals;

@@ -481,7 +482,7 @@ namespace Microsoft.Dafny
   public abstract class MemberDecl : Declaration {

     public ClassDecl EnclosingClass;  // filled in during resolution

     

-    public MemberDecl(Token! tok, string! name, Attributes attributes) {

+    public MemberDecl(IToken! tok, string! name, Attributes attributes) {

       base(tok, name, attributes);

     }

     /// <summary>

@@ -500,7 +501,7 @@ namespace Microsoft.Dafny
     public readonly bool IsGhost;

     public readonly Type! Type;

     

-    public Field(Token! tok, string! name, bool isGhost, Type! type, Attributes attributes) {

+    public Field(IToken! tok, string! name, bool isGhost, Type! type, Attributes attributes) {

       IsGhost = isGhost;

       Type = type;

       base(tok, name, attributes);

@@ -516,7 +517,7 @@ namespace Microsoft.Dafny
   }

   

   public abstract class NonglobalVariable : IVariable {

-    public readonly Token! tok;

+    public readonly IToken! tok;

     readonly string! name;

     public string! Name { get { return name; } }

     readonly int varId = varIdCount++;

@@ -544,7 +545,7 @@ namespace Microsoft.Dafny
       set { isGhost = value; }

     }

     

-    public NonglobalVariable(Token! tok, string! name, Type! type, bool isGhost) {

+    public NonglobalVariable(IToken! tok, string! name, Type! type, bool isGhost) {

       this.tok = tok;

       this.name = name;

       this.type = type;

@@ -558,7 +559,7 @@ namespace Microsoft.Dafny
     public readonly bool InParam;  // true to in-parameter, false for out-parameter

     public override bool IsMutable { get { return !InParam; } }

     

-    public Formal(Token! tok, string! name, Type! type, bool inParam, bool isGhost) {

+    public Formal(IToken! tok, string! name, Type! type, bool inParam, bool isGhost) {

       InParam = inParam;

       base(tok, name, type, isGhost);

     }

@@ -567,7 +568,7 @@ namespace Microsoft.Dafny
   public class BoundVar : NonglobalVariable {

     public override bool IsMutable { get { return false; } }

     

-    public BoundVar(Token! tok, string! name, Type! type) {

+    public BoundVar(IToken! tok, string! name, Type! type) {

       base(tok, name, type, false);

     }

   }

@@ -585,7 +586,7 @@ namespace Microsoft.Dafny
     public readonly List<Expression!>! Decreases;

     public readonly Expression Body;  // an extended expression

     

-    public Function(Token! tok, string! name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,

+    public Function(IToken! tok, string! name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,

                     List<Expression!>! req, List<FrameExpression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {

       this.IsStatic = isStatic;

       this.IsGhost = isGhost;

@@ -613,7 +614,7 @@ namespace Microsoft.Dafny
     public readonly List<Expression!>! Decreases;

     public readonly BlockStmt Body;

     

-    public Method(Token! tok, string! name,

+    public Method(IToken! tok, string! name,

                   bool isStatic, bool isGhost,

                   [Captured] List<TypeParameter!>! typeArgs,

                   [Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,

@@ -638,9 +639,9 @@ namespace Microsoft.Dafny
   // ------------------------------------------------------------------------------------------------------

   

   public abstract class Statement {

-    public readonly Token! Tok;

+    public readonly IToken! Tok;

     public bool IsGhost;  // filled in by resolution

-    public Statement(Token! tok) {

+    public Statement(IToken! tok) {

       this.Tok = tok;

     }

   }

@@ -648,7 +649,7 @@ namespace Microsoft.Dafny
   public abstract class PredicateStmt : Statement {

     [Peer] public readonly Expression! Expr;

     [Captured]

-    public PredicateStmt(Token! tok, Expression! expr)

+    public PredicateStmt(IToken! tok, Expression! expr)

       ensures Owner.Same(this, expr);

     {

       base(tok);

@@ -659,7 +660,7 @@ namespace Microsoft.Dafny
   

   public class AssertStmt : PredicateStmt {

     [Captured]

-    public AssertStmt(Token! tok, Expression! expr)

+    public AssertStmt(IToken! tok, Expression! expr)

       ensures Owner.Same(this, expr);

     {

       base(tok, expr);

@@ -668,7 +669,7 @@ namespace Microsoft.Dafny
   

   public class AssumeStmt : PredicateStmt {

     [Captured]

-    public AssumeStmt(Token! tok, Expression! expr)

+    public AssumeStmt(IToken! tok, Expression! expr)

       ensures Owner.Same(this, expr);

     {

       base(tok, expr);

@@ -677,7 +678,7 @@ namespace Microsoft.Dafny
   

   public class UseStmt : PredicateStmt {

     [Captured]

-    public UseStmt(Token! tok, Expression! expr)

+    public UseStmt(IToken! tok, Expression! expr)

       ensures Owner.Same(this, expr);

     {

       base(tok, expr);

@@ -715,7 +716,7 @@ namespace Microsoft.Dafny
   

   public class PrintStmt : Statement {

     public readonly List<Attributes.Argument!>! Args;

-    public PrintStmt(Token! tok, List<Attributes.Argument!>! args)

+    public PrintStmt(IToken! tok, List<Attributes.Argument!>! args)

     {

       base(tok);

       Args = args;

@@ -724,7 +725,7 @@ namespace Microsoft.Dafny
   

   public class LabelStmt : Statement {

     public readonly string! Label;

-    public LabelStmt(Token! tok, string! label) {

+    public LabelStmt(IToken! tok, string! label) {

       this.Label = label;

       base(tok);

     }

@@ -734,14 +735,14 @@ namespace Microsoft.Dafny
     public readonly string TargetLabel;

     public Statement TargetStmt;  // filled in during resolution

     

-    public BreakStmt(Token! tok, string targetLabel) {

+    public BreakStmt(IToken! tok, string targetLabel) {

       this.TargetLabel = targetLabel;

       base(tok);

     }

   }

   

   public class ReturnStmt : Statement {

-    public ReturnStmt(Token! tok) {

+    public ReturnStmt(IToken! tok) {

       base(tok);

     }

   }

@@ -779,22 +780,22 @@ namespace Microsoft.Dafny
   public class AssignStmt : Statement {

     public readonly Expression! Lhs;

     public readonly AssignmentRhs! Rhs;

-    public AssignStmt(Token! tok, Expression! lhs, Expression! rhs) {  // ordinary assignment statement

+    public AssignStmt(IToken! tok, Expression! lhs, Expression! rhs) {  // ordinary assignment statement

       this.Lhs = lhs;

       this.Rhs = new ExprRhs(rhs);

       base(tok);

     }

-    public AssignStmt(Token! tok, Expression! lhs, Type! type) {  // alloc statement

+    public AssignStmt(IToken! tok, Expression! lhs, Type! type) {  // alloc statement

       this.Lhs = lhs;

       this.Rhs = new TypeRhs(type);

       base(tok);

     }

-    public AssignStmt(Token! tok, Expression! lhs, Type! type, Expression! arraySize) {  // array alloc statement

+    public AssignStmt(IToken! tok, Expression! lhs, Type! type, Expression! arraySize) {  // array alloc statement

       this.Lhs = lhs;

       this.Rhs = new TypeRhs(type, arraySize);

       base(tok);

     }

-    public AssignStmt(Token! tok, Expression! lhs) {  // havoc

+    public AssignStmt(IToken! tok, Expression! lhs) {  // havoc

       this.Lhs = lhs;

       this.Rhs = new HavocRhs();

       base(tok);

@@ -830,7 +831,7 @@ namespace Microsoft.Dafny
     public readonly DeterminedAssignmentRhs Rhs;

     invariant OptionalType != null || Rhs != null;

     

-    public VarDecl(Token! tok, string! name, Type type, bool isGhost, DeterminedAssignmentRhs rhs)

+    public VarDecl(IToken! tok, string! name, Type type, bool isGhost, DeterminedAssignmentRhs rhs)

       requires type != null || rhs != null;

     {

       this.name = name;

@@ -843,7 +844,7 @@ namespace Microsoft.Dafny
   

   public class AutoVarDecl : VarDecl {

     public readonly int Index;

-    public AutoVarDecl(Token! tok, string! name, Type! type, int index)

+    public AutoVarDecl(IToken! tok, string! name, Type! type, int index)

     {

       Index = index;

       base(tok, name, type, false, null);

@@ -864,7 +865,7 @@ namespace Microsoft.Dafny
     public readonly List<Expression!>! Args;

     public Method Method;  // filled in by resolution

     

-    public CallStmt(Token! tok, List<AutoVarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {

+    public CallStmt(IToken! tok, List<AutoVarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {

       this.NewVars = newVars;

       this.Lhs = lhs;

       this.Receiver = receiver;

@@ -876,7 +877,7 @@ namespace Microsoft.Dafny
   

   public class BlockStmt : Statement {

     public readonly List<Statement!>! Body;

-    public BlockStmt(Token! tok, [Captured] List<Statement!>! body) {

+    public BlockStmt(IToken! tok, [Captured] List<Statement!>! body) {

       this.Body = body;

       base(tok);

     }

@@ -888,7 +889,7 @@ namespace Microsoft.Dafny
     public readonly Statement Els;

     invariant Els == null || Els is BlockStmt || Els is IfStmt;

     

-    public IfStmt(Token! tok, Expression guard, Statement! thn, Statement els)

+    public IfStmt(IToken! tok, Expression guard, Statement! thn, Statement els)

       requires els == null || els is BlockStmt || els is IfStmt;

     {

       this.Guard = guard;

@@ -904,7 +905,7 @@ namespace Microsoft.Dafny
     public readonly List<Expression!>! Decreases;

     public readonly Statement! Body;

     

-    public WhileStmt(Token! tok, Expression guard,

+    public WhileStmt(IToken! tok, Expression guard,

                      List<MaybeFreeExpression!>! invariants, List<Expression!>! decreases,

                      Statement! body) {

       this.Guard = guard;

@@ -922,7 +923,7 @@ namespace Microsoft.Dafny
     public readonly List<PredicateStmt!>! BodyPrefix;

     public readonly AssignStmt! BodyAssign;

     

-    public ForeachStmt(Token! tok, BoundVar! boundVar, Expression! collection, Expression! range, List<PredicateStmt!>! bodyPrefix, AssignStmt! bodyAssign) {

+    public ForeachStmt(IToken! tok, BoundVar! boundVar, Expression! collection, Expression! range, List<PredicateStmt!>! bodyPrefix, AssignStmt! bodyAssign) {

       this.BoundVar = boundVar;

       this.Collection = collection;

       this.Range = range;

@@ -936,7 +937,7 @@ namespace Microsoft.Dafny
     public readonly Expression! Source;

     public readonly List<MatchCaseStmt!>! Cases;

     

-    public MatchStmt(Token! tok, Expression! source, [Captured] List<MatchCaseStmt!>! cases) {

+    public MatchStmt(IToken! tok, Expression! source, [Captured] List<MatchCaseStmt!>! cases) {

       this.Source = source;

       this.Cases = cases;

       base(tok);

@@ -944,13 +945,13 @@ namespace Microsoft.Dafny
   }

   

   public class MatchCaseStmt {

-    public readonly Token! tok;

+    public readonly IToken! tok;

     public readonly string! Id;

     public DatatypeCtor Ctor;  // filled in by resolution

     public readonly List<BoundVar!>! Arguments;

     public readonly List<Statement!>! Body;

     

-    public MatchCaseStmt(Token! tok, string! id, [Captured] List<BoundVar!>! arguments, [Captured] List<Statement!>! body) {

+    public MatchCaseStmt(IToken! tok, string! id, [Captured] List<BoundVar!>! arguments, [Captured] List<Statement!>! body) {

       this.tok = tok;

       this.Id = id;

       this.Arguments = arguments;

@@ -961,7 +962,7 @@ namespace Microsoft.Dafny
   // ------------------------------------------------------------------------------------------------------

   

   public abstract class Expression {

-    public readonly Token! tok;

+    public readonly IToken! tok;

     protected Type type;

     public Type Type {  // filled in during resolution

       [Verify(false)]  // TODO: how do we allow Type.get to modify type and still be [Pure]?

@@ -998,7 +999,7 @@ namespace Microsoft.Dafny
       }

     }

     

-    public Expression(Token! tok)

+    public Expression(IToken! tok)

       ensures type == null;  // we would have liked to have written Type==null, but that's not admissible or provable

     {

       this.tok = tok;

@@ -1017,25 +1018,25 @@ namespace Microsoft.Dafny
       }

     }

     

-    public LiteralExpr(Token! tok) {  // represents the Dafny literal "null"

+    public LiteralExpr(IToken! tok) {  // represents the Dafny literal "null"

       this.Value = null;

       base(tok);

     }

     

-    public LiteralExpr(Token! tok, BigInteger n)

+    public LiteralExpr(IToken! tok, BigInteger n)

       requires 0 <= n.Sign;

     {

       this.Value = n;

       base(tok);

     }

     

-    public LiteralExpr(Token! tok, int n)

+    public LiteralExpr(IToken! tok, int n)

       requires 0 <= n;

     {

       this(tok, new BigInteger(n));

     }

     

-    public LiteralExpr(Token! tok, bool b) {

+    public LiteralExpr(IToken! tok, bool b) {

       this.Value = b;

       base(tok);

     }

@@ -1048,7 +1049,7 @@ namespace Microsoft.Dafny
     public DatatypeCtor Ctor;  // filled in by resolution

     public List<Type!>! InferredTypeArgs = new List<Type!>();  // filled in by resolution

     

-    public DatatypeValue(Token! tok, string! datatypeName, string! memberName, [Captured] List<Expression!>! arguments) {

+    public DatatypeValue(IToken! tok, string! datatypeName, string! memberName, [Captured] List<Expression!>! arguments) {

       this.DatatypeName = datatypeName;

       this.MemberName = memberName;

       this.Arguments = arguments;

@@ -1057,13 +1058,13 @@ namespace Microsoft.Dafny
   }

   

   public class ThisExpr : Expression {

-    public ThisExpr(Token! tok) {

+    public ThisExpr(IToken! tok) {

       base(tok);

     }

   }

   

   public class ImplicitThisExpr : ThisExpr {

-    public ImplicitThisExpr(Token! tok) {

+    public ImplicitThisExpr(IToken! tok) {

       base(tok);

     }

   }

@@ -1072,7 +1073,7 @@ namespace Microsoft.Dafny
     public readonly string! Name;

     public IVariable Var;  // filled in by resolution

 

-    public IdentifierExpr(Token! tok, string! name) {

+    public IdentifierExpr(IToken! tok, string! name) {

       Name = name;

       base(tok);

     }

@@ -1080,20 +1081,20 @@ namespace Microsoft.Dafny
 

   public abstract class DisplayExpression : Expression {

     public readonly List<Expression!>! Elements;

-    public DisplayExpression(Token! tok, List<Expression!>! elements) {

+    public DisplayExpression(IToken! tok, List<Expression!>! elements) {

       Elements = elements;

       base(tok);

     }

   }

     

   public class SetDisplayExpr : DisplayExpression {

-    public SetDisplayExpr(Token! tok, List<Expression!>! elements) {

+    public SetDisplayExpr(IToken! tok, List<Expression!>! elements) {

       base(tok, elements);

     }

   }

     

   public class SeqDisplayExpr : DisplayExpression {

-    public SeqDisplayExpr(Token! tok, List<Expression!>! elements) {

+    public SeqDisplayExpr(IToken! tok, List<Expression!>! elements) {

       base(tok, elements);

     }

   }

@@ -1103,7 +1104,7 @@ namespace Microsoft.Dafny
     public readonly string! FieldName;

     public Field Field;  // filled in by resolution

     

-    public FieldSelectExpr(Token! tok, Expression! obj, string! fieldName) {

+    public FieldSelectExpr(IToken! tok, Expression! obj, string! fieldName) {

       this.Obj = obj;

       this.FieldName = fieldName;

       base(tok);

@@ -1118,7 +1119,7 @@ namespace Microsoft.Dafny
     invariant SelectOne ==> E1 == null;

     invariant E0 != null || E1 != null;

     

-    public SeqSelectExpr(Token! tok, bool selectOne, Expression! seq, Expression e0, Expression e1)

+    public SeqSelectExpr(IToken! tok, bool selectOne, Expression! seq, Expression e0, Expression e1)

       requires selectOne ==> e1 == null;

       requires e0 != null || e1 != null;

     {

@@ -1135,7 +1136,7 @@ namespace Microsoft.Dafny
     public readonly Expression! Index;

     public readonly Expression! Value;

     

-    public SeqUpdateExpr(Token! tok, Expression! seq, Expression! index, Expression! val)

+    public SeqUpdateExpr(IToken! tok, Expression! seq, Expression! index, Expression! val)

     {

       Seq = seq;

       Index = index;

@@ -1151,7 +1152,7 @@ namespace Microsoft.Dafny
     public Function Function;  // filled in by resolution

     

     [Captured]

-    public FunctionCallExpr(Token! tok, string! fn, Expression! receiver, [Captured] List<Expression!>! args)

+    public FunctionCallExpr(IToken! tok, string! fn, Expression! receiver, [Captured] List<Expression!>! args)

       ensures type == null;

       ensures Owner.Same(this, receiver);

     {

@@ -1166,7 +1167,7 @@ namespace Microsoft.Dafny
   public class OldExpr : Expression {

     [Peer] public readonly Expression! E;

     [Captured]

-    public OldExpr(Token! tok, Expression! expr) {

+    public OldExpr(IToken! tok, Expression! expr) {

       base(tok);

       Owner.AssignSame(this, expr);

       E = expr;

@@ -1175,7 +1176,7 @@ namespace Microsoft.Dafny
 

   public class FreshExpr : Expression {

     public readonly Expression! E;

-    public FreshExpr(Token! tok, Expression! expr) {

+    public FreshExpr(IToken! tok, Expression! expr) {

       E = expr;

       base(tok);

     }

@@ -1186,7 +1187,7 @@ namespace Microsoft.Dafny
     public readonly Opcode Op;

     public readonly Expression! E;

     

-    public UnaryExpr(Token! tok, Opcode op, Expression! e) {

+    public UnaryExpr(IToken! tok, Opcode op, Expression! e) {

       this.Op = op;

       this.E = e;

       base(tok);

@@ -1243,7 +1244,7 @@ namespace Microsoft.Dafny
     public readonly Expression! E0;

     public readonly Expression! E1;

     

-    public BinaryExpr(Token! tok, Opcode op, Expression! e0, Expression! e1) {

+    public BinaryExpr(IToken! tok, Opcode op, Expression! e0, Expression! e1) {

       this.Op = op;

       this.E0 = e0;

       this.E1 = e1;

@@ -1257,7 +1258,7 @@ namespace Microsoft.Dafny
     public readonly Triggers Trigs;

     public readonly Attributes Attributes;

     

-    public QuantifierExpr(Token! tok, List<BoundVar!>! bvars, Expression! body, Triggers trigs, Attributes attrs) {

+    public QuantifierExpr(IToken! tok, List<BoundVar!>! bvars, Expression! body, Triggers trigs, Attributes attrs) {

       this.BoundVars = bvars;

       this.Body = body;

       this.Trigs = trigs;

@@ -1277,19 +1278,19 @@ namespace Microsoft.Dafny
   }

   

   public class ForallExpr : QuantifierExpr {

-    public ForallExpr(Token! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {

+    public ForallExpr(IToken! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {

       base(tok, bvars, body, trig, attrs);

     }

   }

   

   public class ExistsExpr : QuantifierExpr {

-    public ExistsExpr(Token! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {

+    public ExistsExpr(IToken! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {

       base(tok, bvars, body, trig, attrs);

     }

   }

   

   public class WildcardExpr : Expression {  // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)

-    public WildcardExpr(Token! tok) {

+    public WildcardExpr(IToken! tok) {

       base(tok);

     }

   }

@@ -1299,7 +1300,7 @@ namespace Microsoft.Dafny
     public readonly Expression! Thn;

     public readonly Expression! Els;

     

-    public ITEExpr(Token! tok, Expression! test, Expression! thn, Expression! els) {

+    public ITEExpr(IToken! tok, Expression! test, Expression! thn, Expression! els) {

       this.Test = test;

       this.Thn = thn;

       this.Els = els;

@@ -1311,7 +1312,7 @@ namespace Microsoft.Dafny
     public readonly Expression! Source;

     public readonly List<MatchCaseExpr!>! Cases;

     

-    public MatchExpr(Token! tok, Expression! source, [Captured] List<MatchCaseExpr!>! cases) {

+    public MatchExpr(IToken! tok, Expression! source, [Captured] List<MatchCaseExpr!>! cases) {

       this.Source = source;

       this.Cases = cases;

       base(tok);

@@ -1319,13 +1320,13 @@ namespace Microsoft.Dafny
   }

   

   public class MatchCaseExpr {

-    public readonly Token! tok;

+    public readonly IToken! tok;

     public readonly string! Id;

     public DatatypeCtor Ctor;  // filled in by resolution

     public readonly List<BoundVar!>! Arguments;

     public readonly Expression! Body;

     

-    public MatchCaseExpr(Token! tok, string! id, [Captured] List<BoundVar!>! arguments, Expression! body) {

+    public MatchCaseExpr(IToken! tok, string! id, [Captured] List<BoundVar!>! arguments, Expression! body) {

       this.tok = tok;

       this.Id = id;

       this.Arguments = arguments;

diff --git a/Dafny/DafnyMain.ssc b/Dafny/DafnyMain.ssc
index a7d863fe..21375145 100644
--- a/Dafny/DafnyMain.ssc
+++ b/Dafny/DafnyMain.ssc
@@ -18,7 +18,6 @@ namespace Microsoft.Dafny {
       modifies Bpl.CommandLineOptions.Clo.XmlSink.*;

     {

       program = null;

-      Dafny.Errors.count = 0;

       List<ModuleDecl!> modules = new List<ModuleDecl!>();

       foreach (string! dafnyFileName in fileNames){

         if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {

@@ -35,7 +34,7 @@ namespace Microsoft.Dafny {
           errorCount = Dafny.Parser.Parse(dafnyFileName, modules);

           if (errorCount != 0) 

           {

-            return string.Format("{0} parse errors detected in {1}", Dafny.Errors.count, dafnyFileName);

+            return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);

           }

         } 

         catch (IOException e) 

diff --git a/Dafny/Makefile b/Dafny/Makefile
index fd2141b3..e545fbae 100644
--- a/Dafny/Makefile
+++ b/Dafny/Makefile
@@ -1,13 +1,18 @@
 COCO = ..\..\Binaries\Coco.exe

 ASML = ..\..\Binaries\asmlc.boot.exe

 

+# ###############################################################################

+# The frame files are no longer in this directory. They must be downloaded

+# from http://boogiepartners.codeplex.com/ and then copied into this directory.

+# ###############################################################################

+

 # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they

 # are both generated in one go and I don't know a better way to tell

 # nmake that.  --KRML

 all: Parser.ssc 

 

 Parser.ssc: Scanner.frame Parser.frame Dafny.atg

-	$(COCO) Dafny.atg

+	$(COCO) Dafny.atg -namespace Microsoft.Dafny

 	copy Parser.cs Parser.ssc

 	copy Scanner.cs Scanner.ssc

 

diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc
index 3752fd33..0f85bbe8 100644
--- a/Dafny/Parser.ssc
+++ b/Dafny/Parser.ssc
@@ -1,22 +1,38 @@
 using System.Collections.Generic;

 using System.Numerics;

 using Microsoft.Boogie;

+using System.IO;

+using System.Text;

+

+

+

+

+using System;

 using Microsoft.Contracts;

 

 namespace Microsoft.Dafny {

 

+

+

 public class Parser {

-	const int maxT = 100;

+	public const int _EOF = 0;

+	public const int _ident = 1;

+	public const int _digits = 2;

+	public const int _string = 3;

+	public const int maxT = 100;

 

 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

 	

-	static Token/*!*/ token;			// last recognized token

-	static Token/*!*/ t;				// lookahead token

-	static int errDist = minErrDist;

+	public Scanner/*!*/ scanner;

+	public Errors/*!*/  errors;

 

-	static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();

+	public Token/*!*/ t;    // last recognized token

+	public Token/*!*/ la;   // lookahead token

+	int errDist = minErrDist;

+

+static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();

 

 

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

@@ -62,15 +78,14 @@ private static Expression! ConvertToLocal(Expression! e)
 /// Note: first initialize the Scanner.

 ///</summary>

 public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws System.IO.IOException */ {

+  string s;

   if (filename == "stdin.dfy") {

-    BoogiePL.Buffer.Fill(System.Console.In);

-    Scanner.Init(filename);

-    return Parse(modules);

+    s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string!>());

+    return Parse(s, modules);

   } else {

     using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

-      BoogiePL.Buffer.Fill(reader);

-      Scanner.Init(filename);

-      return Parse(modules);

+      s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string!>());

+      return Parse(s, filename, modules);

     }

   }

 }

@@ -81,106 +96,122 @@ public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (List<ModuleDecl!>! modules) {

+public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules) {

   List<ModuleDecl!> oldModules = theModules;

   theModules = modules;

-  Parse();

+  byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s);

+  MemoryStream ms = new MemoryStream(buffer,false);

+  Errors errors = new Errors();

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

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

+  parser.Parse();

   theModules = oldModules;

-  return Errors.count;

+  return parser.errors.count;

 }

 

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

 

 

-	static void Error(int n) {

-		if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);

-		errDist = 0;

+	public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {

+		this.scanner = scanner;

+		this.errors = errors;

+		Token! tok = new Token();

+		tok.val = "";

+		this.la = tok;

+		this.t = new Token(); // just to satisfy its non-null constraint

 	}

-	

-	public static void SemErr(string! msg) {

-		if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);

+

+	void SynErr (int n) {

+		if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);

 		errDist = 0;

 	}

 

-	public static void SemErr(Token! tok, string! msg) {

-		if (errDist >= minErrDist) Errors.SemErr(tok.filename, tok.line, tok.col, msg);

+	public void SemErr (string! msg) {

+		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

+	

+    public void SemErr(IToken! tok, string! msg) {

+	  errors.SemErr(tok, msg);

+	}

 

-	static void Get() {

+	void Get () {

 		for (;;) {

-			token = t;

-			t = Scanner.Scan();

-			if (t.kind<=maxT) {errDist++; return;}

+			t = la;

+			la = scanner.Scan();

+			if (la.kind <= maxT) { ++errDist; break; }

 

-			t = token;

+			la = t;

 		}

 	}

 	

-	static void Expect(int n) {

-		if (t.kind==n) Get(); else Error(n);

+	void Expect (int n) {

+		if (la.kind==n) Get(); else { SynErr(n); }

 	}

 	

-	static bool StartOf(int s) {

-		return set[s, t.kind];

+	bool StartOf (int s) {

+		return set[s, la.kind];

 	}

 	

-	static void ExpectWeak(int n, int follow) {

-		if (t.kind == n) Get();

+	void ExpectWeak (int n, int follow) {

+		if (la.kind == n) Get();

 		else {

-			Error(n);

+			SynErr(n);

 			while (!StartOf(follow)) Get();

 		}

 	}

-	

-	static bool WeakSeparator(int n, int syFol, int repFol) {

-		bool[] s = new bool[maxT+1];

-		if (t.kind == n) {Get(); return true;}

-		else if (StartOf(repFol)) return false;

+

+

+	bool WeakSeparator(int n, int syFol, int repFol) {

+		int kind = la.kind;

+		if (kind == n) {Get(); return true;}

+		else if (StartOf(repFol)) {return false;}

 		else {

-			for (int i=0; i <= maxT; i++) {

-				s[i] = set[syFol, i] || set[repFol, i] || set[0, i];

+			SynErr(n);

+			while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {

+				Get();

+				kind = la.kind;

 			}

-			Error(n);

-			while (!s[t.kind]) Get();

 			return StartOf(syFol);

 		}

 	}

+

 	

-	static void Dafny() {

+	void Dafny() {

 		ClassDecl! c; DatatypeDecl! dt;

-		Attributes attrs;  Token! id;  List<string!> theImports;

-		  List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();

-		ModuleDecl module;

-		

-		// to support multiple files, create a default module only if theModules doesn't already contain one

-		DefaultModuleDecl defaultModule = null;

-		foreach (ModuleDecl mdecl in theModules) {

-		  defaultModule = mdecl as DefaultModuleDecl;

-		  if (defaultModule != null) { break; }

-		}

-		bool defaultModuleCreatedHere = false;

-		if (defaultModule == null) {

-		  defaultModuleCreatedHere = true;

-		  defaultModule = new DefaultModuleDecl();

-		}

+		Attributes attrs;  IToken! id;  List<string!> theImports;

 		

+		     List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();

+		     ModuleDecl module;

+		     

+		     // to support multiple files, create a default module only if theModules doesn't already contain one

+		     DefaultModuleDecl defaultModule = null;

+		     foreach (ModuleDecl mdecl in theModules) {

+		       defaultModule = mdecl as DefaultModuleDecl;

+		       if (defaultModule != null) { break; }

+		     }

+		     bool defaultModuleCreatedHere = false;

+		     if (defaultModule == null) {

+		       defaultModuleCreatedHere = true;

+		       defaultModule = new DefaultModuleDecl();

+		     }

+		  

 		while (StartOf(1)) {

-			if (t.kind == 4) {

+			if (la.kind == 4) {

 				Get();

 				attrs = null;  theImports = new List<string!>(); 

-				while (t.kind == 6) {

+				while (la.kind == 6) {

 					Attribute(ref attrs);

 				}

 				Ident(out id);

-				if (t.kind == 5) {

+				if (la.kind == 5) {

 					Get();

 					Idents(theImports);

 				}

 				module = new ModuleDecl(id, id.val, theImports, attrs); 

 				Expect(6);

-				while (t.kind == 8 || t.kind == 12) {

-					if (t.kind == 8) {

+				while (la.kind == 8 || la.kind == 12) {

+					if (la.kind == 8) {

 						ClassDecl(module, out c);

 						module.TopLevelDecls.Add(c); 

 					} else {

@@ -190,10 +221,10 @@ public static int Parse (List<ModuleDecl!>! modules) {
 				}

 				theModules.Add(module); 

 				Expect(7);

-			} else if (t.kind == 8) {

+			} else if (la.kind == 8) {

 				ClassDecl(defaultModule, out c);

 				defaultModule.TopLevelDecls.Add(c); 

-			} else if (t.kind == 12) {

+			} else if (la.kind == 12) {

 				DatatypeDecl(defaultModule, out dt);

 				defaultModule.TopLevelDecls.Add(dt); 

 			} else {

@@ -217,40 +248,40 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Expect(0);

 	}

 

-	static void Attribute(ref Attributes attrs) {

+	void Attribute(ref Attributes attrs) {

 		Expect(6);

 		AttributeBody(ref attrs);

 		Expect(7);

 	}

 

-	static void Ident(out Token! x) {

+	void Ident(out IToken! x) {

 		Expect(1);

-		x = token; 

+		x = t; 

 	}

 

-	static void Idents(List<string!>! ids) {

-		Token! id; 

+	void Idents(List<string!>! ids) {

+		IToken! id; 

 		Ident(out id);

 		ids.Add(id.val); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			Ident(out id);

 			ids.Add(id.val); 

 		}

 	}

 

-	static void ClassDecl(ModuleDecl! module, out ClassDecl! c) {

-		Token! id;

+	void ClassDecl(ModuleDecl! module, out ClassDecl! c) {

+		IToken! id;

 		Attributes attrs = null;

 		List<TypeParameter!> typeArgs = new List<TypeParameter!>();

 		List<MemberDecl!> members = new List<MemberDecl!>();

 		

 		Expect(8);

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		Expect(6);

@@ -261,38 +292,38 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); 

 	}

 

-	static void DatatypeDecl(ModuleDecl! module, out DatatypeDecl! dt) {

-		Token! id;

+	void DatatypeDecl(ModuleDecl! module, out DatatypeDecl! dt) {

+		IToken! id;

 		Attributes attrs = null;

 		List<TypeParameter!> typeArgs = new List<TypeParameter!>();

 		List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();

 		

 		Expect(12);

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		Expect(6);

-		while (t.kind == 1 || t.kind == 6) {

+		while (la.kind == 1 || la.kind == 6) {

 			DatatypeMemberDecl(ctors);

 		}

 		Expect(7);

 		dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); 

 	}

 

-	static void ClassMemberDecl(List<MemberDecl!>! mm) {

+	void ClassMemberDecl(List<MemberDecl!>! mm) {

 		Method! m;

 		Function! f;

 		MemberModifiers mmod = new MemberModifiers();

 		

-		while (t.kind == 9 || t.kind == 10 || t.kind == 11) {

-			if (t.kind == 9) {

+		while (la.kind == 9 || la.kind == 10 || la.kind == 11) {

+			if (la.kind == 9) {

 				Get();

 				mmod.IsGhost = true; 

-			} else if (t.kind == 10) {

+			} else if (la.kind == 10) {

 				Get();

 				mmod.IsStatic = true; 

 			} else {

@@ -300,23 +331,23 @@ public static int Parse (List<ModuleDecl!>! modules) {
 				mmod.IsUnlimited = true; 

 			}

 		}

-		if (t.kind == 14) {

+		if (la.kind == 14) {

 			FieldDecl(mmod, mm);

-		} else if (t.kind == 34) {

+		} else if (la.kind == 34) {

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (t.kind == 19) {

+		} else if (la.kind == 19) {

 			MethodDecl(mmod, out m);

 			mm.Add(m); 

-		} else Error(101);

+		} else SynErr(101);

 	}

 

-	static void GenericParameters(List<TypeParameter!>! typeArgs) {

-		Token! id; 

+	void GenericParameters(List<TypeParameter!>! typeArgs) {

+		IToken! id; 

 		Expect(17);

 		Ident(out id);

 		typeArgs.Add(new TypeParameter(id, id.val)); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			Ident(out id);

 			typeArgs.Add(new TypeParameter(id, id.val)); 

@@ -324,20 +355,20 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Expect(18);

 	}

 

-	static void FieldDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {

+	void FieldDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {

 		Attributes attrs = null;

-		Token! id;  Type! ty;

+		IToken! id;  Type! ty;

 		

 		Expect(14);

-		if (mmod.IsUnlimited) { SemErr(token, "fields cannot be declared 'unlimited'"); }

-		if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }

+		if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }

+		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

 		

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		IdentType(out id, out ty);

 		mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			IdentType(out id, out ty);

 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

@@ -345,9 +376,9 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Expect(13);

 	}

 

-	static void FunctionDecl(MemberModifiers mmod, out Function! f) {

+	void FunctionDecl(MemberModifiers mmod, out Function! f) {

 		Attributes attrs = null;

-		Token! id;

+		IToken! id;

 		List<TypeParameter!> typeArgs = new List<TypeParameter!>();

 		List<Formal!> formals = new List<Formal!>();

 		Type! returnType;

@@ -358,42 +389,42 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		bool isFunctionMethod = false;

 		

 		Expect(34);

-		if (t.kind == 19) {

+		if (la.kind == 19) {

 			Get();

 			isFunctionMethod = true; 

 		}

-		if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); }

+		if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }

 		

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

 		Formals(true, false, formals);

 		Expect(16);

 		Type(out returnType);

-		if (t.kind == 13) {

+		if (la.kind == 13) {

 			Get();

-			while (t.kind == 23 || t.kind == 25 || t.kind == 35) {

+			while (la.kind == 23 || la.kind == 25 || la.kind == 35) {

 				FunctionSpec(reqs, reads, decreases);

 			}

 		} else if (StartOf(3)) {

-			while (t.kind == 23 || t.kind == 25 || t.kind == 35) {

+			while (la.kind == 23 || la.kind == 25 || la.kind == 35) {

 				FunctionSpec(reqs, reads, decreases);

 			}

 			FunctionBody(out bb);

 			body = bb; 

-		} else Error(102);

+		} else SynErr(102);

 		parseVarScope.PopMarker();

 		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

 		

 	}

 

-	static void MethodDecl(MemberModifiers mmod, out Method! m) {

-		Token! id;

+	void MethodDecl(MemberModifiers mmod, out Method! m) {

+		IToken! id;

 		Attributes attrs = null;

 		List<TypeParameter!>! typeArgs = new List<TypeParameter!>();

 		List<Formal!> ins = new List<Formal!>();

@@ -405,22 +436,22 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Statement! bb;  BlockStmt body = null;

 		

 		Expect(19);

-		if (mmod.IsUnlimited) { SemErr(token, "methods cannot be declared 'unlimited'"); }

+		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

 		

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

 		Formals(true, true, ins);

-		if (t.kind == 20) {

+		if (la.kind == 20) {

 			Get();

 			Formals(false, true, outs);

 		}

-		if (t.kind == 13) {

+		if (la.kind == 13) {

 			Get();

 			while (StartOf(4)) {

 				MethodSpec(req, mod, ens, dec);

@@ -431,27 +462,27 @@ public static int Parse (List<ModuleDecl!>! modules) {
 			}

 			BlockStmt(out bb);

 			body = (BlockStmt)bb; 

-		} else Error(103);

+		} else SynErr(103);

 		parseVarScope.PopMarker();

 		m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

 		

 	}

 

-	static void DatatypeMemberDecl(List<DatatypeCtor!>! ctors) {

+	void DatatypeMemberDecl(List<DatatypeCtor!>! ctors) {

 		Attributes attrs = null;

-		Token! id;

+		IToken! id;

 		List<TypeParameter!> typeArgs = new List<TypeParameter!>();

 		List<Formal!> formals = new List<Formal!>();

 		

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			GenericParameters(typeArgs);

 		}

 		parseVarScope.PushMarker(); 

-		if (t.kind == 26) {

+		if (la.kind == 26) {

 			FormalsOptionalIds(formals);

 		}

 		parseVarScope.PopMarker();

@@ -460,13 +491,13 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Expect(13);

 	}

 

-	static void FormalsOptionalIds(List<Formal!>! formals) {

-		Token! id;  Type! ty;  string! name;  bool isGhost; 

+	void FormalsOptionalIds(List<Formal!>! formals) {

+		IToken! id;  Type! ty;  string! name;  bool isGhost; 

 		Expect(26);

 		if (StartOf(6)) {

 			TypeIdentOptional(out id, out name, out ty, out isGhost);

 			formals.Add(new Formal(id, name, ty, true, isGhost));  parseVarScope.Push(name, name); 

-			while (t.kind == 15) {

+			while (la.kind == 15) {

 				Get();

 				TypeIdentOptional(out id, out name, out ty, out isGhost);

 				formals.Add(new Formal(id, name, ty, true, isGhost));  parseVarScope.Push(name, name); 

@@ -475,31 +506,31 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Expect(27);

 	}

 

-	static void IdentType(out Token! id, out Type! ty) {

+	void IdentType(out IToken! id, out Type! ty) {

 		Ident(out id);

 		Expect(16);

 		Type(out ty);

 	}

 

-	static void GIdentType(bool allowGhost, out Token! id, out Type! ty, out bool isGhost) {

+	void GIdentType(bool allowGhost, out IToken! id, out Type! ty, out bool isGhost) {

 		isGhost = false; 

-		if (t.kind == 9) {

+		if (la.kind == 9) {

 			Get();

-			if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); } 

+			if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } 

 		}

 		IdentType(out id, out ty);

 	}

 

-	static void Type(out Type! ty) {

-		Token! tok; 

+	void Type(out Type! ty) {

+		IToken! tok; 

 		TypeAndToken(out tok, out ty);

 	}

 

-	static void IdentTypeOptional(out BoundVar! var) {

-		Token! id;  Type! ty;  Type optType = null;

+	void IdentTypeOptional(out BoundVar! var) {

+		IToken! id;  Type! ty;  Type optType = null;

 		

 		Ident(out id);

-		if (t.kind == 16) {

+		if (la.kind == 16) {

 			Get();

 			Type(out ty);

 			optType = ty; 

@@ -507,14 +538,14 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); 

 	}

 

-	static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty, out bool isGhost) {

+	void TypeIdentOptional(out IToken! id, out string! identName, out Type! ty, out bool isGhost) {

 		string name = null;  isGhost = false; 

-		if (t.kind == 9) {

+		if (la.kind == 9) {

 			Get();

 			isGhost = true; 

 		}

 		TypeAndToken(out id, out ty);

-		if (t.kind == 16) {

+		if (la.kind == 16) {

 			Get();

 			UserDefinedType udt = ty as UserDefinedType;

 			if (udt != null && udt.TypeArgs.Count == 0) {

@@ -533,46 +564,46 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		

 	}

 

-	static void TypeAndToken(out Token! tok, out Type! ty) {

+	void TypeAndToken(out IToken! tok, out Type! ty) {

 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

 		List<Type!>! gt;

 		

-		if (t.kind == 28) {

+		if (la.kind == 28) {

 			Get();

-			tok = token; 

-		} else if (t.kind == 29) {

+			tok = t; 

+		} else if (la.kind == 29) {

 			Get();

-			tok = token;  ty = new IntType(); 

-		} else if (t.kind == 30) {

+			tok = t;  ty = new IntType(); 

+		} else if (la.kind == 30) {

 			Get();

-			tok = token;  gt = new List<Type!>(); 

+			tok = t;  gt = new List<Type!>(); 

 			GenericInstantiation(gt);

 			if (gt.Count != 1) {

 			 SemErr("set type expects exactly one type argument");

 			}

 			ty = new SetType(gt[0]);

 			

-		} else if (t.kind == 31) {

+		} else if (la.kind == 31) {

 			Get();

-			tok = token;  gt = new List<Type!>(); 

+			tok = t;  gt = new List<Type!>(); 

 			GenericInstantiation(gt);

 			if (gt.Count != 1) {

 			 SemErr("seq type expects exactly one type argument");

 			}

 			ty = new SeqType(gt[0]);

 			

-		} else if (t.kind == 1 || t.kind == 32 || t.kind == 33) {

+		} else if (la.kind == 1 || la.kind == 32 || la.kind == 33) {

 			ReferenceType(out tok, out ty);

-		} else Error(104);

+		} else SynErr(104);

 	}

 

-	static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {

-		Token! id;  Type! ty;  bool isGhost; 

+	void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {

+		IToken! id;  Type! ty;  bool isGhost; 

 		Expect(26);

-		if (t.kind == 1 || t.kind == 9) {

+		if (la.kind == 1 || la.kind == 9) {

 			GIdentType(allowGhosts, out id, out ty, out isGhost);

 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); 

-			while (t.kind == 15) {

+			while (la.kind == 15) {

 				Get();

 				GIdentType(allowGhosts, out id, out ty, out isGhost);

 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); 

@@ -581,53 +612,53 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Expect(27);

 	}

 

-	static void MethodSpec(List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,

+	void MethodSpec(List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,

 List<Expression!>! decreases) {

 		Expression! e;  FrameExpression! fe;  bool isFree = false;

 		

-		if (t.kind == 21) {

+		if (la.kind == 21) {

 			Get();

 			if (StartOf(7)) {

 				FrameExpression(out fe);

 				mod.Add(fe); 

-				while (t.kind == 15) {

+				while (la.kind == 15) {

 					Get();

 					FrameExpression(out fe);

 					mod.Add(fe); 

 				}

 			}

 			Expect(13);

-		} else if (t.kind == 22 || t.kind == 23 || t.kind == 24) {

-			if (t.kind == 22) {

+		} else if (la.kind == 22 || la.kind == 23 || la.kind == 24) {

+			if (la.kind == 22) {

 				Get();

 				isFree = true; 

 			}

-			if (t.kind == 23) {

+			if (la.kind == 23) {

 				Get();

 				Expression(out e);

 				Expect(13);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

-			} else if (t.kind == 24) {

+			} else if (la.kind == 24) {

 				Get();

 				Expression(out e);

 				Expect(13);

 				ens.Add(new MaybeFreeExpression(e, isFree)); 

-			} else Error(105);

-		} else if (t.kind == 25) {

+			} else SynErr(105);

+		} else if (la.kind == 25) {

 			Get();

 			Expressions(decreases);

 			Expect(13);

-		} else Error(106);

+		} else SynErr(106);

 	}

 

-	static void BlockStmt(out Statement! block) {

-		Token! x;

+	void BlockStmt(out Statement! block) {

+		IToken! x;

 		List<Statement!> body = new List<Statement!>();

 		Statement! s;

 		

 		parseVarScope.PushMarker(); 

 		Expect(6);

-		x = token; 

+		x = t; 

 		while (StartOf(8)) {

 			Stmt(body);

 		}

@@ -636,10 +667,10 @@ List<Expression!>! decreases) {
 		parseVarScope.PopMarker(); 

 	}

 

-	static void FrameExpression(out FrameExpression! fe) {

-		Expression! e;  Token! id;  string fieldName = null; 

+	void FrameExpression(out FrameExpression! fe) {

+		Expression! e;  IToken! id;  string fieldName = null; 

 		Expression(out e);

-		if (t.kind == 37) {

+		if (la.kind == 37) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

@@ -647,13 +678,13 @@ List<Expression!>! decreases) {
 		fe = new FrameExpression(e, fieldName); 

 	}

 

-	static void Expression(out Expression! e) {

-		Token! x;  Expression! e0;  Expression! e1 = dummyExpr;

+	void Expression(out Expression! e) {

+		IToken! x;  Expression! e0;  Expression! e1 = dummyExpr;

 		e = dummyExpr;

 		

-		if (t.kind == 49) {

+		if (la.kind == 49) {

 			Get();

-			x = token; 

+			x = t; 

 			Expression(out e);

 			Expect(61);

 			Expression(out e0);

@@ -662,26 +693,26 @@ List<Expression!>! decreases) {
 			e = new ITEExpr(x, e, e0, e1); 

 		} else if (StartOf(9)) {

 			EquivExpression(out e);

-		} else Error(107);

+		} else SynErr(107);

 	}

 

-	static void Expressions(List<Expression!>! args) {

+	void Expressions(List<Expression!>! args) {

 		Expression! e; 

 		Expression(out e);

 		args.Add(e); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			Expression(out e);

 			args.Add(e); 

 		}

 	}

 

-	static void GenericInstantiation(List<Type!>! gt) {

+	void GenericInstantiation(List<Type!>! gt) {

 		Type! ty; 

 		Expect(17);

 		Type(out ty);

 		gt.Add(ty); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			Type(out ty);

 			gt.Add(ty); 

@@ -689,117 +720,117 @@ List<Expression!>! decreases) {
 		Expect(18);

 	}

 

-	static void ReferenceType(out Token! tok, out Type! ty) {

+	void ReferenceType(out IToken! tok, out Type! ty) {

 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

 		List<Type!>! gt;

 		

-		if (t.kind == 32) {

+		if (la.kind == 32) {

 			Get();

-			tok = token;  ty = new ObjectType(); 

-		} else if (t.kind == 33) {

+			tok = t;  ty = new ObjectType(); 

+		} else if (la.kind == 33) {

 			Get();

-			tok = token;  gt = new List<Type!>(); 

+			tok = t;  gt = new List<Type!>(); 

 			GenericInstantiation(gt);

 			if (gt.Count != 1) {

 			 SemErr("array type expects exactly one type argument");

 			}

 			ty = UserDefinedType.ArrayType(tok, gt[0]);

 			

-		} else if (t.kind == 1) {

+		} else if (la.kind == 1) {

 			Ident(out tok);

 			gt = new List<Type!>(); 

-			if (t.kind == 17) {

+			if (la.kind == 17) {

 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt); 

-		} else Error(108);

+		} else SynErr(108);

 	}

 

-	static void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {

+	void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {

 		Expression! e;  FrameExpression! fe; 

-		if (t.kind == 23) {

+		if (la.kind == 23) {

 			Get();

 			Expression(out e);

 			Expect(13);

 			reqs.Add(e); 

-		} else if (t.kind == 35) {

+		} else if (la.kind == 35) {

 			Get();

 			if (StartOf(10)) {

 				PossiblyWildFrameExpression(out fe);

 				reads.Add(fe); 

-				while (t.kind == 15) {

+				while (la.kind == 15) {

 					Get();

 					PossiblyWildFrameExpression(out fe);

 					reads.Add(fe); 

 				}

 			}

 			Expect(13);

-		} else if (t.kind == 25) {

+		} else if (la.kind == 25) {

 			Get();

 			Expressions(decreases);

 			Expect(13);

-		} else Error(109);

+		} else SynErr(109);

 	}

 

-	static void FunctionBody(out Expression! e) {

+	void FunctionBody(out Expression! e) {

 		e = dummyExpr; 

 		Expect(6);

-		if (t.kind == 38) {

+		if (la.kind == 38) {

 			MatchExpression(out e);

 		} else if (StartOf(7)) {

 			Expression(out e);

-		} else Error(110);

+		} else SynErr(110);

 		Expect(7);

 	}

 

-	static void PossiblyWildFrameExpression(out FrameExpression! fe) {

+	void PossiblyWildFrameExpression(out FrameExpression! fe) {

 		fe = dummyFrameExpr; 

-		if (t.kind == 36) {

+		if (la.kind == 36) {

 			Get();

-			fe = new FrameExpression(new WildcardExpr(token), null); 

+			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(7)) {

 			FrameExpression(out fe);

-		} else Error(111);

+		} else SynErr(111);

 	}

 

-	static void PossiblyWildExpression(out Expression! e) {

+	void PossiblyWildExpression(out Expression! e) {

 		e = dummyExpr; 

-		if (t.kind == 36) {

+		if (la.kind == 36) {

 			Get();

-			e = new WildcardExpr(token); 

+			e = new WildcardExpr(t); 

 		} else if (StartOf(7)) {

 			Expression(out e);

-		} else Error(112);

+		} else SynErr(112);

 	}

 

-	static void MatchExpression(out Expression! e) {

-		Token! x;  MatchCaseExpr! c;

+	void MatchExpression(out Expression! e) {

+		IToken! x;  MatchCaseExpr! c;

 		List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();

 		

 		Expect(38);

-		x = token; 

+		x = t; 

 		Expression(out e);

-		while (t.kind == 39) {

+		while (la.kind == 39) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

 		e = new MatchExpr(x, e, cases); 

 	}

 

-	static void CaseExpression(out MatchCaseExpr! c) {

-		Token! x, id, arg;

+	void CaseExpression(out MatchCaseExpr! c) {

+		IToken! x, id, arg;

 		List<BoundVar!> arguments = new List<BoundVar!>();

 		Expression! body;

 		

 		Expect(39);

-		x = token;  parseVarScope.PushMarker(); 

+		x = t;  parseVarScope.PushMarker(); 

 		Ident(out id);

-		if (t.kind == 26) {

+		if (la.kind == 26) {

 			Get();

 			Ident(out arg);

 			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

 			parseVarScope.Push(arg.val, arg.val); 

-			while (t.kind == 15) {

+			while (la.kind == 15) {

 				Get();

 				Ident(out arg);

 				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

@@ -813,25 +844,25 @@ List<Expression!>! decreases) {
 		parseVarScope.PopMarker(); 

 	}

 

-	static void Stmt(List<Statement!>! ss) {

+	void Stmt(List<Statement!>! ss) {

 		Statement! s; 

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			BlockStmt(out s);

 			ss.Add(s); 

 		}

 		if (StartOf(11)) {

 			OneStmt(out s);

 			ss.Add(s); 

-		} else if (t.kind == 9 || t.kind == 14) {

+		} else if (la.kind == 9 || la.kind == 14) {

 			VarDeclStmts(ss);

-		} else Error(113);

+		} else SynErr(113);

 	}

 

-	static void OneStmt(out Statement! s) {

-		Token! x;  Token! id;  string label = null;

+	void OneStmt(out Statement! s) {

+		IToken! x;  IToken! id;  string label = null;

 		s = dummyStmt;  /* to please the compiler */

 		

-		switch (t.kind) {

+		switch (la.kind) {

 		case 57: {

 			AssertStmt(out s);

 			break;

@@ -878,7 +909,7 @@ List<Expression!>! decreases) {
 		}

 		case 41: {

 			Get();

-			x = token; 

+			x = t; 

 			Ident(out id);

 			Expect(16);

 			s = new LabelStmt(x, id.val); 

@@ -886,8 +917,8 @@ List<Expression!>! decreases) {
 		}

 		case 42: {

 			Get();

-			x = token; 

-			if (t.kind == 1) {

+			x = t; 

+			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

 			}

@@ -897,25 +928,25 @@ List<Expression!>! decreases) {
 		}

 		case 43: {

 			Get();

-			x = token; 

+			x = t; 

 			Expect(13);

 			s = new ReturnStmt(x); 

 			break;

 		}

-		default: Error(114); break;

+		default: SynErr(114); break;

 		}

 	}

 

-	static void VarDeclStmts(List<Statement!>! ss) {

+	void VarDeclStmts(List<Statement!>! ss) {

 		VarDecl! d;  bool isGhost = false; 

-		if (t.kind == 9) {

+		if (la.kind == 9) {

 			Get();

 			isGhost = true; 

 		}

 		Expect(14);

 		IdentTypeRhs(out d, isGhost);

 		ss.Add(d);  parseVarScope.Push(d.Name, d.Name); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			IdentTypeRhs(out d, isGhost);

 			ss.Add(d);  parseVarScope.Push(d.Name, d.Name); 

@@ -923,42 +954,42 @@ List<Expression!>! decreases) {
 		Expect(13);

 	}

 

-	static void AssertStmt(out Statement! s) {

-		Token! x;  Expression! e; 

+	void AssertStmt(out Statement! s) {

+		IToken! x;  Expression! e; 

 		Expect(57);

-		x = token; 

+		x = t; 

 		Expression(out e);

 		Expect(13);

 		s = new AssertStmt(x, e); 

 	}

 

-	static void AssumeStmt(out Statement! s) {

-		Token! x;  Expression! e; 

+	void AssumeStmt(out Statement! s) {

+		IToken! x;  Expression! e; 

 		Expect(58);

-		x = token; 

+		x = t; 

 		Expression(out e);

 		Expect(13);

 		s = new AssumeStmt(x, e); 

 	}

 

-	static void UseStmt(out Statement! s) {

-		Token! x;  Expression! e; 

+	void UseStmt(out Statement! s) {

+		IToken! x;  Expression! e; 

 		Expect(59);

-		x = token; 

+		x = t; 

 		Expression(out e);

 		Expect(13);

 		s = new UseStmt(x, e); 

 	}

 

-	static void PrintStmt(out Statement! s) {

-		Token! x;  Attributes.Argument! arg;

+	void PrintStmt(out Statement! s) {

+		IToken! x;  Attributes.Argument! arg;

 		List<Attributes.Argument!> args = new List<Attributes.Argument!>();

 		

 		Expect(60);

-		x = token; 

+		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			AttributeArg(out arg);

 			args.Add(arg); 

@@ -967,8 +998,8 @@ List<Expression!>! decreases) {
 		s = new PrintStmt(x, args); 

 	}

 

-	static void AssignStmt(out Statement! s) {

-		Token! x;

+	void AssignStmt(out Statement! s) {

+		IToken! x;

 		Expression! lhs;

 		Expression rhs;

 		Type ty;

@@ -976,7 +1007,7 @@ List<Expression!>! decreases) {
 		

 		LhsExpr(out lhs);

 		Expect(44);

-		x = token; 

+		x = t; 

 		AssignRhs(out rhs, out ty);

 		if (ty == null) {

 		 assert rhs != null;

@@ -990,26 +1021,26 @@ List<Expression!>! decreases) {
 		Expect(13);

 	}

 

-	static void HavocStmt(out Statement! s) {

-		Token! x;  Expression! lhs; 

+	void HavocStmt(out Statement! s) {

+		IToken! x;  Expression! lhs; 

 		Expect(48);

-		x = token; 

+		x = t; 

 		LhsExpr(out lhs);

 		Expect(13);

 		s = new AssignStmt(x, lhs); 

 	}

 

-	static void CallStmt(out Statement! s) {

-		Token! x, id;

+	void CallStmt(out Statement! s) {

+		IToken! x, id;

 		Expression! e;

 		List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

 		List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();

 		

 		Expect(53);

-		x = token; 

+		x = t; 

 		CallStmtSubExpr(out e);

-		if (t.kind == 15 || t.kind == 44) {

-			if (t.kind == 15) {

+		if (la.kind == 15 || la.kind == 44) {

+			if (la.kind == 15) {

 				Get();

 				e = ConvertToLocal(e);

 				if (e is IdentifierExpr) {

@@ -1022,7 +1053,7 @@ List<Expression!>! decreases) {
 				

 				Ident(out id);

 				RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); 

-				while (t.kind == 15) {

+				while (la.kind == 15) {

 					Get();

 					Ident(out id);

 					RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); 

@@ -1054,32 +1085,32 @@ List<Expression!>! decreases) {
 		

 	}

 

-	static void IfStmt(out Statement! ifStmt) {

-		Token! x;

+	void IfStmt(out Statement! ifStmt) {

+		IToken! x;

 		Expression guard;

 		Statement! thn;

 		Statement! s;

 		Statement els = null;

 		

 		Expect(49);

-		x = token; 

+		x = t; 

 		Guard(out guard);

 		BlockStmt(out thn);

-		if (t.kind == 50) {

+		if (la.kind == 50) {

 			Get();

-			if (t.kind == 49) {

+			if (la.kind == 49) {

 				IfStmt(out s);

 				els = s; 

-			} else if (t.kind == 6) {

+			} else if (la.kind == 6) {

 				BlockStmt(out s);

 				els = s; 

-			} else Error(115);

+			} else SynErr(115);

 		}

 		ifStmt = new IfStmt(x, guard, thn, els); 

 	}

 

-	static void WhileStmt(out Statement! stmt) {

-		Token! x;

+	void WhileStmt(out Statement! stmt) {

+		IToken! x;

 		Expression guard;

 		bool isFree;  Expression! e;

 		List<MaybeFreeExpression!> invariants = new List<MaybeFreeExpression!>();

@@ -1087,13 +1118,13 @@ List<Expression!>! decreases) {
 		Statement! body;

 		

 		Expect(51);

-		x = token; 

+		x = t; 

 		Guard(out guard);

 		assume guard == null || Owner.None(guard); 

-		while (t.kind == 22 || t.kind == 25 || t.kind == 52) {

-			if (t.kind == 22 || t.kind == 52) {

+		while (la.kind == 22 || la.kind == 25 || la.kind == 52) {

+			if (la.kind == 22 || la.kind == 52) {

 				isFree = false; 

-				if (t.kind == 22) {

+				if (la.kind == 22) {

 					Get();

 					isFree = true; 

 				}

@@ -1105,7 +1136,7 @@ List<Expression!>! decreases) {
 				Get();

 				PossiblyWildExpression(out e);

 				decreases.Add(e); 

-				while (t.kind == 15) {

+				while (la.kind == 15) {

 					Get();

 					PossiblyWildExpression(out e);

 					decreases.Add(e); 

@@ -1117,14 +1148,14 @@ List<Expression!>! decreases) {
 		stmt = new WhileStmt(x, guard, invariants, decreases, body); 

 	}

 

-	static void MatchStmt(out Statement! s) {

+	void MatchStmt(out Statement! s) {

 		Token x;  Expression! e;  MatchCaseStmt! c;

 		List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>(); 

 		Expect(38);

-		x = token; 

+		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (t.kind == 39) {

+		while (la.kind == 39) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1132,8 +1163,8 @@ List<Expression!>! decreases) {
 		s = new MatchStmt(x, e, cases); 

 	}

 

-	static void ForeachStmt(out Statement! s) {

-		Token! x, boundVar;

+	void ForeachStmt(out Statement! s) {

+		IToken! x, boundVar;

 		Type! ty;

 		Expression! collection;

 		Expression! range;

@@ -1142,30 +1173,30 @@ List<Expression!>! decreases) {
 		

 		parseVarScope.PushMarker(); 

 		Expect(54);

-		x = token;

+		x = t;

 		range = new LiteralExpr(x, true);

 		ty = new InferredTypeProxy();

 		

 		Expect(26);

 		Ident(out boundVar);

-		if (t.kind == 16) {

+		if (la.kind == 16) {

 			Get();

 			Type(out ty);

 		}

 		Expect(55);

 		Expression(out collection);

 		parseVarScope.Push(boundVar.val, boundVar.val); 

-		if (t.kind == 56) {

+		if (la.kind == 56) {

 			Get();

 			Expression(out range);

 		}

 		Expect(27);

 		Expect(6);

-		while (t.kind == 57 || t.kind == 58 || t.kind == 59) {

-			if (t.kind == 57) {

+		while (la.kind == 57 || la.kind == 58 || la.kind == 59) {

+			if (la.kind == 57) {

 				AssertStmt(out s);

 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

-			} else if (t.kind == 58) {

+			} else if (la.kind == 58) {

 				AssumeStmt(out s);

 				if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } 

 			} else {

@@ -1176,10 +1207,10 @@ List<Expression!>! decreases) {
 		if (StartOf(12)) {

 			AssignStmt(out s);

 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 

-		} else if (t.kind == 48) {

+		} else if (la.kind == 48) {

 			HavocStmt(out s);

 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 

-		} else Error(116);

+		} else SynErr(116);

 		Expect(7);

 		if (bodyAssign != null) {

 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);

@@ -1190,19 +1221,19 @@ List<Expression!>! decreases) {
 		parseVarScope.PopMarker(); 

 	}

 

-	static void LhsExpr(out Expression! e) {

+	void LhsExpr(out Expression! e) {

 		SelectExpression(out e);

 	}

 

-	static void AssignRhs(out Expression e, out Type ty) {

-		Token! x;  Expression! ee;  Type! tt;

+	void AssignRhs(out Expression e, out Type ty) {

+		IToken! x;  Expression! ee;  Type! tt;

 		e = null;  ty = null;

 		

-		if (t.kind == 45) {

+		if (la.kind == 45) {

 			Get();

 			TypeAndToken(out x, out tt);

 			ty = tt; 

-			if (t.kind == 46) {

+			if (la.kind == 46) {

 				Get();

 				Expression(out ee);

 				Expect(47);

@@ -1211,34 +1242,34 @@ List<Expression!>! decreases) {
 		} else if (StartOf(7)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(117);

+		} else SynErr(117);

 		if (e == null && ty == null) { e = dummyExpr; } 

 	}

 

-	static void SelectExpression(out Expression! e) {

-		Token! id;  e = dummyExpr; 

-		if (t.kind == 1) {

+	void SelectExpression(out Expression! e) {

+		IToken! id;  e = dummyExpr; 

+		if (la.kind == 1) {

 			IdentOrFuncExpression(out e);

-		} else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {

+		} else if (la.kind == 26 || la.kind == 92 || la.kind == 93) {

 			ObjectExpression(out e);

-		} else Error(118);

-		while (t.kind == 46 || t.kind == 89) {

+		} else SynErr(118);

+		while (la.kind == 46 || la.kind == 89) {

 			SelectOrCallSuffix(ref e);

 		}

 	}

 

-	static void IdentTypeRhs(out VarDecl! d, bool isGhost) {

-		Token! id;  Type! ty;  Expression! e;

+	void IdentTypeRhs(out VarDecl! d, bool isGhost) {

+		IToken! id;  Type! ty;  Expression! e;

 		Expression rhs = null;  Type newType = null;

 		Type optionalType = null;  DeterminedAssignmentRhs optionalRhs = null;

 		

 		Ident(out id);

-		if (t.kind == 16) {

+		if (la.kind == 16) {

 			Get();

 			Type(out ty);

 			optionalType = ty; 

 		}

-		if (t.kind == 44) {

+		if (la.kind == 44) {

 			Get();

 			AssignRhs(out rhs, out newType);

 		}

@@ -1257,33 +1288,33 @@ List<Expression!>! decreases) {
 		

 	}

 

-	static void Guard(out Expression e) {

+	void Guard(out Expression e) {

 		Expression! ee;  e = null; 

 		Expect(26);

-		if (t.kind == 36) {

+		if (la.kind == 36) {

 			Get();

 			e = null; 

 		} else if (StartOf(7)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(119);

+		} else SynErr(119);

 		Expect(27);

 	}

 

-	static void CaseStatement(out MatchCaseStmt! c) {

-		Token! x, id, arg;

+	void CaseStatement(out MatchCaseStmt! c) {

+		IToken! x, id, arg;

 		List<BoundVar!> arguments = new List<BoundVar!>();

 		List<Statement!> body = new List<Statement!>();

 		

 		Expect(39);

-		x = token;  parseVarScope.PushMarker(); 

+		x = t;  parseVarScope.PushMarker(); 

 		Ident(out id);

-		if (t.kind == 26) {

+		if (la.kind == 26) {

 			Get();

 			Ident(out arg);

 			arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

 			parseVarScope.Push(arg.val, arg.val); 

-			while (t.kind == 15) {

+			while (la.kind == 15) {

 				Get();

 				Ident(out arg);

 				arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));

@@ -1301,83 +1332,83 @@ List<Expression!>! decreases) {
 		parseVarScope.PopMarker(); 

 	}

 

-	static void CallStmtSubExpr(out Expression! e) {

+	void CallStmtSubExpr(out Expression! e) {

 		e = dummyExpr; 

-		if (t.kind == 1) {

+		if (la.kind == 1) {

 			IdentOrFuncExpression(out e);

-		} else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {

+		} else if (la.kind == 26 || la.kind == 92 || la.kind == 93) {

 			ObjectExpression(out e);

 			SelectOrCallSuffix(ref e);

-		} else Error(120);

-		while (t.kind == 46 || t.kind == 89) {

+		} else SynErr(120);

+		while (la.kind == 46 || la.kind == 89) {

 			SelectOrCallSuffix(ref e);

 		}

 	}

 

-	static void AttributeArg(out Attributes.Argument! arg) {

+	void AttributeArg(out Attributes.Argument! arg) {

 		Expression! e;  arg = dummyAttrArg; 

-		if (t.kind == 3) {

+		if (la.kind == 3) {

 			Get();

-			arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2)); 

+			arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); 

 		} else if (StartOf(7)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else Error(121);

+		} else SynErr(121);

 	}

 

-	static void EquivExpression(out Expression! e0) {

-		Token! x;  Expression! e1; 

+	void EquivExpression(out Expression! e0) {

+		IToken! x;  Expression! e1; 

 		ImpliesExpression(out e0);

-		while (t.kind == 62 || t.kind == 63) {

+		while (la.kind == 62 || la.kind == 63) {

 			EquivOp();

-			x = token; 

+			x = t; 

 			ImpliesExpression(out e1);

 			e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); 

 		}

 	}

 

-	static void ImpliesExpression(out Expression! e0) {

-		Token! x;  Expression! e1; 

+	void ImpliesExpression(out Expression! e0) {

+		IToken! x;  Expression! e1; 

 		LogicalExpression(out e0);

-		if (t.kind == 64 || t.kind == 65) {

+		if (la.kind == 64 || la.kind == 65) {

 			ImpliesOp();

-			x = token; 

+			x = t; 

 			ImpliesExpression(out e1);

 			e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); 

 		}

 	}

 

-	static void EquivOp() {

-		if (t.kind == 62) {

+	void EquivOp() {

+		if (la.kind == 62) {

 			Get();

-		} else if (t.kind == 63) {

+		} else if (la.kind == 63) {

 			Get();

-		} else Error(122);

+		} else SynErr(122);

 	}

 

-	static void LogicalExpression(out Expression! e0) {

-		Token! x;  Expression! e1; 

+	void LogicalExpression(out Expression! e0) {

+		IToken! x;  Expression! e1; 

 		RelationalExpression(out e0);

 		if (StartOf(13)) {

-			if (t.kind == 66 || t.kind == 67) {

+			if (la.kind == 66 || la.kind == 67) {

 				AndOp();

-				x = token; 

+				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (t.kind == 66 || t.kind == 67) {

+				while (la.kind == 66 || la.kind == 67) {

 					AndOp();

-					x = token; 

+					x = t; 

 					RelationalExpression(out e1);

 					e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

 				}

 			} else {

 				OrOp();

-				x = token; 

+				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (t.kind == 68 || t.kind == 69) {

+				while (la.kind == 68 || la.kind == 69) {

 					OrOp();

-					x = token; 

+					x = t; 

 					RelationalExpression(out e1);

 					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

 				}

@@ -1385,16 +1416,16 @@ List<Expression!>! decreases) {
 		}

 	}

 

-	static void ImpliesOp() {

-		if (t.kind == 64) {

+	void ImpliesOp() {

+		if (la.kind == 64) {

 			Get();

-		} else if (t.kind == 65) {

+		} else if (la.kind == 65) {

 			Get();

-		} else Error(123);

+		} else SynErr(123);

 	}

 

-	static void RelationalExpression(out Expression! e0) {

-		Token! x;  Expression! e1;  BinaryExpr.Opcode op; 

+	void RelationalExpression(out Expression! e0) {

+		IToken! x;  Expression! e1;  BinaryExpr.Opcode op; 

 		Term(out e0);

 		if (StartOf(14)) {

 			RelOp(out x, out op);

@@ -1403,206 +1434,206 @@ List<Expression!>! decreases) {
 		}

 	}

 

-	static void AndOp() {

-		if (t.kind == 66) {

+	void AndOp() {

+		if (la.kind == 66) {

 			Get();

-		} else if (t.kind == 67) {

+		} else if (la.kind == 67) {

 			Get();

-		} else Error(124);

+		} else SynErr(124);

 	}

 

-	static void OrOp() {

-		if (t.kind == 68) {

+	void OrOp() {

+		if (la.kind == 68) {

 			Get();

-		} else if (t.kind == 69) {

+		} else if (la.kind == 69) {

 			Get();

-		} else Error(125);

+		} else SynErr(125);

 	}

 

-	static void Term(out Expression! e0) {

-		Token! x;  Expression! e1;  BinaryExpr.Opcode op; 

+	void Term(out Expression! e0) {

+		IToken! x;  Expression! e1;  BinaryExpr.Opcode op; 

 		Factor(out e0);

-		while (t.kind == 79 || t.kind == 80) {

+		while (la.kind == 79 || la.kind == 80) {

 			AddOp(out x, out op);

 			Factor(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

 		}

 	}

 

-	static void RelOp(out Token! x, out BinaryExpr.Opcode op) {

+	void RelOp(out IToken! x, out BinaryExpr.Opcode op) {

 		x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

-		switch (t.kind) {

+		switch (la.kind) {

 		case 70: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Eq; 

+			x = t;  op = BinaryExpr.Opcode.Eq; 

 			break;

 		}

 		case 17: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Lt; 

+			x = t;  op = BinaryExpr.Opcode.Lt; 

 			break;

 		}

 		case 18: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Gt; 

+			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

 		}

 		case 71: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Le; 

+			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

 		case 72: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Ge; 

+			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

 		case 73: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Neq; 

+			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

 		case 74: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Disjoint; 

+			x = t;  op = BinaryExpr.Opcode.Disjoint; 

 			break;

 		}

 		case 55: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.In; 

+			x = t;  op = BinaryExpr.Opcode.In; 

 			break;

 		}

 		case 75: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.NotIn; 

+			x = t;  op = BinaryExpr.Opcode.NotIn; 

 			break;

 		}

 		case 76: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Neq; 

+			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

 		case 77: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Le; 

+			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

 		case 78: {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Ge; 

+			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: Error(126); break;

+		default: SynErr(126); break;

 		}

 	}

 

-	static void Factor(out Expression! e0) {

-		Token! x;  Expression! e1;  BinaryExpr.Opcode op; 

+	void Factor(out Expression! e0) {

+		IToken! x;  Expression! e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

-		while (t.kind == 36 || t.kind == 81 || t.kind == 82) {

+		while (la.kind == 36 || la.kind == 81 || la.kind == 82) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

 		}

 	}

 

-	static void AddOp(out Token! x, out BinaryExpr.Opcode op) {

+	void AddOp(out IToken! x, out BinaryExpr.Opcode op) {

 		x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (t.kind == 79) {

+		if (la.kind == 79) {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Add; 

-		} else if (t.kind == 80) {

+			x = t;  op = BinaryExpr.Opcode.Add; 

+		} else if (la.kind == 80) {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Sub; 

-		} else Error(127);

+			x = t;  op = BinaryExpr.Opcode.Sub; 

+		} else SynErr(127);

 	}

 

-	static void UnaryExpression(out Expression! e) {

-		Token! x;  e = dummyExpr; 

-		if (t.kind == 80) {

+	void UnaryExpression(out Expression! e) {

+		IToken! x;  e = dummyExpr; 

+		if (la.kind == 80) {

 			Get();

-			x = token; 

+			x = t; 

 			UnaryExpression(out e);

 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 

-		} else if (t.kind == 83 || t.kind == 84) {

+		} else if (la.kind == 83 || la.kind == 84) {

 			NegOp();

-			x = token; 

+			x = t; 

 			UnaryExpression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 		} else if (StartOf(12)) {

 			SelectExpression(out e);

 		} else if (StartOf(15)) {

 			ConstAtomExpression(out e);

-		} else Error(128);

+		} else SynErr(128);

 	}

 

-	static void MulOp(out Token! x, out BinaryExpr.Opcode op) {

+	void MulOp(out IToken! x, out BinaryExpr.Opcode op) {

 		x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (t.kind == 36) {

+		if (la.kind == 36) {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Mul; 

-		} else if (t.kind == 81) {

+			x = t;  op = BinaryExpr.Opcode.Mul; 

+		} else if (la.kind == 81) {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Div; 

-		} else if (t.kind == 82) {

+			x = t;  op = BinaryExpr.Opcode.Div; 

+		} else if (la.kind == 82) {

 			Get();

-			x = token;  op = BinaryExpr.Opcode.Mod; 

-		} else Error(129);

+			x = t;  op = BinaryExpr.Opcode.Mod; 

+		} else SynErr(129);

 	}

 

-	static void NegOp() {

-		if (t.kind == 83) {

+	void NegOp() {

+		if (la.kind == 83) {

 			Get();

-		} else if (t.kind == 84) {

+		} else if (la.kind == 84) {

 			Get();

-		} else Error(130);

+		} else SynErr(130);

 	}

 

-	static void ConstAtomExpression(out Expression! e) {

-		Token! x, dtName, id;  BigInteger n;  List<Expression!>! elements;

+	void ConstAtomExpression(out Expression! e) {

+		IToken! x, dtName, id;  BigInteger n;  List<Expression!>! elements;

 		e = dummyExpr;  

 		

-		switch (t.kind) {

+		switch (la.kind) {

 		case 85: {

 			Get();

-			e = new LiteralExpr(token, false); 

+			e = new LiteralExpr(t, false); 

 			break;

 		}

 		case 86: {

 			Get();

-			e = new LiteralExpr(token, true); 

+			e = new LiteralExpr(t, true); 

 			break;

 		}

 		case 87: {

 			Get();

-			e = new LiteralExpr(token); 

+			e = new LiteralExpr(t); 

 			break;

 		}

 		case 2: {

 			Nat(out n);

-			e = new LiteralExpr(token, n); 

+			e = new LiteralExpr(t, n); 

 			break;

 		}

 		case 88: {

 			Get();

-			x = token; 

+			x = t; 

 			Ident(out dtName);

 			Expect(89);

 			Ident(out id);

 			elements = new List<Expression!>(); 

-			if (t.kind == 26) {

+			if (la.kind == 26) {

 				Get();

 				if (StartOf(7)) {

 					Expressions(elements);

 				}

 				Expect(27);

 			}

-			e = new DatatypeValue(token, dtName.val, id.val, elements); 

+			e = new DatatypeValue(t, dtName.val, id.val, elements); 

 			break;

 		}

 		case 90: {

 			Get();

-			x = token; 

+			x = t; 

 			Expect(26);

 			Expression(out e);

 			Expect(27);

@@ -1611,7 +1642,7 @@ List<Expression!>! decreases) {
 		}

 		case 56: {

 			Get();

-			x = token; 

+			x = t; 

 			Expression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); 

 			Expect(56);

@@ -1619,7 +1650,7 @@ List<Expression!>! decreases) {
 		}

 		case 6: {

 			Get();

-			x = token;  elements = new List<Expression!>(); 

+			x = t;  elements = new List<Expression!>(); 

 			if (StartOf(7)) {

 				Expressions(elements);

 			}

@@ -1629,7 +1660,7 @@ List<Expression!>! decreases) {
 		}

 		case 46: {

 			Get();

-			x = token;  elements = new List<Expression!>(); 

+			x = t;  elements = new List<Expression!>(); 

 			if (StartOf(7)) {

 				Expressions(elements);

 			}

@@ -1637,14 +1668,14 @@ List<Expression!>! decreases) {
 			Expect(47);

 			break;

 		}

-		default: Error(131); break;

+		default: SynErr(131); break;

 		}

 	}

 

-	static void Nat(out BigInteger n) {

+	void Nat(out BigInteger n) {

 		Expect(2);

 		try {

-		 n = BigInteger.Parse(token.val);

+		 n = BigInteger.Parse(t.val);

 		} catch (System.FormatException) {

 		  SemErr("incorrectly formatted number");

 		  n = BigInteger.Zero;

@@ -1652,10 +1683,10 @@ List<Expression!>! decreases) {
 		

 	}

 

-	static void IdentOrFuncExpression(out Expression! e) {

-		Token! id;  e = dummyExpr;  List<Expression!>! args; 

+	void IdentOrFuncExpression(out Expression! e) {

+		IToken! id;  e = dummyExpr;  List<Expression!>! args; 

 		Ident(out id);

-		if (t.kind == 26) {

+		if (la.kind == 26) {

 			Get();

 			args = new List<Expression!>(); 

 			if (StartOf(7)) {

@@ -1674,38 +1705,38 @@ List<Expression!>! decreases) {
 		

 	}

 

-	static void ObjectExpression(out Expression! e) {

-		Token! x;  e = dummyExpr; 

-		if (t.kind == 92) {

+	void ObjectExpression(out Expression! e) {

+		IToken! x;  e = dummyExpr; 

+		if (la.kind == 92) {

 			Get();

-			e = new ThisExpr(token); 

-		} else if (t.kind == 93) {

+			e = new ThisExpr(t); 

+		} else if (la.kind == 93) {

 			Get();

-			x = token; 

+			x = t; 

 			Expect(26);

 			Expression(out e);

 			Expect(27);

 			e = new OldExpr(x, e); 

-		} else if (t.kind == 26) {

+		} else if (la.kind == 26) {

 			Get();

 			if (StartOf(16)) {

 				QuantifierGuts(out e);

 			} else if (StartOf(7)) {

 				Expression(out e);

-			} else Error(132);

+			} else SynErr(132);

 			Expect(27);

-		} else Error(133);

+		} else SynErr(133);

 	}

 

-	static void SelectOrCallSuffix(ref Expression! e) {

-		Token! id, x;  List<Expression!>! args;

+	void SelectOrCallSuffix(ref Expression! e) {

+		IToken! id, x;  List<Expression!>! args;

 		Expression e0 = null;  Expression e1 = null;  Expression! ee;  bool anyDots = false;

 		bool func = false;

 		

-		if (t.kind == 89) {

+		if (la.kind == 89) {

 			Get();

 			Ident(out id);

-			if (t.kind == 26) {

+			if (la.kind == 26) {

 				Get();

 				args = new List<Expression!>();  func = true; 

 				if (StartOf(7)) {

@@ -1715,14 +1746,14 @@ List<Expression!>! decreases) {
 				e = new FunctionCallExpr(id, id.val, e, args); 

 			}

 			if (!func) { e = new FieldSelectExpr(id, e, id.val); } 

-		} else if (t.kind == 46) {

+		} else if (la.kind == 46) {

 			Get();

-			x = token; 

+			x = t; 

 			if (StartOf(7)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (t.kind == 44 || t.kind == 91) {

-					if (t.kind == 91) {

+				if (la.kind == 44 || la.kind == 91) {

+					if (la.kind == 91) {

 						Get();

 						anyDots = true; 

 						if (StartOf(7)) {

@@ -1735,11 +1766,11 @@ List<Expression!>! decreases) {
 						e1 = ee; 

 					}

 				}

-			} else if (t.kind == 91) {

+			} else if (la.kind == 91) {

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else Error(134);

+			} else SynErr(134);

 			if (!anyDots && e0 == null) {

 			 /* a parsing error occurred */

 			 e0 = dummyExpr;

@@ -1757,35 +1788,35 @@ List<Expression!>! decreases) {
 			}

 			

 			Expect(47);

-		} else Error(135);

+		} else SynErr(135);

 	}

 

-	static void QuantifierGuts(out Expression! q) {

-		Token! x = Token.NoToken;

+	void QuantifierGuts(out Expression! q) {

+		IToken! x = Token.NoToken;

 		bool univ = false;

 		BoundVar! bv;

 		List<BoundVar!> bvars = new List<BoundVar!>();

-		Token! tok;  Expr! e;  ExprSeq! es;

+		IToken! tok;  Expr! e;  ExprSeq! es;

 		Attributes attrs = null;

 		Triggers trigs = null;

 		Expression! body;

 		

-		if (t.kind == 94 || t.kind == 95) {

+		if (la.kind == 94 || la.kind == 95) {

 			Forall();

-			x = token;  univ = true; 

-		} else if (t.kind == 96 || t.kind == 97) {

+			x = t;  univ = true; 

+		} else if (la.kind == 96 || la.kind == 97) {

 			Exists();

-			x = token; 

-		} else Error(136);

+			x = t; 

+		} else SynErr(136);

 		parseVarScope.PushMarker(); 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

 			IdentTypeOptional(out bv);

 			bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

 		}

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			AttributeOrTrigger(ref attrs, ref trigs);

 		}

 		QSep();

@@ -1799,56 +1830,56 @@ List<Expression!>! decreases) {
 		

 	}

 

-	static void Forall() {

-		if (t.kind == 94) {

+	void Forall() {

+		if (la.kind == 94) {

 			Get();

-		} else if (t.kind == 95) {

+		} else if (la.kind == 95) {

 			Get();

-		} else Error(137);

+		} else SynErr(137);

 	}

 

-	static void Exists() {

-		if (t.kind == 96) {

+	void Exists() {

+		if (la.kind == 96) {

 			Get();

-		} else if (t.kind == 97) {

+		} else if (la.kind == 97) {

 			Get();

-		} else Error(138);

+		} else SynErr(138);

 	}

 

-	static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {

+	void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {

 		List<Expression!> es = new List<Expression!>();

 		

 		Expect(6);

-		if (t.kind == 16) {

+		if (la.kind == 16) {

 			AttributeBody(ref attrs);

 		} else if (StartOf(7)) {

 			es = new List<Expression!>(); 

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else Error(139);

+		} else SynErr(139);

 		Expect(7);

 	}

 

-	static void QSep() {

-		if (t.kind == 98) {

+	void QSep() {

+		if (la.kind == 98) {

 			Get();

-		} else if (t.kind == 99) {

+		} else if (la.kind == 99) {

 			Get();

-		} else Error(140);

+		} else SynErr(140);

 	}

 

-	static void AttributeBody(ref Attributes attrs) {

+	void AttributeBody(ref Attributes attrs) {

 		string aName;

 		List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();

 		Attributes.Argument! aArg;

 		

 		Expect(16);

 		Expect(1);

-		aName = token.val; 

+		aName = t.val; 

 		if (StartOf(17)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

-			while (t.kind == 15) {

+			while (la.kind == 15) {

 				Get();

 				AttributeArg(out aArg);

 				aArgs.Add(aArg); 

@@ -1859,120 +1890,150 @@ List<Expression!>! decreases) {
 

 

 

-	public static void Parse() {

-		Errors.SynErr = new ErrorProc(SynErr);

-		t = new Token();

+	public void Parse() {

+		la = new Token();

+		la.val = "";		

 		Get();

 		Dafny();

 

+    Expect(0);

 	}

+	

+	static readonly bool[,]! set = {

+		{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,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, x,x,x,x, x,x,x,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,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,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,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, 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,x,x, x,x,x,x, x,T,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,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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,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, T,T,x,x, x,x,x,x, x,x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},

+		{x,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,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,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, T,T,x,x, x,x,x,x, x,x},

+		{x,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,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, 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,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,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x, x,x,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,T,x, x,x,x,x, x,x,x,x, 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,T,T,T, T,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},

+		{x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x}

 

-	[Microsoft.Contracts.Verify(false)]

-	static void SynErr(int n, string filename, int line, int col) {

-		Errors.count++;

-		System.Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);

+	};

+} // end Parser

+

+

+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 string errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text

+  public string! errMsgFormat4 = "{0}({1},{2}): Error: {3}"; // 0=line, 1=column, 2=text

+  public string! errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text

+  

+	public void SynErr (string filename, int line, int col, int n) {

 		string s;

+		Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);

 		switch (n) {

 			case 0: s = "EOF expected"; break;

 			case 1: s = "ident expected"; break;

 			case 2: s = "digits expected"; break;

 			case 3: s = "string expected"; break;

-			case 4: s = "module expected"; break;

-			case 5: s = "imports expected"; break;

-			case 6: s = "{ expected"; break;

-			case 7: s = "} expected"; break;

-			case 8: s = "class expected"; break;

-			case 9: s = "ghost expected"; break;

-			case 10: s = "static expected"; break;

-			case 11: s = "unlimited expected"; break;

-			case 12: s = "datatype expected"; break;

-			case 13: s = "; expected"; break;

-			case 14: s = "var expected"; break;

-			case 15: s = ", expected"; break;

-			case 16: s = ": expected"; break;

-			case 17: s = "< expected"; break;

-			case 18: s = "> expected"; break;

-			case 19: s = "method expected"; break;

-			case 20: s = "returns expected"; break;

-			case 21: s = "modifies expected"; break;

-			case 22: s = "free expected"; break;

-			case 23: s = "requires expected"; break;

-			case 24: s = "ensures expected"; break;

-			case 25: s = "decreases expected"; break;

-			case 26: s = "( expected"; break;

-			case 27: s = ") expected"; break;

-			case 28: s = "bool expected"; break;

-			case 29: s = "int expected"; break;

-			case 30: s = "set expected"; break;

-			case 31: s = "seq expected"; break;

-			case 32: s = "object expected"; break;

-			case 33: s = "array expected"; break;

-			case 34: s = "function expected"; break;

-			case 35: s = "reads expected"; break;

-			case 36: s = "* expected"; break;

-			case 37: s = "` expected"; break;

-			case 38: s = "match expected"; break;

-			case 39: s = "case expected"; break;

-			case 40: s = "=> expected"; break;

-			case 41: s = "label expected"; break;

-			case 42: s = "break expected"; break;

-			case 43: s = "return expected"; break;

-			case 44: s = ":= expected"; break;

-			case 45: s = "new expected"; break;

-			case 46: s = "[ expected"; break;

-			case 47: s = "] expected"; break;

-			case 48: s = "havoc expected"; break;

-			case 49: s = "if expected"; break;

-			case 50: s = "else expected"; break;

-			case 51: s = "while expected"; break;

-			case 52: s = "invariant expected"; break;

-			case 53: s = "call expected"; break;

-			case 54: s = "foreach expected"; break;

-			case 55: s = "in expected"; break;

-			case 56: s = "| expected"; break;

-			case 57: s = "assert expected"; break;

-			case 58: s = "assume expected"; break;

-			case 59: s = "use expected"; break;

-			case 60: s = "print expected"; break;

-			case 61: s = "then expected"; break;

-			case 62: s = "<==> expected"; break;

-			case 63: s = "\\u21d4 expected"; break;

-			case 64: s = "==> expected"; break;

-			case 65: s = "\\u21d2 expected"; break;

-			case 66: s = "&& expected"; break;

-			case 67: s = "\\u2227 expected"; break;

-			case 68: s = "|| expected"; break;

-			case 69: s = "\\u2228 expected"; break;

-			case 70: s = "== expected"; break;

-			case 71: s = "<= expected"; break;

-			case 72: s = ">= expected"; break;

-			case 73: s = "!= expected"; break;

-			case 74: s = "!! expected"; break;

-			case 75: s = "!in expected"; break;

-			case 76: s = "\\u2260 expected"; break;

-			case 77: s = "\\u2264 expected"; break;

-			case 78: s = "\\u2265 expected"; break;

-			case 79: s = "+ expected"; break;

-			case 80: s = "- expected"; break;

-			case 81: s = "/ expected"; break;

-			case 82: s = "% expected"; break;

-			case 83: s = "! expected"; break;

-			case 84: s = "\\u00ac expected"; break;

-			case 85: s = "false expected"; break;

-			case 86: s = "true expected"; break;

-			case 87: s = "null expected"; break;

-			case 88: s = "# expected"; break;

-			case 89: s = ". expected"; break;

-			case 90: s = "fresh expected"; break;

-			case 91: s = ".. expected"; break;

-			case 92: s = "this expected"; break;

-			case 93: s = "old expected"; break;

-			case 94: s = "forall expected"; break;

-			case 95: s = "\\u2200 expected"; break;

-			case 96: s = "exists expected"; break;

-			case 97: s = "\\u2203 expected"; break;

-			case 98: s = ":: expected"; break;

-			case 99: s = "\\u2022 expected"; break;

+			case 4: s = "\"module\" expected"; break;

+			case 5: s = "\"imports\" expected"; break;

+			case 6: s = "\"{\" expected"; break;

+			case 7: s = "\"}\" expected"; break;

+			case 8: s = "\"class\" expected"; break;

+			case 9: s = "\"ghost\" expected"; break;

+			case 10: s = "\"static\" expected"; break;

+			case 11: s = "\"unlimited\" expected"; break;

+			case 12: s = "\"datatype\" expected"; break;

+			case 13: s = "\";\" expected"; break;

+			case 14: s = "\"var\" expected"; break;

+			case 15: s = "\",\" expected"; break;

+			case 16: s = "\":\" expected"; break;

+			case 17: s = "\"<\" expected"; break;

+			case 18: s = "\">\" expected"; break;

+			case 19: s = "\"method\" expected"; break;

+			case 20: s = "\"returns\" expected"; break;

+			case 21: s = "\"modifies\" expected"; break;

+			case 22: s = "\"free\" expected"; break;

+			case 23: s = "\"requires\" expected"; break;

+			case 24: s = "\"ensures\" expected"; break;

+			case 25: s = "\"decreases\" expected"; break;

+			case 26: s = "\"(\" expected"; break;

+			case 27: s = "\")\" expected"; break;

+			case 28: s = "\"bool\" expected"; break;

+			case 29: s = "\"int\" expected"; break;

+			case 30: s = "\"set\" expected"; break;

+			case 31: s = "\"seq\" expected"; break;

+			case 32: s = "\"object\" expected"; break;

+			case 33: s = "\"array\" expected"; break;

+			case 34: s = "\"function\" expected"; break;

+			case 35: s = "\"reads\" expected"; break;

+			case 36: s = "\"*\" expected"; break;

+			case 37: s = "\"`\" expected"; break;

+			case 38: s = "\"match\" expected"; break;

+			case 39: s = "\"case\" expected"; break;

+			case 40: s = "\"=>\" expected"; break;

+			case 41: s = "\"label\" expected"; break;

+			case 42: s = "\"break\" expected"; break;

+			case 43: s = "\"return\" expected"; break;

+			case 44: s = "\":=\" expected"; break;

+			case 45: s = "\"new\" expected"; break;

+			case 46: s = "\"[\" expected"; break;

+			case 47: s = "\"]\" expected"; break;

+			case 48: s = "\"havoc\" expected"; break;

+			case 49: s = "\"if\" expected"; break;

+			case 50: s = "\"else\" expected"; break;

+			case 51: s = "\"while\" expected"; break;

+			case 52: s = "\"invariant\" expected"; break;

+			case 53: s = "\"call\" expected"; break;

+			case 54: s = "\"foreach\" expected"; break;

+			case 55: s = "\"in\" expected"; break;

+			case 56: s = "\"|\" expected"; break;

+			case 57: s = "\"assert\" expected"; break;

+			case 58: s = "\"assume\" expected"; break;

+			case 59: s = "\"use\" expected"; break;

+			case 60: s = "\"print\" expected"; break;

+			case 61: s = "\"then\" expected"; break;

+			case 62: s = "\"<==>\" expected"; break;

+			case 63: s = "\"\\u21d4\" expected"; break;

+			case 64: s = "\"==>\" expected"; break;

+			case 65: s = "\"\\u21d2\" expected"; break;

+			case 66: s = "\"&&\" expected"; break;

+			case 67: s = "\"\\u2227\" expected"; break;

+			case 68: s = "\"||\" expected"; break;

+			case 69: s = "\"\\u2228\" expected"; break;

+			case 70: s = "\"==\" expected"; break;

+			case 71: s = "\"<=\" expected"; break;

+			case 72: s = "\">=\" expected"; break;

+			case 73: s = "\"!=\" expected"; break;

+			case 74: s = "\"!!\" expected"; break;

+			case 75: s = "\"!in\" expected"; break;

+			case 76: s = "\"\\u2260\" expected"; break;

+			case 77: s = "\"\\u2264\" expected"; break;

+			case 78: s = "\"\\u2265\" expected"; break;

+			case 79: s = "\"+\" expected"; break;

+			case 80: s = "\"-\" expected"; break;

+			case 81: s = "\"/\" expected"; break;

+			case 82: s = "\"%\" expected"; break;

+			case 83: s = "\"!\" expected"; break;

+			case 84: s = "\"\\u00ac\" expected"; break;

+			case 85: s = "\"false\" expected"; break;

+			case 86: s = "\"true\" expected"; break;

+			case 87: s = "\"null\" expected"; break;

+			case 88: s = "\"#\" expected"; break;

+			case 89: s = "\".\" expected"; break;

+			case 90: s = "\"fresh\" expected"; break;

+			case 91: s = "\"..\" expected"; break;

+			case 92: s = "\"this\" expected"; break;

+			case 93: s = "\"old\" expected"; break;

+			case 94: s = "\"forall\" expected"; break;

+			case 95: s = "\"\\u2200\" expected"; break;

+			case 96: s = "\"exists\" expected"; break;

+			case 97: s = "\"\\u2203\" expected"; break;

+			case 98: s = "\"::\" expected"; break;

+			case 99: s = "\"\\u2022\" expected"; break;

 			case 100: s = "??? expected"; break;

 			case 101: s = "invalid ClassMemberDecl"; break;

 			case 102: s = "invalid FunctionDecl"; break;

@@ -2017,33 +2078,42 @@ List<Expression!>! decreases) {
 

 			default: s = "error " + n; break;

 		}

-		System.Console.WriteLine(s);

-	}

-

-	static bool[,]! set = {

-	{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,x, x,x,x,x, x,x,x,x, x,x},

-	{x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, x,x,x,x, x,x,x,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,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,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,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, 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,x,x, x,x,x,x, x,T,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,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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},

-	{x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,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, T,T,x,x, x,x,x,x, x,x},

-	{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},

-	{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},

-	{x,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,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,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, T,T,x,x, x,x,x,x, x,x},

-	{x,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,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, 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,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,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x, x,x,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,T,x, x,x,x,x, x,x,x,x, 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,T,T,T, T,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},

-	{x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x}

+		//errorStream.WriteLine(errMsgFormat, line, col, s);

+		errorStream.WriteLine(s);

+		count++;

+	}

 

-	};

+	public void SemErr (int line, int col, string! s) {

+		errorStream.WriteLine(errMsgFormat, line, col, s);

+		count++;

+	}

 

-	[Microsoft.Contracts.Verify(false)]

-	static Parser() {}

-} // end Parser

+	public void SemErr (string filename, int line, int col, string! s) {

+		errorStream.WriteLine(errMsgFormat4, filename, line, col, s);

+		count++;

+	}

+	

+	public void SemErr (string s) {

+		errorStream.WriteLine(s);

+		count++;

+	}

+

+    public void SemErr(IToken! tok, string! msg) {  // semantic errors

+      SemErr(tok.filename, tok.line, tok.col, msg);

+    }

+	

+	public void Warning (int line, int col, string s) {

+		errorStream.WriteLine(errMsgFormat, line, col, s);

+	}

+	

+	public void Warning(string s) {

+		errorStream.WriteLine(s);

+	}

+} // Errors

+

+

+public class FatalError: Exception {

+	public FatalError(string m): base(m) {}

+}

 

-} // end namespace

+}
\ No newline at end of file
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc
index 671469f3..701668db 100644
--- a/Dafny/Resolver.ssc
+++ b/Dafny/Resolver.ssc
@@ -7,11 +7,12 @@ using System;
 using System.Collections.Generic;

 using System.Numerics;

 using Microsoft.Contracts;

+using Microsoft.Boogie;

 

 namespace Microsoft.Dafny {

   public class Resolver {

     public int ErrorCount = 0;

-    void Error(Token! tok, string! msg, params object[] args) {

+    void Error(IToken! tok, string! msg, params object[] args) {

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

       Console.WriteLine("{0}({1},{2}): Error: {3}",

@@ -1370,7 +1371,7 @@ namespace Microsoft.Dafny {
       return rr.EType;

     }

 

-    MemberDecl ResolveMember(Token! tok, Type! receiverType, string! memberName, out UserDefinedType ctype)

+    MemberDecl ResolveMember(IToken! tok, Type! receiverType, string! memberName, out UserDefinedType ctype)

       ensures result != null ==> ctype != null && ctype.ResolvedClass != null;

     {

       ctype = UserDefinedType.DenotesClass(receiverType);

@@ -1455,7 +1456,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public static UserDefinedType! GetThisType(Token! tok, ClassDecl! cl) {

+    public static UserDefinedType! GetThisType(IToken! tok, ClassDecl! cl) {

       List<Type!> args = new List<Type!>();

       foreach (TypeParameter tp in cl.TypeArgs) {

         args.Add(new UserDefinedType(tok, tp.Name, tp));

diff --git a/Dafny/Scanner.ssc b/Dafny/Scanner.ssc
index 5fdeefed..98114e54 100644
--- a/Dafny/Scanner.ssc
+++ b/Dafny/Scanner.ssc
@@ -1,248 +1,437 @@
+

+using System;

 using System.IO;

 using System.Collections;

 using System.Collections.Generic;

 using System.Text;

 using Microsoft.Contracts;

-using Bpl = Microsoft.Boogie;

+using Microsoft.Boogie;

 using BoogiePL;

+namespace Microsoft.Dafny {

 

 

-namespace Microsoft.Dafny {

+//-----------------------------------------------------------------------------------

+// Buffer

+//-----------------------------------------------------------------------------------

+public class Buffer {

+	// This Buffer supports the following cases:

+	// 1) seekable stream (file)

+	//    a) whole stream in buffer

+	//    b) part of stream in buffer

+	// 2) non seekable stream (network, console)

+  

+	public const int EOF = 65535 + 1; // char.MaxValue + 1;

+	const int MIN_BUFFER_LENGTH = 1024; // 1KB

+	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

+	byte[]! buf;         // input buffer

+	int bufStart;       // position of first byte in buffer relative to input stream

+	int bufLen;         // length of buffer

+	int fileLen;        // length of input stream (may change if the stream is no file)

+	int bufPos;         // current position in buffer

+	Stream! stream;      // input stream (seekable)

+	bool isUserStream;  // was the stream opened by the user?

+

+    [NotDelayed]

+	public Buffer (Stream! s, bool isUserStream) {

+		stream = s; this.isUserStream = isUserStream;

+		

+		int fl, bl;

+		if (s.CanSeek) {

+			fl = (int) s.Length;

+			bl = fl < MAX_BUFFER_LENGTH ? fl : MAX_BUFFER_LENGTH; // Math.Min(fileLen, MAX_BUFFER_LENGTH);

+			bufStart = Int32.MaxValue; // nothing in the buffer so far

+		} else {

+			fl = bl = bufStart = 0;

+		}

+

+		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

+		fileLen = fl;  bufLen = bl;

+		base();

+		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

+		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

+		if (bufLen == fileLen && s.CanSeek) Close();

+	}

+	

+	protected Buffer(Buffer! b) { // called in UTF8Buffer constructor

+		buf = b.buf;

+		bufStart = b.bufStart;

+		bufLen = b.bufLen;

+		fileLen = b.fileLen;

+		bufPos = b.bufPos;

+		stream = b.stream;

+		// keep destructor from closing the stream

+		//b.stream = null;

+		isUserStream = b.isUserStream;

+		// keep destructor from closing the stream

+		b.isUserStream = true;

+	}

+

+	~Buffer() { Close(); }

+	

+	protected void Close() {

+		if (!isUserStream && stream != null) {

+			stream.Close();

+			//stream = null;

+		}

+	}

+	

+	public virtual int Read () {

+		if (bufPos < bufLen) {

+			return buf[bufPos++];

+		} else if (Pos < fileLen) {

+			Pos = Pos; // shift buffer start to Pos

+			return buf[bufPos++];

+		} else if (stream != null && !stream.CanSeek && ReadNextStreamChunk() > 0) {

+			return buf[bufPos++];

+		} else {

+			return EOF;

+		}

+	}

+

+	public int Peek () {

+		int curPos = Pos;

+		int ch = Read();

+		Pos = curPos;

+		return ch;

+	}

+	

+	public string! GetString (int beg, int end) {

+		int len = 0;

+		char[] buf = new char[end - beg];

+		int oldPos = Pos;

+		Pos = beg;

+		while (Pos < end) buf[len++] = (char) Read();

+		Pos = oldPos;

+		return new String(buf, 0, len);

+	}

+

+	public int Pos {

+		get { return bufPos + bufStart; }

+		set {

+			if (value >= fileLen && stream != null && !stream.CanSeek) {

+				// Wanted position is after buffer and the stream

+				// is not seek-able e.g. network or console,

+				// thus we have to read the stream manually till

+				// the wanted position is in sight.

+				while (value >= fileLen && ReadNextStreamChunk() > 0);

+			}

 

-  [Immutable]

-  public class Token : Bpl.Token {

-    public Token();

-    public Token(int linenum, int colnum) {

-      base(linenum, colnum);

-    }

-    public new static Token! NoToken = new Token();

-  }

+			if (value < 0 || value > fileLen) {

+				throw new FatalError("buffer out of bounds access, position: " + value);

+			}

 

+			if (value >= bufStart && value < bufStart + bufLen) { // already in buffer

+				bufPos = value - bufStart;

+			} else if (stream != null) { // must be swapped in

+				stream.Seek(value, SeekOrigin.Begin);

+				bufLen = stream.Read(buf, 0, buf.Length);

+				bufStart = value; bufPos = 0;

+			} else {

+				// set the position to the end of the file, Pos will return fileLen.

+				bufPos = fileLen - bufStart;

+			}

+		}

+	}

+	

+	// Read the next chunk of bytes from the stream, increases the buffer

+	// if needed and updates the fields fileLen and bufLen.

+	// Returns the number of bytes read.

+	private int ReadNextStreamChunk() {

+		int free = buf.Length - bufLen;

+		if (free == 0) {

+			// in the case of a growing input stream

+			// we can neither seek in the stream, nor can we

+			// foresee the maximum length, thus we must adapt

+			// the buffer size on demand.

+			byte[] newBuf = new byte[bufLen * 2];

+			Array.Copy(buf, newBuf, bufLen);

+			buf = newBuf;

+			free = bufLen;

+		}

+		int read = stream.Read(buf, bufLen, free);

+		if (read > 0) {

+			fileLen = bufLen = (bufLen + read);

+			return read;

+		}

+		// end of stream reached

+		return 0;

+	}

 }

 

-namespace Microsoft.Dafny {

+//-----------------------------------------------------------------------------------

+// UTF8Buffer

+//-----------------------------------------------------------------------------------

+public class UTF8Buffer: Buffer {

+	public UTF8Buffer(Buffer! b): base(b) {}

 

+	public override int Read() {

+		int ch;

+		do {

+			ch = base.Read();

+			// until we find a utf8 start (0xxxxxxx or 11xxxxxx)

+		} while ((ch >= 128) && ((ch & 0xC0) != 0xC0) && (ch != EOF));

+		if (ch < 128 || ch == EOF) {

+			// nothing to do, first 127 chars are the same in ascii and utf8

+			// 0xxxxxxx or end of file character

+		} else if ((ch & 0xF0) == 0xF0) {

+			// 11110xxx 10xxxxxx 10xxxxxx 10xxxxxx

+			int c1 = ch & 0x07; ch = base.Read();

+			int c2 = ch & 0x3F; ch = base.Read();

+			int c3 = ch & 0x3F; ch = base.Read();

+			int c4 = ch & 0x3F;

+			ch = (((((c1 << 6) | c2) << 6) | c3) << 6) | c4;

+		} else if ((ch & 0xE0) == 0xE0) {

+			// 1110xxxx 10xxxxxx 10xxxxxx

+			int c1 = ch & 0x0F; ch = base.Read();

+			int c2 = ch & 0x3F; ch = base.Read();

+			int c3 = ch & 0x3F;

+			ch = (((c1 << 6) | c2) << 6) | c3;

+		} else if ((ch & 0xC0) == 0xC0) {

+			// 110xxxxx 10xxxxxx

+			int c1 = ch & 0x1F; ch = base.Read();

+			int c2 = ch & 0x3F;

+			ch = (c1 << 6) | c2;

+		}

+		return ch;

+	}

+}

 

+//-----------------------------------------------------------------------------------

+// Scanner

+//-----------------------------------------------------------------------------------

 public class Scanner {

-  const char EOF = '\0';

-  const char CR  = '\r';

-  const char LF  = '\n';

+	const char EOL = '\n';

+	const int eofSym = 0; /* pdt */

+	const int maxT = 100;

+	const int noSym = 100;

+

+

+	public Buffer! buffer; // scanner buffer

+	

+	Token! t;          // current token

+	int ch;           // current input character

+	int pos;          // byte position of current character

+	int col;          // column number of current character

+	int line;         // line number of current character

+	int oldEols;      // EOLs that appeared in a comment;

+	static readonly Hashtable! start; // maps first token character to start state

 

-  [Microsoft.Contracts.Verify(false)]

+	Token! tokens;     // list of tokens already peeked (first token is a dummy)

+	Token! pt;         // current peek token

+	

+	char[]! tval = new char[128]; // text of current token

+	int tlen;         // length of current token

+	

+	private string! Filename;

+	private Errors! errorHandler;

+	

 	static Scanner() {

-		start[0] = 55;

-		start[33] = 35;

-		start[34] = 3;

-		start[35] = 48;

-		start[37] = 46;

-		start[38] = 29;

-		start[39] = 1;

-		start[40] = 12;

-		start[41] = 13;

-		start[42] = 14;

-		start[43] = 43;

-		start[44] = 8;

-		start[45] = 44;

-		start[46] = 49;

-		start[47] = 45;

-		start[48] = 2;

-		start[49] = 2;

-		start[50] = 2;

-		start[51] = 2;

-		start[52] = 2;

-		start[53] = 2;

-		start[54] = 2;

-		start[55] = 2;

-		start[56] = 2;

-		start[57] = 2;

-		start[58] = 9;

-		start[59] = 7;

-		start[60] = 10;

-		start[61] = 16;

-		start[62] = 11;

-		start[63] = 1;

-		start[65] = 1;

-		start[66] = 1;

-		start[67] = 1;

-		start[68] = 1;

-		start[69] = 1;

-		start[70] = 1;

-		start[71] = 1;

-		start[72] = 1;

-		start[73] = 1;

-		start[74] = 1;

-		start[75] = 1;

-		start[76] = 1;

-		start[77] = 1;

-		start[78] = 1;

-		start[79] = 1;

-		start[80] = 1;

-		start[81] = 1;

-		start[82] = 1;

-		start[83] = 1;

-		start[84] = 1;

-		start[85] = 1;

-		start[86] = 1;

-		start[87] = 1;

-		start[88] = 1;

-		start[89] = 1;

-		start[90] = 1;

-		start[91] = 19;

-		start[92] = 1;

-		start[93] = 20;

-		start[95] = 1;

-		start[96] = 15;

-		start[97] = 1;

-		start[98] = 1;

-		start[99] = 1;

-		start[100] = 1;

-		start[101] = 1;

-		start[102] = 1;

-		start[103] = 1;

-		start[104] = 1;

-		start[105] = 1;

-		start[106] = 1;

-		start[107] = 1;

-		start[108] = 1;

-		start[109] = 1;

-		start[110] = 1;

-		start[111] = 1;

-		start[112] = 1;

-		start[113] = 1;

-		start[114] = 1;

-		start[115] = 1;

-		start[116] = 1;

-		start[117] = 1;

-		start[118] = 1;

-		start[119] = 1;

-		start[120] = 1;

-		start[121] = 1;

-		start[122] = 1;

-		start[123] = 5;

-		start[124] = 21;

-		start[125] = 6;

-		start[172] = 47;

-		start[8226] = 54;

-		start[8658] = 28;

-		start[8660] = 25;

-		start[8704] = 51;

-		start[8707] = 52;

-		start[8743] = 31;

-		start[8744] = 33;

-		start[8800] = 40;

-		start[8804] = 41;

-		start[8805] = 42;

+		start = new Hashtable(128);

+		for (int i = 39; i <= 39; ++i) start[i] = 1;

+		for (int i = 63; i <= 63; ++i) start[i] = 1;

+		for (int i = 65; i <= 90; ++i) start[i] = 1;

+		for (int i = 92; i <= 92; ++i) start[i] = 1;

+		for (int i = 95; i <= 95; ++i) start[i] = 1;

+		for (int i = 97; i <= 122; ++i) start[i] = 1;

+		for (int i = 48; i <= 57; ++i) start[i] = 2;

+		for (int i = 34; i <= 34; ++i) start[i] = 3;

+		start[123] = 5; 

+		start[125] = 6; 

+		start[59] = 7; 

+		start[44] = 8; 

+		start[58] = 46; 

+		start[60] = 47; 

+		start[62] = 48; 

+		start[40] = 9; 

+		start[41] = 10; 

+		start[42] = 11; 

+		start[96] = 12; 

+		start[61] = 49; 

+		start[91] = 15; 

+		start[93] = 16; 

+		start[124] = 50; 

+		start[8660] = 19; 

+		start[8658] = 21; 

+		start[38] = 22; 

+		start[8743] = 24; 

+		start[8744] = 26; 

+		start[33] = 51; 

+		start[8800] = 32; 

+		start[8804] = 33; 

+		start[8805] = 34; 

+		start[43] = 35; 

+		start[45] = 36; 

+		start[47] = 37; 

+		start[37] = 38; 

+		start[172] = 39; 

+		start[35] = 40; 

+		start[46] = 52; 

+		start[8704] = 42; 

+		start[8707] = 43; 

+		start[8226] = 45; 

+		start[Buffer.EOF] = -1;

+

 	}

-	const int noSym = 100;

-	static short[] start = new short[16385];

-

-

-

-  static Token/*!*/ t;          // current token

-  static char ch;               // current input character

-  static int pos;               // column number of current character

-  static int line;              // line number of current character

-  static int lineStart;         // start position of current line

-  static Queue! oldEols;        // EOLs that appeared in a comment;

-  static BitArray/*!*/ ignore;  // set of characters to be ignored by the scanner  

-  static string Filename;

-

-  ///<summary>

-  ///Initializes the scanner. Note: first fill the Buffer.

-  ///</summary>

-  ///<param name="filename">File name used for error reporting</param>

-  public static void Init (string filename) {

-    Filename = filename;

-    pos = -1; line = 1; lineStart = 0;

-    oldEols = new Queue();

-    NextCh();

-		ignore = new BitArray(16384);

-		ignore[9] = true; ignore[10] = true; ignore[13] = true; ignore[32] = true; 

-		

-  }

-  

-  private static void NextCh() {

-    if (oldEols.Count > 0) {

-      ch = (char) ((!)oldEols.Dequeue());

-    } else {

-      while (true) {

-        ch = (char)BoogiePL.Buffer.Read(); pos++;

-        if (ch == BoogiePL.Buffer.eof) {

-          ch = EOF;

-        } else if (ch == LF) {

-          line++;

-          lineStart = pos + 1;

-

-        } else if (ch == '#' && pos == lineStart) {

-          int prLine = line;

-          int prColumn = pos - lineStart;  // which is 0

-

-          string hashLine = BoogiePL.Buffer.ReadToEOL();  pos += hashLine.Length;

-          line++;

-          lineStart = pos + 1;

-

-          hashLine = hashLine.TrimEnd(null);

-          if (hashLine.StartsWith("line ") || hashLine == "line") {

-            // parse #line pragma:  #line num [filename]

-            string h = hashLine.Substring(4).TrimStart(null);

-            int x = h.IndexOf(' ');

-            if (x == -1) {

-              x = h.Length;  // this will be convenient below when we look for a filename

-            }

-            try {

-              int li = int.Parse(h.Substring(0, x));

-

-              h = h.Substring(x).Trim();

-

-              // act on #line

-              line = li;

-              if (h.Length != 0) {

-                // a filename was specified

-                Filename = h;

-              }

-              continue;  // successfully parsed and acted on the #line pragma

-

-            } catch (System.FormatException) {

-              // just fall down through to produce an error message

-            }

-            Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);

-            continue;

-          }

-

-          Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);

-          continue;

-        }

-        return;

-      }

-    }

-  }

-  

-
-	static bool Comment0() {

-		int level = 1, line0 = line, lineStart0 = lineStart;

+	

+	[NotDelayed]

+	public Scanner (string! fileName, Errors! errorHandler) {

+		this.errorHandler = errorHandler;

+		pt = tokens = new Token();  // first token is a dummy

+		t = new Token(); // dummy because t is a non-null field

+		try {

+			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

+			buffer = new Buffer(stream, false);

+			Filename = fileName;

+			base();

+			Init();

+		} catch (IOException) {

+			throw new FatalError("Cannot open file " + fileName);

+		}

+	}

+	

+	[NotDelayed]

+	public Scanner (Stream! s, Errors! errorHandler, string! fileName) {

+		pt = tokens = new Token();  // first token is a dummy

+		t = new Token(); // dummy because t is a non-null field

+		buffer = new Buffer(s, true);

+		this.errorHandler = errorHandler;

+		this.Filename = fileName;

+		base();

+		Init();

+	}

+	

+	void Init() {

+		pos = -1; line = 1; col = 0;

+		oldEols = 0;

+		NextCh();

+		if (ch == 0xEF) { // check optional byte order mark for UTF-8

+			NextCh(); int ch1 = ch;

+			NextCh(); int ch2 = ch;

+			if (ch1 != 0xBB || ch2 != 0xBF) {

+				throw new FatalError(String.Format("illegal byte order mark: EF {0,2:X} {1,2:X}", ch1, ch2));

+			}

+			buffer = new UTF8Buffer(buffer); col = 0;

+			NextCh();

+		}

+		pt = tokens = new Token();  // first token is a dummy

+	}

+

+	string! ReadToEOL(){

+	  int p = buffer.Pos;

+	  int ch = buffer.Read();

+      // replace isolated '\r' by '\n' in order to make

+	  // eol handling uniform across Windows, Unix and Mac

+	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

+	  while (ch != EOL && ch != Buffer.EOF){

+	    ch = buffer.Read();

+		// replace isolated '\r' by '\n' in order to make

+		// eol handling uniform across Windows, Unix and Mac

+		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

+	  }

+	  string! s = buffer.GetString(p, buffer.Pos);

+	  return s;

+	}

+

+	void NextCh() {

+		if (oldEols > 0) { ch = EOL; oldEols--; } 

+		else {

+//			pos = buffer.Pos;

+//			ch = buffer.Read(); col++;

+//			// replace isolated '\r' by '\n' in order to make

+//			// eol handling uniform across Windows, Unix and Mac

+//			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

+//			if (ch == EOL) { line++; col = 0; }

+			

+			while (true) {

+			    pos = buffer.Pos;

+				ch = buffer.Read(); col++;

+				// replace isolated '\r' by '\n' in order to make

+				// eol handling uniform across Windows, Unix and Mac

+				if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

+				if (ch == EOL) {

+					line++; col = 0; 

+				} else if (ch == '#' && col == 1) {

+				  int prLine = line;

+				  int prColumn = 0;

+

+				  string! hashLine = ReadToEOL();

+				  col = 0;

+				  line++;

+

+				  hashLine = hashLine.TrimEnd(null);

+				  if (hashLine.StartsWith("line ") || hashLine == "line") {

+					// parse #line pragma:  #line num [filename]

+					string h = hashLine.Substring(4).TrimStart(null);

+					int x = h.IndexOf(' ');

+					if (x == -1) {

+					  x = h.Length;  // this will be convenient below when we look for a filename

+					}

+					try {

+					  int li = int.Parse(h.Substring(0, x));

+

+					  h = h.Substring(x).Trim();

+

+					  // act on #line

+					  line = li;

+					  if (h.Length != 0) {

+						// a filename was specified

+						Filename = h;

+					  }

+					  continue;  // successfully parsed and acted on the #line pragma

+

+					} catch (FormatException) {

+					  // just fall down through to produce an error message

+					}

+					this.errorHandler.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);

+					continue;

+				  }

+

+				  this.errorHandler.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);

+				  continue;

+				}

+				return;

+			  }

+

+			

+		}

+

+	}

+

+	void AddCh() {

+		if (tlen >= tval.Length) {

+			char[] newBuf = new char[2 * tval.Length];

+			Array.Copy(tval, 0, newBuf, 0, tval.Length);

+			tval = newBuf;

+		}

+		if (ch != Buffer.EOF) {

+			tval[tlen++] = (char) ch;

+			NextCh();

+		}

+	}

+

+

+

+	bool Comment0() {

+		int level = 1, pos0 = pos, line0 = line, col0 = col;

 		NextCh();

 		if (ch == '/') {

 			NextCh();

 			for(;;) {

 				if (ch == 10) {

 					level--;

-					if (level == 0) {

-						while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}

-						NextCh(); return true;

-					}

+					if (level == 0) { oldEols = line - line0; NextCh(); return true; }

 					NextCh();

-				} else if (ch == EOF) return false;

+				} else if (ch == Buffer.EOF) return false;

 				else NextCh();

 			}

 		} else {

-			if (ch==CR) {line--; lineStart = lineStart0;}

-			pos = pos - 2; Buffer.Pos = pos+1; NextCh();

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

 		}

 		return false;

 	}

-
-	static bool Comment1() {

-		int level = 1, line0 = line, lineStart0 = lineStart;

+

+	bool Comment1() {

+		int level = 1, pos0 = pos, line0 = line, col0 = col;

 		NextCh();

 		if (ch == '*') {

 			NextCh();

@@ -251,10 +440,7 @@ public class Scanner {
 					NextCh();

 					if (ch == '/') {

 						level--;

-						if (level == 0) {

-							while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}

-							NextCh(); return true;

-						}

+						if (level == 0) { oldEols = line - line0; NextCh(); return true; }

 						NextCh();

 					}

 				} else if (ch == '/') {

@@ -262,19 +448,18 @@ public class Scanner {
 					if (ch == '*') {

 						level++; NextCh();

 					}

-				} else if (ch == EOF) return false;

+				} else if (ch == Buffer.EOF) return false;

 				else NextCh();

 			}

 		} else {

-			if (ch==CR) {line--; lineStart = lineStart0;}

-			pos = pos - 2; Buffer.Pos = pos+1; NextCh();

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

 		}

 		return false;

 	}

 

-  

-  static void CheckLiteral() {

-    switch (t.val) {

+

+	void CheckLiteral() {

+		switch (t.val) {

 			case "module": t.kind = 4; break;

 			case "imports": t.kind = 5; break;

 			case "class": t.kind = 8; break;

@@ -326,185 +511,212 @@ public class Scanner {
 			case "forall": t.kind = 94; break;

 			case "exists": t.kind = 96; break;

 			default: break;

+		}

+	}

 

-    }

-  }

-

-  public static Token/*!*/ Scan() {

-    while (ignore[ch]) { NextCh(); }

-		if (ch == '/' && Comment0()  || ch == '/' && Comment1() ) return Scan();

-    t = new Token();

-    t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;

-    int state = (/*^ (!) ^*/ start)[ch];

-    StringBuilder buf = new StringBuilder(16);

-    buf.Append(ch); NextCh();

-    

-    switch (state) {

-      case 0: {t.kind = noSym; goto done;} // NextCh already done

+	Token! NextToken() {

+		while (ch == ' ' ||

+			ch >= 9 && ch <= 10 || ch == 13

+		) NextCh();

+		if (ch == '/' && Comment0() ||ch == '/' && Comment1()) return NextToken();

+		int recKind = noSym;

+		int recEnd = pos;

+		t = new Token();

+		t.pos = pos; t.col = col; t.line = line; 

+		t.filename = this.Filename;

+		int state;

+		if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; }

+		else { state = 0; }

+		tlen = 0; AddCh();

+		

+		switch (state) {

+			case -1: { t.kind = eofSym; break; } // NextCh already done

+			case 0: {

+				if (recKind != noSym) {

+					tlen = recEnd - t.pos;

+					SetScannerBehindT();

+				}

+				t.kind = recKind; break;

+			} // NextCh already done

 			case 1:

-				if ((ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z')) {buf.Append(ch); NextCh(); goto case 1;}

-				else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}

+				recEnd = pos; recKind = 1;

+				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 1;}

+				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}

 			case 2:

-				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 2;}

-				else {t.kind = 2; goto done;}

+				recEnd = pos; recKind = 2;

+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 2;}

+				else {t.kind = 2; break;}

 			case 3:

-				if ((ch == '"')) {buf.Append(ch); NextCh(); goto case 4;}

-				else if ((ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~')) {buf.Append(ch); NextCh(); goto case 3;}

-				else {t.kind = noSym; goto done;}

+				if (ch == '"') {AddCh(); goto case 4;}

+				else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 3;}

+				else {goto case 0;}

 			case 4:

-				{t.kind = 3; goto done;}

+				{t.kind = 3; break;}

 			case 5:

-				{t.kind = 6; goto done;}

+				{t.kind = 6; break;}

 			case 6:

-				{t.kind = 7; goto done;}

+				{t.kind = 7; break;}

 			case 7:

-				{t.kind = 13; goto done;}

+				{t.kind = 13; break;}

 			case 8:

-				{t.kind = 15; goto done;}

+				{t.kind = 15; break;}

 			case 9:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 18;}

-				else if (ch == ':') {buf.Append(ch); NextCh(); goto case 53;}

-				else {t.kind = 16; goto done;}

+				{t.kind = 26; break;}

 			case 10:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 22;}

-				else {t.kind = 17; goto done;}

+				{t.kind = 27; break;}

 			case 11:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}

-				else {t.kind = 18; goto done;}

+				{t.kind = 36; break;}

 			case 12:

-				{t.kind = 26; goto done;}

+				{t.kind = 37; break;}

 			case 13:

-				{t.kind = 27; goto done;}

+				{t.kind = 40; break;}

 			case 14:

-				{t.kind = 36; goto done;}

+				{t.kind = 44; break;}

 			case 15:

-				{t.kind = 37; goto done;}

+				{t.kind = 46; break;}

 			case 16:

-				if (ch == '>') {buf.Append(ch); NextCh(); goto case 17;}

-				else if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;}

-				else {t.kind = noSym; goto done;}

+				{t.kind = 47; break;}

 			case 17:

-				{t.kind = 40; goto done;}

+				if (ch == '>') {AddCh(); goto case 18;}

+				else {goto case 0;}

 			case 18:

-				{t.kind = 44; goto done;}

+				{t.kind = 62; break;}

 			case 19:

-				{t.kind = 46; goto done;}

+				{t.kind = 63; break;}

 			case 20:

-				{t.kind = 47; goto done;}

+				{t.kind = 64; break;}

 			case 21:

-				if (ch == '|') {buf.Append(ch); NextCh(); goto case 32;}

-				else {t.kind = 56; goto done;}

+				{t.kind = 65; break;}

 			case 22:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}

-				else {t.kind = 71; goto done;}

+				if (ch == '&') {AddCh(); goto case 23;}

+				else {goto case 0;}

 			case 23:

-				if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}

-				else {t.kind = noSym; goto done;}

+				{t.kind = 66; break;}

 			case 24:

-				{t.kind = 62; goto done;}

+				{t.kind = 67; break;}

 			case 25:

-				{t.kind = 63; goto done;}

+				{t.kind = 68; break;}

 			case 26:

-				if (ch == '>') {buf.Append(ch); NextCh(); goto case 27;}

-				else {t.kind = 70; goto done;}

+				{t.kind = 69; break;}

 			case 27:

-				{t.kind = 64; goto done;}

+				{t.kind = 72; break;}

 			case 28:

-				{t.kind = 65; goto done;}

+				{t.kind = 73; break;}

 			case 29:

-				if (ch == '&') {buf.Append(ch); NextCh(); goto case 30;}

-				else {t.kind = noSym; goto done;}

+				{t.kind = 74; break;}

 			case 30:

-				{t.kind = 66; goto done;}

+				if (ch == 'n') {AddCh(); goto case 31;}

+				else {goto case 0;}

 			case 31:

-				{t.kind = 67; goto done;}

+				{t.kind = 75; break;}

 			case 32:

-				{t.kind = 68; goto done;}

+				{t.kind = 76; break;}

 			case 33:

-				{t.kind = 69; goto done;}

+				{t.kind = 77; break;}

 			case 34:

-				{t.kind = 72; goto done;}

+				{t.kind = 78; break;}

 			case 35:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 36;}

-				else if (ch == '!') {buf.Append(ch); NextCh(); goto case 37;}

-				else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 38;}

-				else {t.kind = 83; goto done;}

+				{t.kind = 79; break;}

 			case 36:

-				{t.kind = 73; goto done;}

+				{t.kind = 80; break;}

 			case 37:

-				{t.kind = 74; goto done;}

+				{t.kind = 81; break;}

 			case 38:

-				if (ch == 'n') {buf.Append(ch); NextCh(); goto case 39;}

-				else {t.kind = noSym; goto done;}

+				{t.kind = 82; break;}

 			case 39:

-				{t.kind = 75; goto done;}

+				{t.kind = 84; break;}

 			case 40:

-				{t.kind = 76; goto done;}

+				{t.kind = 88; break;}

 			case 41:

-				{t.kind = 77; goto done;}

+				{t.kind = 91; break;}

 			case 42:

-				{t.kind = 78; goto done;}

+				{t.kind = 95; break;}

 			case 43:

-				{t.kind = 79; goto done;}

+				{t.kind = 97; break;}

 			case 44:

-				{t.kind = 80; goto done;}

+				{t.kind = 98; break;}

 			case 45:

-				{t.kind = 81; goto done;}

+				{t.kind = 99; break;}

 			case 46:

-				{t.kind = 82; goto done;}

+				recEnd = pos; recKind = 16;

+				if (ch == '=') {AddCh(); goto case 14;}

+				else if (ch == ':') {AddCh(); goto case 44;}

+				else {t.kind = 16; break;}

 			case 47:

-				{t.kind = 84; goto done;}

+				recEnd = pos; recKind = 17;

+				if (ch == '=') {AddCh(); goto case 53;}

+				else {t.kind = 17; break;}

 			case 48:

-				{t.kind = 88; goto done;}

+				recEnd = pos; recKind = 18;

+				if (ch == '=') {AddCh(); goto case 27;}

+				else {t.kind = 18; break;}

 			case 49:

-				if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}

-				else {t.kind = 89; goto done;}

+				if (ch == '>') {AddCh(); goto case 13;}

+				else if (ch == '=') {AddCh(); goto case 54;}

+				else {goto case 0;}

 			case 50:

-				{t.kind = 91; goto done;}

+				recEnd = pos; recKind = 56;

+				if (ch == '|') {AddCh(); goto case 25;}

+				else {t.kind = 56; break;}

 			case 51:

-				{t.kind = 95; goto done;}

+				recEnd = pos; recKind = 83;

+				if (ch == '=') {AddCh(); goto case 28;}

+				else if (ch == '!') {AddCh(); goto case 29;}

+				else if (ch == 'i') {AddCh(); goto case 30;}

+				else {t.kind = 83; break;}

 			case 52:

-				{t.kind = 97; goto done;}

+				recEnd = pos; recKind = 89;

+				if (ch == '.') {AddCh(); goto case 41;}

+				else {t.kind = 89; break;}

 			case 53:

-				{t.kind = 98; goto done;}

+				recEnd = pos; recKind = 71;

+				if (ch == '=') {AddCh(); goto case 17;}

+				else {t.kind = 71; break;}

 			case 54:

-				{t.kind = 99; goto done;}

-			case 55: {t.kind = 0; goto done;}

-    }

-    done:

-    t.val = buf.ToString();

-    return t;

-  }

+				recEnd = pos; recKind = 70;

+				if (ch == '>') {AddCh(); goto case 20;}

+				else {t.kind = 70; break;}

 

-} // end Scanner

+		}

+		t.val = new String(tval, 0, tlen);

+		return t;

+	}

+	

+	private void SetScannerBehindT() {

+		buffer.Pos = t.pos;

+		NextCh();

+		line = t.line; col = t.col;

+		for (int i = 0; i < tlen; i++) NextCh();

+	}

+	

+	// get the next token (possibly a token already seen during peeking)

+	public Token! Scan () {

+		if (tokens.next == null) {

+			return NextToken();

+		} else {

+			pt = tokens = tokens.next;

+			return tokens;

+		}

+	}

 

+	// peek for the next token, ignore pragmas

+	public Token! Peek () {

+		do {

+			if (pt.next == null) {

+				pt.next = NextToken();

+			}

+			pt = pt.next;

+		} while (pt.kind > maxT); // skip pragmas

+	

+		return pt;

+	}

 

-public delegate void ErrorProc(int n, string filename, int line, int col);

+	// make sure that peeking starts at the current scan position

+	public void ResetPeek () { pt = tokens; }

 

-public class Errors {

-  public static int count = 0;  // number of errors detected

-  public static ErrorProc/*!*/ SynErr;  // syntactic errors

-  

-  public static void SemErr(string filename, int line, int col, string! msg) {  // semantic errors

-    System.ConsoleColor color = System.Console.ForegroundColor;

-    System.Console.ForegroundColor = System.ConsoleColor.Red;

-    System.Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);

-    System.Console.ForegroundColor = color;

-    count++;

-  }

-  

-  public static void SemErr(Bpl.IToken! tok, string! msg) {  // semantic errors

-    SemErr(tok.filename, tok.line, tok.col, msg);

-  }

-  

-  public static void Exception (string s) {

-    System.ConsoleColor color = System.Console.ForegroundColor;

-    System.Console.ForegroundColor = System.ConsoleColor.Red;

-    System.Console.WriteLine(s);

-    System.Console.ForegroundColor = color;

-    System.Environment.Exit(0);

-  }

+} // end Scanner

+

+public delegate void ErrorProc(int n, string filename, int line, int col);

 

-} // Errors

 

-} // end namespace

+}
\ No newline at end of file
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 348fdd2b..4d9f3993 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -9,6 +9,7 @@ using System.Numerics;
 using Microsoft.Contracts;

 using Bpl = Microsoft.Boogie;

 using System.Text;

+using Microsoft.Boogie;

 

 namespace Microsoft.Dafny {

   public class Translator {

@@ -31,9 +32,9 @@ namespace Microsoft.Dafny {
 

     // Machinery for providing information to the Counterexample Visualizer

     readonly Dictionary<string!,int>! cevFilenames = new Dictionary<string!,int>();

-    readonly Dictionary<Token!,Bpl.Constant!>! cevLocations = new Dictionary<Token!,Bpl.Constant!>();

+    readonly Dictionary<IToken!,Bpl.Constant!>! cevLocations = new Dictionary<IToken!,Bpl.Constant!>();

     readonly Dictionary<string!,Bpl.Constant!>! cevVariables = new Dictionary<string!,Bpl.Constant!>();

-    Bpl.Expr! CevLocation(Token! tok)

+    Bpl.Expr! CevLocation(IToken! tok)

       requires predef != null && sink != null;

     {

       Bpl.Constant c;

@@ -89,15 +90,15 @@ namespace Microsoft.Dafny {
       public readonly Bpl.Type! CevVariableKind;

       public readonly Bpl.Type! CevEventType;

       private readonly Bpl.TypeSynonymDecl! setTypeCtor;

-      public Bpl.Type! SetType(Token! tok, Bpl.Type! ty) {

+      public Bpl.Type! SetType(IToken! tok, Bpl.Type! ty) {

         return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));

       }

       private readonly Bpl.TypeCtorDecl! seqTypeCtor;

-      public Bpl.Type! SeqType(Token! tok, Bpl.Type! ty) {

+      public Bpl.Type! SeqType(IToken! tok, Bpl.Type! ty) {

         return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));

       }

       readonly Bpl.TypeCtorDecl! fieldName;

-      public Bpl.Type! FieldName(Token! tok, Bpl.Type! ty) {

+      public Bpl.Type! FieldName(IToken! tok, Bpl.Type! ty) {

         return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));

       }

       public readonly Bpl.Type! HeapType;

@@ -109,7 +110,7 @@ namespace Microsoft.Dafny {
       public readonly Bpl.Type! DtCtorId;

       public readonly Bpl.Expr! Null;

       private readonly Bpl.Constant! allocField;

-      public Bpl.IdentifierExpr! Alloc(Token! tok) {

+      public Bpl.IdentifierExpr! Alloc(IToken! tok) {

         return new Bpl.IdentifierExpr(tok, allocField);

       }

 

@@ -247,11 +248,20 @@ namespace Microsoft.Dafny {
       //using (System.IO.Stream stream = (!) System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource

       string! codebase = (!) System.IO.Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);

       string! preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");

+      

+      Bpl.Program prelude;

+      int errorCount = Bpl.Parser.Parse(preludePath, out prelude);

+      if (prelude == null || errorCount > 0) {

+        return null;

+      } else {

+        return prelude;

+      }

+/*      

       List<string!> defines = new List<string!>();

       using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))

       {

         BoogiePL.Buffer.Fill(new System.IO.StreamReader(stream), defines);

-        BoogiePL.Scanner.Init("<DafnyPrelude.bpl>");

+        //BoogiePL.Scanner.Init("<DafnyPrelude.bpl>");

         Bpl.Program prelude;

         int errorCount = BoogiePL.Parser.Parse(out prelude);

         if (prelude == null || errorCount > 0) {

@@ -260,6 +270,7 @@ namespace Microsoft.Dafny {
           return prelude;

         }

       }

+*/      

     }

     

     public Bpl.Program! Translate(Program! program) {

@@ -660,7 +671,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    Bpl.Expr! InSeqRange(Token! tok, Bpl.Expr! index, Bpl.Expr! seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {

+    Bpl.Expr! InSeqRange(IToken! tok, Bpl.Expr! index, Bpl.Expr! seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {

       if (lowerBound == null) {

         lowerBound = Bpl.Expr.Literal(0);

       }

@@ -679,7 +690,7 @@ namespace Microsoft.Dafny {
     int loopHeapVarCount = 0;

     int otherTmpVarCount = 0;

     Bpl.IdentifierExpr _phvie = null;

-    Bpl.IdentifierExpr! GetPrevHeapVar_IdExpr(Token! tok, Bpl.VariableSeq! locals)  // local variable that's shared between statements that need it

+    Bpl.IdentifierExpr! GetPrevHeapVar_IdExpr(IToken! tok, Bpl.VariableSeq! locals)  // local variable that's shared between statements that need it

       requires predef != null;

     {

       if (_phvie == null) {

@@ -691,7 +702,7 @@ namespace Microsoft.Dafny {
       return _phvie;

     }

     Bpl.IdentifierExpr _nwie = null;

-    Bpl.IdentifierExpr! GetNewVar_IdExpr(Token! tok, Bpl.VariableSeq! locals)  // local variable that's shared between statements that need it

+    Bpl.IdentifierExpr! GetNewVar_IdExpr(IToken! tok, Bpl.VariableSeq! locals)  // local variable that's shared between statements that need it

       requires predef != null;

     {

       if (_nwie == null) {

@@ -795,7 +806,7 @@ namespace Microsoft.Dafny {
         assert p != null;

         builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",

           new Bpl.ExprSeq(

-            CevLocation((Dafny.Token)p.tok),

+            CevLocation(p.tok),

             new Bpl.IdentifierExpr(p.tok, "cev_parameter", predef.CevVariableKind),

             CevVariable(p.tok, p.Name),

             new Bpl.IdentifierExpr(p.tok, p.Name, p.TypedIdent.Type)),  // it's important not to pass in just p, because that resolves to the proc's param, not the impl's param

@@ -805,7 +816,7 @@ namespace Microsoft.Dafny {
         assert p != null;

         builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",

           new Bpl.ExprSeq(

-            CevLocation((Dafny.Token)p.tok),

+            CevLocation(p.tok),

             new Bpl.IdentifierExpr(p.tok, "cev_local", predef.CevVariableKind),  // treat out-parameters as locals

             CevVariable(p.tok, p.Name),

             new Bpl.IdentifierExpr(p.tok, p.Name, p.TypedIdent.Type)),  // it's important not to pass in just p, because that resolves to the proc's param, not the impl's param

@@ -816,7 +827,7 @@ namespace Microsoft.Dafny {
       DefineFrame(m.tok, m.Mod, builder, localVariables);

     }

     

-    void DefineFrame(Token! tok, List<FrameExpression!>! frameClause, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)

+    void DefineFrame(IToken! tok, List<FrameExpression!>! frameClause, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)

       requires predef != null;

     {

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);

@@ -839,7 +850,7 @@ namespace Microsoft.Dafny {
       builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));

     }

 

-    void CheckFrameSubset(Token! tok, List<FrameExpression!>! calleeFrame,

+    void CheckFrameSubset(IToken! tok, List<FrameExpression!>! calleeFrame,

                           Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap,

                           ExpressionTranslator! etran, Bpl.StmtListBuilder! builder, string! errorMessage)

       requires predef != null;

@@ -959,7 +970,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, Bpl.Expr! f, List<FrameExpression!>! rw, ExpressionTranslator! etran,

+    Bpl.Expr! InRWClause(IToken! tok, Bpl.Expr! o, Bpl.Expr! f, List<FrameExpression!>! rw, ExpressionTranslator! etran,

                          Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap)

       requires predef != null;

       // requires o to denote an expression of type RefType

@@ -1225,7 +1236,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CheckNonNull(Token! tok, Expression! e, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)

+    void CheckNonNull(IToken! tok, Expression! e, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)

       requires predef != null;

     {

       if (e is ThisExpr) {

@@ -1490,7 +1501,7 @@ namespace Microsoft.Dafny {
       return cc;

     }

     

-    Bpl.Expr GetTypeExpr(Token! tok, Type! type)

+    Bpl.Expr GetTypeExpr(IToken! tok, Type! type)

       requires predef != null;

     {

       while (true) {

@@ -1706,13 +1717,13 @@ namespace Microsoft.Dafny {
     }

     

     class BoilerplateTriple {  // a triple that is now a quintuple

-      public readonly Token! tok;

+      public readonly IToken! tok;

       public readonly bool IsFree;

       public readonly Bpl.Expr! Expr;

       public readonly string ErrorMessage;

       invariant IsFree || ErrorMessage != null;

       public readonly string Comment;

-      public BoilerplateTriple(Token! tok, bool isFree, Bpl.Expr! expr, string errorMessage, string comment)

+      public BoilerplateTriple(IToken! tok, bool isFree, Bpl.Expr! expr, string errorMessage, string comment)

         requires isFree || errorMessage != null;

       {

         this.tok = tok;

@@ -1730,7 +1741,7 @@ namespace Microsoft.Dafny {
     ///  S2. the post-state of the two-state interval

     /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.

     /// </summary>

-    List<BoilerplateTriple!>! GetTwoStateBoilerplate(Token! tok, Method! method, ExpressionTranslator! etranPre, ExpressionTranslator! etran)

+    List<BoilerplateTriple!>! GetTwoStateBoilerplate(IToken! tok, Method! method, ExpressionTranslator! etranPre, ExpressionTranslator! etran)

     {

       List<BoilerplateTriple!> boilerplate = new List<BoilerplateTriple!>();

       

@@ -1751,7 +1762,7 @@ namespace Microsoft.Dafny {
     ///  S2. the post-state of the two-state interval

     /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.

     /// </summary>

-    Bpl.Expr! FrameCondition(Token! tok, List<FrameExpression!>! modifiesClause, ExpressionTranslator! etranPre, ExpressionTranslator! etran)

+    Bpl.Expr! FrameCondition(IToken! tok, List<FrameExpression!>! modifiesClause, ExpressionTranslator! etranPre, ExpressionTranslator! etran)

       requires predef != null;

     {

       // generate:

@@ -1838,7 +1849,7 @@ namespace Microsoft.Dafny {
       return cmd;

     }

 

-    Bpl.Ensures! Ensures(Token! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)

+    Bpl.Ensures! Ensures(IToken! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)

     {

       Bpl.Ensures ens = new Bpl.Ensures(tok, free, condition, comment);

       if (errorMessage != null) {

@@ -1847,7 +1858,7 @@ namespace Microsoft.Dafny {
       return ens;

     }

 

-    Bpl.Requires! Requires(Token! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)

+    Bpl.Requires! Requires(IToken! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)

     {

       Bpl.Requires req = new Bpl.Requires(tok, free, condition, comment);

       if (errorMessage != null) {

@@ -2266,7 +2277,7 @@ namespace Microsoft.Dafny {
           // time for the actual loop body

           TrStmt(s.Body, loopBodyBuilder, locals, etran);

           // check definedness of decreases expressions

-          List<Token!> toks = new List<Token!>();

+          List<IToken!> toks = new List<IToken!>();

           List<Type!> types = new List<Type!>();

           List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();

           foreach (Expression e in theDecreases) {

@@ -2457,7 +2468,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    static Expression! CreateIntLiteral(Token! tok, int n)

+    static Expression! CreateIntLiteral(IToken! tok, int n)

     {

       if (0 <= n) {

         Expression lit = new LiteralExpr(tok, n);

@@ -2468,7 +2479,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    static Expression! CreateIntSub(Token! tok, Expression! e0, Expression! e1)

+    static Expression! CreateIntSub(IToken! tok, Expression! e0, Expression! e1)

       requires e0.Type is IntType && e1.Type is IntType;

     {

       BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);

@@ -2477,7 +2488,7 @@ namespace Microsoft.Dafny {
       return s;

     }

     

-    static Expression! CreateIntITE(Token! tok, Expression! test, Expression! e0, Expression! e1)

+    static Expression! CreateIntITE(IToken! tok, Expression! test, Expression! e0, Expression! e1)

       requires test.Type is BoolType && e0.Type is IntType && e1.Type is IntType;

     {

       ITEExpr ite = new ITEExpr(tok, test, e0, e1);

@@ -2504,12 +2515,12 @@ namespace Microsoft.Dafny {
       yield return expr;

     }

     

-    void CheckCallTermination(Token! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,

+    void CheckCallTermination(IToken! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,

                               Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,

                               ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)

     {

       int N = min{contextDecreases.Count, calleeDecreases.Count};

-      List<Token!> toks = new List<Token!>();

+      List<IToken!> toks = new List<IToken!>();

       List<Type!> types = new List<Type!>();

       List<Bpl.Expr!> callee = new List<Bpl.Expr!>();

       List<Bpl.Expr!> caller = new List<Bpl.Expr!>();

@@ -2532,7 +2543,7 @@ namespace Microsoft.Dafny {
     /// Returns the expression that says whether or not the decreases function has gone down.  ee0 represents the new

     /// values and ee1 represents old values.

     /// </summary>

-    Bpl.Expr! DecreasesCheck(List<Token!>! toks, List<Type!>! types, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,

+    Bpl.Expr! DecreasesCheck(List<IToken!>! toks, List<Type!>! types, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,

                              Bpl.StmtListBuilder! builder, ExpressionTranslator! etran, string! suffixMsg)

       requires predef != null;

       requires types.Count == ee0.Count && ee0.Count == ee1.Count;

@@ -2605,7 +2616,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    void ComputeLessEq(Token! tok, Type! ty, Bpl.Expr! e0, Bpl.Expr! e1, out Bpl.Expr! less, out Bpl.Expr! eq, ExpressionTranslator! etran)

+    void ComputeLessEq(IToken! tok, Type! ty, Bpl.Expr! e0, Bpl.Expr! e1, out Bpl.Expr! less, out Bpl.Expr! eq, ExpressionTranslator! etran)

       requires predef != null;

     {

       if (ty is BoolType) {

@@ -2641,7 +2652,7 @@ namespace Microsoft.Dafny {
       builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));

     }

     

-    Bpl.Expr GetWhereClause(Token! tok, Bpl.Expr! x, Type! type, ExpressionTranslator! etran)

+    Bpl.Expr GetWhereClause(IToken! tok, Bpl.Expr! x, Type! type, ExpressionTranslator! etran)

       requires predef != null;

     {

       if (type is TypeProxy) {

@@ -2703,7 +2714,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    void TrAssignment(Token! tok, Expression! lhs, AssignmentRhs! rhs, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! locals,

+    void TrAssignment(IToken! tok, Expression! lhs, AssignmentRhs! rhs, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! locals,

                       ExpressionTranslator! etran)

       requires predef != null;

     {

@@ -2809,7 +2820,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    Bpl.AssumeCmd! AssumeGoodHeap(Token! tok, ExpressionTranslator! etran) {

+    Bpl.AssumeCmd! AssumeGoodHeap(IToken! tok, ExpressionTranslator! etran) {

       return new Bpl.AssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));

     }

     

@@ -2821,7 +2832,7 @@ namespace Microsoft.Dafny {
       public readonly Translator! translator;

       readonly Function applyLimited_CurrentFunction;

       

-      public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Token! heapToken) {

+      public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, IToken! heapToken) {

         this.translator = translator;

         this.predef = predef;

         HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);

@@ -2854,7 +2865,7 @@ namespace Microsoft.Dafny {
         return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction);

       }

       

-      public Bpl.IdentifierExpr! TheFrame(Token! tok)

+      public Bpl.IdentifierExpr! TheFrame(IToken! tok)

         ensures result.Type != null;

       {

         Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");

@@ -3211,12 +3222,12 @@ namespace Microsoft.Dafny {
         }

       }

       

-      public Bpl.Expr! ProperSubset(Token! tok, Bpl.Expr! e0, Bpl.Expr! e1) {

+      public Bpl.Expr! ProperSubset(IToken! tok, Bpl.Expr! e0, Bpl.Expr! e1) {

         return Bpl.Expr.And(

           translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e0, e1),

           Bpl.Expr.Not(translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e1, e0)));

       }

-      public Bpl.Expr! ProperPrefix(Token! tok, Bpl.Expr! e0, Bpl.Expr! e1) {

+      public Bpl.Expr! ProperPrefix(IToken! tok, Bpl.Expr! e0, Bpl.Expr! e1) {

         Bpl.Expr len0 = translator.FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);

         Bpl.Expr len1 = translator.FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);

         return Bpl.Expr.And(

@@ -3246,7 +3257,7 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.Eq(f0, f1);

       }

 

-      public Bpl.Expr! CondApplyBox(Token! tok, Bpl.Expr! e, Type! fromType, Type! toType) {

+      public Bpl.Expr! CondApplyBox(IToken! tok, Bpl.Expr! e, Type! fromType, Type! toType) {

         if (!ModeledAsBoxType(fromType) && ModeledAsBoxType(toType)) {

           return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);

         } else {

@@ -3254,7 +3265,7 @@ namespace Microsoft.Dafny {
         }

       }

       

-      public Bpl.Expr! BoxIfNecessary(Token! tok, Bpl.Expr! e, Type! fromType) {

+      public Bpl.Expr! BoxIfNecessary(IToken! tok, Bpl.Expr! e, Type! fromType) {

         if (!ModeledAsBoxType(fromType)) {

           return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);

         } else {

@@ -3262,7 +3273,7 @@ namespace Microsoft.Dafny {
         }

       }

       

-      public Bpl.Expr! CondApplyUnbox(Token! tok, Bpl.Expr! e, Type! fromType, Type! toType) {

+      public Bpl.Expr! CondApplyUnbox(IToken! tok, Bpl.Expr! e, Type! fromType, Type! toType) {

         if (ModeledAsBoxType(fromType) && !ModeledAsBoxType(toType)) {

           return translator.FunctionCall(tok, BuiltinFunction.Unbox, translator.TrType(toType), e);

         } else {

@@ -3285,7 +3296,7 @@ namespace Microsoft.Dafny {
         return t.IsTypeParameter;

       }

 

-      public Bpl.IdentifierExpr! TrVar(Token! tok, IVariable! var) {

+      public Bpl.IdentifierExpr! TrVar(IToken! tok, IVariable! var) {

         return new Bpl.IdentifierExpr(tok, var.UniqueName, translator.TrType(var.Type));

       }

       

@@ -3293,7 +3304,7 @@ namespace Microsoft.Dafny {
       /// Translate like s[Box(elmt)], but try to avoid as many set functions as possible in the

       /// translation, because such functions can mess up triggering.

       /// </summary>

-      public Bpl.Expr! TrInSet(Token! tok, Bpl.Expr! elmt, Expression! s, Type! elmtType) {

+      public Bpl.Expr! TrInSet(IToken! tok, Bpl.Expr! elmt, Expression! s, Type! elmtType) {

         if (s is BinaryExpr) {

           BinaryExpr bin = (BinaryExpr)s;

           switch (bin.ResolvedOp) {

@@ -3345,15 +3356,15 @@ namespace Microsoft.Dafny {
       

       // --------------- help routines ---------------

 

-      public Bpl.Expr! IsAlloced(Token! tok, Bpl.Expr! e) {

+      public Bpl.Expr! IsAlloced(IToken! tok, Bpl.Expr! e) {

         return IsAlloced(tok, e, HeapExpr);

       }

           

-      Bpl.Expr! IsAlloced(Token! tok, Bpl.Expr! e, Bpl.Expr! heap) {

+      Bpl.Expr! IsAlloced(IToken! tok, Bpl.Expr! e, Bpl.Expr! heap) {

         return Bpl.Expr.SelectTok(tok, heap, e, predef.Alloc(tok));

       }

       

-      public Bpl.Expr! GoodRef(Token! tok, Bpl.Expr! e, Type! type) {

+      public Bpl.Expr! GoodRef(IToken! tok, Bpl.Expr! e, Type! type) {

         Bpl.Expr goodRef;

         if (type is UserDefinedType && ((UserDefinedType)type).ResolvedClass != null) {

           // Heap[e, alloc] && dtype(e) == T

@@ -3364,13 +3375,13 @@ namespace Microsoft.Dafny {
         }

       }

       

-      public Bpl.Expr! GoodRef_Class(Token! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)

+      public Bpl.Expr! GoodRef_Class(IToken! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)

         requires type.ResolvedClass is ClassDecl;

       {

         return GoodRef_Ref(tok, e, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)), type.TypeArgs, isNew);

       }

       

-      public Bpl.Expr! GoodRef_Ref(Token! tok, Bpl.Expr! e, Bpl.Expr! type, List<Type!>! typeArgs, bool isNew) {

+      public Bpl.Expr! GoodRef_Ref(IToken! tok, Bpl.Expr! e, Bpl.Expr! type, List<Type!>! typeArgs, bool isNew) {

         // Heap[e, alloc]

         Bpl.Expr r = IsAlloced(tok, e);

         if (isNew) {

@@ -3396,7 +3407,7 @@ namespace Microsoft.Dafny {
         return r;

       }

       

-      public Bpl.Expr TypeAlloced(Token! tok, Bpl.Expr! e, Type! type) {

+      public Bpl.Expr TypeAlloced(IToken! tok, Bpl.Expr! e, Type! type) {

         while (true) {

           TypeProxy proxy = type as TypeProxy;

           if (proxy == null) {

@@ -3493,7 +3504,7 @@ namespace Microsoft.Dafny {
     }

     

     // The "typeInstantiation" argument is passed in to help construct the result type of the function.

-    Bpl.NAryExpr! FunctionCall(Token! tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[]! args)

+    Bpl.NAryExpr! FunctionCall(IToken! tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[]! args)

       requires predef != null;

     {

       switch (f) {

@@ -3667,12 +3678,12 @@ namespace Microsoft.Dafny {
       }

     }

     

-    Bpl.NAryExpr! FunctionCall(Token! tok, string! function, Bpl.Type! returnType, params Bpl.Expr[]! args)

+    Bpl.NAryExpr! FunctionCall(IToken! tok, string! function, Bpl.Type! returnType, params Bpl.Expr[]! args)

     {

       return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), new Bpl.ExprSeq(args));

     }

 

-    Bpl.NAryExpr! FunctionCall(Token! tok, string! function, Bpl.Type! returnType, List<Bpl.Expr!>! args)

+    Bpl.NAryExpr! FunctionCall(IToken! tok, string! function, Bpl.Type! returnType, List<Bpl.Expr!>! args)

     {

       Bpl.ExprSeq aa = new Bpl.ExprSeq();

       foreach (Bpl.Expr arg in args) {

diff --git a/Dafny/parser.frame b/Dafny/parser.frame
deleted file mode 100644
index de0ba1fb..00000000
--- a/Dafny/parser.frame
+++ /dev/null
@@ -1,103 +0,0 @@
-

-using Microsoft.Contracts;

-

-namespace Microsoft.-->namespace {

-

-public class Parser {

--->constants

-	const bool T = true;

-	const bool x = false;

-	const int minErrDist = 2;

-	

-	static Token/*!*/ token;			// last recognized token

-	static Token/*!*/ t;				// lookahead token

-	static int errDist = minErrDist;

-

-	-->declarations

-

-	static void Error(int n) {

-		if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);

-		errDist = 0;

-	}

-	

-	public static void SemErr(string! msg) {

-		if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);

-		errDist = 0;

-	}

-

-	public static void SemErr(Token! tok, string! msg) {

-		if (errDist >= minErrDist) Errors.SemErr(tok.filename, tok.line, tok.col, msg);

-		errDist = 0;

-	}

-

-	static void Get() {

-		for (;;) {

-			token = t;

-			t = Scanner.Scan();

-			if (t.kind<=maxT) {errDist++; return;}

--->pragmas

-			t = token;

-		}

-	}

-	

-	static void Expect(int n) {

-		if (t.kind==n) Get(); else Error(n);

-	}

-	

-	static bool StartOf(int s) {

-		return set[s, t.kind];

-	}

-	

-	static void ExpectWeak(int n, int follow) {

-		if (t.kind == n) Get();

-		else {

-			Error(n);

-			while (!StartOf(follow)) Get();

-		}

-	}

-	

-	static bool WeakSeparator(int n, int syFol, int repFol) {

-		bool[] s = new bool[maxT+1];

-		if (t.kind == n) {Get(); return true;}

-		else if (StartOf(repFol)) return false;

-		else {

-			for (int i=0; i <= maxT; i++) {

-				s[i] = set[syFol, i] || set[repFol, i] || set[0, i];

-			}

-			Error(n);

-			while (!s[t.kind]) Get();

-			return StartOf(syFol);

-		}

-	}

-	

--->productions

-

-	public static void Parse() {

-		Errors.SynErr = new ErrorProc(SynErr);

-		t = new Token();

-		Get();

--->parseRoot

-	}

-

-	[Microsoft.Contracts.Verify(false)]

-	static void SynErr(int n, string filename, int line, int col) {

-		Errors.count++;

-		System.Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);

-		string s;

-		switch (n) {

--->errors

-			default: s = "error " + n; break;

-		}

-		System.Console.WriteLine(s);

-	}

-

-	static bool[,]! set = {

--->initialization

-	};

-

-	[Microsoft.Contracts.Verify(false)]

-	static Parser() {}

-} // end Parser

-

-} // end namespace

-$$$
\ No newline at end of file
diff --git a/Dafny/scanner.frame b/Dafny/scanner.frame
deleted file mode 100644
index a526c7f2..00000000
--- a/Dafny/scanner.frame
+++ /dev/null
@@ -1,170 +0,0 @@
-using System.IO;

-using System.Collections;

-using System.Collections.Generic;

-using System.Text;

-using Microsoft.Contracts;

-using Bpl = Microsoft.Boogie;

-using BoogiePL;

-

-

-namespace Microsoft.Dafny {

-

-  [Immutable]

-  public class Token : Bpl.Token {

-    public Token();

-    public Token(int linenum, int colnum) {

-      base(linenum, colnum);

-    }

-    public new static Token! NoToken = new Token();

-  }

-

-}

-

-namespace Microsoft.-->namespace {

-

-

-public class Scanner {

-  const char EOF = '\0';

-  const char CR  = '\r';

-  const char LF  = '\n';

-

-  [Microsoft.Contracts.Verify(false)]

--->declarations

-

-

-  static Token/*!*/ t;          // current token

-  static char ch;               // current input character

-  static int pos;               // column number of current character

-  static int line;              // line number of current character

-  static int lineStart;         // start position of current line

-  static Queue! oldEols;        // EOLs that appeared in a comment;

-  static BitArray/*!*/ ignore;  // set of characters to be ignored by the scanner  

-  static string Filename;

-

-  ///<summary>

-  ///Initializes the scanner. Note: first fill the Buffer.

-  ///</summary>

-  ///<param name="filename">File name used for error reporting</param>

-  public static void Init (string filename) {

-    Filename = filename;

-    pos = -1; line = 1; lineStart = 0;

-    oldEols = new Queue();

-    NextCh();

--->initialization

-  }

-  

-  private static void NextCh() {

-    if (oldEols.Count > 0) {

-      ch = (char) ((!)oldEols.Dequeue());

-    } else {

-      while (true) {

-        ch = (char)BoogiePL.Buffer.Read(); pos++;

-        if (ch == BoogiePL.Buffer.eof) {

-          ch = EOF;

-        } else if (ch == LF) {

-          line++;

-          lineStart = pos + 1;

-

-        } else if (ch == '#' && pos == lineStart) {

-          int prLine = line;

-          int prColumn = pos - lineStart;  // which is 0

-

-          string hashLine = BoogiePL.Buffer.ReadToEOL();  pos += hashLine.Length;

-          line++;

-          lineStart = pos + 1;

-

-          hashLine = hashLine.TrimEnd(null);

-          if (hashLine.StartsWith("line ") || hashLine == "line") {

-            // parse #line pragma:  #line num [filename]

-            string h = hashLine.Substring(4).TrimStart(null);

-            int x = h.IndexOf(' ');

-            if (x == -1) {

-              x = h.Length;  // this will be convenient below when we look for a filename

-            }

-            try {

-              int li = int.Parse(h.Substring(0, x));

-

-              h = h.Substring(x).Trim();

-

-              // act on #line

-              line = li;

-              if (h.Length != 0) {

-                // a filename was specified

-                Filename = h;

-              }

-              continue;  // successfully parsed and acted on the #line pragma

-

-            } catch (System.FormatException) {

-              // just fall down through to produce an error message

-            }

-            Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);

-            continue;

-          }

-

-          Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);

-          continue;

-        }

-        return;

-      }

-    }

-  }

-  

--->comment

-  

-  static void CheckLiteral() {

-    switch (t.val) {

--->literals

-    }

-  }

-

-  public static Token/*!*/ Scan() {

-    while (ignore[ch]) { NextCh(); }

--->scan1

-    t = new Token();

-    t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;

-    int state = (/*^ (!) ^*/ start)[ch];

-    StringBuilder buf = new StringBuilder(16);

-    buf.Append(ch); NextCh();

-    

-    switch (state) {

-      case 0: {t.kind = noSym; goto done;} // NextCh already done

--->scan2

-    }

-    done:

-    t.val = buf.ToString();

-    return t;

-  }

-

-} // end Scanner

-

-

-public delegate void ErrorProc(int n, string filename, int line, int col);

-

-public class Errors {

-  public static int count = 0;  // number of errors detected

-  public static ErrorProc/*!*/ SynErr;  // syntactic errors

-  

-  public static void SemErr(string filename, int line, int col, string! msg) {  // semantic errors

-    System.ConsoleColor color = System.Console.ForegroundColor;

-    System.Console.ForegroundColor = System.ConsoleColor.Red;

-    System.Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);

-    System.Console.ForegroundColor = color;

-    count++;

-  }

-  

-  public static void SemErr(Bpl.IToken! tok, string! msg) {  // semantic errors

-    SemErr(tok.filename, tok.line, tok.col, msg);

-  }

-  

-  public static void Exception (string s) {

-    System.ConsoleColor color = System.Console.ForegroundColor;

-    System.Console.ForegroundColor = System.ConsoleColor.Red;

-    System.Console.WriteLine(s);

-    System.Console.ForegroundColor = color;

-    System.Environment.Exit(0);

-  }

-

-} // Errors

-

-} // end namespace

-$$$

diff --git a/DafnyDriver/DafnyDriver.ssc b/DafnyDriver/DafnyDriver.ssc
index 8920db94..d9d9a6be 100644
--- a/DafnyDriver/DafnyDriver.ssc
+++ b/DafnyDriver/DafnyDriver.ssc
@@ -350,7 +350,7 @@ namespace Microsoft.Boogie
     /// </summary>

     static Program ParseBoogieProgram(List<string!>! fileNames, bool suppressTraceOutput)

     {

-      BoogiePL.Errors.count = 0;

+      //BoogiePL.Errors.count = 0;

       Program program = null;

       bool okay = true;

       foreach (string bplFileName in fileNames) {

@@ -366,9 +366,9 @@ namespace Microsoft.Boogie
         Program programSnippet;

         int errorCount;

         try {

-          errorCount = BoogiePL.Parser.Parse(bplFileName, out programSnippet);

+          errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, out programSnippet);

           if (programSnippet == null || errorCount != 0) {

-            Console.WriteLine("{0} parse errors detected in {1}", BoogiePL.Errors.count, bplFileName);

+            Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

             okay = false;

             continue;

           }