Dafny: added iterators; for now, only parsing and resolving (and printing and refining), no compilation or verification

17 files changed, 1667 insertions, 776 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 6d99ce9b..408e9797 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -42,6 +42,24 @@ namespace Microsoft.Dafny
         var ctors = dd.Ctors.ConvertAll(CloneCtor);

         var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));

         return dt;

+      } else if (d is IteratorDecl) {

+        var dd = (IteratorDecl)d;

+        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

+        var ins = dd.Ins.ConvertAll(CloneFormal);

+        var outs = dd.Outs.ConvertAll(CloneFormal);

+        var reads = CloneSpecFrameExpr(dd.Reads);

+        var mod = CloneSpecFrameExpr(dd.Modifies);

+        var decr = CloneSpecExpr(dd.Decreases);

+        var req = dd.Requires.ConvertAll(CloneMayBeFreeExpr);

+        var yreq = dd.YieldRequires.ConvertAll(CloneMayBeFreeExpr);

+        var ens = dd.Ensures.ConvertAll(CloneMayBeFreeExpr);

+        var yens = dd.YieldEnsures.ConvertAll(CloneMayBeFreeExpr);

+        var body = CloneBlockStmt(dd.Body);

+        var iter = new IteratorDecl(Tok(dd.tok), dd.Name, dd.Module,

+          tps, ins, outs, reads, mod, decr,

+          req, ens, yreq, yens,

+          body, CloneAttributes(dd.Attributes), dd.SignatureIsOmitted);

+        return iter;

       } else if (d is ClassDecl) {

         if (d is DefaultClassDecl) {

           var dd = (ClassDecl)d;

@@ -387,6 +405,10 @@ namespace Microsoft.Dafny
         var s = (ReturnStmt)stmt;

         r = new ReturnStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS));

 

+      } else if (stmt is YieldStmt) {

+        var s = (YieldStmt)stmt;

+        r = new YieldStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS));

+

       } else if (stmt is AssignStmt) {

         var s = (AssignStmt)stmt;

         r = new AssignStmt(Tok(s.Tok), CloneExpr(s.Lhs), CloneRHS(s.Rhs));

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index a138f4d9..a6e05c22 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -92,6 +92,8 @@ namespace Microsoft.Dafny {
             wr.WriteLine(" { }");

             CompileDatatypeConstructors(dt, indent);

             CompileDatatypeStruct(dt, indent);

+          } else if (d is IteratorDecl) {

+            throw new NotImplementedException();  // TODO

           } else if (d is ClassDecl) {

             ClassDecl cl = (ClassDecl)d;

             Indent(indent);

@@ -942,6 +944,8 @@ namespace Microsoft.Dafny {
         if (s.hiddenUpdate != null)

           TrStmt(s.hiddenUpdate, indent);

         Indent(indent); wr.WriteLine("return;");

+      } else if (stmt is YieldStmt) {

+        throw new NotImplementedException();  // TODO

       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

         var resolved = s.ResolvedStatements;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3afdc061..dcc9a3ca 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -139,7 +139,7 @@ IGNORE cr + lf + tab
 /*------------------------------------------------------------------------*/

 PRODUCTIONS

 Dafny

-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;

+= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

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

      ModuleDecl submodule;

      // to support multiple files, create a default module only if theModule is null

@@ -159,6 +159,8 @@ Dafny
       DatatypeDecl<defaultModule, out dt>       (. defaultModule.TopLevelDecls.Add(dt); .)

     | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .)

       ArbitraryTypeDecl<defaultModule, out at>  (. defaultModule.TopLevelDecls.Add(at); .)

+    | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .)

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

     | ClassMemberDecl<membersDefaultClass, isGhost, false>

     )

   }

@@ -178,7 +180,7 @@ Dafny
   EOF

   .

 SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule>

-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;

+= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

      Attributes attrs = null;  IToken/*!*/ id; 

      List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;

      List<IToken> idRefined = null, idPath = null, idAssignment = null;

@@ -196,13 +198,15 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl
        "{"                                       (. module.BodyStartTok = t; .)

         { (. isGhost = false; .)

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

-            ( SubModuleDecl<module, isGhost, out sm>        (. module.TopLevelDecls.Add(sm); .)

+            ( SubModuleDecl<module, isGhost, out sm>       (. module.TopLevelDecls.Add(sm); .)

             | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .)

-              ClassDecl<module, out c>           (. module.TopLevelDecls.Add(c); .)

+              ClassDecl<module, out c>                     (. module.TopLevelDecls.Add(c); .)

             | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .)

-              DatatypeDecl<module, out dt>       (. module.TopLevelDecls.Add(dt); .)

+              DatatypeDecl<module, out dt>                 (. module.TopLevelDecls.Add(dt); .)

             | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .)

-              ArbitraryTypeDecl<module, out at>  (. module.TopLevelDecls.Add(at); .)

+              ArbitraryTypeDecl<module, out at>            (. module.TopLevelDecls.Add(at); .)

+            | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .)

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

             | ClassMemberDecl<namedModuleDefaultClassMembers, isGhost, false>

             )

         }

@@ -393,6 +397,55 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
   .)

   .

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

+IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter>

+= (. Contract.Ensures(Contract.ValueAtReturn(out iter) != null);

+     IToken/*!*/ id;

+     Attributes attrs = null;

+     List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

+     IToken openParen;

+     List<Formal/*!*/> ins = new List<Formal/*!*/>();

+     List<Formal/*!*/> outs = new List<Formal/*!*/>();

+     List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

+     List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();

+     List<Expression/*!*/> decreases = new List<Expression>();

+     List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();

+     List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();

+     List<MaybeFreeExpression/*!*/> yieldReq = new List<MaybeFreeExpression/*!*/>();

+     List<MaybeFreeExpression/*!*/> yieldEns = new List<MaybeFreeExpression/*!*/>();

+     List<Expression/*!*/> dec = new List<Expression/*!*/>();

+     Attributes readsAttrs = null;

+     Attributes modAttrs = null;

+     Attributes decrAttrs = null;

+     BlockStmt body = null;

+     bool signatureOmitted = false;

+     IToken bodyStart = Token.NoToken;

+     IToken bodyEnd = Token.NoToken;

+  .)

+  SYNC

+  "iterator"

+  { Attribute<ref attrs> }

+  NoUSIdent<out id>

+  (

+    [ GenericParameters<typeArgs> ]

+    Formals<true, true, ins, out openParen>

+    [ "yields"

+      Formals<false, true, outs, out openParen>

+    ]

+  | "..."                                       (. signatureOmitted = true; openParen = Token.NoToken; .)

+  )

+  { IteratorSpec<reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs> }

+  [ BlockStmt<out body, out bodyStart, out bodyEnd>

+  ]

+  (. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,

+                             new Specification<FrameExpression>(mod, modAttrs), new Specification<FrameExpression>(reads, readsAttrs),

+                             new Specification<Expression>(decreases, decrAttrs),

+                             req, ens, yieldReq, yieldEns,

+                             body, attrs, signatureOmitted);

+     iter.BodyStartTok = bodyStart;

+     iter.BodyEndTok = bodyEnd;

+ .)

+  .

+/*------------------------------------------------------------------------*/

 GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>

 = (. Contract.Requires(cce.NonNullElements(typeArgs));

      IToken/*!*/ id;

@@ -490,6 +543,44 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
   | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, true> SYNC ";"

   )

   .

+IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,

+              List<MaybeFreeExpression/*!*/>/*!*/ req, List<MaybeFreeExpression/*!*/>/*!*/ ens,

+              List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*/ yieldEns,

+              ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs.>

+= (. Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;

+  .)

+  SYNC

+  ( "reads"    { IF(IsAttribute()) Attribute<ref readsAttrs> }

+               [ FrameExpression<out fe>                     (. reads.Add(fe); .)

+                 { "," FrameExpression<out fe>               (. reads.Add(fe); .)

+                 }

+               ] SYNC ";"

+  | "modifies" { IF(IsAttribute()) Attribute<ref modAttrs> }

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

+                 { "," FrameExpression<out fe>               (. mod.Add(fe); .)

+                 }

+               ] SYNC ";"

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

+    ]

+    [ "yield"                                                (. isYield = true; .)

+    ]

+    ( "requires" Expression<out e> SYNC ";"                  (. if (isYield) {

+                                                                  yieldReq.Add(new MaybeFreeExpression(e, isFree));

+                                                                } else {

+                                                                  req.Add(new MaybeFreeExpression(e, isFree));

+                                                                }

+                                                             .)

+    | "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> }

+      Expression<out e> SYNC ";"                             (. if (isYield) {

+                                                                  yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

+                                                                } else {

+                                                                  ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

+                                                                }

+                                                             .)

+    )

+  | "decreases" { IF(IsAttribute()) Attribute<ref decrAttrs> } DecreasesList<decreases, false> SYNC ";"

+  )

+  .

 Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen.>

 = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; .)

   "("                                                                  (. openParen = t; .)

@@ -814,14 +905,22 @@ ReturnStmt<out Statement/*!*/ s>
    IToken returnTok = null;

    List<AssignmentRhs> rhss = null;

    AssignmentRhs r;

+   bool isYield = false;

    .)

-  "return"                           (. returnTok = t; .)

+  ( "return"                         (. returnTok = t; .)

+  | "yield"                          (. returnTok = t; isYield = true; .)

+  )

   [

       Rhs<out r, null>               (. rhss = new List<AssignmentRhs>(); rhss.Add(r); .)

       { "," Rhs<out r, null>         (. rhss.Add(r); .)

         }

   ]

-  ";"                                (. s = new ReturnStmt(returnTok, rhss); .)

+  ";"                                (. if (isYield) {

+                                          s = new YieldStmt(returnTok, rhss);

+                                        } else {

+                                          s = new ReturnStmt(returnTok, rhss);

+                                        }

+                                     .)

   .

 UpdateStmt<out Statement/*!*/ s>

 = (. List<Expression> lhss = new List<Expression>();

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c8c61c55..71e48fdf 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -287,6 +287,16 @@ namespace Microsoft.Dafny {
         return IsCoDatatype;  // TODO: should really check structure of the type recursively

       }

     }

+    public IteratorDecl AsIteratorType {

+      get {

+        UserDefinedType udt = this as UserDefinedType;

+        if (udt == null) {

+          return null;

+        } else {

+          return udt.ResolvedClass as IteratorDecl;

+        }

+      }

+    }

     public bool IsTypeParameter {

       get {

         return AsTypeParameter != null;

@@ -465,7 +475,7 @@ namespace Microsoft.Dafny {
       }

     }

 

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

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

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

 

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

@@ -481,7 +491,7 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// This constructor constructs a resolved class type

+    /// This constructor constructs a resolved class/datatype/iterator type

     /// </summary>

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

       Contract.Requires(tok != null);

@@ -577,6 +587,8 @@ namespace Microsoft.Dafny {
             i++;

           }

           return true;

+        } else if (ResolvedClass is IteratorDecl) {

+          return false;

         } else if (ResolvedParam != null) {

           return ResolvedParam.MustSupportEquality;

         }

@@ -898,7 +910,7 @@ namespace Microsoft.Dafny {
     public ModuleDefinition RefinementBase;  // filled in during resolution (null if no refinement base)

     

     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 readonly Graph<ICallable/*!*/> CallGraph = new Graph<ICallable/*!*/>();  // filled in during resolution

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

     public readonly bool IsGhost;

     public readonly bool IsAbstract; // True iff this module represents an abstract interface

@@ -1146,6 +1158,85 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public interface ICodeContext : ICallable

+  {

+    bool IsGhost { get; }

+    bool IsStatic { get; }

+    List<TypeParameter> TypeArgs { get; }

+    List<Formal> Ins { get ; }

+    List<Formal> Outs { get; }

+    ModuleDefinition EnclosingModule { get; }  // to be called only after signature-resolution is complete

+  }

+

+  public class IteratorDecl : TopLevelDecl, ICodeContext

+  {

+    public readonly List<Formal> Ins;

+    public readonly List<Formal> Outs;

+    public readonly List<Formal> OutsHistory;  // these are the 'xs' variables

+    public readonly Specification<FrameExpression> Reads;

+    public readonly Specification<FrameExpression> Modifies;

+    public readonly Specification<Expression> Decreases;

+    public readonly List<MaybeFreeExpression> Requires;

+    public readonly List<MaybeFreeExpression> Ensures;

+    public readonly List<MaybeFreeExpression> YieldRequires;

+    public readonly List<MaybeFreeExpression> YieldEnsures;

+    public readonly BlockStmt Body;

+    public readonly bool SignatureIsOmitted;

+    public Dictionary<string, MemberDecl> ImplicitlyDefinedMembers;  // filled in during resolution

+    public IteratorDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

+                        List<Formal> ins, List<Formal> outs,

+                        Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,

+                        List<MaybeFreeExpression> requires,

+                        List<MaybeFreeExpression> ensures,

+                        List<MaybeFreeExpression> yieldRequires,

+                        List<MaybeFreeExpression> yieldEnsures,

+                        BlockStmt body, Attributes attributes, bool signatureIsOmitted)

+      : base(tok, name, module, typeArgs, attributes)

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(module != null);

+      Contract.Requires(typeArgs != null);

+      Contract.Requires(ins != null);

+      Contract.Requires(outs != null);

+      Contract.Requires(reads != null);

+      Contract.Requires(mod != null);

+      Contract.Requires(decreases != null);

+      Contract.Requires(requires != null);

+      Contract.Requires(ensures != null);

+      Contract.Requires(yieldRequires != null);

+      Contract.Requires(yieldEnsures != null);

+      Ins = ins;

+      Outs = outs;

+      Reads = reads;

+      Modifies = mod;

+      Decreases = decreases;

+      Requires = requires;

+      Ensures = ensures;

+      YieldRequires = yieldRequires;

+      YieldEnsures = yieldEnsures;

+      Body = body;

+      SignatureIsOmitted = signatureIsOmitted;

+

+      OutsHistory = new List<Formal>();

+      foreach (var p in Outs) {

+        OutsHistory.Add(new Formal(p.tok, p.Name + "s", new SeqType(p.Type), false, true));

+      }

+    }

+

+    bool ICodeContext.IsGhost { get { return false; } }

+    bool ICodeContext.IsStatic { get { return true; } }

+    List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }

+    List<Formal> ICodeContext.Ins { get { return this.Ins; } }

+    List<Formal> ICodeContext.Outs { get { return this.Outs; } }

+    ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }

+  }

+

+  /// <summary>

+  /// An "ICallable" is a function, method, or iterator.

+  /// </summary>

+  public interface ICallable { }

+

   public abstract class MemberDecl : Declaration {

     public readonly bool IsStatic;

     public readonly bool IsGhost;

@@ -1303,31 +1394,31 @@ namespace Microsoft.Dafny {
     public string Name {

       get {

         Contract.Ensures(Contract.Result<string>() != null);

-        throw new NotImplementedException();

+        throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here

       }

     }

     public string DisplayName {

       get {

         Contract.Ensures(Contract.Result<string>() != null);

-        throw new NotImplementedException();

+        throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here

       }

     }

     public string UniqueName {

       get {

         Contract.Ensures(Contract.Result<string>() != null);

-        throw new NotImplementedException();

+        throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here

       }

     }

     public string CompileName {

       get {

         Contract.Ensures(Contract.Result<string>() != null);

-        throw new NotImplementedException();

+        throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here

       }

     }

     public Type Type {

       get {

         Contract.Ensures(Contract.Result<Type>() != null);

-        throw new NotImplementedException();

+        throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here

       }

     }

     public bool IsMutable {

@@ -1502,7 +1593,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class Function : MemberDecl, TypeParameter.ParentType {

+  public class Function : MemberDecl, TypeParameter.ParentType, ICallable {

     public bool IsRecursive;  // filled in during resolution

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly IToken OpenParen;  // can be null (for predicates), if there are no formals

@@ -1588,7 +1679,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class Method : MemberDecl, TypeParameter.ParentType

+  public class Method : MemberDecl, TypeParameter.ParentType, ICodeContext

   {

     public readonly bool SignatureIsOmitted;

     public bool MustReverify;

@@ -1643,6 +1734,18 @@ namespace Microsoft.Dafny {
       this.SignatureIsOmitted = signatureOmitted;

       MustReverify = false;

     }

+

+    bool ICodeContext.IsGhost { get { return this.IsGhost; } }

+    bool ICodeContext.IsStatic { get { return this.IsStatic; } }

+    List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }

+    List<Formal> ICodeContext.Ins { get { return this.Ins; } }

+    List<Formal> ICodeContext.Outs { get { return this.Outs; } }

+    ModuleDefinition ICodeContext.EnclosingModule {

+      get {

+        Contract.Assert(this.EnclosingClass != null);  // this getter is supposed to be called only after signature-resolution is complete

+        return this.EnclosingClass.Module;

+      }

+    }

   }

 

   public class Constructor : Method

@@ -1854,10 +1957,11 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class ReturnStmt : Statement {

+  public abstract class ProduceStmt : Statement

+  {

     public List<AssignmentRhs> rhss;

     public UpdateStmt hiddenUpdate;

-    public ReturnStmt(IToken tok, List<AssignmentRhs> rhss)

+    public ProduceStmt(IToken tok, List<AssignmentRhs> rhss)

       : base(tok) {

       Contract.Requires(tok != null);

       this.rhss = rhss;

@@ -1876,7 +1980,24 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public abstract class AssignmentRhs {

+  public class ReturnStmt : ProduceStmt

+  {

+    public ReturnStmt(IToken tok, List<AssignmentRhs> rhss)

+      : base(tok, rhss) {

+      Contract.Requires(tok != null);

+    }

+  }

+

+  public class YieldStmt : ProduceStmt

+  {

+    public YieldStmt(IToken tok, List<AssignmentRhs> rhss)

+      : base(tok, rhss) {

+      Contract.Requires(tok != null);

+    }

+  }

+

+  public abstract class AssignmentRhs

+  {

     public readonly IToken Tok;

 

     private Attributes attributes;

@@ -2900,15 +3021,27 @@ namespace Microsoft.Dafny {
   public class StaticReceiverExpr : LiteralExpr

   {

     public StaticReceiverExpr(IToken tok, ClassDecl cl)

-      : base(tok)  // constructs a LiteralExpr representing the 'null' literal

+      : this(cl, tok)  // constructs a LiteralExpr representing the 'null' literal

     {

       Contract.Requires(tok != null);

       Contract.Requires(cl != null);

+    }

+    public StaticReceiverExpr(IToken tok, IteratorDecl iter)

+      : this(iter, tok)  // constructs a LiteralExpr representing the 'null' literal

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(iter != null);

+    }

+    private StaticReceiverExpr(TopLevelDecl decl, IToken tok)  // switch the order of the parameters, just to disambiguate calls

+      : base(tok)  // constructs a LiteralExpr representing the 'null' literal

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(decl != null);

       var typeArgs = new List<Type>();

-      foreach (var ta in cl.TypeArgs) {

+      foreach (var ta in decl.TypeArgs) {

         typeArgs.Add(new InferredTypeProxy());

       }

-      Type = new UserDefinedType(tok, cl.Name, cl, typeArgs);

+      Type = new UserDefinedType(tok, decl.Name, decl, typeArgs);

     }

   }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 69d13347..6b4be0eb 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -21,7 +21,7 @@ public class Parser {
 	public const int _colon = 5;

 	public const int _lbrace = 6;

 	public const int _rbrace = 7;

-	public const int maxT = 111;

+	public const int maxT = 114;

 

 	const bool T = true;

 	const bool x = false;

@@ -189,7 +189,7 @@ bool IsAttribute() {
 

 

 	void Dafny() {

-		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;

+		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

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

 		ModuleDecl submodule;

 		// to support multiple files, create a default module only if theModule is null

@@ -204,24 +204,42 @@ bool IsAttribute() {
 				Get();

 				isGhost = true; 

 			}

-			if (la.kind == 9 || la.kind == 11) {

+			switch (la.kind) {

+			case 9: case 11: {

 				SubModuleDecl(defaultModule, isGhost, out submodule);

 				defaultModule.TopLevelDecls.Add(submodule); 

-			} else if (la.kind == 18) {

+				break;

+			}

+			case 18: {

 				if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } 

 				ClassDecl(defaultModule, out c);

 				defaultModule.TopLevelDecls.Add(c); 

-			} else if (la.kind == 20 || la.kind == 21) {

+				break;

+			}

+			case 20: case 21: {

 				if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } 

 				DatatypeDecl(defaultModule, out dt);

 				defaultModule.TopLevelDecls.Add(dt); 

-			} else if (la.kind == 25) {

+				break;

+			}

+			case 25: {

 				if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } 

 				ArbitraryTypeDecl(defaultModule, out at);

 				defaultModule.TopLevelDecls.Add(at); 

-			} else if (StartOf(2)) {

+				break;

+			}

+			case 29: {

+				if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } 

+				IteratorDecl(defaultModule, out iter);

+				defaultModule.TopLevelDecls.Add(iter); 

+				break;

+			}

+			case 8: case 19: case 23: case 34: case 35: case 52: case 53: case 54: {

 				ClassMemberDecl(membersDefaultClass, isGhost, false);

-			} else SynErr(112);

+				break;

+			}

+			default: SynErr(115); break;

+			}

 		}

 		DefaultClassDecl defaultClass = null;

 		foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

@@ -239,7 +257,7 @@ bool IsAttribute() {
 	}

 

 	void SubModuleDecl(ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule) {

-		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;

+		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

 		Attributes attrs = null;  IToken/*!*/ id; 

 		List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;

 		List<IToken> idRefined = null, idPath = null, idAssignment = null;

@@ -268,24 +286,42 @@ bool IsAttribute() {
 					Get();

 					isGhost = true; 

 				}

-				if (la.kind == 9 || la.kind == 11) {

+				switch (la.kind) {

+				case 9: case 11: {

 					SubModuleDecl(module, isGhost, out sm);

 					module.TopLevelDecls.Add(sm); 

-				} else if (la.kind == 18) {

+					break;

+				}

+				case 18: {

 					if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } 

 					ClassDecl(module, out c);

 					module.TopLevelDecls.Add(c); 

-				} else if (la.kind == 20 || la.kind == 21) {

+					break;

+				}

+				case 20: case 21: {

 					if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } 

 					DatatypeDecl(module, out dt);

 					module.TopLevelDecls.Add(dt); 

-				} else if (la.kind == 25) {

+					break;

+				}

+				case 25: {

 					if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } 

 					ArbitraryTypeDecl(module, out at);

 					module.TopLevelDecls.Add(at); 

-				} else if (StartOf(2)) {

+					break;

+				}

+				case 29: {

+					if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } 

+					IteratorDecl(module, out iter);

+					module.TopLevelDecls.Add(iter); 

+					break;

+				}

+				case 8: case 19: case 23: case 34: case 35: case 52: case 53: case 54: {

 					ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);

-				} else SynErr(113);

+					break;

+				}

+				default: SynErr(116); break;

+				}

 			}

 			Expect(7);

 			module.BodyEndTok = t;

@@ -315,8 +351,8 @@ bool IsAttribute() {
 				}

 				Expect(14);

 				submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened); 

-			} else SynErr(114);

-		} else SynErr(115);

+			} else SynErr(117);

+		} else SynErr(118);

 	}

 

 	void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {

@@ -328,13 +364,13 @@ bool IsAttribute() {
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

-		while (!(la.kind == 0 || la.kind == 18)) {SynErr(116); Get();}

+		while (!(la.kind == 0 || la.kind == 18)) {SynErr(119); Get();}

 		Expect(18);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 29) {

+		if (la.kind == 32) {

 			GenericParameters(typeArgs);

 		}

 		Expect(6);

@@ -359,18 +395,18 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		bool co = false;

 		

-		while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(117); Get();}

+		while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(120); Get();}

 		if (la.kind == 20) {

 			Get();

 		} else if (la.kind == 21) {

 			Get();

 			co = true; 

-		} else SynErr(118);

+		} else SynErr(121);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 29) {

+		if (la.kind == 32) {

 			GenericParameters(typeArgs);

 		}

 		Expect(13);

@@ -380,7 +416,7 @@ bool IsAttribute() {
 			Get();

 			DatatypeMemberDecl(ctors);

 		}

-		while (!(la.kind == 0 || la.kind == 14)) {SynErr(119); Get();}

+		while (!(la.kind == 0 || la.kind == 14)) {SynErr(122); Get();}

 		Expect(14);

 		if (co) {

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

@@ -409,10 +445,69 @@ bool IsAttribute() {
 			eqSupport = TypeParameter.EqualitySupportValue.Required; 

 		}

 		at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); 

-		while (!(la.kind == 0 || la.kind == 14)) {SynErr(120); Get();}

+		while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();}

 		Expect(14);

 	}

 

+	void IteratorDecl(ModuleDefinition module, out IteratorDecl/*!*/ iter) {

+		Contract.Ensures(Contract.ValueAtReturn(out iter) != null);

+		IToken/*!*/ id;

+		Attributes attrs = null;

+		List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();

+		IToken openParen;

+		List<Formal/*!*/> ins = new List<Formal/*!*/>();

+		List<Formal/*!*/> outs = new List<Formal/*!*/>();

+		List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

+		List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();

+		List<Expression/*!*/> decreases = new List<Expression>();

+		List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();

+		List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();

+		List<MaybeFreeExpression/*!*/> yieldReq = new List<MaybeFreeExpression/*!*/>();

+		List<MaybeFreeExpression/*!*/> yieldEns = new List<MaybeFreeExpression/*!*/>();

+		List<Expression/*!*/> dec = new List<Expression/*!*/>();

+		Attributes readsAttrs = null;

+		Attributes modAttrs = null;

+		Attributes decrAttrs = null;

+		BlockStmt body = null;

+		bool signatureOmitted = false;

+		IToken bodyStart = Token.NoToken;

+		IToken bodyEnd = Token.NoToken;

+		

+		while (!(la.kind == 0 || la.kind == 29)) {SynErr(124); Get();}

+		Expect(29);

+		while (la.kind == 6) {

+			Attribute(ref attrs);

+		}

+		NoUSIdent(out id);

+		if (la.kind == 26 || la.kind == 32) {

+			if (la.kind == 32) {

+				GenericParameters(typeArgs);

+			}

+			Formals(true, true, ins, out openParen);

+			if (la.kind == 30) {

+				Get();

+				Formals(false, true, outs, out openParen);

+			}

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

+			Get();

+			signatureOmitted = true; openParen = Token.NoToken; 

+		} else SynErr(125);

+		while (StartOf(3)) {

+			IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);

+		}

+		if (la.kind == 6) {

+			BlockStmt(out body, out bodyStart, out bodyEnd);

+		}

+		iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,

+		                       new Specification<FrameExpression>(mod, modAttrs), new Specification<FrameExpression>(reads, readsAttrs),

+		                       new Specification<Expression>(decreases, decrAttrs),

+		                       req, ens, yieldReq, yieldEns,

+		                       body, attrs, signatureOmitted);

+		iter.BodyStartTok = bodyStart;

+		iter.BodyEndTok = bodyEnd;

+		

+	}

+

 	void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) {

 		Contract.Requires(cce.NonNullElements(mm));

 		Method/*!*/ m;

@@ -431,13 +526,13 @@ bool IsAttribute() {
 		}

 		if (la.kind == 23) {

 			FieldDecl(mmod, mm);

-		} else if (la.kind == 48 || la.kind == 49 || la.kind == 50) {

+		} else if (la.kind == 52 || la.kind == 53 || la.kind == 54) {

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (la.kind == 31 || la.kind == 32) {

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

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

-		} else SynErr(121);

+		} else SynErr(126);

 	}

 

 	void Attribute(ref Attributes attrs) {

@@ -478,7 +573,7 @@ bool IsAttribute() {
 		IToken/*!*/ id;

 		TypeParameter.EqualitySupportValue eqSupport;

 		

-		Expect(29);

+		Expect(32);

 		NoUSIdent(out id);

 		eqSupport = TypeParameter.EqualitySupportValue.Unspecified; 

 		if (la.kind == 26) {

@@ -500,7 +595,7 @@ bool IsAttribute() {
 			}

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

 		}

-		Expect(30);

+		Expect(33);

 	}

 

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

@@ -508,7 +603,7 @@ bool IsAttribute() {
 		Attributes attrs = null;

 		IToken/*!*/ id;  Type/*!*/ ty;

 		

-		while (!(la.kind == 0 || la.kind == 23)) {SynErr(122); Get();}

+		while (!(la.kind == 0 || la.kind == 23)) {SynErr(127); Get();}

 		Expect(23);

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

 		

@@ -522,7 +617,7 @@ bool IsAttribute() {
 			IdentType(out id, out ty, false);

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

 		}

-		while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();}

+		while (!(la.kind == 0 || la.kind == 14)) {SynErr(128); Get();}

 		Expect(14);

 	}

 

@@ -545,9 +640,9 @@ bool IsAttribute() {
 		IToken bodyEnd = Token.NoToken;

 		bool signatureOmitted = false;

 		

-		if (la.kind == 48) {

+		if (la.kind == 52) {

 			Get();

-			if (la.kind == 31) {

+			if (la.kind == 34) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -557,22 +652,22 @@ bool IsAttribute() {
 				Attribute(ref attrs);

 			}

 			NoUSIdent(out id);

-			if (la.kind == 26 || la.kind == 29) {

-				if (la.kind == 29) {

+			if (la.kind == 26 || la.kind == 32) {

+				if (la.kind == 32) {

 					GenericParameters(typeArgs);

 				}

 				Formals(true, isFunctionMethod, formals, out openParen);

 				Expect(5);

 				Type(out returnType);

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

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

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(124);

-		} else if (la.kind == 49) {

+			} else SynErr(129);

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

 			Get();

 			isPredicate = true; 

-			if (la.kind == 31) {

+			if (la.kind == 34) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -582,8 +677,8 @@ bool IsAttribute() {
 				Attribute(ref attrs);

 			}

 			NoUSIdent(out id);

-			if (StartOf(3)) {

-				if (la.kind == 29) {

+			if (StartOf(4)) {

+				if (la.kind == 32) {

 					GenericParameters(typeArgs);

 				}

 				if (la.kind == 26) {

@@ -593,12 +688,12 @@ bool IsAttribute() {
 						SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 

 					}

 				}

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

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

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(125);

-		} else if (la.kind == 50) {

+			} else SynErr(130);

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

 			Get();

 			isCoPredicate = true; 

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

@@ -607,8 +702,8 @@ bool IsAttribute() {
 				Attribute(ref attrs);

 			}

 			NoUSIdent(out id);

-			if (StartOf(3)) {

-				if (la.kind == 29) {

+			if (StartOf(4)) {

+				if (la.kind == 32) {

 					GenericParameters(typeArgs);

 				}

 				if (la.kind == 26) {

@@ -618,14 +713,14 @@ bool IsAttribute() {
 						SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); 

 					}

 				}

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

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

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(126);

-		} else SynErr(127);

+			} else SynErr(131);

+		} else SynErr(132);

 		decreases = isCoPredicate ? null : new List<Expression/*!*/>(); 

-		while (StartOf(4)) {

+		while (StartOf(5)) {

 			FunctionSpec(reqs, reads, ens, decreases);

 		}

 		if (la.kind == 6) {

@@ -666,10 +761,10 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(la.kind == 0 || la.kind == 31 || la.kind == 32)) {SynErr(128); Get();}

-		if (la.kind == 31) {

+		while (!(la.kind == 0 || la.kind == 34 || la.kind == 35)) {SynErr(133); Get();}

+		if (la.kind == 34) {

 			Get();

-		} else if (la.kind == 32) {

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

 			Get();

 			if (allowConstructor) {

 			 isConstructor = true;

@@ -677,7 +772,7 @@ bool IsAttribute() {
 			 SemErr(t, "constructors are only allowed in classes");

 			}

 			

-		} else SynErr(129);

+		} else SynErr(134);

 		if (isConstructor) {

 		 if (mmod.IsGhost) {

 		   SemErr(t, "constructors cannot be declared 'ghost'");

@@ -691,21 +786,21 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 26 || la.kind == 29) {

-			if (la.kind == 29) {

+		if (la.kind == 26 || la.kind == 32) {

+			if (la.kind == 32) {

 				GenericParameters(typeArgs);

 			}

 			Formals(true, !mmod.IsGhost, ins, out openParen);

-			if (la.kind == 33) {

+			if (la.kind == 36) {

 				Get();

 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 				Formals(false, !mmod.IsGhost, outs, out openParen);

 			}

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

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

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

-		} else SynErr(130);

-		while (StartOf(5)) {

+		} else SynErr(135);

+		while (StartOf(6)) {

 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);

 		}

 		if (la.kind == 6) {

@@ -742,7 +837,7 @@ bool IsAttribute() {
 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 

 		Expect(26);

-		if (StartOf(6)) {

+		if (StartOf(7)) {

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

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

 			while (la.kind == 24) {

@@ -849,22 +944,22 @@ bool IsAttribute() {
 		List<Type/*!*/>/*!*/ gt;

 		

 		switch (la.kind) {

-		case 40: {

+		case 44: {

 			Get();

 			tok = t; 

 			break;

 		}

-		case 41: {

+		case 45: {

 			Get();

 			tok = t;  ty = new NatType(); 

 			break;

 		}

-		case 42: {

+		case 46: {

 			Get();

 			tok = t;  ty = new IntType(); 

 			break;

 		}

-		case 43: {

+		case 47: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -875,7 +970,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 44: {

+		case 48: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -886,7 +981,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 45: {

+		case 49: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -897,7 +992,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 46: {

+		case 50: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -908,11 +1003,11 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 1: case 3: case 47: {

+		case 1: case 3: case 51: {

 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(131); break;

+		default: SynErr(136); break;

 		}

 	}

 

@@ -932,18 +1027,35 @@ bool IsAttribute() {
 		Expect(28);

 	}

 

-	void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,

-List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs) {

-		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

-		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

+	void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,

+List<MaybeFreeExpression/*!*/>/*!*/ req, List<MaybeFreeExpression/*!*/>/*!*/ ens,

+List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*/ yieldEns,

+ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {

+		Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;

 		

-		while (!(StartOf(7))) {SynErr(132); Get();}

-		if (la.kind == 35) {

+		while (!(StartOf(8))) {SynErr(137); Get();}

+		if (la.kind == 42) {

+			Get();

+			while (IsAttribute()) {

+				Attribute(ref readsAttrs);

+			}

+			if (StartOf(9)) {

+				FrameExpression(out fe);

+				reads.Add(fe); 

+				while (la.kind == 24) {

+					Get();

+					FrameExpression(out fe);

+					reads.Add(fe); 

+				}

+			}

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(138); Get();}

+			Expect(14);

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

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref modAttrs);

 			}

-			if (StartOf(8)) {

+			if (StartOf(9)) {

 				FrameExpression(out fe);

 				mod.Add(fe); 

 				while (la.kind == 24) {

@@ -952,38 +1064,52 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					mod.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 14)) {SynErr(133); Get();}

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(139); Get();}

 			Expect(14);

-		} else if (la.kind == 36 || la.kind == 37 || la.kind == 38) {

-			if (la.kind == 36) {

+		} else if (StartOf(10)) {

+			if (la.kind == 38) {

 				Get();

 				isFree = true; 

 			}

-			if (la.kind == 37) {

+			if (la.kind == 43) {

+				Get();

+				isYield = true; 

+			}

+			if (la.kind == 39) {

 				Get();

 				Expression(out e);

-				while (!(la.kind == 0 || la.kind == 14)) {SynErr(134); Get();}

+				while (!(la.kind == 0 || la.kind == 14)) {SynErr(140); Get();}

 				Expect(14);

-				req.Add(new MaybeFreeExpression(e, isFree)); 

-			} else if (la.kind == 38) {

+				if (isYield) {

+				 yieldReq.Add(new MaybeFreeExpression(e, isFree));

+				} else {

+				 req.Add(new MaybeFreeExpression(e, isFree));

+				}

+				

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

 				}

 				Expression(out e);

-				while (!(la.kind == 0 || la.kind == 14)) {SynErr(135); Get();}

+				while (!(la.kind == 0 || la.kind == 14)) {SynErr(141); Get();}

 				Expect(14);

-				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

-			} else SynErr(136);

-		} else if (la.kind == 39) {

+				if (isYield) {

+				 yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

+				} else {

+				 ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

+				}

+				

+			} else SynErr(142);

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

 			Get();

 			while (IsAttribute()) {

-				Attribute(ref decAttrs);

+				Attribute(ref decrAttrs);

 			}

-			DecreasesList(decreases, true);

-			while (!(la.kind == 0 || la.kind == 14)) {SynErr(137); Get();}

+			DecreasesList(decreases, false);

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(143); Get();}

 			Expect(14);

-		} else SynErr(138);

+		} else SynErr(144);

 	}

 

 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

@@ -992,7 +1118,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(6);

 		bodyStart = t; 

-		while (StartOf(9)) {

+		while (StartOf(11)) {

 			Stmt(body);

 		}

 		Expect(7);

@@ -1000,6 +1126,60 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		block = new BlockStmt(bodyStart, body); 

 	}

 

+	void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,

+List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs) {

+		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

+		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

+		

+		while (!(StartOf(12))) {SynErr(145); Get();}

+		if (la.kind == 37) {

+			Get();

+			while (IsAttribute()) {

+				Attribute(ref modAttrs);

+			}

+			if (StartOf(9)) {

+				FrameExpression(out fe);

+				mod.Add(fe); 

+				while (la.kind == 24) {

+					Get();

+					FrameExpression(out fe);

+					mod.Add(fe); 

+				}

+			}

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(146); Get();}

+			Expect(14);

+		} else if (la.kind == 38 || la.kind == 39 || la.kind == 40) {

+			if (la.kind == 38) {

+				Get();

+				isFree = true; 

+			}

+			if (la.kind == 39) {

+				Get();

+				Expression(out e);

+				while (!(la.kind == 0 || la.kind == 14)) {SynErr(147); Get();}

+				Expect(14);

+				req.Add(new MaybeFreeExpression(e, isFree)); 

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

+				Get();

+				while (IsAttribute()) {

+					Attribute(ref ensAttrs);

+				}

+				Expression(out e);

+				while (!(la.kind == 0 || la.kind == 14)) {SynErr(148); Get();}

+				Expect(14);

+				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

+			} else SynErr(149);

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

+			Get();

+			while (IsAttribute()) {

+				Attribute(ref decAttrs);

+			}

+			DecreasesList(decreases, true);

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(150); Get();}

+			Expect(14);

+		} else SynErr(151);

+	}

+

 	void FrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null);

 		Expression/*!*/ e;

@@ -1007,21 +1187,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		string fieldName = null;  IToken feTok = null;

 		fe = null;

 		

-		if (StartOf(10)) {

+		if (StartOf(13)) {

 			Expression(out e);

 			feTok = e.tok; 

-			if (la.kind == 53) {

+			if (la.kind == 56) {

 				Get();

 				Ident(out id);

 				fieldName = id.val;  feTok = id; 

 			}

 			fe = new FrameExpression(feTok, e, fieldName); 

-		} else if (la.kind == 53) {

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

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

 			fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); 

-		} else SynErr(139);

+		} else SynErr(152);

 	}

 

 	void Expression(out Expression/*!*/ e) {

@@ -1051,7 +1231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {

 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 

-		Expect(29);

+		Expect(32);

 		Type(out ty);

 		gt.Add(ty); 

 		while (la.kind == 24) {

@@ -1059,7 +1239,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(30);

+		Expect(33);

 	}

 

 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

@@ -1068,7 +1248,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Type/*!*/>/*!*/ gt;

 		List<IToken> path;

 		

-		if (la.kind == 47) {

+		if (la.kind == 51) {

 			Get();

 			tok = t;  ty = new ObjectType(); 

 		} else if (la.kind == 3) {

@@ -1093,11 +1273,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Get();

 				Ident(out tok);

 			}

-			if (la.kind == 29) {

+			if (la.kind == 32) {

 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt, path); 

-		} else SynErr(140);

+		} else SynErr(153);

 	}

 

 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {

@@ -1105,16 +1285,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(cce.NonNullElements(reads));

 		Contract.Requires(decreases == null || cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

-		if (la.kind == 37) {

-			while (!(la.kind == 0 || la.kind == 37)) {SynErr(141); Get();}

+		if (la.kind == 39) {

+			while (!(la.kind == 0 || la.kind == 39)) {SynErr(154); Get();}

 			Get();

 			Expression(out e);

-			while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();}

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(155); Get();}

 			Expect(14);

 			reqs.Add(e); 

-		} else if (la.kind == 51) {

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

 			Get();

-			if (StartOf(11)) {

+			if (StartOf(14)) {

 				PossiblyWildFrameExpression(out fe);

 				reads.Add(fe); 

 				while (la.kind == 24) {

@@ -1123,15 +1303,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					reads.Add(fe); 

 				}

 			}

-			while (!(la.kind == 0 || la.kind == 14)) {SynErr(143); Get();}

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(156); Get();}

 			Expect(14);

-		} else if (la.kind == 38) {

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

 			Get();

 			Expression(out e);

-			while (!(la.kind == 0 || la.kind == 14)) {SynErr(144); Get();}

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(157); Get();}

 			Expect(14);

 			ens.Add(e); 

-		} else if (la.kind == 39) {

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

 			Get();

 			if (decreases == null) {

 			 SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");

@@ -1139,9 +1319,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			

 			DecreasesList(decreases, false);

-			while (!(la.kind == 0 || la.kind == 14)) {SynErr(145); Get();}

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(158); Get();}

 			Expect(14);

-		} else SynErr(146);

+		} else SynErr(159);

 	}

 

 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

@@ -1155,23 +1335,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 

-		if (la.kind == 52) {

+		if (la.kind == 55) {

 			Get();

 			fe = new FrameExpression(t, new WildcardExpr(t), null); 

-		} else if (StartOf(8)) {

+		} else if (StartOf(9)) {

 			FrameExpression(out fe);

-		} else SynErr(147);

+		} else SynErr(160);

 	}

 

 	void PossiblyWildExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e)!=null);

 		e = dummyExpr; 

-		if (la.kind == 52) {

+		if (la.kind == 55) {

 			Get();

 			e = new WildcardExpr(t); 

-		} else if (StartOf(10)) {

+		} else if (StartOf(13)) {

 			Expression(out e);

-		} else SynErr(148);

+		} else SynErr(161);

 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

@@ -1188,26 +1368,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

-		while (!(StartOf(12))) {SynErr(149); Get();}

+		while (!(StartOf(15))) {SynErr(162); Get();}

 		switch (la.kind) {

 		case 6: {

 			BlockStmt(out bs, out bodyStart, out bodyEnd);

 			s = bs; 

 			break;

 		}

-		case 72: {

+		case 75: {

 			AssertStmt(out s);

 			break;

 		}

-		case 60: {

+		case 63: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 73: {

+		case 76: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 22: case 26: case 97: case 98: case 99: case 100: case 101: case 102: {

+		case 1: case 2: case 22: case 26: case 100: case 101: case 102: case 103: case 104: case 105: {

 			UpdateStmt(out s);

 			break;

 		}

@@ -1215,23 +1395,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);

 			break;

 		}

-		case 65: {

+		case 68: {

 			IfStmt(out s);

 			break;

 		}

-		case 69: {

+		case 72: {

 			WhileStmt(out s);

 			break;

 		}

-		case 71: {

+		case 74: {

 			MatchStmt(out s);

 			break;

 		}

-		case 74: {

+		case 77: {

 			ParallelStmt(out s);

 			break;

 		}

-		case 54: {

+		case 57: {

 			Get();

 			x = t; 

 			NoUSIdent(out id);

@@ -1240,33 +1420,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

 			break;

 		}

-		case 55: {

+		case 58: {

 			Get();

 			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

 				NoUSIdent(out id);

 				label = id.val; 

-			} else if (la.kind == 14 || la.kind == 55) {

-				while (la.kind == 55) {

+			} else if (la.kind == 14 || la.kind == 58) {

+				while (la.kind == 58) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(150);

-			while (!(la.kind == 0 || la.kind == 14)) {SynErr(151); Get();}

+			} else SynErr(163);

+			while (!(la.kind == 0 || la.kind == 14)) {SynErr(164); Get();}

 			Expect(14);

 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 			break;

 		}

-		case 58: {

+		case 43: case 61: {

 			ReturnStmt(out s);

 			break;

 		}

-		case 34: {

+		case 31: {

 			SkeletonStmt(out s);

 			Expect(14);

 			break;

 		}

-		default: SynErr(152); break;

+		default: SynErr(165); break;

 		}

 	}

 

@@ -1274,16 +1454,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

 		Expression e = null; Attributes attrs = null;

 		

-		Expect(72);

+		Expect(75);

 		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

-		if (StartOf(10)) {

+		if (StartOf(13)) {

 			Expression(out e);

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

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

 			Get();

-		} else SynErr(153);

+		} else SynErr(166);

 		Expect(14);

 		if (e == null) {

 		 s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);

@@ -1297,16 +1477,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

 		Expression e = null; Attributes attrs = null;

 		

-		Expect(60);

+		Expect(63);

 		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

-		if (StartOf(10)) {

+		if (StartOf(13)) {

 			Expression(out e);

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

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

 			Get();

-		} else SynErr(154);

+		} else SynErr(167);

 		if (e == null) {

 		 s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

 		} else {

@@ -1320,7 +1500,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

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

 		

-		Expect(73);

+		Expect(76);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

@@ -1351,14 +1531,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(14);

 			rhss.Add(new ExprRhs(e, attrs)); 

-		} else if (la.kind == 24 || la.kind == 57 || la.kind == 59) {

+		} else if (la.kind == 24 || la.kind == 60 || la.kind == 62) {

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 24) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			if (la.kind == 57) {

+			if (la.kind == 60) {

 				Get();

 				x = t; 

 				Rhs(out r, lhs0);

@@ -1368,20 +1548,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Rhs(out r, lhs0);

 					rhss.Add(r); 

 				}

-			} else if (la.kind == 59) {

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

 				Get();

 				x = t; 

-				if (la.kind == 60) {

+				if (la.kind == 63) {

 					Get();

 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(155);

+			} else SynErr(168);

 			Expect(14);

 		} else if (la.kind == 5) {

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(156);

+		} else SynErr(169);

 		if (suchThat != null) {

 		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

 		} else {

@@ -1416,8 +1596,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); 

 		}

-		if (la.kind == 57 || la.kind == 59) {

-			if (la.kind == 57) {

+		if (la.kind == 60 || la.kind == 62) {

+			if (la.kind == 60) {

 				Get();

 				assignTok = t;

 				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

@@ -1433,7 +1613,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {

 				Get();

 				assignTok = t; 

-				if (la.kind == 60) {

+				if (la.kind == 63) {

 					Get();

 					suchThatAssume = t; 

 				}

@@ -1472,9 +1652,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(65);

+		Expect(68);

 		x = t; 

-		if (la.kind == 26 || la.kind == 34) {

+		if (la.kind == 26 || la.kind == 31) {

 			if (la.kind == 26) {

 				Guard(out guard);

 			} else {

@@ -1482,15 +1662,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				guardOmitted = true; 

 			}

 			BlockStmt(out thn, out bodyStart, out bodyEnd);

-			if (la.kind == 66) {

+			if (la.kind == 69) {

 				Get();

-				if (la.kind == 65) {

+				if (la.kind == 68) {

 					IfStmt(out s);

 					els = s; 

 				} else if (la.kind == 6) {

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; 

-				} else SynErr(157);

+				} else SynErr(170);

 			}

 			if (guardOmitted) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);

@@ -1501,7 +1681,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 6) {

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(158);

+		} else SynErr(171);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1517,9 +1697,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(69);

+		Expect(72);

 		x = t; 

-		if (la.kind == 26 || la.kind == 34) {

+		if (la.kind == 26 || la.kind == 31) {

 			if (la.kind == 26) {

 				Guard(out guard);

 				Contract.Assume(guard == null || cce.Owner.None(guard)); 

@@ -1530,10 +1710,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			if (la.kind == 6) {

 				BlockStmt(out body, out bodyStart, out bodyEnd);

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

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

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(159);

+			} else SynErr(172);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

@@ -1549,22 +1729,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);

 			}

 			

-		} else if (StartOf(13)) {

+		} else if (StartOf(16)) {

 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 

-		} else SynErr(160);

+		} else SynErr(173);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 

-		Expect(71);

+		Expect(74);

 		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (la.kind == 67) {

+		while (la.kind == 70) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1584,7 +1764,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(74);

+		Expect(77);

 		x = t; 

 		Expect(26);

 		if (la.kind == 1) {

@@ -1597,13 +1777,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (range == null) { range = new LiteralExpr(x, true); }

 		

 		Expect(28);

-		while (la.kind == 36 || la.kind == 38) {

+		while (la.kind == 38 || la.kind == 40) {

 			isFree = false; 

-			if (la.kind == 36) {

+			if (la.kind == 38) {

 				Get();

 				isFree = true; 

 			}

-			Expect(38);

+			Expect(40);

 			Expression(out e);

 			Expect(14);

 			ens.Add(new MaybeFreeExpression(e, isFree)); 

@@ -1616,10 +1796,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken returnTok = null;

 		List<AssignmentRhs> rhss = null;

 		AssignmentRhs r;

+		bool isYield = false;

 		

-		Expect(58);

-		returnTok = t; 

-		if (StartOf(14)) {

+		if (la.kind == 61) {

+			Get();

+			returnTok = t; 

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

+			Get();

+			returnTok = t; isYield = true; 

+		} else SynErr(174);

+		if (StartOf(17)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

 			while (la.kind == 24) {

@@ -1629,7 +1815,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 		}

 		Expect(14);

-		s = new ReturnStmt(returnTok, rhss); 

+		if (isYield) {

+		 s = new YieldStmt(returnTok, rhss);

+		} else {

+		 s = new ReturnStmt(returnTok, rhss);

+		}

+		

 	}

 

 	void SkeletonStmt(out Statement s) {

@@ -1637,9 +1828,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> exprs = null;

 		IToken tok, dotdotdot, whereTok;

 		Expression e; 

-		Expect(34);

+		Expect(31);

 		dotdotdot = t; 

-		if (la.kind == 56) {

+		if (la.kind == 59) {

 			Get();

 			names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;

 			Ident(out tok);

@@ -1649,7 +1840,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Ident(out tok);

 				names.Add(tok); 

 			}

-			Expect(57);

+			Expect(60);

 			Expression(out e);

 			exprs.Add(e); 

 			while (la.kind == 24) {

@@ -1676,16 +1867,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = dummyRhs;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 61) {

+		if (la.kind == 64) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 17 || la.kind == 26 || la.kind == 62) {

-				if (la.kind == 62) {

+			if (la.kind == 17 || la.kind == 26 || la.kind == 65) {

+				if (la.kind == 65) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(63);

+					Expect(66);

 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

 					

 				} else if (la.kind == 17) {

@@ -1693,7 +1884,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Ident(out x);

 					Expect(26);

 					args = new List<Expression/*!*/>(); 

-					if (StartOf(10)) {

+					if (StartOf(13)) {

 						Expressions(args);

 					}

 					Expect(28);

@@ -1711,7 +1902,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					 x = null;

 					}

 					args = new List<Expression/*!*/>(); 

-					if (StartOf(10)) {

+					if (StartOf(13)) {

 						Expressions(args);

 					}

 					Expect(28);

@@ -1727,18 +1918,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);

 			}

 			

-		} else if (la.kind == 64) {

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

 			Get();

 			x = t; 

 			Expression(out e);

 			r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); 

-		} else if (la.kind == 52) {

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

 			Get();

 			r = new HavocRhs(t); 

-		} else if (StartOf(10)) {

+		} else if (StartOf(13)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(161);

+		} else SynErr(175);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1750,16 +1941,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 17 || la.kind == 62) {

+			while (la.kind == 17 || la.kind == 65) {

 				Suffix(ref e);

 			}

-		} else if (StartOf(15)) {

+		} else if (StartOf(18)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

-			while (la.kind == 17 || la.kind == 62) {

+			while (la.kind == 17 || la.kind == 65) {

 				Suffix(ref e);

 			}

-		} else SynErr(162);

+		} else SynErr(176);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -1776,13 +1967,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void Guard(out Expression e) {

 		Expression/*!*/ ee;  e = null; 

 		Expect(26);

-		if (la.kind == 52) {

+		if (la.kind == 55) {

 			Get();

 			e = null; 

-		} else if (StartOf(10)) {

+		} else if (StartOf(13)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(163);

+		} else SynErr(177);

 		Expect(28);

 	}

 

@@ -1793,13 +1984,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;

 		

 		Expect(6);

-		while (la.kind == 67) {

+		while (la.kind == 70) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(68);

+			Expect(71);

 			body = new List<Statement>(); 

-			while (StartOf(9)) {

+			while (StartOf(11)) {

 				Stmt(body);

 			}

 			alternatives.Add(new GuardedAlternative(x, e, body)); 

@@ -1814,29 +2005,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		decreases = new List<Expression/*!*/>();

 		mod = null;

 		

-		while (StartOf(16)) {

-			if (la.kind == 36 || la.kind == 70) {

+		while (StartOf(19)) {

+			if (la.kind == 38 || la.kind == 73) {

 				Invariant(out invariant);

-				while (!(la.kind == 0 || la.kind == 14)) {SynErr(164); Get();}

+				while (!(la.kind == 0 || la.kind == 14)) {SynErr(178); Get();}

 				Expect(14);

 				invariants.Add(invariant); 

-			} else if (la.kind == 39) {

-				while (!(la.kind == 0 || la.kind == 39)) {SynErr(165); Get();}

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

+				while (!(la.kind == 0 || la.kind == 41)) {SynErr(179); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

-				while (!(la.kind == 0 || la.kind == 14)) {SynErr(166); Get();}

+				while (!(la.kind == 0 || la.kind == 14)) {SynErr(180); Get();}

 				Expect(14);

 			} else {

-				while (!(la.kind == 0 || la.kind == 35)) {SynErr(167); Get();}

+				while (!(la.kind == 0 || la.kind == 37)) {SynErr(181); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

 				}

 				mod = mod ?? new List<FrameExpression>(); 

-				if (StartOf(8)) {

+				if (StartOf(9)) {

 					FrameExpression(out fe);

 					mod.Add(fe); 

 					while (la.kind == 24) {

@@ -1845,7 +2036,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

-				while (!(la.kind == 0 || la.kind == 14)) {SynErr(168); Get();}

+				while (!(la.kind == 0 || la.kind == 14)) {SynErr(182); Get();}

 				Expect(14);

 			}

 		}

@@ -1853,12 +2044,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 36 || la.kind == 70)) {SynErr(169); Get();}

-		if (la.kind == 36) {

+		while (!(la.kind == 0 || la.kind == 38 || la.kind == 73)) {SynErr(183); Get();}

+		if (la.kind == 38) {

 			Get();

 			isFree = true; 

 		}

-		Expect(70);

+		Expect(73);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1873,7 +2064,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

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

 		

-		Expect(67);

+		Expect(70);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 26) {

@@ -1887,8 +2078,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(28);

 		}

-		Expect(68);

-		while (StartOf(9)) {

+		Expect(71);

+		while (StartOf(11)) {

 			Stmt(body);

 		}

 		c = new MatchCaseStmt(x, id.val, arguments, body); 

@@ -1899,10 +2090,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 4) {

 			Get();

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

-		} else if (StartOf(10)) {

+		} else if (StartOf(13)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(170);

+		} else SynErr(184);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1930,7 +2121,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void EquivExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		ImpliesExpression(out e0);

-		while (la.kind == 75 || la.kind == 76) {

+		while (la.kind == 78 || la.kind == 79) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1941,7 +2132,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		LogicalExpression(out e0);

-		if (la.kind == 77 || la.kind == 78) {

+		if (la.kind == 80 || la.kind == 81) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1950,23 +2141,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void EquivOp() {

-		if (la.kind == 75) {

+		if (la.kind == 78) {

 			Get();

-		} else if (la.kind == 76) {

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

 			Get();

-		} else SynErr(171);

+		} else SynErr(185);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0);

-		if (StartOf(17)) {

-			if (la.kind == 79 || la.kind == 80) {

+		if (StartOf(20)) {

+			if (la.kind == 82 || la.kind == 83) {

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (la.kind == 79 || la.kind == 80) {

+				while (la.kind == 82 || la.kind == 83) {

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1977,7 +2168,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (la.kind == 81 || la.kind == 82) {

+				while (la.kind == 84 || la.kind == 85) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1988,11 +2179,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 77) {

+		if (la.kind == 80) {

 			Get();

-		} else if (la.kind == 78) {

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

 			Get();

-		} else SynErr(172);

+		} else SynErr(186);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e) {

@@ -2009,7 +2200,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Term(out e0);

 		e = e0; 

-		if (StartOf(18)) {

+		if (StartOf(21)) {

 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

@@ -2017,7 +2208,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (op == BinaryExpr.Opcode.Disjoint)

 			 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

 			

-			while (StartOf(18)) {

+			while (StartOf(21)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

 				 ops = new List<BinaryExpr.Opcode>();

@@ -2086,25 +2277,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 79) {

+		if (la.kind == 82) {

 			Get();

-		} else if (la.kind == 80) {

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

 			Get();

-		} else SynErr(173);

+		} else SynErr(187);

 	}

 

 	void OrOp() {

-		if (la.kind == 81) {

+		if (la.kind == 84) {

 			Get();

-		} else if (la.kind == 82) {

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

 			Get();

-		} else SynErr(174);

+		} else SynErr(188);

 	}

 

 	void Term(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		Factor(out e0);

-		while (la.kind == 92 || la.kind == 93) {

+		while (la.kind == 95 || la.kind == 96) {

 			AddOp(out x, out op);

 			Factor(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -2122,45 +2313,45 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Eq; 

 			break;

 		}

-		case 29: {

+		case 32: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Lt; 

 			break;

 		}

-		case 30: {

+		case 33: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

 		}

-		case 83: {

+		case 86: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 84: {

+		case 87: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		case 85: {

+		case 88: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 86: {

+		case 89: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Disjoint; 

 			break;

 		}

-		case 87: {

+		case 90: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.In; 

 			break;

 		}

-		case 88: {

+		case 91: {

 			Get();

 			x = t;  y = Token.NoToken; 

-			if (la.kind == 87) {

+			if (la.kind == 90) {

 				Get();

 				y = t; 

 			}

@@ -2175,29 +2366,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 			break;

 		}

-		case 89: {

+		case 92: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Neq; 

 			break;

 		}

-		case 90: {

+		case 93: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Le; 

 			break;

 		}

-		case 91: {

+		case 94: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(175); break;

+		default: SynErr(189); break;

 		}

 	}

 

 	void Factor(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

-		while (la.kind == 52 || la.kind == 94 || la.kind == 95) {

+		while (la.kind == 55 || la.kind == 97 || la.kind == 98) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -2206,103 +2397,103 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 92) {

+		if (la.kind == 95) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Add; 

-		} else if (la.kind == 93) {

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

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(176);

+		} else SynErr(190);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 

 		switch (la.kind) {

-		case 93: {

+		case 96: {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 

 			break;

 		}

-		case 88: case 96: {

+		case 91: case 99: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 23: case 43: case 54: case 60: case 65: case 71: case 72: case 105: case 106: case 107: case 108: {

+		case 23: case 47: case 57: case 63: case 68: case 74: case 75: case 108: case 109: case 110: case 111: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 17 || la.kind == 62) {

+			while (la.kind == 17 || la.kind == 65) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 62: {

+		case 6: case 65: {

 			DisplayExpr(out e);

-			while (la.kind == 17 || la.kind == 62) {

+			while (la.kind == 17 || la.kind == 65) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 44: {

+		case 48: {

 			MultiSetExpr(out e);

-			while (la.kind == 17 || la.kind == 62) {

+			while (la.kind == 17 || la.kind == 65) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 46: {

+		case 50: {

 			Get();

 			x = t; 

-			if (la.kind == 62) {

+			if (la.kind == 65) {

 				MapDisplayExpr(x, out e);

-				while (la.kind == 17 || la.kind == 62) {

+				while (la.kind == 17 || la.kind == 65) {

 					Suffix(ref e);

 				}

 			} else if (la.kind == 1) {

 				MapComprehensionExpr(x, out e);

-			} else if (StartOf(19)) {

+			} else if (StartOf(22)) {

 				SemErr("map must be followed by literal in brackets or comprehension."); 

-			} else SynErr(177);

+			} else SynErr(191);

 			break;

 		}

-		case 2: case 22: case 26: case 97: case 98: case 99: case 100: case 101: case 102: {

+		case 2: case 22: case 26: case 100: case 101: case 102: case 103: case 104: case 105: {

 			ConstAtomExpression(out e);

-			while (la.kind == 17 || la.kind == 62) {

+			while (la.kind == 17 || la.kind == 65) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(178); break;

+		default: SynErr(192); break;

 		}

 	}

 

 	void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 52) {

+		if (la.kind == 55) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mul; 

-		} else if (la.kind == 94) {

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

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Div; 

-		} else if (la.kind == 95) {

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

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(179);

+		} else SynErr(193);

 	}

 

 	void NegOp() {

-		if (la.kind == 88) {

+		if (la.kind == 91) {

 			Get();

-		} else if (la.kind == 96) {

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

 			Get();

-		} else SynErr(180);

+		} else SynErr(194);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -2311,30 +2502,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 65: {

+		case 68: {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(103);

+			Expect(106);

 			Expression(out e0);

-			Expect(66);

+			Expect(69);

 			Expression(out e1);

 			e = new ITEExpr(x, e, e0, e1); 

 			break;

 		}

-		case 71: {

+		case 74: {

 			MatchExpression(out e);

 			break;

 		}

-		case 105: case 106: case 107: case 108: {

+		case 108: case 109: case 110: case 111: {

 			QuantifierGuts(out e);

 			break;

 		}

-		case 43: {

+		case 47: {

 			ComprehensionExpr(out e);

 			break;

 		}

-		case 72: {

+		case 75: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2343,7 +2534,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AssertExpr(x, e0, e1); 

 			break;

 		}

-		case 60: {

+		case 63: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2356,11 +2547,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LetExpr(out e);

 			break;

 		}

-		case 54: {

+		case 57: {

 			NamedExpr(out e);

 			break;

 		}

-		default: SynErr(181); break;

+		default: SynErr(195); break;

 		}

 	}

 

@@ -2379,7 +2570,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 26) {

 			Get();

 			openParen = t;  args = new List<Expression>(); 

-			if (StartOf(10)) {

+			if (StartOf(13)) {

 				Expressions(args);

 			}

 			Expect(28);

@@ -2399,31 +2590,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 26) {

 				Get();

 				IToken openParen = t;  args = new List<Expression/*!*/>();  func = true; 

-				if (StartOf(10)) {

+				if (StartOf(13)) {

 					Expressions(args);

 				}

 				Expect(28);

 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 

 			}

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

-		} else if (la.kind == 62) {

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

 			Get();

 			x = t; 

-			if (StartOf(10)) {

+			if (StartOf(13)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 104) {

+				if (la.kind == 107) {

 					Get();

 					anyDots = true; 

-					if (StartOf(10)) {

+					if (StartOf(13)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

-				} else if (la.kind == 57) {

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

-				} else if (la.kind == 24 || la.kind == 63) {

+				} else if (la.kind == 24 || la.kind == 66) {

 					while (la.kind == 24) {

 						Get();

 						Expression(out ee);

@@ -2434,15 +2625,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(182);

-			} else if (la.kind == 104) {

+				} else SynErr(196);

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

 				Get();

 				anyDots = true; 

-				if (StartOf(10)) {

+				if (StartOf(13)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(183);

+			} else SynErr(197);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -2465,8 +2656,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-			Expect(63);

-		} else SynErr(184);

+			Expect(66);

+		} else SynErr(198);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2477,20 +2668,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 6) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

-			if (StartOf(10)) {

+			if (StartOf(13)) {

 				Expressions(elements);

 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

-		} else if (la.kind == 62) {

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

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

-			if (StartOf(10)) {

+			if (StartOf(13)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(63);

-		} else SynErr(185);

+			Expect(66);

+		} else SynErr(199);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2498,12 +2689,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(44);

+		Expect(48);

 		x = t; 

 		if (la.kind == 6) {

 			Get();

 			elements = new List<Expression/*!*/>(); 

-			if (StartOf(10)) {

+			if (StartOf(13)) {

 				Expressions(elements);

 			}

 			e = new MultiSetDisplayExpr(x, elements);

@@ -2514,9 +2705,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

 			Expect(28);

-		} else if (StartOf(20)) {

+		} else if (StartOf(23)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(186);

+		} else SynErr(200);

 	}

 

 	void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {

@@ -2524,12 +2715,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;

 		e = dummyExpr;

 		

-		Expect(62);

-		if (StartOf(10)) {

+		Expect(65);

+		if (StartOf(13)) {

 			MapLiteralExpressions(out elements);

 		}

 		e = new MapDisplayExpr(mapToken, elements);

-		Expect(63);

+		Expect(66);

 	}

 

 	void MapComprehensionExpr(IToken/*!*/ mapToken, out Expression e) {

@@ -2557,17 +2748,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 97: {

+		case 100: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 98: {

+		case 101: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 99: {

+		case 102: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -2577,12 +2768,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, n); 

 			break;

 		}

-		case 100: {

+		case 103: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 101: {

+		case 104: {

 			Get();

 			x = t; 

 			Expect(26);

@@ -2591,7 +2782,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 102: {

+		case 105: {

 			Get();

 			x = t; 

 			Expect(26);

@@ -2616,7 +2807,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(28);

 			break;

 		}

-		default: SynErr(187); break;

+		default: SynErr(201); break;

 		}

 	}

 

@@ -2635,34 +2826,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ d, r;

 		elements = new List<ExpressionPair/*!*/>(); 

 		Expression(out d);

-		Expect(57);

+		Expect(60);

 		Expression(out r);

 		elements.Add(new ExpressionPair(d,r)); 

 		while (la.kind == 24) {

 			Get();

 			Expression(out d);

-			Expect(57);

+			Expect(60);

 			Expression(out r);

 			elements.Add(new ExpressionPair(d,r)); 

 		}

 	}

 

 	void QSep() {

-		if (la.kind == 109) {

+		if (la.kind == 112) {

 			Get();

-		} else if (la.kind == 110) {

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

 			Get();

-		} else SynErr(188);

+		} else SynErr(202);

 	}

 

 	void MatchExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

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

 		

-		Expect(71);

+		Expect(74);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 67) {

+		while (la.kind == 70) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2677,13 +2868,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression/*!*/ body;

 		

-		if (la.kind == 105 || la.kind == 106) {

+		if (la.kind == 108 || la.kind == 109) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 107 || la.kind == 108) {

+		} else if (la.kind == 110 || la.kind == 111) {

 			Exists();

 			x = t; 

-		} else SynErr(189);

+		} else SynErr(203);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2703,7 +2894,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ range;

 		Expression body = null;

 		

-		Expect(43);

+		Expect(47);

 		x = t; 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

@@ -2714,7 +2905,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		Expect(22);

 		Expression(out range);

-		if (la.kind == 109 || la.kind == 110) {

+		if (la.kind == 112 || la.kind == 113) {

 			QSep();

 			Expression(out body);

 		}

@@ -2740,7 +2931,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			IdentTypeOptional(out d);

 			letVars.Add(d); 

 		}

-		Expect(57);

+		Expect(60);

 		Expression(out e);

 		letRHSs.Add(e); 

 		while (la.kind == 24) {

@@ -2758,7 +2949,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		Expression expr;

 		

-		Expect(54);

+		Expect(57);

 		x = t; 

 		NoUSIdent(out d);

 		Expect(5);

@@ -2773,7 +2964,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(67);

+		Expect(70);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 26) {

@@ -2787,25 +2978,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(28);

 		}

-		Expect(68);

+		Expect(71);

 		Expression(out body);

 		c = new MatchCaseExpr(x, id.val, arguments, body); 

 	}

 

 	void Forall() {

-		if (la.kind == 105) {

+		if (la.kind == 108) {

 			Get();

-		} else if (la.kind == 106) {

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

 			Get();

-		} else SynErr(190);

+		} else SynErr(204);

 	}

 

 	void Exists() {

-		if (la.kind == 107) {

+		if (la.kind == 110) {

 			Get();

-		} else if (la.kind == 108) {

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

 			Get();

-		} else SynErr(191);

+		} else SynErr(205);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2816,7 +3007,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(5);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(21)) {

+		if (StartOf(24)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 24) {

@@ -2841,28 +3032,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, x,x,T,x, x,x,x,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, x,T,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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},

-		{T,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,T,x, x,T,x,T, T,x,x,x, x,T,T,T, 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,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,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,T,x,T, 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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, 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,x,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,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,T,T,T, T,T,T,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,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,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,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, 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,x,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,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,T,T,T, T,T,T,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,T, T,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,T,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, 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,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,x,x, x,x,x,x, x,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,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,T, T,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,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,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,x, x,x,x,x, x,x,x,T, 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,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, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, 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, T,T,x,x, x,T,x,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

-		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,T,x, 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, T,T,x,x, x,T,x,x, x,x,T,T, x,x,T,T, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

-		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}

+		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, x,x,T,x, x,T,x,T, x,x,T,T, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,T, x,x,x,x, T,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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,T,x, x,T,x,x, T,x,T,T, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, 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,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x,T, 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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, 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,x, x,x,x,x, x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x, x,T,T,x, x,T,x,T, x,x,x,x, T,x,x,x, T,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, T,T,T,T, T,T,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, 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,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, T,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},

+		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x, x,T,T,x, x,T,x,T, x,x,x,x, T,x,x,x, T,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, T,T,T,T, T,T,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,T,T,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, x,T,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,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,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,x,x, x,x,x,x, x,x,x,x, 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,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,T,T,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,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,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,x, x,x,x,x, x,x,x,T, 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,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, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, T,x,x,T, T,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,T, T,x,x,x, T,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},

+		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,T,x, T,x,x,T, T,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,T, T,x,x,x, T,x,x,x, x,T,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},

+		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}

 

 	};

 } // end Parser

@@ -2916,169 +3110,183 @@ public class Errors {
 			case 26: s = "\"(\" expected"; break;

 			case 27: s = "\"==\" expected"; break;

 			case 28: s = "\")\" expected"; break;

-			case 29: s = "\"<\" expected"; break;

-			case 30: s = "\">\" expected"; break;

-			case 31: s = "\"method\" expected"; break;

-			case 32: s = "\"constructor\" expected"; break;

-			case 33: s = "\"returns\" expected"; break;

-			case 34: s = "\"...\" expected"; break;

-			case 35: s = "\"modifies\" expected"; break;

-			case 36: s = "\"free\" expected"; break;

-			case 37: s = "\"requires\" expected"; break;

-			case 38: s = "\"ensures\" expected"; break;

-			case 39: s = "\"decreases\" expected"; break;

-			case 40: s = "\"bool\" expected"; break;

-			case 41: s = "\"nat\" expected"; break;

-			case 42: s = "\"int\" expected"; break;

-			case 43: s = "\"set\" expected"; break;

-			case 44: s = "\"multiset\" expected"; break;

-			case 45: s = "\"seq\" expected"; break;

-			case 46: s = "\"map\" expected"; break;

-			case 47: s = "\"object\" expected"; break;

-			case 48: s = "\"function\" expected"; break;

-			case 49: s = "\"predicate\" expected"; break;

-			case 50: s = "\"copredicate\" expected"; break;

-			case 51: s = "\"reads\" expected"; break;

-			case 52: s = "\"*\" expected"; break;

-			case 53: s = "\"`\" expected"; break;

-			case 54: s = "\"label\" expected"; break;

-			case 55: s = "\"break\" expected"; break;

-			case 56: s = "\"where\" expected"; break;

-			case 57: s = "\":=\" expected"; break;

-			case 58: s = "\"return\" expected"; break;

-			case 59: s = "\":|\" expected"; break;

-			case 60: s = "\"assume\" expected"; break;

-			case 61: s = "\"new\" expected"; break;

-			case 62: s = "\"[\" expected"; break;

-			case 63: s = "\"]\" expected"; break;

-			case 64: s = "\"choose\" expected"; break;

-			case 65: s = "\"if\" expected"; break;

-			case 66: s = "\"else\" expected"; break;

-			case 67: s = "\"case\" expected"; break;

-			case 68: s = "\"=>\" expected"; break;

-			case 69: s = "\"while\" expected"; break;

-			case 70: s = "\"invariant\" expected"; break;

-			case 71: s = "\"match\" expected"; break;

-			case 72: s = "\"assert\" expected"; break;

-			case 73: s = "\"print\" expected"; break;

-			case 74: s = "\"parallel\" expected"; break;

-			case 75: s = "\"<==>\" expected"; break;

-			case 76: s = "\"\\u21d4\" expected"; break;

-			case 77: s = "\"==>\" expected"; break;

-			case 78: s = "\"\\u21d2\" expected"; break;

-			case 79: s = "\"&&\" expected"; break;

-			case 80: s = "\"\\u2227\" expected"; break;

-			case 81: s = "\"||\" expected"; break;

-			case 82: s = "\"\\u2228\" expected"; break;

-			case 83: s = "\"<=\" expected"; break;

-			case 84: s = "\">=\" expected"; break;

-			case 85: s = "\"!=\" expected"; break;

-			case 86: s = "\"!!\" expected"; break;

-			case 87: s = "\"in\" expected"; break;

-			case 88: s = "\"!\" expected"; break;

-			case 89: s = "\"\\u2260\" expected"; break;

-			case 90: s = "\"\\u2264\" expected"; break;

-			case 91: s = "\"\\u2265\" expected"; break;

-			case 92: s = "\"+\" expected"; break;

-			case 93: s = "\"-\" expected"; break;

-			case 94: s = "\"/\" expected"; break;

-			case 95: s = "\"%\" expected"; break;

-			case 96: s = "\"\\u00ac\" expected"; break;

-			case 97: s = "\"false\" expected"; break;

-			case 98: s = "\"true\" expected"; break;

-			case 99: s = "\"null\" expected"; break;

-			case 100: s = "\"this\" expected"; break;

-			case 101: s = "\"fresh\" expected"; break;

-			case 102: s = "\"old\" expected"; break;

-			case 103: s = "\"then\" expected"; break;

-			case 104: s = "\"..\" expected"; break;

-			case 105: s = "\"forall\" expected"; break;

-			case 106: s = "\"\\u2200\" expected"; break;

-			case 107: s = "\"exists\" expected"; break;

-			case 108: s = "\"\\u2203\" expected"; break;

-			case 109: s = "\"::\" expected"; break;

-			case 110: s = "\"\\u2022\" expected"; break;

-			case 111: s = "??? expected"; break;

-			case 112: s = "invalid Dafny"; break;

-			case 113: s = "invalid SubModuleDecl"; break;

-			case 114: s = "invalid SubModuleDecl"; break;

-			case 115: s = "invalid SubModuleDecl"; break;

-			case 116: s = "this symbol not expected in ClassDecl"; break;

-			case 117: s = "this symbol not expected in DatatypeDecl"; break;

-			case 118: s = "invalid DatatypeDecl"; break;

-			case 119: s = "this symbol not expected in DatatypeDecl"; break;

-			case 120: s = "this symbol not expected in ArbitraryTypeDecl"; break;

-			case 121: s = "invalid ClassMemberDecl"; break;

-			case 122: s = "this symbol not expected in FieldDecl"; break;

-			case 123: s = "this symbol not expected in FieldDecl"; break;

-			case 124: s = "invalid FunctionDecl"; break;

-			case 125: s = "invalid FunctionDecl"; break;

-			case 126: s = "invalid FunctionDecl"; break;

-			case 127: s = "invalid FunctionDecl"; break;

-			case 128: s = "this symbol not expected in MethodDecl"; break;

-			case 129: s = "invalid MethodDecl"; break;

-			case 130: s = "invalid MethodDecl"; break;

-			case 131: s = "invalid TypeAndToken"; break;

-			case 132: s = "this symbol not expected in MethodSpec"; break;

-			case 133: s = "this symbol not expected in MethodSpec"; break;

-			case 134: s = "this symbol not expected in MethodSpec"; break;

-			case 135: s = "this symbol not expected in MethodSpec"; break;

-			case 136: s = "invalid MethodSpec"; break;

-			case 137: s = "this symbol not expected in MethodSpec"; break;

-			case 138: s = "invalid MethodSpec"; break;

-			case 139: s = "invalid FrameExpression"; break;

-			case 140: s = "invalid ReferenceType"; break;

-			case 141: s = "this symbol not expected in FunctionSpec"; break;

-			case 142: s = "this symbol not expected in FunctionSpec"; break;

-			case 143: s = "this symbol not expected in FunctionSpec"; break;

-			case 144: s = "this symbol not expected in FunctionSpec"; break;

-			case 145: s = "this symbol not expected in FunctionSpec"; break;

-			case 146: s = "invalid FunctionSpec"; break;

-			case 147: s = "invalid PossiblyWildFrameExpression"; break;

-			case 148: s = "invalid PossiblyWildExpression"; break;

-			case 149: s = "this symbol not expected in OneStmt"; break;

-			case 150: s = "invalid OneStmt"; break;

-			case 151: s = "this symbol not expected in OneStmt"; break;

-			case 152: s = "invalid OneStmt"; break;

-			case 153: s = "invalid AssertStmt"; break;

-			case 154: s = "invalid AssumeStmt"; break;

-			case 155: s = "invalid UpdateStmt"; break;

-			case 156: s = "invalid UpdateStmt"; break;

-			case 157: s = "invalid IfStmt"; break;

-			case 158: s = "invalid IfStmt"; break;

-			case 159: s = "invalid WhileStmt"; break;

-			case 160: s = "invalid WhileStmt"; break;

-			case 161: s = "invalid Rhs"; break;

-			case 162: s = "invalid Lhs"; break;

-			case 163: s = "invalid Guard"; break;

-			case 164: s = "this symbol not expected in LoopSpec"; break;

-			case 165: s = "this symbol not expected in LoopSpec"; break;

-			case 166: s = "this symbol not expected in LoopSpec"; break;

-			case 167: s = "this symbol not expected in LoopSpec"; break;

-			case 168: s = "this symbol not expected in LoopSpec"; break;

-			case 169: s = "this symbol not expected in Invariant"; break;

-			case 170: s = "invalid AttributeArg"; break;

-			case 171: s = "invalid EquivOp"; break;

-			case 172: s = "invalid ImpliesOp"; break;

-			case 173: s = "invalid AndOp"; break;

-			case 174: s = "invalid OrOp"; break;

-			case 175: s = "invalid RelOp"; break;

-			case 176: s = "invalid AddOp"; break;

-			case 177: s = "invalid UnaryExpression"; break;

-			case 178: s = "invalid UnaryExpression"; break;

-			case 179: s = "invalid MulOp"; break;

-			case 180: s = "invalid NegOp"; break;

-			case 181: s = "invalid EndlessExpression"; break;

-			case 182: s = "invalid Suffix"; break;

-			case 183: s = "invalid Suffix"; break;

-			case 184: s = "invalid Suffix"; break;

-			case 185: s = "invalid DisplayExpr"; break;

-			case 186: s = "invalid MultiSetExpr"; break;

-			case 187: s = "invalid ConstAtomExpression"; break;

-			case 188: s = "invalid QSep"; break;

-			case 189: s = "invalid QuantifierGuts"; break;

-			case 190: s = "invalid Forall"; break;

-			case 191: s = "invalid Exists"; break;

+			case 29: s = "\"iterator\" expected"; break;

+			case 30: s = "\"yields\" expected"; break;

+			case 31: s = "\"...\" expected"; break;

+			case 32: s = "\"<\" expected"; break;

+			case 33: s = "\">\" expected"; break;

+			case 34: s = "\"method\" expected"; break;

+			case 35: s = "\"constructor\" expected"; break;

+			case 36: s = "\"returns\" expected"; break;

+			case 37: s = "\"modifies\" expected"; break;

+			case 38: s = "\"free\" expected"; break;

+			case 39: s = "\"requires\" expected"; break;

+			case 40: s = "\"ensures\" expected"; break;

+			case 41: s = "\"decreases\" expected"; break;

+			case 42: s = "\"reads\" expected"; break;

+			case 43: s = "\"yield\" expected"; break;

+			case 44: s = "\"bool\" expected"; break;

+			case 45: s = "\"nat\" expected"; break;

+			case 46: s = "\"int\" expected"; break;

+			case 47: s = "\"set\" expected"; break;

+			case 48: s = "\"multiset\" expected"; break;

+			case 49: s = "\"seq\" expected"; break;

+			case 50: s = "\"map\" expected"; break;

+			case 51: s = "\"object\" expected"; break;

+			case 52: s = "\"function\" expected"; break;

+			case 53: s = "\"predicate\" expected"; break;

+			case 54: s = "\"copredicate\" expected"; break;

+			case 55: s = "\"*\" expected"; break;

+			case 56: s = "\"`\" expected"; break;

+			case 57: s = "\"label\" expected"; break;

+			case 58: s = "\"break\" expected"; break;

+			case 59: s = "\"where\" expected"; break;

+			case 60: s = "\":=\" expected"; break;

+			case 61: s = "\"return\" expected"; break;

+			case 62: s = "\":|\" expected"; break;

+			case 63: s = "\"assume\" expected"; break;

+			case 64: s = "\"new\" expected"; break;

+			case 65: s = "\"[\" expected"; break;

+			case 66: s = "\"]\" expected"; break;

+			case 67: s = "\"choose\" expected"; break;

+			case 68: s = "\"if\" expected"; break;

+			case 69: s = "\"else\" expected"; break;

+			case 70: s = "\"case\" expected"; break;

+			case 71: s = "\"=>\" expected"; break;

+			case 72: s = "\"while\" expected"; break;

+			case 73: s = "\"invariant\" expected"; break;

+			case 74: s = "\"match\" expected"; break;

+			case 75: s = "\"assert\" expected"; break;

+			case 76: s = "\"print\" expected"; break;

+			case 77: s = "\"parallel\" expected"; break;

+			case 78: s = "\"<==>\" expected"; break;

+			case 79: s = "\"\\u21d4\" expected"; break;

+			case 80: s = "\"==>\" expected"; break;

+			case 81: s = "\"\\u21d2\" expected"; break;

+			case 82: s = "\"&&\" expected"; break;

+			case 83: s = "\"\\u2227\" expected"; break;

+			case 84: s = "\"||\" expected"; break;

+			case 85: s = "\"\\u2228\" expected"; break;

+			case 86: s = "\"<=\" expected"; break;

+			case 87: s = "\">=\" expected"; break;

+			case 88: s = "\"!=\" expected"; break;

+			case 89: s = "\"!!\" expected"; break;

+			case 90: s = "\"in\" expected"; break;

+			case 91: s = "\"!\" expected"; break;

+			case 92: s = "\"\\u2260\" expected"; break;

+			case 93: s = "\"\\u2264\" expected"; break;

+			case 94: s = "\"\\u2265\" expected"; break;

+			case 95: s = "\"+\" expected"; break;

+			case 96: s = "\"-\" expected"; break;

+			case 97: s = "\"/\" expected"; break;

+			case 98: s = "\"%\" expected"; break;

+			case 99: s = "\"\\u00ac\" expected"; break;

+			case 100: s = "\"false\" expected"; break;

+			case 101: s = "\"true\" expected"; break;

+			case 102: s = "\"null\" expected"; break;

+			case 103: s = "\"this\" expected"; break;

+			case 104: s = "\"fresh\" expected"; break;

+			case 105: s = "\"old\" expected"; break;

+			case 106: s = "\"then\" expected"; break;

+			case 107: s = "\"..\" expected"; break;

+			case 108: s = "\"forall\" expected"; break;

+			case 109: s = "\"\\u2200\" expected"; break;

+			case 110: s = "\"exists\" expected"; break;

+			case 111: s = "\"\\u2203\" expected"; break;

+			case 112: s = "\"::\" expected"; break;

+			case 113: s = "\"\\u2022\" expected"; break;

+			case 114: s = "??? expected"; break;

+			case 115: s = "invalid Dafny"; break;

+			case 116: s = "invalid SubModuleDecl"; break;

+			case 117: s = "invalid SubModuleDecl"; break;

+			case 118: s = "invalid SubModuleDecl"; break;

+			case 119: s = "this symbol not expected in ClassDecl"; break;

+			case 120: s = "this symbol not expected in DatatypeDecl"; break;

+			case 121: s = "invalid DatatypeDecl"; break;

+			case 122: s = "this symbol not expected in DatatypeDecl"; break;

+			case 123: s = "this symbol not expected in ArbitraryTypeDecl"; break;

+			case 124: s = "this symbol not expected in IteratorDecl"; break;

+			case 125: s = "invalid IteratorDecl"; break;

+			case 126: s = "invalid ClassMemberDecl"; break;

+			case 127: s = "this symbol not expected in FieldDecl"; break;

+			case 128: s = "this symbol not expected in FieldDecl"; break;

+			case 129: s = "invalid FunctionDecl"; break;

+			case 130: s = "invalid FunctionDecl"; break;

+			case 131: s = "invalid FunctionDecl"; break;

+			case 132: s = "invalid FunctionDecl"; break;

+			case 133: s = "this symbol not expected in MethodDecl"; break;

+			case 134: s = "invalid MethodDecl"; break;

+			case 135: s = "invalid MethodDecl"; break;

+			case 136: s = "invalid TypeAndToken"; break;

+			case 137: s = "this symbol not expected in IteratorSpec"; break;

+			case 138: s = "this symbol not expected in IteratorSpec"; break;

+			case 139: s = "this symbol not expected in IteratorSpec"; break;

+			case 140: s = "this symbol not expected in IteratorSpec"; break;

+			case 141: s = "this symbol not expected in IteratorSpec"; break;

+			case 142: s = "invalid IteratorSpec"; break;

+			case 143: s = "this symbol not expected in IteratorSpec"; break;

+			case 144: s = "invalid IteratorSpec"; break;

+			case 145: s = "this symbol not expected in MethodSpec"; break;

+			case 146: s = "this symbol not expected in MethodSpec"; break;

+			case 147: s = "this symbol not expected in MethodSpec"; break;

+			case 148: s = "this symbol not expected in MethodSpec"; break;

+			case 149: s = "invalid MethodSpec"; break;

+			case 150: s = "this symbol not expected in MethodSpec"; break;

+			case 151: s = "invalid MethodSpec"; break;

+			case 152: s = "invalid FrameExpression"; break;

+			case 153: s = "invalid ReferenceType"; break;

+			case 154: s = "this symbol not expected in FunctionSpec"; break;

+			case 155: s = "this symbol not expected in FunctionSpec"; break;

+			case 156: s = "this symbol not expected in FunctionSpec"; break;

+			case 157: s = "this symbol not expected in FunctionSpec"; break;

+			case 158: s = "this symbol not expected in FunctionSpec"; break;

+			case 159: s = "invalid FunctionSpec"; break;

+			case 160: s = "invalid PossiblyWildFrameExpression"; break;

+			case 161: s = "invalid PossiblyWildExpression"; break;

+			case 162: s = "this symbol not expected in OneStmt"; break;

+			case 163: s = "invalid OneStmt"; break;

+			case 164: s = "this symbol not expected in OneStmt"; break;

+			case 165: s = "invalid OneStmt"; break;

+			case 166: s = "invalid AssertStmt"; break;

+			case 167: s = "invalid AssumeStmt"; break;

+			case 168: s = "invalid UpdateStmt"; break;

+			case 169: s = "invalid UpdateStmt"; break;

+			case 170: s = "invalid IfStmt"; break;

+			case 171: s = "invalid IfStmt"; break;

+			case 172: s = "invalid WhileStmt"; break;

+			case 173: s = "invalid WhileStmt"; break;

+			case 174: s = "invalid ReturnStmt"; break;

+			case 175: s = "invalid Rhs"; break;

+			case 176: s = "invalid Lhs"; break;

+			case 177: s = "invalid Guard"; break;

+			case 178: s = "this symbol not expected in LoopSpec"; break;

+			case 179: s = "this symbol not expected in LoopSpec"; break;

+			case 180: s = "this symbol not expected in LoopSpec"; break;

+			case 181: s = "this symbol not expected in LoopSpec"; break;

+			case 182: s = "this symbol not expected in LoopSpec"; break;

+			case 183: s = "this symbol not expected in Invariant"; break;

+			case 184: s = "invalid AttributeArg"; break;

+			case 185: s = "invalid EquivOp"; break;

+			case 186: s = "invalid ImpliesOp"; break;

+			case 187: s = "invalid AndOp"; break;

+			case 188: s = "invalid OrOp"; break;

+			case 189: s = "invalid RelOp"; break;

+			case 190: s = "invalid AddOp"; break;

+			case 191: s = "invalid UnaryExpression"; break;

+			case 192: s = "invalid UnaryExpression"; break;

+			case 193: s = "invalid MulOp"; break;

+			case 194: s = "invalid NegOp"; break;

+			case 195: s = "invalid EndlessExpression"; break;

+			case 196: s = "invalid Suffix"; break;

+			case 197: s = "invalid Suffix"; break;

+			case 198: s = "invalid Suffix"; break;

+			case 199: s = "invalid DisplayExpr"; break;

+			case 200: s = "invalid MultiSetExpr"; break;

+			case 201: s = "invalid ConstAtomExpression"; break;

+			case 202: s = "invalid QSep"; break;

+			case 203: s = "invalid QuantifierGuts"; break;

+			case 204: s = "invalid Forall"; break;

+			case 205: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 24941ce1..5c5c95b5 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -36,10 +36,10 @@ namespace Microsoft.Dafny {
       PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0);

     }

 

-    public void PrintTopLevelDecls(List<TopLevelDecl> classes, int indent) {

-      Contract.Requires(classes!= null);

+    public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent) {

+      Contract.Requires(decls!= null);

       int i = 0;

-      foreach (TopLevelDecl d in classes) {

+      foreach (TopLevelDecl d in decls) {

         Contract.Assert(d != null);

         if (d is ArbitraryTypeDecl) {

           var at = (ArbitraryTypeDecl)d;

@@ -62,8 +62,63 @@ namespace Microsoft.Dafny {
             // print nothing

           } else {

             if (i++ != 0) { wr.WriteLine(); }

-            PrintClass_Members(cl, indent);

+            PrintMembers(cl.Members, indent);

           }

+        } else if (d is IteratorDecl) {

+          var iter = (IteratorDecl)d;

+          Indent(indent);

+          PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs);

+          if (iter.SignatureIsOmitted) {

+            wr.WriteLine(" ...");

+          } else {

+            PrintFormals(iter.Ins);

+            if (iter.Outs.Count != 0) {

+              if (iter.Ins.Count + iter.Outs.Count <= 3) {

+                wr.Write(" yields ");

+              } else {

+                wr.WriteLine();

+                Indent(indent + 2 * IndentAmount);

+                wr.Write("yields ");

+              }

+              PrintFormals(iter.Outs);

+            }

+            wr.WriteLine();

+          }

+

+          int ind = indent + IndentAmount;

+          PrintSpec("requires", iter.Requires, ind);

+          if (iter.Reads.Expressions != null) {

+            PrintFrameSpecLine("reads", iter.Reads.Expressions, ind, iter.Reads.HasAttributes() ? iter.Reads.Attributes : null);

+          }

+          if (iter.Modifies.Expressions != null) {

+            PrintFrameSpecLine("modifies", iter.Modifies.Expressions, ind, iter.Modifies.HasAttributes() ? iter.Modifies.Attributes : null);

+          }

+          PrintSpec("yield requires", iter.YieldRequires, ind);

+          PrintSpec("yield ensures", iter.YieldEnsures, ind);

+          PrintSpec("ensures", iter.Ensures, ind);

+          PrintDecreasesSpec(iter.Decreases, ind);

+

+          if (iter.Body != null) {

+            Indent(indent);

+            PrintStatement(iter.Body, indent);

+            wr.WriteLine();

+          }

+

+          if (DafnyOptions.O.DafnyPrintResolvedFile != null) {

+            // also print the members that were created as part of the interpretation of the iterator

+            Contract.Assert(iter.ImplicitlyDefinedMembers != null);  // filled in during resolution

+            var members = new List<MemberDecl>();

+            foreach (var m in iter.ImplicitlyDefinedMembers.Values) {

+              members.Add(m);

+            }

+            wr.WriteLine("/*---------- iterator members ----------");

+            PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);

+            wr.WriteLine(" {");

+            PrintMembers(members, indent + IndentAmount);

+            Indent(indent); wr.WriteLine("}");

+            wr.WriteLine("---------- iterator members ----------*/");

+          }

+

         } else if (d is ModuleDecl) {

           wr.WriteLine();

           Indent(indent);

@@ -92,6 +147,8 @@ namespace Microsoft.Dafny {
             wr.Write(" {0} ", ((AbstractModuleDecl)d).Name);

             wr.WriteLine("as {0};", Util.Comma(".", ((AbstractModuleDecl)d).Path, id => id.val));

           }

+        } else {

+          Contract.Assert(false);  // unexpected TopLevelDecl

         }

       }

     }

@@ -104,19 +161,18 @@ namespace Microsoft.Dafny {
         wr.WriteLine(" { }");

       } else {

         wr.WriteLine(" {");

-        PrintClass_Members(c, indent + IndentAmount);

+        PrintMembers(c.Members, indent + IndentAmount);

         Indent(indent);

         wr.WriteLine("}");

       }

     }

 

-    public void PrintClass_Members(ClassDecl c, int indent)

+    public void PrintMembers(List<MemberDecl> members, int indent)

     {

-      Contract.Requires(c != null);

-      Contract.Requires( c.Members.Count != 0);

+      Contract.Requires(members != null);

 

       int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field

-      foreach (MemberDecl m in c.Members) {

+      foreach (MemberDecl m in members) {

         if (m is Method) {

           if (state != 0) { wr.WriteLine(); }

           PrintMethod((Method)m, indent);

@@ -286,7 +342,7 @@ namespace Microsoft.Dafny {
             wr.Write(" returns ");

           } else {

             wr.WriteLine();

-            Indent(3 * IndentAmount);

+            Indent(indent + 2 * IndentAmount);

             wr.Write("returns ");

           }

           PrintFormals(method.Outs);

@@ -458,9 +514,9 @@ namespace Microsoft.Dafny {
           wr.Write(";");

         }

 

-      } else if (stmt is ReturnStmt) {

-        var s = (ReturnStmt) stmt;

-        wr.Write("return");

+      } else if (stmt is ProduceStmt) {

+        var s = (ProduceStmt) stmt;

+        wr.Write(s is YieldStmt ? "yield" : "return");

         if (s.rhss != null) {

           var sep = " ";

           foreach (var rhs in s.rhss) {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index f8f00904..f2a386f4 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -128,37 +128,46 @@ namespace Microsoft.Dafny
               } else if (dDemandsEqualitySupport) {

                 if (nw is ClassDecl) {

                   // fine, as long as "nw" does not take any type parameters

-                  if (nw.TypeArgs.Count != 0) {

-                    reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);

+                  if (nw.TypeArgs.Count != d.TypeArgs.Count) {

+                    reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters", nw.Name);

                   }

+                } else if (nw is IteratorDecl) {

+                  reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by an iterator");

                 } else if (nw is CoDatatypeDecl) {

                   reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

                 } else {

                   Contract.Assert(nw is IndDatatypeDecl);

-                  if (nw.TypeArgs.Count != 0) {

-                    reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);

+                  if (nw.TypeArgs.Count != d.TypeArgs.Count) {

+                    reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes a different number of type parameters", nw.Name);

                   } else {

                     // Here, we need to figure out if the new type supports equality.  But we won't know about that until resolution has

                     // taken place, so we defer it until the PostResolve phase.

                     var udt = new UserDefinedType(nw.tok, nw.Name, nw, new List<Type>());

-                    postTasks.Enqueue(delegate()

-                    {

+                    postTasks.Enqueue(delegate() {

                       if (!udt.SupportsEquality) {

                         reporter.Error(udt.tok, "datatype '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", udt.Name);

                       }

                     });

                   }

                 }

+              } else if (d.TypeArgs.Count != nw.TypeArgs.Count) {

+                reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters", nw.Name);

               }

             }

           } else if (nw is ArbitraryTypeDecl) {

             reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);

           } else if (nw is DatatypeDecl) {

             reporter.Error(nw, "a datatype declaration ({0}) in a refinement module can only replace an arbitrary-type declaration", nw.Name);

+          } else if (nw is IteratorDecl) {

+            if (d is IteratorDecl) {

+              m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d);

+            } else {

+              reporter.Error(nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);

+            }

           } else {

             Contract.Assert(nw is ClassDecl);

             if (d is DatatypeDecl) {

-              reporter.Error(nw, "a class declaration ({0}) in a refining module cannot replace a datatype declaration in the refinement base", nw.Name);

+              reporter.Error(nw, "a class declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);

             } else {

               m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d);

             }

@@ -533,6 +542,66 @@ namespace Microsoft.Dafny
 

     // -------------------------------------------------- Merging ---------------------------------------------------------------

 

+    IteratorDecl MergeIterator(IteratorDecl nw, IteratorDecl prev) {

+      Contract.Requires(nw != null);

+      Contract.Requires(prev != null);

+

+      if (nw.Requires.Count != 0) {

+        reporter.Error(nw.Requires[0].E.tok, "a refining iterator is not allowed to add preconditions");

+      }

+      if (nw.YieldRequires.Count != 0) {

+        reporter.Error(nw.YieldRequires[0].E.tok, "a refining iterator is not allowed to add yield preconditions");

+      }

+      if (nw.Reads.Expressions.Count != 0) {

+        reporter.Error(nw.Reads.Expressions[0].E.tok, "a refining iterator is not allowed to extend the reads clause");

+      }

+      if (nw.Modifies.Expressions.Count != 0) {

+        reporter.Error(nw.Modifies.Expressions[0].E.tok, "a refining iterator is not allowed to extend the modifies clause");

+      }

+      if (nw.Decreases.Expressions.Count != 0) {

+        reporter.Error(nw.Decreases.Expressions[0].tok, "a refining iterator is not allowed to extend the decreases clause");

+      }

+

+      if (nw.SignatureIsOmitted) {

+        Contract.Assert(nw.TypeArgs.Count == 0);

+        Contract.Assert(nw.Ins.Count == 0);

+        Contract.Assert(nw.Outs.Count == 0);

+      } else {

+        CheckAgreement_TypeParameters(nw.tok, prev.TypeArgs, nw.TypeArgs, nw.Name, "iterator");

+        CheckAgreement_Parameters(nw.tok, prev.Ins, nw.Ins, nw.Name, "iterator", "in-parameter");

+        CheckAgreement_Parameters(nw.tok, prev.Outs, nw.Outs, nw.Name, "iterator", "yield-parameter");

+      }

+

+      BlockStmt newBody;

+      if (nw.Body == null) {

+        newBody = prev.Body;

+      } else if (prev.Body == null) {

+        newBody = nw.Body;

+      } else {

+        newBody = MergeBlockStmt(nw.Body, prev.Body);

+      }

+

+      var ens = prev.Ensures.ConvertAll(rawCloner.CloneMayBeFreeExpr);

+      ens.AddRange(nw.Ensures);

+      var yens = prev.YieldEnsures.ConvertAll(rawCloner.CloneMayBeFreeExpr);

+      yens.AddRange(nw.YieldEnsures);

+

+      return new IteratorDecl(new RefinementToken(nw.tok, moduleUnderConstruction), nw.Name, moduleUnderConstruction,

+        nw.SignatureIsOmitted ? prev.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam) : nw.TypeArgs,

+        nw.SignatureIsOmitted ? prev.Ins.ConvertAll(refinementCloner.CloneFormal) : nw.Ins,

+        nw.SignatureIsOmitted ? prev.Outs.ConvertAll(refinementCloner.CloneFormal) : nw.Outs,

+        refinementCloner.CloneSpecFrameExpr(prev.Reads),

+        refinementCloner.CloneSpecFrameExpr(prev.Modifies),

+        refinementCloner.CloneSpecExpr(prev.Decreases),

+        prev.Requires.ConvertAll(refinementCloner.CloneMayBeFreeExpr),

+        ens,

+        prev.YieldRequires.ConvertAll(refinementCloner.CloneMayBeFreeExpr),

+        yens,

+        newBody,

+        refinementCloner.MergeAttributes(prev.Attributes, nw.Attributes),

+        false);

+    }

+

     ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {

       CheckAgreement_TypeParameters(nw.tok, prev.TypeArgs, nw.TypeArgs, nw.Name, "class");

 

@@ -1209,8 +1278,8 @@ namespace Microsoft.Dafny
       }

       if (s is SkeletonStatement) {

         reporter.Error(s, "skeleton statement may not be used here; it does not have a matching statement in what is being replaced");

-      } else if (s is ReturnStmt) {

-        reporter.Error(s, "return statements are not allowed in skeletons");

+      } else if (s is ProduceStmt) {

+        reporter.Error(s, (s is YieldStmt ? "yield" : "return") + " statements are not allowed in skeletons");

       } else if (s is BreakStmt) {

         var b = (BreakStmt)s;

         if (b.TargetLabel != null ? !labels.Contains(b.TargetLabel) : loopLevels < b.BreakCount) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 53449979..7b11a932 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -522,14 +522,95 @@ namespace Microsoft.Dafny
               }

             }

           }

+

+        } else if (d is IteratorDecl) {

+          var iter = (IteratorDecl)d;

+

+          // register the names of the implicit members

+          var members = new Dictionary<string, MemberDecl>();

+          iter.ImplicitlyDefinedMembers = members;

+

+          // First, register the iterator's in- and out-parameters as readonly fields

+          foreach (var p in iter.Ins) {

+            if (members.ContainsKey(p.Name)) {

+              Error(p, "Name of in-parameter is used by another member of the iterator: {0}", p.Name);

+            } else {

+              var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);

+              field.EnclosingClass = iter;  // resolve here

+              members.Add(p.Name, field);

+            }

+          }

+          foreach (var p in iter.Outs) {

+            if (members.ContainsKey(p.Name)) {

+              Error(p, "Name of yield-parameter is used by another member of the iterator: {0}", p.Name);

+            } else {

+              var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);

+              field.EnclosingClass = iter;  // resolve here

+              members.Add(p.Name, field);

+            }

+          }

+          var yieldHistoryVariables = new List<MemberDecl>();

+          foreach (var p in iter.OutsHistory) {

+            if (members.ContainsKey(p.Name)) {

+              Error(p.tok, "Name of implicit yield-history variable '{0}' is already used by another member of the iterator", p.Name);

+            } else {

+              var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);

+              field.EnclosingClass = iter;  // resolve here

+              yieldHistoryVariables.Add(field);  // just record this field for now (until all parameters have been added as members)

+            }

+          }

+          yieldHistoryVariables.ForEach(f => members.Add(f.Name, f));  // now that already-used 'xs' names have been checked for, add these yield-history variables

+

+          var iterTypeArgs = new List<Type>();

+          iter.TypeArgs.ForEach(tp => iterTypeArgs.Add(new UserDefinedType(tp.tok, tp.Name, tp)));

+          var iterType = new UserDefinedType(iter.tok, iter.Name, iter, iterTypeArgs);

+          // Note, the typeArgs parameter to the following Method/Predicate constructors is passed in as the empty list.  What that is

+          // saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the

+          // iterator type) does.

+          // Also add "Valid" and "MoveNext"

+          var init = new Method(iter.tok, iter.Name, true, false, new List<TypeParameter>(),

+            iter.Ins, new List<Formal>() { new Formal(iter.tok, "iter", iterType, false, false) },

+            /* TODO: Fill in the spec here */

+            new List<MaybeFreeExpression>(), new Specification<FrameExpression>(null, null), new List<MaybeFreeExpression>(), new Specification<Expression>(null, null),

+            null, null, false);

+          var valid = new Predicate(iter.tok, "Valid", false, true, new List<TypeParameter>(), iter.tok,

+            new List<Formal>(), new List<Expression>(), new List<FrameExpression>()/*TODO: does this need to be filled?*/, new List<Expression>(), new Specification<Expression>(null, null),

+            null/*TODO: does this need to be fileld?*/, Predicate.BodyOriginKind.OriginalOrInherited, null, false);

+          var moveNext = new Method(iter.tok, "MoveNext", false, false, new List<TypeParameter>(),

+            new List<Formal>(), new List<Formal>() { new Formal(iter.tok, "more", Type.Bool, false, false) },

+            /* TODO: Do the first 3 of the specification components on the next line need to be filled in? */

+            new List<MaybeFreeExpression>(), new Specification<FrameExpression>(null, null), new List<MaybeFreeExpression>(), new Specification<Expression>(null, null),

+            null, null, false);

+          init.EnclosingClass = iter;

+          valid.EnclosingClass = iter;

+          moveNext.EnclosingClass = iter;

+          MemberDecl member;

+          if (members.TryGetValue(init.Name, out member)) {

+            Error(member.tok, "member name '{0}' is already predefined for this iterator", init.Name);

+          } else {

+            members.Add(init.Name, init);

+          }

+          // If the name of the iterator is "Valid" or "MoveNext", one of the following will produce an error message.  That

+          // error message may not be as clear as it could be, but the situation also seems unlikely to ever occur in practice.

+          if (members.TryGetValue("Valid", out member)) {

+            Error(member.tok, "member name 'Valid' is already predefined for iterators");

+          } else {

+            members.Add(valid.Name, valid);

+          }

+          if (members.TryGetValue("MoveNext", out member)) {

+            Error(member.tok, "member name 'MoveNext' is already predefined for iterators");

+          } else {

+            members.Add(moveNext.Name, moveNext);

+          }

+

         } else {

           DatatypeDecl dt = (DatatypeDecl)d;

 

           // register the names of the constructors

-          Dictionary<string, DatatypeCtor> ctors = new Dictionary<string, DatatypeCtor>();

+          var ctors = new Dictionary<string, DatatypeCtor>();

           datatypeCtors.Add(dt, ctors);

           // ... and of the other members

-          Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();

+          var members = new Dictionary<string, MemberDecl>();

           datatypeMembers.Add(dt, members);

 

           foreach (DatatypeCtor ctor in dt.Ctors) {

@@ -921,9 +1002,11 @@ namespace Microsoft.Dafny
       foreach (TopLevelDecl d in declarations) {

         Contract.Assert(d != null);

         allTypeParameters.PushMarker();

-        ResolveTypeParameters(d.TypeArgs, true, d, true);

+        ResolveTypeParameters(d.TypeArgs, true, d);

         if (d is ArbitraryTypeDecl) {

           // nothing to do

+        } else if (d is IteratorDecl) {

+          ResolveIteratorSignature((IteratorDecl)d);

         } else if (d is ClassDecl) {

           ResolveClassMemberTypes((ClassDecl)d);

         } else if (d is ModuleDecl) {

@@ -957,8 +1040,15 @@ namespace Microsoft.Dafny
       foreach (TopLevelDecl d in declarations) {

         Contract.Assert(d != null);

         allTypeParameters.PushMarker();

-        ResolveTypeParameters(d.TypeArgs, false, d, true);

-        if (d is ClassDecl) {

+        ResolveTypeParameters(d.TypeArgs, false, d);

+        if (d is IteratorDecl) {

+          var iter = (IteratorDecl)d;

+          allTypeParameters.PushMarker();

+          ResolveTypeParameters(iter.TypeArgs, false, iter);

+          ResolveIterator(iter);

+          allTypeParameters.PopMarker();

+

+        } else if (d is ClassDecl) {

           ResolveClassMemberBodies((ClassDecl)d);

         }

         allTypeParameters.PopMarker();

@@ -1067,7 +1157,27 @@ namespace Microsoft.Dafny
         } while (inferredSomething);

         // Now do it for Function and Method signatures

         foreach (var d in declarations) {

-          if (d is ClassDecl) {

+          if (d is IteratorDecl) {

+            var iter = (IteratorDecl)d;

+            foreach (var tp in iter.TypeArgs) {

+              if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {

+                // here's our chance to infer the need for equality support

+                foreach (var p in iter.Ins) {

+                  if (InferRequiredEqualitySupport(tp, p.Type)) {

+                    tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                    goto DONE;

+                  }

+                }

+                foreach (var p in iter.Outs) {

+                  if (InferRequiredEqualitySupport(tp, p.Type)) {

+                    tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                    goto DONE;

+                  }

+                }

+              DONE: ;

+              }

+            }

+          } else  if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             foreach (var member in cl.Members) {

               if (!member.IsGhost) {

@@ -1116,7 +1226,22 @@ namespace Microsoft.Dafny
         // Check that all == and != operators in non-ghost contexts are applied to equality-supporting types.

         // Note that this check can only be done after determining which expressions are ghosts.

         foreach (var d in declarations) {

-          if (d is ClassDecl) {

+          if (d is IteratorDecl) {

+            var iter = (IteratorDecl)d;

+            foreach (var p in iter.Ins) {

+              if (!p.IsGhost) {

+                CheckEqualityTypes_Type(p.tok, p.Type);

+              }

+            }

+            foreach (var p in iter.Outs) {

+              if (!p.IsGhost) {

+                CheckEqualityTypes_Type(p.tok, p.Type);

+              }

+            }

+            if (iter.Body != null) {

+              CheckEqualityTypes_Stmt(iter.Body);

+            }

+          } else  if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             foreach (var member in cl.Members) {

               if (!member.IsGhost) {

@@ -1430,8 +1555,8 @@ namespace Microsoft.Dafny
           }

         }

       } else if (stmt is BreakStmt) {

-      } else if (stmt is ReturnStmt) {

-        var s = (ReturnStmt)stmt;

+      } else if (stmt is ProduceStmt) {

+        var s = (ProduceStmt)stmt;

         if (s.rhss != null) {

           s.rhss.Iter(CheckEqualityTypes_Rhs);

         }

@@ -1654,8 +1779,8 @@ namespace Microsoft.Dafny
         var s = (PrintStmt)stmt;

         s.Args.Iter(arg => CheckTypeInference(arg.E));

       } else if (stmt is BreakStmt) {

-      } else if (stmt is ReturnStmt) {

-        var s = (ReturnStmt)stmt;

+      } else if (stmt is ProduceStmt) {

+        var s = (ProduceStmt)stmt;

         if (s.rhss != null) {

           s.rhss.Iter(rhs => rhs.SubExpressions.Iter(e => CheckTypeInference(e)));

         }

@@ -1794,14 +1919,14 @@ namespace Microsoft.Dafny
         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

-          ResolveTypeParameters(f.TypeArgs, true, f, false);

+          ResolveTypeParameters(f.TypeArgs, true, f);

           ResolveFunctionSignature(f);

           allTypeParameters.PopMarker();

 

         } else if (member is Method) {

           Method m = (Method)member;

           allTypeParameters.PushMarker();

-          ResolveTypeParameters(m.TypeArgs, true, m, false);

+          ResolveTypeParameters(m.TypeArgs, true, m);

           ResolveMethodSignature(m);

           allTypeParameters.PopMarker();

 

@@ -1830,14 +1955,14 @@ namespace Microsoft.Dafny
         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

-          ResolveTypeParameters(f.TypeArgs, false, f, false);

+          ResolveTypeParameters(f.TypeArgs, false, f);

           ResolveFunction(f);

           allTypeParameters.PopMarker();

 

         } else if (member is Method) {

           Method m = (Method)member;

           allTypeParameters.PushMarker();

-          ResolveTypeParameters(m.TypeArgs, false, m, false);

+          ResolveTypeParameters(m.TypeArgs, false, m);

           ResolveMethod(m);

           allTypeParameters.PopMarker();

         } else {

@@ -2106,8 +2231,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent, bool isToplevel) {

-

+    void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {

       Contract.Requires(tparams != null);

       Contract.Requires(parent != null);

       // push non-duplicated type parameter names

@@ -2332,6 +2456,113 @@ namespace Microsoft.Dafny
     }

 

     /// <summary>

+    /// Assumes type parameters have already been pushed

+    /// </summary>

+    void ResolveIteratorSignature(IteratorDecl iter) {

+      Contract.Requires(iter != null);

+      scope.PushMarker();

+      if (iter.SignatureIsOmitted) {

+        Error(iter, "iterator signature can be omitted only in refining methods");

+      }

+      var defaultTypeArguments = iter.TypeArgs.Count == 0 ? iter.TypeArgs : null;

+      // resolve in-parameters

+      foreach (Formal p in iter.Ins) {

+        if (!scope.Push(p.Name, p)) {

+          Error(p, "Duplicate parameter name: {0}", p.Name);

+        }

+        ResolveType(p.tok, p.Type, defaultTypeArguments, true);

+      }

+      // resolve yield-parameters

+      foreach (Formal p in iter.Outs) {

+        if (!scope.Push(p.Name, p)) {

+          Error(p, "Duplicate parameter name: {0}", p.Name);

+        }

+        ResolveType(p.tok, p.Type, defaultTypeArguments, true);

+      }

+      // resolve yield-history variables

+      foreach (Formal p in iter.OutsHistory) {

+        if (!scope.Push(p.Name, p)) {

+          Error(p, "Name conflict with yield-history variable: {0}", p.Name);

+        }

+        ResolveType(p.tok, p.Type, defaultTypeArguments, true);

+      }

+      scope.PopMarker();

+    }

+

+    /// <summary>

+    /// Assumes type parameters have already been pushed

+    /// </summary>

+    void ResolveIterator(IteratorDecl iter) {

+      Contract.Requires(iter != null);

+

+      // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported

+      scope.PushMarker();

+      scope.AllowInstance = false;  // disallow 'this' from use, which means that the special fields and methods added are not accessible in the syntactically given spec

+      iter.Ins.ForEach(p => scope.Push(p.Name, p));

+

+      // Start resolving specification...

+      foreach (FrameExpression fe in iter.Reads.Expressions) {

+        ResolveFrameExpression(fe, "reads");

+      }

+      foreach (FrameExpression fe in iter.Modifies.Expressions) {

+        ResolveFrameExpression(fe, "modifies");

+      }

+      foreach (Expression e in iter.Decreases.Expressions) {

+        ResolveExpression(e, false);

+        // any type is fine

+      }

+

+      foreach (MaybeFreeExpression e in iter.Requires) {

+        ResolveExpression(e.E, false);

+        Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.E.Type, Type.Bool)) {

+          Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

+        }

+      }

+

+      // In the postcondition, the yield-history variables are also in scope

+      iter.OutsHistory.ForEach(p => scope.Push(p.Name, p));

+

+      foreach (MaybeFreeExpression e in iter.Ensures) {

+        ResolveExpression(e.E, true);

+        Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.E.Type, Type.Bool)) {

+          Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

+        }

+      }

+

+      // For the attributes, yield precondition, yield postcondition, and body, the yield-parameters are also available

+      scope.PushMarker();  // make the yield-parameters appear in the same scope as the outer-most locals of the body (since this is what is done for methods)

+      iter.Outs.ForEach(p => scope.Push(p.Name, p));

+

+      ResolveAttributes(iter.Attributes, false);

+

+      foreach (MaybeFreeExpression e in iter.YieldRequires) {

+        ResolveExpression(e.E, false);

+        Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.E.Type, Type.Bool)) {

+          Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);

+        }

+      }

+

+      foreach (MaybeFreeExpression e in iter.YieldEnsures) {

+        ResolveExpression(e.E, true);

+        Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.E.Type, Type.Bool)) {

+          Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);

+        }

+      }

+

+      // Resolve body

+      if (iter.Body != null) {

+        ResolveBlockStatement(iter.Body, false, iter);

+      }

+

+      scope.PopMarker();  // for the yield-parameters and outermost-level locals

+      scope.PopMarker();  // for the in-parameters and yield-history variables

+    }

+

+    /// <summary>

     /// If ResolveType encounters a type "T" that takes type arguments but wasn't given any, then:

     /// * If "defaultTypeArguments" is non-null and "defaultTypeArgument.Count" equals the number

     ///   of type arguments that "T" expects, then use these default type arguments as "T"'s arguments.

@@ -2726,9 +2957,9 @@ namespace Microsoft.Dafny
     /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it

     /// at run time.  That means it must not have any side effects on non-ghost variables, for example.

     /// </summary>

-    public void ResolveStatement(Statement stmt, bool specContextOnly, Method method) {

+    public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) {

       Contract.Requires(stmt != null);

-      Contract.Requires(method != null);

+      Contract.Requires(codeContext != null);

       if (stmt is PredicateStmt) {

         PredicateStmt s = (PredicateStmt)stmt;

         ResolveAttributes(s.Attributes, false);

@@ -2775,22 +3006,25 @@ namespace Microsoft.Dafny
           }

         }

 

-      } else if (stmt is ReturnStmt) {

-        if (specContextOnly && !method.IsGhost) {

-          // TODO: investigate. This error message is suspicious. It seems that a return statement is only

-          // disallowed from a ghost if or while in a non-ghost method, which is not what this says.

-          Error(stmt, "return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

+      } else if (stmt is ProduceStmt) {

+        var kind = stmt is YieldStmt ? "yield" : "return";

+        if (stmt is YieldStmt && !(codeContext is IteratorDecl)) {

+          Error(stmt, "yield statement is allowed only in iterators");

+        } else if (stmt is ReturnStmt && !(codeContext is Method)) {

+          Error(stmt, "return statement is allowed only in method");

+        } else if (specContextOnly && !codeContext.IsGhost) {

+          Error(stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind);

         }

-        ReturnStmt s = (ReturnStmt)stmt;

+        var s = (ProduceStmt)stmt;

         if (s.rhss != null) {

-          if (method.Outs.Count != s.rhss.Count)

-            Error(s, "number of return parameters does not match declaration (found {0}, expected {1})", s.rhss.Count, method.Outs.Count);

+          if (codeContext.Outs.Count != s.rhss.Count)

+            Error(s, "number of {2} parameters does not match declaration (found {0}, expected {1})", s.rhss.Count, codeContext.Outs.Count, kind);

           else {

             Contract.Assert(s.rhss.Count > 0);

             // Create a hidden update statement using the out-parameter formals, resolve the RHS, and check that the RHS is good.

             List<Expression> formals = new List<Expression>();

             int i = 0;

-            foreach (Formal f in method.Outs) {

+            foreach (Formal f in codeContext.Outs) {

               IdentifierExpr ident = new IdentifierExpr(f.tok, f.Name);

               ident.Var = f;

               ident.Type = ident.Var.Type;

@@ -2806,22 +3040,22 @@ namespace Microsoft.Dafny
               i++;

             }

             s.hiddenUpdate = new UpdateStmt(s.Tok, formals, s.rhss, true);

-            // resolving the update statement will check for return statement specifics.

-            ResolveStatement(s.hiddenUpdate, specContextOnly, method);

+            // resolving the update statement will check for return/yield statement specifics.

+            ResolveStatement(s.hiddenUpdate, specContextOnly, codeContext);

           }

-        } else {// this is a regular return statement.

+        } else {// this is a regular return/yield statement.

           s.hiddenUpdate = null;

         }

       } else if (stmt is ConcreteUpdateStatement) {

-        ResolveUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, method);

+        ResolveUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

         foreach (var vd in s.Lhss) {

-          ResolveStatement(vd, specContextOnly, method);

+          ResolveStatement(vd, specContextOnly, codeContext);

           s.ResolvedStatements.Add(vd);

         }

         if (s.Update != null) {

-          ResolveStatement(s.Update, specContextOnly, method);

+          ResolveStatement(s.Update, specContextOnly, codeContext);

           s.ResolvedStatements.Add(s.Update);

         }

 

@@ -2843,7 +3077,7 @@ namespace Microsoft.Dafny
           if (var == null) {

             // the LHS didn't resolve correctly; some error would already have been reported

           } else {

-            lvalueIsGhost = var.IsGhost || method.IsGhost;

+            lvalueIsGhost = var.IsGhost || codeContext.IsGhost;

             if (!var.IsMutable) {

               Error(stmt, "LHS of assignment must denote a mutable variable or field");

             }

@@ -2913,7 +3147,7 @@ namespace Microsoft.Dafny
             }

           } else if (s.Rhs is TypeRhs) {

             TypeRhs rr = (TypeRhs)s.Rhs;

-            Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, method);

+            Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, codeContext);

             if (!lvalueIsGhost) {

               if (rr.ArrayDimensions != null) {

                 foreach (var dim in rr.ArrayDimensions) {

@@ -2952,11 +3186,11 @@ namespace Microsoft.Dafny
 

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

-        ResolveCallStmt(s, specContextOnly, method, null);

+        ResolveCallStmt(s, specContextOnly, codeContext, null);

 

       } else if (stmt is BlockStmt) {

         scope.PushMarker();

-        ResolveBlockStatement((BlockStmt)stmt, specContextOnly, method);

+        ResolveBlockStatement((BlockStmt)stmt, specContextOnly, codeContext);

         scope.PopMarker();

 

       } else if (stmt is IfStmt) {

@@ -2975,14 +3209,14 @@ namespace Microsoft.Dafny
           }

         }

         s.IsGhost = branchesAreSpecOnly;

-        ResolveStatement(s.Thn, branchesAreSpecOnly, method);

+        ResolveStatement(s.Thn, branchesAreSpecOnly, codeContext);

         if (s.Els != null) {

-          ResolveStatement(s.Els, branchesAreSpecOnly, method);

+          ResolveStatement(s.Els, branchesAreSpecOnly, codeContext);

         }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

-        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, method);

+        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, codeContext);

 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

@@ -3027,12 +3261,12 @@ namespace Microsoft.Dafny
           inSpecOnlyContext.Add(s, specContextOnly);

         }

 

-        ResolveStatement(s.Body, bodyMustBeSpecOnly, method);

+        ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);

         loopStack.RemoveAt(loopStack.Count - 1);  // pop

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

-        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, method);

+        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext);

         foreach (MaybeFreeExpression inv in s.Invariants) {

           ResolveExpression(inv.E, true);

           Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression

@@ -3091,7 +3325,7 @@ namespace Microsoft.Dafny
         var prevLoopStack = loopStack;

         labeledStatements = new Scope<Statement>();

         loopStack = new List<Statement>();

-        ResolveStatement(s.Body, bodyMustBeSpecOnly, method);

+        ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);

         labeledStatements = prevLblStmts;

         loopStack = prevLoopStack;

         scope.PopMarker();

@@ -3195,7 +3429,7 @@ namespace Microsoft.Dafny
             i++;

           }

           foreach (Statement ss in mc.Body) {

-            ResolveStatement(ss, bodyIsSpecOnly, method);

+            ResolveStatement(ss, bodyIsSpecOnly, codeContext);

           }

           scope.PopMarker();

         }

@@ -3218,13 +3452,15 @@ namespace Microsoft.Dafny
         Error(s.Tok, "skeleton statements are allowed only in refining methods");

         // nevertheless, resolve the underlying statement; hey, why not

         if (s.S != null) {

-          ResolveStatement(s.S, specContextOnly, method);

+          ResolveStatement(s.S, specContextOnly, codeContext);

         }

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();

       }

     }

-    private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, Method method) {

+    private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {

+      Contract.Requires(codeContext != null);

+

       int prevErrorCount = ErrorCount;

       // First, resolve all LHS's and expression-looking RHS's.

       SeqSelectExpr arrayRangeLhs = null;

@@ -3273,7 +3509,7 @@ namespace Microsoft.Dafny
           bool isEffectful;

           if (rhs is TypeRhs) {

             var tr = (TypeRhs)rhs;

-            ResolveTypeRhs(tr, s, specContextOnly, method);

+            ResolveTypeRhs(tr, s, specContextOnly, codeContext);

             isEffectful = tr.InitCall != null;

           } else if (rhs is HavocRhs) {

             isEffectful = false;

@@ -3379,14 +3615,14 @@ namespace Microsoft.Dafny
       }

 

       foreach (var a in s.ResolvedStatements) {

-        ResolveStatement(a, specContextOnly, method);

+        ResolveStatement(a, specContextOnly, codeContext);

       }

       s.IsGhost = s.ResolvedStatements.TrueForAll(ss => ss.IsGhost);

     }

 

-    bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {

+    bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {

       Contract.Requires(alternatives != null);

-      Contract.Requires(method != null);

+      Contract.Requires(codeContext != null);

 

       bool isGhost = specContextOnly;

       // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement

@@ -3412,7 +3648,7 @@ namespace Microsoft.Dafny
       foreach (var alternative in alternatives) {

         scope.PushMarker();

         foreach (Statement ss in alternative.Body) {

-          ResolveStatement(ss, isGhost, method);

+          ResolveStatement(ss, isGhost, codeContext);

         }

         scope.PopMarker();

       }

@@ -3427,9 +3663,9 @@ namespace Microsoft.Dafny
     /// Resolves the given call statement.

     /// Assumes all LHSs have already been resolved (and checked for mutability).

     /// </summary>

-    void ResolveCallStmt(CallStmt s, bool specContextOnly, Method method, Type receiverType) {

+    void ResolveCallStmt(CallStmt s, bool specContextOnly, ICodeContext codeContext, Type receiverType) {

       Contract.Requires(s != null);

-      Contract.Requires(method != null);

+      Contract.Requires(codeContext != null);

       bool isInitCall = receiverType != null;

 

       // resolve receiver

@@ -3441,14 +3677,12 @@ namespace Microsoft.Dafny
       // resolve the method name

       NonProxyType nptype;

       MemberDecl member = ResolveMember(s.Tok, receiverType, s.MethodName, out nptype);

-      Method callee = null;

+      ICodeContext callee = null;

       if (member == null) {

         // error has already been reported by ResolveMember

-      } else if (!(member is Method)) {

-        Error(s, "member {0} in type {1} does not refer to a method", s.MethodName, nptype);

-      } else {

-        callee = (Method)member;

-        s.Method = callee;

+      } else if (member is Method) {

+        s.Method = (Method)member;

+        callee = s.Method;

         if (!isInitCall && callee is Constructor) {

           Error(s, "a constructor is only allowed to be called when an object is being allocated");

         }

@@ -3456,6 +3690,8 @@ namespace Microsoft.Dafny
         if (specContextOnly && !callee.IsGhost) {

           Error(s, "only ghost methods can be called from this context");

         }

+      } else {

+        Error(s, "member {0} in type {1} does not refer to a method", s.MethodName, nptype);

       }

 

       // resolve left-hand sides

@@ -3565,23 +3801,21 @@ namespace Microsoft.Dafny
         }

 

         // Resolution termination check

-        if (method.EnclosingClass != null && callee.EnclosingClass != null) {

-          ModuleDefinition callerModule = method.EnclosingClass.Module;

-          ModuleDefinition calleeModule = callee.EnclosingClass.Module;

-          if (callerModule == calleeModule) {

-            // intra-module call; this is allowed; add edge in module's call graph

-            callerModule.CallGraph.AddEdge(method, callee);

-          } else {

-            //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));

-            //

-          }

+        ModuleDefinition callerModule = codeContext.EnclosingModule;

+        ModuleDefinition calleeModule = callee.EnclosingModule;

+        if (callerModule == calleeModule) {

+          // intra-module call; this is allowed; add edge in module's call graph

+          callerModule.CallGraph.AddEdge(codeContext, callee);

+        } else {

+          //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));

+          //

         }

       }

     }

 

-    void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, Method method) {

+    void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, ICodeContext codeContext) {

       Contract.Requires(blockStmt != null);

-      Contract.Requires(method != null);

+      Contract.Requires(codeContext != null);

 

       foreach (Statement ss in blockStmt.Body) {

         labeledStatements.PushMarker();

@@ -3602,7 +3836,7 @@ namespace Microsoft.Dafny
             }

           }

         }

-        ResolveStatement(ss, specContextOnly, method);

+        ResolveStatement(ss, specContextOnly, codeContext);

         labeledStatements.PopMarker();

       }

     }

@@ -3620,6 +3854,8 @@ namespace Microsoft.Dafny
         // this case is checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack

       } else if (stmt is ReturnStmt) {

         Error(stmt, "return statement is not allowed inside a parallel statement");

+      } else if (stmt is YieldStmt) {

+        Error(stmt, "yield statement is not allowed inside a parallel statement");

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

         foreach (var lhs in s.Lhss) {

@@ -3746,10 +3982,10 @@ namespace Microsoft.Dafny
       }

     }

 

-    Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, Method method) {

+    Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) {

       Contract.Requires(rr != null);

       Contract.Requires(stmt != null);

-      Contract.Requires(method != null);

+      Contract.Requires(codeContext != null);

       Contract.Ensures(Contract.Result<Type>() != null);

 

       if (rr.Type == null) {

@@ -3760,7 +3996,7 @@ namespace Microsoft.Dafny
           } else {

             bool callsConstructor = false;

             if (rr.InitCall != null) {

-              ResolveCallStmt(rr.InitCall, specContextOnly, method, rr.EType);

+              ResolveCallStmt(rr.InitCall, specContextOnly, codeContext, rr.EType);

               if (rr.InitCall.Method is Constructor) {

                 callsConstructor = true;

               }

@@ -3833,6 +4069,18 @@ namespace Microsoft.Dafny
         }

       }

 

+      IteratorDecl iter = receiverType.AsIteratorType;

+      if (iter != null) {

+        MemberDecl member;  

+        if (!iter.ImplicitlyDefinedMembers.TryGetValue(memberName, out member)) {

+          Error(tok, "member {0} does not exist in iterator {1}", memberName, iter.Name);

+          return null;

+        } else {

+          nptype = (UserDefinedType)receiverType;

+          return member;

+        }

+      }

+

       Error(tok, "type {0} does not have a member {1}", receiverType, memberName);

       return null;

     }

@@ -3947,7 +4195,6 @@ namespace Microsoft.Dafny
     /// </summary>

     void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {

       Contract.Requires(expr != null);

-      Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

       if (expr.Type != null) {

         // expression has already been resovled

@@ -3991,7 +4238,9 @@ namespace Microsoft.Dafny
         if (!scope.AllowInstance) {

           Error(expr, "'this' is not allowed in a 'static' context");

         }

-        expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporting

+        if (currentClass != null) {

+          expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporting

+        }

 

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

@@ -4740,7 +4989,6 @@ namespace Microsoft.Dafny
     /// </summary>

     void CheckIsNonGhost(Expression expr) {

       Contract.Requires(expr != null);

-      Contract.Requires(currentClass != null);

       Contract.Requires(expr.WasResolved());  // this check approximates the requirement that "expr" be resolved

 

       if (expr is IdentifierExpr) {

@@ -4930,6 +5178,7 @@ namespace Microsoft.Dafny
       //       (if two imported types have the same name, an error message is produced here)

       //  - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)

       //  - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

+      //  - iterator

       //  - static function or method in the enclosing module, or its imports.

 

       Expression r = null;  // resolved version of e

@@ -4949,6 +5198,14 @@ namespace Microsoft.Dafny
       } else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

           Error(id, "The name {0} ambiguously refers to a type in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());

+        } else if (decl is IteratorDecl) {

+          // ----- root is an iterator

+          if (e.Tokens.Count != 1 || e.Arguments == null) {

+            Error(id, "name of iterator ('{0}') is used as a variable", id.val);

+          } else {

+            r = new StaticReceiverExpr(id, (IteratorDecl)decl);

+            call = new CallRhs(e.tok, r, id.val, e.Arguments);

+          }

         } else if (e.Tokens.Count == 1 && e.Arguments == null) {

           Error(id, "name of type ('{0}') is used as a variable", id.val);

         } else if (e.Tokens.Count == 1 && e.Arguments != null) {

@@ -4993,7 +5250,7 @@ namespace Microsoft.Dafny
           }

         }

 

-      } else if ((classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member))

+      } else if ((currentClass != null && classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member))

                  || moduleInfo.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

       {

         // ----- field, function, or method

@@ -5062,6 +5319,14 @@ namespace Microsoft.Dafny
             Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);

           }

           call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall);

+        } else if (decl is IteratorDecl) {

+          // ----- root is an iterator

+          if (p + 1 == e.Tokens.Count || e.Arguments == null) {

+            Error(id, "name of iterator ('{0}') is used as a variable", id.val);

+          } else {

+            r = new StaticReceiverExpr(id, (IteratorDecl)decl);

+            call = new CallRhs(e.tok, r, id.val, e.Arguments);

+          }

         } else {

           // ----- root is a datatype

           var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

@@ -5145,14 +5410,26 @@ namespace Microsoft.Dafny
       if (p < e.Tokens.Count) {

         Contract.Assert(e.Arguments != null);

 

-        Dictionary<string, MemberDecl> members;

-        MemberDecl member;

-        UserDefinedType receiverType = UserDefinedType.DenotesClass(r.Type);

-        if (allowMethodCall &&

-          receiverType != null &&

-          classMembers.TryGetValue((ClassDecl)receiverType.ResolvedClass, out members) &&

-          members.TryGetValue(e.Tokens[p].val, out member) &&

-          member is Method) {

+        

+        bool itIsAMethod = false;

+        if (allowMethodCall) {

+          var udt = r.Type.Normalize() as UserDefinedType;

+          if (udt != null && udt.ResolvedClass != null) {

+            Dictionary<string, MemberDecl> members;

+            if (udt.ResolvedClass is ClassDecl) {

+              classMembers.TryGetValue((ClassDecl)udt.ResolvedClass, out members);

+            } else if (udt.ResolvedClass is IteratorDecl) {

+              members = ((IteratorDecl)udt.ResolvedClass).ImplicitlyDefinedMembers;

+            } else {

+              members = null;

+            }

+            MemberDecl member;

+            if (members != null && members.TryGetValue(e.Tokens[p].val, out member) && member is Method) {

+              itIsAMethod = true;

+            }

+          }

+        }

+        if (itIsAMethod) {

           // method

           call = new CallRhs(e.Tokens[p], r, e.Tokens[p].val, e.Arguments);

           r = null;

@@ -5652,12 +5929,12 @@ namespace Microsoft.Dafny
 

     void ResolveReceiver(Expression expr, bool twoState) {

       Contract.Requires(expr != null);

-      Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

 

       if (expr is ThisExpr && !expr.WasResolved()) {

         // Allow 'this' here, regardless of scope.AllowInstance.  The caller is responsible for

         // making sure 'this' does not really get used when it's not available.

+        Contract.Assume(currentClass != null);  // this is really a precondition, in this case

         expr.Type = GetThisType(expr.tok, currentClass);

       } else {

         ResolveExpression(expr, twoState);

@@ -5863,7 +6140,7 @@ namespace Microsoft.Dafny
     /// </summary>

     bool UsesSpecFeatures(Expression expr) {

       Contract.Requires(expr != null);

-      Contract.Requires(currentClass != null);

+      Contract.Requires(expr.WasResolved());  // this check approximates the requirement that "expr" be resolved

 

       if (expr is LiteralExpr) {

         return false;

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index a6123fbb..0ebbab1f 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {

 	const char EOL = '\n';

 	const int eofSym = 0; /* pdt */

-	const int maxT = 111;

-	const int noSym = 111;

+	const int maxT = 114;

+	const int noSym = 114;

 

 

 	[ContractInvariantMethod]

@@ -501,52 +501,55 @@ public class Scanner {
 			case "codatatype": t.kind = 21; break;

 			case "var": t.kind = 23; break;

 			case "type": t.kind = 25; break;

-			case "method": t.kind = 31; break;

-			case "constructor": t.kind = 32; break;

-			case "returns": t.kind = 33; break;

-			case "modifies": t.kind = 35; break;

-			case "free": t.kind = 36; break;

-			case "requires": t.kind = 37; break;

-			case "ensures": t.kind = 38; break;

-			case "decreases": t.kind = 39; break;

-			case "bool": t.kind = 40; break;

-			case "nat": t.kind = 41; break;

-			case "int": t.kind = 42; break;

-			case "set": t.kind = 43; break;

-			case "multiset": t.kind = 44; break;

-			case "seq": t.kind = 45; break;

-			case "map": t.kind = 46; break;

-			case "object": t.kind = 47; break;

-			case "function": t.kind = 48; break;

-			case "predicate": t.kind = 49; break;

-			case "copredicate": t.kind = 50; break;

-			case "reads": t.kind = 51; break;

-			case "label": t.kind = 54; break;

-			case "break": t.kind = 55; break;

-			case "where": t.kind = 56; break;

-			case "return": t.kind = 58; break;

-			case "assume": t.kind = 60; break;

-			case "new": t.kind = 61; break;

-			case "choose": t.kind = 64; break;

-			case "if": t.kind = 65; break;

-			case "else": t.kind = 66; break;

-			case "case": t.kind = 67; break;

-			case "while": t.kind = 69; break;

-			case "invariant": t.kind = 70; break;

-			case "match": t.kind = 71; break;

-			case "assert": t.kind = 72; break;

-			case "print": t.kind = 73; break;

-			case "parallel": t.kind = 74; break;

-			case "in": t.kind = 87; break;

-			case "false": t.kind = 97; break;

-			case "true": t.kind = 98; break;

-			case "null": t.kind = 99; break;

-			case "this": t.kind = 100; break;

-			case "fresh": t.kind = 101; break;

-			case "old": t.kind = 102; break;

-			case "then": t.kind = 103; break;

-			case "forall": t.kind = 105; break;

-			case "exists": t.kind = 107; break;

+			case "iterator": t.kind = 29; break;

+			case "yields": t.kind = 30; break;

+			case "method": t.kind = 34; break;

+			case "constructor": t.kind = 35; break;

+			case "returns": t.kind = 36; break;

+			case "modifies": t.kind = 37; break;

+			case "free": t.kind = 38; break;

+			case "requires": t.kind = 39; break;

+			case "ensures": t.kind = 40; break;

+			case "decreases": t.kind = 41; break;

+			case "reads": t.kind = 42; break;

+			case "yield": t.kind = 43; break;

+			case "bool": t.kind = 44; break;

+			case "nat": t.kind = 45; break;

+			case "int": t.kind = 46; break;

+			case "set": t.kind = 47; break;

+			case "multiset": t.kind = 48; break;

+			case "seq": t.kind = 49; break;

+			case "map": t.kind = 50; break;

+			case "object": t.kind = 51; break;

+			case "function": t.kind = 52; break;

+			case "predicate": t.kind = 53; break;

+			case "copredicate": t.kind = 54; break;

+			case "label": t.kind = 57; break;

+			case "break": t.kind = 58; break;

+			case "where": t.kind = 59; break;

+			case "return": t.kind = 61; break;

+			case "assume": t.kind = 63; break;

+			case "new": t.kind = 64; break;

+			case "choose": t.kind = 67; break;

+			case "if": t.kind = 68; break;

+			case "else": t.kind = 69; break;

+			case "case": t.kind = 70; break;

+			case "while": t.kind = 72; break;

+			case "invariant": t.kind = 73; break;

+			case "match": t.kind = 74; break;

+			case "assert": t.kind = 75; break;

+			case "print": t.kind = 76; break;

+			case "parallel": t.kind = 77; break;

+			case "in": t.kind = 90; break;

+			case "false": t.kind = 100; break;

+			case "true": t.kind = 101; break;

+			case "null": t.kind = 102; break;

+			case "this": t.kind = 103; break;

+			case "fresh": t.kind = 104; break;

+			case "old": t.kind = 105; break;

+			case "then": t.kind = 106; break;

+			case "forall": t.kind = 108; break;

+			case "exists": t.kind = 110; break;

 			default: break;

 		}

 	}

@@ -660,73 +663,73 @@ public class Scanner {
 			case 22:

 				{t.kind = 28; break;}

 			case 23:

-				{t.kind = 34; break;}

+				{t.kind = 31; break;}

 			case 24:

-				{t.kind = 52; break;}

+				{t.kind = 55; break;}

 			case 25:

-				{t.kind = 53; break;}

+				{t.kind = 56; break;}

 			case 26:

-				{t.kind = 57; break;}

+				{t.kind = 60; break;}

 			case 27:

-				{t.kind = 59; break;}

-			case 28:

 				{t.kind = 62; break;}

+			case 28:

+				{t.kind = 65; break;}

 			case 29:

-				{t.kind = 63; break;}

+				{t.kind = 66; break;}

 			case 30:

-				{t.kind = 68; break;}

+				{t.kind = 71; break;}

 			case 31:

 				if (ch == '>') {AddCh(); goto case 32;}

 				else {goto case 0;}

 			case 32:

-				{t.kind = 75; break;}

+				{t.kind = 78; break;}

 			case 33:

-				{t.kind = 76; break;}

+				{t.kind = 79; break;}

 			case 34:

-				{t.kind = 77; break;}

+				{t.kind = 80; break;}

 			case 35:

-				{t.kind = 78; break;}

+				{t.kind = 81; break;}

 			case 36:

 				if (ch == '&') {AddCh(); goto case 37;}

 				else {goto case 0;}

 			case 37:

-				{t.kind = 79; break;}

+				{t.kind = 82; break;}

 			case 38:

-				{t.kind = 80; break;}

+				{t.kind = 83; break;}

 			case 39:

-				{t.kind = 81; break;}

+				{t.kind = 84; break;}

 			case 40:

-				{t.kind = 82; break;}

+				{t.kind = 85; break;}

 			case 41:

-				{t.kind = 84; break;}

+				{t.kind = 87; break;}

 			case 42:

-				{t.kind = 85; break;}

+				{t.kind = 88; break;}

 			case 43:

-				{t.kind = 86; break;}

-			case 44:

 				{t.kind = 89; break;}

+			case 44:

+				{t.kind = 92; break;}

 			case 45:

-				{t.kind = 90; break;}

+				{t.kind = 93; break;}

 			case 46:

-				{t.kind = 91; break;}

+				{t.kind = 94; break;}

 			case 47:

-				{t.kind = 92; break;}

+				{t.kind = 95; break;}

 			case 48:

-				{t.kind = 93; break;}

+				{t.kind = 96; break;}

 			case 49:

-				{t.kind = 94; break;}

+				{t.kind = 97; break;}

 			case 50:

-				{t.kind = 95; break;}

+				{t.kind = 98; break;}

 			case 51:

-				{t.kind = 96; break;}

+				{t.kind = 99; break;}

 			case 52:

-				{t.kind = 106; break;}

+				{t.kind = 109; break;}

 			case 53:

-				{t.kind = 108; break;}

+				{t.kind = 111; break;}

 			case 54:

-				{t.kind = 109; break;}

+				{t.kind = 112; break;}

 			case 55:

-				{t.kind = 110; break;}

+				{t.kind = 113; break;}

 			case 56:

 				recEnd = pos; recKind = 5;

 				if (ch == '=') {AddCh(); goto case 26;}

@@ -747,30 +750,30 @@ public class Scanner {
 				if (ch == '|') {AddCh(); goto case 39;}

 				else {t.kind = 22; break;}

 			case 60:

-				recEnd = pos; recKind = 29;

+				recEnd = pos; recKind = 32;

 				if (ch == '=') {AddCh(); goto case 65;}

-				else {t.kind = 29; break;}

+				else {t.kind = 32; break;}

 			case 61:

-				recEnd = pos; recKind = 30;

+				recEnd = pos; recKind = 33;

 				if (ch == '=') {AddCh(); goto case 41;}

-				else {t.kind = 30; break;}

+				else {t.kind = 33; break;}

 			case 62:

-				recEnd = pos; recKind = 88;

+				recEnd = pos; recKind = 91;

 				if (ch == '=') {AddCh(); goto case 42;}

 				else if (ch == '!') {AddCh(); goto case 43;}

-				else {t.kind = 88; break;}

+				else {t.kind = 91; break;}

 			case 63:

 				recEnd = pos; recKind = 27;

 				if (ch == '>') {AddCh(); goto case 34;}

 				else {t.kind = 27; break;}

 			case 64:

-				recEnd = pos; recKind = 104;

+				recEnd = pos; recKind = 107;

 				if (ch == '.') {AddCh(); goto case 23;}

-				else {t.kind = 104; break;}

+				else {t.kind = 107; break;}

 			case 65:

-				recEnd = pos; recKind = 83;

+				recEnd = pos; recKind = 86;

 				if (ch == '=') {AddCh(); goto case 31;}

-				else {t.kind = 83; break;}

+				else {t.kind = 86; break;}

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a090515e..54a4bec5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -345,6 +345,8 @@ namespace Microsoft.Dafny {
             AddDatatype((DatatypeDecl)d);

           } else if (d is ModuleDecl) {

             // submodules have already been added as a top level module, ignore this.

+          } else if (d is IteratorDecl) {

+            throw new NotImplementedException();  // TODO

           } else if (d is ClassDecl) {

             AddClassMembers((ClassDecl)d);

           } else {

@@ -3766,6 +3768,8 @@ namespace Microsoft.Dafny {
           TrStmt(s.hiddenUpdate, builder, locals, etran);

         }

         builder.Add(new Bpl.ReturnCmd(stmt.Tok));

+      } else if (stmt is YieldStmt) {

+        throw new NotImplementedException(); // TODO

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

         AddComment(builder, s, "assign-such-that statement");

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index b7d48d7e..0dfb0be4 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -510,7 +510,7 @@ ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowe
 ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

 ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

 ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)

@@ -1344,8 +1344,8 @@ Dafny program verifier finished with 12 verified, 0 errors
 -------------------- EqualityTypes.dfy --------------------

 EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype

 EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality

-EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes type parameters

-EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes type parameters

+EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes a different number of type parameters

+EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters

 EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality

 EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality

 EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index e658bfe9..4f437d23 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -31,13 +31,15 @@
 

    `(,(dafny-regexp-opt '(

         "class" "datatype" "codatatype" "type" "function" "predicate" "copredicate"

+        "iterator"

         "ghost" "var" "method" "constructor"

         "module" "import" "default" "as" "opened" "static" "refines"

-        "returns" "requires" "ensures" "modifies" "reads" "free"

+        "returns" "yields" "requires" "ensures" "modifies" "reads" "free"

         "invariant" "decreases"

         )) . font-lock-builtin-face)

    `(,(dafny-regexp-opt '(

-        "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "while" "print" "where"

+        "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"

+        "while" "print" "where"

         "old" "forall" "exists" "new" "parallel" "in" "this" "fresh"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face)

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 81dd0dd1..9d6f0882 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -17,12 +17,13 @@ namespace Demo
         StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");

 

         this.MarkReservedWords(  // NOTE: these keywords must also appear once more below

-          "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",

+          "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype",

+          "iterator", "type",

           "assert", "assume", "new", "this", "object", "refines",

           "module", "import", "as", "default", "opened",

           "if", "then", "else", "while", "invariant",

-          "break", "label", "return", "parallel", "print",

-          "returns", "requires", "ensures", "modifies", "reads", "decreases",

+          "break", "label", "return", "yield", "parallel", "print",

+          "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",

           "bool", "nat", "int", "false", "true", "null",

           "function", "predicate", "copredicate", "free",

           "in", "forall", "exists",

@@ -269,6 +270,7 @@ namespace Demo
           | "datatype"

           | "codatatype"

           | "type"

+          | "iterator"

           | "assert"

           | "assume"

           | "new"

@@ -288,9 +290,11 @@ namespace Demo
           | "break"

           | "label"

           | "return"

+          | "yield"

           | "parallel"

           | "print"

           | "returns"

+          | "yields"

           | "requires"

           | "ensures"

           | "modifies"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index 80a6dbb5..5ecc8dc2 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -139,7 +139,7 @@ namespace DafnyLanguage
             foreach (var ctor in dt.Ctors) {

               foreach (var dtor in ctor.Destructors) {

                 if (dtor != null) {

-                  IdRegion.Add(newRegions, dtor.tok, dtor, "destructor", true, module);

+                  IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module);

                 }

               }

             }

@@ -175,7 +175,7 @@ namespace DafnyLanguage
                 }

               } else if (member is Field) {

                 var fld = (Field)member;

-                IdRegion.Add(newRegions, fld.tok, fld, "field", true, module);

+                IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);

               }

             }

           }

@@ -194,7 +194,8 @@ namespace DafnyLanguage
         ExprRegions(fe.E, regions, module);

       }

       if (fe.Field != null) {

-        IdRegion.Add(regions, fe.tok, fe.Field, "field", false, module);

+        Microsoft.Dafny.Type showType = null;  // TODO: if we had the instantiated type of this field, that would have been nice to use here (but the Resolver currently does not compute or store the instantiated type for a FrameExpression)

+        IdRegion.Add(regions, fe.tok, fe.Field, showType, "field", false, module);

       }

     }

 

@@ -206,7 +207,7 @@ namespace DafnyLanguage
         IdRegion.Add(regions, e.tok, e.Var, false, module);

       } else if (expr is FieldSelectExpr) {

         var e = (FieldSelectExpr)expr;

-        IdRegion.Add(regions, e.tok, e.Field, "field", false, module);

+        IdRegion.Add(regions, e.tok, e.Field, e.Type, "field", false, module);

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         foreach (var bv in e.BoundVars) {

@@ -298,13 +299,13 @@ namespace DafnyLanguage
           regions.Add(new IdRegion(tok, v, isDefinition, context));

         }

       }

-      public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {

+      public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {

         Contract.Requires(regions != null);

         Contract.Requires(tok != null);

         Contract.Requires(decl != null);

         Contract.Requires(kind != null);

         if (SurfaceSyntaxToken(tok)) {

-          regions.Add(new IdRegion(tok, decl, kind, isDefinition, context));

+          regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));

         }

       }

 

@@ -325,13 +326,16 @@ namespace DafnyLanguage
         HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);

         Kind = !isDefinition ? OccurrenceKind.Use : VarDecl.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition;

       }

-      private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {

+      private IdRegion(Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {

         Contract.Requires(tok != null);

         Contract.Requires(decl != null);

         Contract.Requires(kind != null);

+        if (showType == null) {

+          showType = decl.Type;

+        }

         Start = tok.pos;

         Length = decl.Name.Length;

-        HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullNameInContext(context), decl.Type.TypeName(context), decl.IsGhost ? "ghost " : "", kind);

+        HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullNameInContext(context), showType.TypeName(context), decl.IsGhost ? "ghost " : "", kind);

         Kind = !isDefinition ? OccurrenceKind.Use : OccurrenceKind.Definition;

       }

     }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 5853f180..22388704 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -253,6 +253,7 @@ namespace DafnyLanguage
                 case "in":

                 case "int":

                 case "invariant":

+                case "iterator":

                 case "label":

                 case "match":

                 case "method":

@@ -282,6 +283,8 @@ namespace DafnyLanguage
                 case "type":

                 case "var":

                 case "while":

+                case "yield":

+                case "yields":

                 #endregion

                   break;

                 default:

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 81b04694..88f9c2a2 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,15 +5,17 @@
 \usepackage{listings}

 

 \lstdefinelanguage{dafny}{

-  morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,map,%

+  morekeywords={class,datatype,codatatype,type,iterator,

+      bool,nat,int,object,set,multiset,seq,array,array2,array3,map,

       function,predicate,copredicate,

       ghost,var,static,refines,

-      method,constructor,returns,module,import,default,opened,as,in,

+      method,constructor,returns,yields,module,import,default,opened,as,in,

       requires,modifies,ensures,reads,decreases,free,

       % expressions

       match,case,false,true,null,old,fresh,choose,this,

       % statements

-      assert,assume,print,new,if,then,else,while,invariant,break,label,return,parallel,where

+      assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,

+      parallel,where

       },

   literate=%

     {:}{$\colon$}1

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index c61e5ebc..d67d275a 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -6,11 +6,12 @@
 syntax clear
 syntax case match
 syntax keyword dafnyFunction function predicate copredicate method constructor
-syntax keyword dafnyTypeDef class datatype codatatype type module import opened as default
+syntax keyword dafnyTypeDef class datatype codatatype type iterator
+syntax keyword module import opened as default
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while parallel
-syntax keyword dafnyStatement assume assert return new print break label where
-syntax keyword dafnyKeyword var ghost returns null static this refines
+syntax keyword dafnyStatement assume assert return yield new print break label where
+syntax keyword dafnyKeyword var ghost returns yields null static this refines
 syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
 syntax keyword dafnyOperator forall exists old fresh choose