path: root/Source/Dafny/Dafny.atg

	/*-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------
// Dafny
// Rustan Leino, first created 25 January 2008
//--------------------------------------------------------------------------*/
using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
using System.Text;
COMPILER Dafny
/*--------------------------------------------------------------------------*/
readonly Expression/*!*/ dummyExpr;
readonly AssignmentRhs/*!*/ dummyRhs;
readonly FrameExpression/*!*/ dummyFrameExpr;
readonly Statement/*!*/ dummyStmt;
readonly Attributes.Argument/*!*/ dummyAttrArg;
readonly ModuleDecl theModule;
readonly BuiltIns theBuiltIns;
readonly bool theVerifyThisFile;
int anonymousIds = 0;

struct MemberModifiers {
  public bool IsGhost;
  public bool IsStatic;
}

///<summary>
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ {
  Contract.Requires(filename != null);
  Contract.Requires(module != null);
  string s;
  if (filename == "stdin.dfy") {
    s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
    return Parse(s, filename, module, builtIns, errors, verifyThisFile);
  } else {
    using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
      s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
      return Parse(s, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);
    }
  }
}
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {
  Contract.Requires(s != null);
  Contract.Requires(filename != null);
  Contract.Requires(module != null);
  Errors errors = new Errors();
  return Parse(s, filename, module, builtIns, errors, verifyThisFile);
}
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner with the given Errors sink.
///</summary>
public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,
                         Errors/*!*/ errors, bool verifyThisFile=true) {
  Contract.Requires(s != null);
  Contract.Requires(filename != null);
  Contract.Requires(module != null);
  Contract.Requires(errors != null);
  byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
  MemoryStream ms = new MemoryStream(buffer,false);
  Scanner scanner = new Scanner(ms, errors, filename);
  Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile);
  parser.Parse();
  return parser.errors.count;
}
public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
  : this(scanner, errors)  // the real work
{
  // initialize readonly fields
  dummyExpr = new LiteralExpr(Token.NoToken);
  dummyRhs = new ExprRhs(dummyExpr, null);
  dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
  dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null);
  dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
  theModule = module;
  theBuiltIns = builtIns;
  theVerifyThisFile = verifyThisFile;
}

bool IsAttribute() {
  Token x = scanner.Peek();
  return la.kind == _lbrace && x.kind == _colon;
}

bool IsAlternative() {
  Token x = scanner.Peek();
  return la.kind == _lbrace && x.val == "case";
}

bool IsLoopSpec() {
  return la.val == "invariant" | la.val == "decreases" | la.val == "modifies";
}

bool IsLoopSpecOrAlternative() {
  Token x = scanner.Peek();
  return IsLoopSpec() || (la.kind == _lbrace && x.val == "case");
}

bool IsParenStar() {
  scanner.ResetPeek();
  Token x = scanner.Peek();
  return la.kind == _openparen && x.kind == _star;
}

string UnwildIdent(string x, bool allowWildcardId) {
  if (x.StartsWith("_")) {
    if (allowWildcardId && x.Length == 1) {
      return "_v" + anonymousIds++;
    } else {
      SemErr("cannot declare identifier beginning with underscore");
    }
  }
  return x;
}

bool IsLambda(bool allowLambda)
{
  return allowLambda &&
    (la.kind == _darrow || la.kind == _arrow
    || la.kind == _reads || la.kind == _requires);
}

bool IsIdentParen() {
  Token x = scanner.Peek();
  return la.kind == _ident && x.kind == _openparen;
}

bool IsIdentColonOrBar() {
  Token x = scanner.Peek();
  return la.kind == _ident && (x.kind == _colon || x.kind == _verticalbar);
}

bool SemiFollowsCall(bool allowSemi, Expression e) {
  return allowSemi && la.kind == _semi &&
    (e is FunctionCallExpr || e is ApplyExpr ||
     (e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));
}

bool CloseOptionalParen(bool usesOptionalParen) {
  return usesOptionalParen && la.kind == _closeparen;
}

bool CloseOptionalBrace(bool usesOptionalBrace) {
  return usesOptionalBrace && la.kind == _rbrace;
}

/*--------------------------------------------------------------------------*/
CHARACTERS
  letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
  digit = "0123456789".
  posDigit = "123456789".
  hexdigit = "0123456789ABCDEFabcdef".
  special = "'_?\\".
  glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
  cr        = '\r'.
  lf        = '\n'.
  tab       = '\t'.
  space = ' '.
  quote = '"'.
  nondigit = letter + special.
  idchar = nondigit + digit.
  nonidchar = ANY - idchar.
  nonquote = letter + digit + space + glyph.
  /* exclude the characters in 'array' */
  nondigitMinusA = nondigit - 'a'.
  idcharMinusA = idchar - 'a'.
  idcharMinusR = idchar - 'r'.
  idcharMinusY = idchar - 'y'.
  idcharMinusPosDigit = idchar - posDigit.
/*------------------------------------------------------------------------*/
TOKENS
  ident =  nondigitMinusA {idchar}            /* if char 0 is not an 'a', then anything else is fine */
        |  'a' [ idcharMinusR {idchar} ]      /* if char 0 is an 'a', then either there is no char 1 or char 1 is not an 'r' */
        |  'a' 'r' [ idcharMinusR {idchar} ]  /* etc. */
        |  'a' 'r' 'r' [ idcharMinusA {idchar} ]
        |  'a' 'r' 'r' 'a' [ idcharMinusY {idchar} ]
        |  'a' 'r' 'r' 'a' 'y' idcharMinusPosDigit {idchar}
        |  'a' 'r' 'r' 'a' 'y' posDigit {idchar} nondigit {idchar}.
  digits = digit {digit}.
  hexdigits = "0x" hexdigit {hexdigit}.
  decimaldigits = digit {digit} '.' digit {digit}.
  arrayToken = "array" [posDigit {digit}].
  string = quote {nonquote} quote.
  colon = ':'.
  verticalbar = '|'.
  semi = ';'.
  darrow = "=>".
  arrow = "->".
  reads = "reads".
  requires = "requires".
  lbrace = '{'.
  rbrace = '}'.
  openparen = '('.
  closeparen = ')'.
  star = '*'.
  notIn = "!in" CONTEXT (nonidchar).
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
IGNORE cr + lf + tab
/*------------------------------------------------------------------------*/
PRODUCTIONS
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
     List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
     ModuleDecl submodule;
     // to support multiple files, create a default module only if theModule is null
     DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
     // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
	 TraitDecl/*!*/ trait;
     Contract.Assert(defaultModule != null);
  .)
  { "include" string                            (. {
                                                    string parsedFile = t.filename;
                                                    string includedFile = t.val.Substring(1, t.val.Length - 2);
                                                    string fullPath = includedFile;
                                                    if (!Path.IsPathRooted(includedFile)) {
                                                      string basePath = Path.GetDirectoryName(parsedFile);
                                                      includedFile = Path.Combine(basePath, includedFile);
                                                      fullPath = Path.GetFullPath(includedFile);
                                                    }
                                                    defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
                                                   }
                                                .)
  }
  { SubModuleDecl<defaultModule, out submodule> (. defaultModule.TopLevelDecls.Add(submodule); .)
  | ClassDecl<defaultModule, out c>             (. defaultModule.TopLevelDecls.Add(c); .)
  | DatatypeDecl<defaultModule, out dt>         (. defaultModule.TopLevelDecls.Add(dt); .)
  | NewtypeDecl<defaultModule, out td>          (. defaultModule.TopLevelDecls.Add(td); .)
  | OtherTypeDecl<defaultModule, out td>        (. defaultModule.TopLevelDecls.Add(td); .)
  | IteratorDecl<defaultModule, out iter>       (. defaultModule.TopLevelDecls.Add(iter); .)
  | TraitDecl<defaultModule, out trait>    (. defaultModule.TopLevelDecls.Add(trait); .)
  | ClassMemberDecl<membersDefaultClass, false>
  }
  (. // find the default class in the default module, then append membersDefaultClass to its member list
     DefaultClassDecl defaultClass = null;
     foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
       defaultClass = topleveldecl as DefaultClassDecl;
       if (defaultClass != null) {
         defaultClass.Members.AddRange(membersDefaultClass);
         break;
       }
     }
     if (defaultClass == null) { // create the default class here, because it wasn't found
       defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);
       defaultModule.TopLevelDecls.Add(defaultClass);
     } .)
  EOF
  .
SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
     Attributes attrs = null;  IToken/*!*/ id;
     TraitDecl/*!*/ trait;
	 List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
     List<IToken> idRefined = null, idPath = null, idAssignment = null;
     ModuleDefinition module;
     ModuleDecl sm;
     submodule = null; // appease compiler
     bool isAbstract = false;
     bool opened = false;
  .)
  ( [ "abstract"  (. isAbstract = true; .) ]
    "module"
    { Attribute<ref attrs> }
    NoUSIdent<out id>

      [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .)
       "{"                                       (. module.BodyStartTok = t; .)
        { SubModuleDecl<module, out sm>                (. module.TopLevelDecls.Add(sm); .)
        | ClassDecl<module, out c>                     (. module.TopLevelDecls.Add(c); .)
        | TraitDecl<module, out trait>                 (. module.TopLevelDecls.Add(trait); .)
		| DatatypeDecl<module, out dt>                 (. module.TopLevelDecls.Add(dt); .)
        | NewtypeDecl<module, out td>                  (. module.TopLevelDecls.Add(td); .)
        | OtherTypeDecl<module, out td>                (. module.TopLevelDecls.Add(td); .)
        | IteratorDecl<module, out iter>               (. module.TopLevelDecls.Add(iter); .)
        | ClassMemberDecl<namedModuleDefaultClassMembers, false>
        }
      "}"                                  (. module.BodyEndTok = t;
                                              module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
                                              submodule = new LiteralModuleDecl(module, parent); .)
  |
    "import" ["opened" (.opened = true;.)]
    NoUSIdent<out id>
    [ "=" QualifiedName<out idPath>
      (. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
    | "as" QualifiedName<out idPath>  ["default" QualifiedName<out idAssignment> ]
      (. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .)
    ]
    [ SYNC ";"
        // This semi-colon used to be required, but it seems silly to have it.
        // To stage the transition toward not having it at all, let's make it optional for now.  Then,
        // in a next big version of Dafny, including the following warning message:
        //     (. errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
        // And in a version after that, don't allow the semi-colon at all.
    ]
    (. if (submodule == null) {
         idPath = new List<IToken>();
         idPath.Add(id);
         submodule = new AliasModuleDecl(idPath, id, parent, opened);
       }
    .)
  )
.

QualifiedName<.out List<IToken> ids.>
= (. IToken id; IToken idPrime; ids = new List<IToken>(); .)
  Ident<out id>                               (. ids.Add(id); .)
  { IdentOrDigitsSuffix<out id, out idPrime>  (. ids.Add(id);
                                                 if (idPrime != null) { ids.Add(idPrime); }
                                              .)
  }
  .

ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
= (. Contract.Requires(module != null);
     Contract.Ensures(Contract.ValueAtReturn(out c) != null);
     IToken/*!*/ id;
     List<IToken>/*!*/ traitId=null;
	 Attributes attrs = null;
     List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
     List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
     IToken bodyStart;
  .)
  SYNC
  "class"
  { Attribute<ref attrs> }
  NoUSIdent<out id>
  [ GenericParameters<typeArgs> ]
  ["extends" QualifiedName<out traitId>]
  "{"                                            (. bodyStart = t; .)
  { ClassMemberDecl<members, true>
  }
  "}"
  (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);
     c.BodyStartTok = bodyStart;
     c.BodyEndTok = t;
  .)
  .

    TraitDecl<ModuleDefinition/*!*/ module, out TraitDecl/*!*/ trait>
  = (. Contract.Requires(module != null);
	   Contract.Ensures(Contract.ValueAtReturn(out trait) != null);
	   IToken/*!*/ id;
	   Attributes attrs = null;
	   List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>(); //traits should not support type parameters at the moment
	   List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
	   IToken bodyStart;
    .)
	SYNC
	"trait"
	{ Attribute<ref attrs> }
	NoUSIdent<out id>
	[ GenericParameters<typeArgs> ]
	"{"                                            (. bodyStart = t; .)
    { ClassMemberDecl<members, true>
    }
    "}"
	(. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
     trait.BodyStartTok = bodyStart;
     trait.BodyEndTok = t;
    .)
	.

ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
= (. Contract.Requires(cce.NonNullElements(mm));
     Method/*!*/ m;
     Function/*!*/ f;
     MemberModifiers mmod = new MemberModifiers();
  .)
  { "ghost"                                (. mmod.IsGhost = true; .)
  | "static"                               (. mmod.IsStatic = true; .)
  }
  ( FieldDecl<mmod, mm>
  | FunctionDecl<mmod, out f>                   (. mm.Add(f); .)
  | MethodDecl<mmod, allowConstructors, out m>  (. mm.Add(m); .)
  )
  .
DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt>
= (. Contract.Requires(module != null);
     Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
     IToken/*!*/ id;
     Attributes attrs = null;
     List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
     List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
     IToken bodyStart = Token.NoToken;  // dummy assignment
     bool co = false;
  .)
  SYNC
  ( "datatype"
  | "codatatype"     (. co = true; .)
  )
  { Attribute<ref attrs> }
  NoUSIdent<out id>
  [ GenericParameters<typeArgs> ]
  "="                                      (. bodyStart = t; .)
  DatatypeMemberDecl<ctors>
  { "|" DatatypeMemberDecl<ctors> }
  [ SYNC ";"
      // This semi-colon used to be required, but it seems silly to have it.
      // To stage the transition toward not having it at all, let's make it optional for now.  Then,
      // in a next big version of Dafny, including the following warning message:
      //     (. errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
      // And in a version after that, don't allow the semi-colon at all.
  ]
  (. if (co) {
       dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
     } else {
       dt = new IndDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
     }
     dt.BodyStartTok = bodyStart;
     dt.BodyEndTok = t;
  .)
  .
DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
= (. Contract.Requires(cce.NonNullElements(ctors));
     Attributes attrs = null;
     IToken/*!*/ id;
     List<Formal/*!*/> formals = new List<Formal/*!*/>();
  .)
  { Attribute<ref attrs> }
  NoUSIdent<out id>
  [ FormalsOptionalIds<formals> ]
  (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
  .
FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
     Attributes attrs = null;
     IToken/*!*/ id;  Type/*!*/ ty;
  .)
  SYNC
  "var"
  (. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
  .)
  { Attribute<ref attrs> }
  FIdentType<out id, out ty>                        (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
  { "," FIdentType<out id, out ty>                  (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
  }
  SYNC ";"
  .
NewtypeDecl<ModuleDefinition module, out TopLevelDecl td>
= (. IToken id, bvId;
     Attributes attrs = null;
     td = null;
     Type baseType = null;
     Expression wh;
  .)
  "newtype"
  { Attribute<ref attrs> }
  NoUSIdent<out id>
  "="
  ( IF(IsIdentColonOrBar())
    NoUSIdent<out bvId>
    [ ":" Type<out baseType> ]       (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false); } .)
    "|"
    Expression<out wh, false, true>  (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
  | Type<out baseType>               (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)
  )
  [ SYNC ";"
      // In a future version of Dafny, including the following warning message:
      //     (. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
      // And in a version after that, don't allow the semi-colon at all.
  ]
  .
OtherTypeDecl<ModuleDefinition module, out TopLevelDecl td>
= (. IToken id;
     Attributes attrs = null;
     var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
     var typeArgs = new List<TypeParameter>();
     td = null;
     Type ty;
  .)
  "type"
  { Attribute<ref attrs> }
  NoUSIdent<out id>
  ( "(" "==" ")"               (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
    [ GenericParameters<typeArgs> ]
  |
    [ GenericParameters<typeArgs> ]
    [ "="
      Type<out ty>             (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)
    ]
  )                            (. if (td == null) {
                                    td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
                                  }
                               .)
  [ SYNC ";"
      // This semi-colon used to be required, but it seems silly to have it.
      // To stage the transition toward not having it at all, let's make it optional for now.  Then,
      // in a next big version of Dafny, including the following warning message:
      //     (. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
      // And in a version after that, don't allow the semi-colon at all.
  ]
  .
GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
/* isGhost always returns as false if allowGhostKeyword is false */
= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
     Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
     isGhost = false; .)
  [ "ghost"                    (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
  ]
  IdentType<out id, out ty, true>
  .
FIdentType<out IToken/*!*/ id, out Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
    id = Token.NoToken;
  .)
  ( WildIdent<out id, false>
  | digits         (. id = t; .)
  )
  ":"
  Type<out ty>
  .
IdentType<out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
  WildIdent<out id, allowWildcardId>
  ":"
  Type<out ty>
  .
LocalIdentTypeOptional<out LocalVariable var, bool isGhost>
= (. IToken id;  Type ty;  Type optType = null;
  .)
  WildIdent<out id, true>
  [ ":" Type<out ty>             (. optType = ty; .)
  ]
  (. var = new LocalVariable(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
  .
IdentTypeOptional<out BoundVar var>
= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);
     IToken id;  Type ty;  Type optType = null;
  .)
  WildIdent<out id, true>
  [ ":" Type<out ty>             (. optType = ty; .)
  ]
  (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
  .
TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost>
= (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
     Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
     Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
     string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; .)
  [ "ghost"                            (. isGhost = true; .)
  ]
  ( TypeAndToken<out id, out ty>
    [ ":"
      (. /* try to convert ty to an identifier */
         UserDefinedType udt = ty as UserDefinedType;
         if (udt != null && udt.TypeArgs.Count == 0) {
           name = udt.Name;
         } else {
           SemErr(id, "invalid formal-parameter name in datatype constructor");
         }
      .)
      Type<out ty>
    ]
  | digits         (. id = t; name = id.val;.)
    ":"
    Type<out ty>
  )
  (. if (name != null) {
       identName = name;
     } else {
       identName = "#" + anonymousIds++;
     }
  .)
  .
/*------------------------------------------------------------------------*/
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;
     IToken signatureEllipsis = null;
     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"
      | "returns"           (. SemErr(t, "iterators don't have a 'returns' clause; did you mean 'yields'?"); .)
      )
      Formals<false, true, outs, out openParen>
    ]
  | "..."                                       (. signatureEllipsis = t; 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>(reads, readsAttrs),
                             new Specification<FrameExpression>(mod, modAttrs),
                             new Specification<Expression>(decreases, decrAttrs),
                             req, ens, yieldReq, yieldEns,
                             body, attrs, signatureEllipsis);
     iter.BodyStartTok = bodyStart;
     iter.BodyEndTok = bodyEnd;
 .)
  .
/*------------------------------------------------------------------------*/
GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
     IToken/*!*/ id;
     TypeParameter.EqualitySupportValue eqSupport;
  .)
  "<"
  NoUSIdent<out id>          (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
  [ "(" "==" ")"             (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
    ]                        (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
  { "," NoUSIdent<out id>    (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
    [ "(" "==" ")"           (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
    ]                        (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
  }
  ">"
  .
/*------------------------------------------------------------------------*/
MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
     IToken/*!*/ id = Token.NoToken;
     bool hasName = false;  IToken keywordToken;
     Attributes attrs = null;
     List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();
     IToken openParen;
     List<Formal/*!*/> ins = new List<Formal/*!*/>();
     List<Formal/*!*/> outs = new List<Formal/*!*/>();
     List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();
     List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
     List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();
     List<Expression/*!*/> dec = new List<Expression/*!*/>();
     Attributes decAttrs = null;
     Attributes modAttrs = null;
     BlockStmt body = null;
     bool isLemma = false;
     bool isConstructor = false;
     bool isCoLemma = false;
     IToken signatureEllipsis = null;
     IToken bodyStart = Token.NoToken;
     IToken bodyEnd = Token.NoToken;
  .)
  SYNC
  ( "method"
  | "lemma"                         (. isLemma = true; .)
  | "colemma"                       (. isCoLemma = true; .)
  | "comethod"                      (. isCoLemma = true;
                                       errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");
                                    .)
  | "constructor"                   (. if (allowConstructor) {
                                         isConstructor = true;
                                       } else {
                                         SemErr(t, "constructors are allowed only in classes");
                                       }
                                    .)
  )                                 (. keywordToken = t; .)
  (. if (isLemma) {
       if (mmod.IsGhost) {
         SemErr(t, "lemmas cannot be declared 'ghost' (they are automatically 'ghost')");
       }
     } else if (isConstructor) {
       if (mmod.IsGhost) {
         SemErr(t, "constructors cannot be declared 'ghost'");
       }
       if (mmod.IsStatic) {
         SemErr(t, "constructors cannot be declared 'static'");
       }
     } else if (isCoLemma) {
       if (mmod.IsGhost) {
         SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')");
       }
     }
  .)
  { Attribute<ref attrs> }
  [ NoUSIdent<out id>               (. hasName = true; .)
  ]
  (. if (!hasName) {
       id = keywordToken;
       if (!isConstructor) {
         SemErr(la, "a method must be given a name (expecting identifier)");
       }
     }
  .)
  (
    [ GenericParameters<typeArgs> ]
    Formals<true, !mmod.IsGhost, ins, out openParen>
    [ "returns"                                 (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
      Formals<false, !mmod.IsGhost, outs, out openParen>
    ]
  | "..."                                       (. signatureEllipsis = t; openParen = Token.NoToken; .)
  )
  { MethodSpec<req, mod, ens, dec, ref decAttrs, ref modAttrs> }
  [ BlockStmt<out body, out bodyStart, out bodyEnd>
  ]
  (.
     if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {
        SemErr(t, "only ghost methods can have the :axiom attribute");
     }

     if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {
        SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");
     }

     IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
     if (isConstructor) {
       m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
                           req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
     } else if (isCoLemma) {
       m = new CoLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,
                       req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
     } else if (isLemma) {
       m = new Lemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,
                     req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
     } else {
       m = new Method(tok, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
                      req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
     }
     m.BodyStartTok = bodyStart;
     m.BodyEndTok = bodyEnd;
 .)
  .
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;
  .)
  SYNC
  ( "modifies" { IF(IsAttribute()) Attribute<ref modAttrs> }
               [ FrameExpression<out fe>                     (. mod.Add(fe); .)
                 { "," FrameExpression<out fe>               (. mod.Add(fe); .)
                 }
               ] SYNC ";"
  | [ "free"                                                 (. isFree = true; .)
    ]
    ( "requires" Expression<out e, false, true> SYNC ";"           (. req.Add(new MaybeFreeExpression(e, isFree)); .)
    | "ensures"
      { IF(IsAttribute()) Attribute<ref ensAttrs> }
      Expression<out e, false, true> SYNC ";"                      (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)
    )
  | "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, false, true> 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, false, true> 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; .)
  [
    GIdentType<allowGhostKeyword, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
    { "," GIdentType<allowGhostKeyword, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
    }
  ]
  ")"
  .
FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; .)
  "("
  [
    TypeIdentOptional<out id, out name, out ty, out isGhost>        (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
    { "," TypeIdentOptional<out id, out name, out ty, out isGhost>  (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
    }
  ]
  ")"
  .
/*------------------------------------------------------------------------*/
Type<out Type ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)
  TypeAndToken<out tok, out ty>
  .

TypeAndToken<out IToken tok, out Type ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
     tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
     List<Type> gt = null;
  .)
  ( "bool"                          (. tok = t; .)
  | "nat"                           (. tok = t;  ty = new NatType(); .)
  | "int"                           (. tok = t;  ty = new IntType(); .)
  | "real"                          (. tok = t;  ty = new RealType(); .)
  | "set"                           (. tok = t;  gt = new List<Type/*!*/>(); .)
    [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {
                                         SemErr("set type expects only one type argument");
                                       }
                                       ty = new SetType(gt.Count == 1 ? gt[0] : null);
                                    .)
  | "multiset"                      (. tok = t;  gt = new List<Type/*!*/>(); .)
    [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {
                                         SemErr("multiset type expects only one type argument");
                                       }
                                       ty = new MultiSetType(gt.Count == 1 ? gt[0] : null);
                                    .)
  | "seq"                           (. tok = t;  gt = new List<Type/*!*/>(); .)
    [ GenericInstantiation<gt> ]    (. if (gt.Count > 1) {
                                         SemErr("seq type expects only one type argument");
                                       }
                                       ty = new SeqType(gt.Count == 1 ? gt[0] : null);
                                    .)
  | "map"                           (. tok = t;  gt = new List<Type/*!*/>(); .)
    [ GenericInstantiation<gt> ]    (. if (gt.Count == 0) {
                                         ty = new MapType(null, null);
                                       } else if (gt.Count != 2) {
                                         SemErr("map type expects two type arguments");
                                         ty = new MapType(gt[0], gt.Count == 1 ? new InferredTypeProxy() : gt[1]);
                                       } else {
                                         ty = new MapType(gt[0], gt[1]);
                                       }
                                    .)
  | "("                             (. tok = t; gt = new List<Type>(); .)
    [ Type<out ty>                  (. gt.Add(ty); .)
      { "," Type<out ty>            (. gt.Add(ty); .)
      }
    ]
    ")"                             (. if (gt.Count == 1) {
                                         // just return the type 'ty'
                                       } else {
                                         // make sure the nullary tuple type exists
                                         var dims = gt.Count;
                                         var tmp = theBuiltIns.TupleType(tok, dims, true);
                                         ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());
                                       }
                                    .)
    | ReferenceType<out tok, out ty>
  )
  [ (. Type t2; .)
    "->"                  (. tok = t; .)
    Type<out t2>
    (. if (gt == null) {
         gt = new List<Type>{ ty };
       }
       ty = new ArrowType(tok, gt, t2);
       theBuiltIns.CreateArrowTypeDecl(gt.Count);
    .)
  ]

  .
ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
     tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
     List<Type> gt;
     List<IToken> path;
  .)
  ( "object"                        (. tok = t;  ty = new ObjectType(); .)
  | arrayToken                      (. tok = t;  gt = new List<Type>(); .)
    [ GenericInstantiation<gt> ]    (. int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
                                       ty = theBuiltIns.ArrayType(tok, dims, gt, true);
                                    .)
  | Ident<out tok>                  (. gt = new List<Type>();
                                       path = new List<IToken>(); .)
    {                               (. path.Add(tok); .)
      "." Ident<out tok>
    }
    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, path); .)
  )
  .
GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
  "<"
    Type<out ty>                     (. gt.Add(ty); .)
    { "," Type<out ty>               (. gt.Add(ty); .)
    }
  ">"
  .
/*------------------------------------------------------------------------*/
FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
= (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
     Attributes attrs = null;
     IToken/*!*/ id = Token.NoToken;  // to please compiler
     List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
     List<Formal/*!*/> formals = new List<Formal/*!*/>();
     Type/*!*/ returnType = new BoolType();
     List<Expression/*!*/> reqs = new List<Expression/*!*/>();
     List<Expression/*!*/> ens = new List<Expression/*!*/>();
     List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
     List<Expression/*!*/> decreases;
     Expression body = null;
     bool isPredicate = false;  bool isCoPredicate = false;
     bool isFunctionMethod = false;
     IToken openParen = null;
     IToken bodyStart = Token.NoToken;
     IToken bodyEnd = Token.NoToken;
     IToken signatureEllipsis = null;
  .)
  /* ----- function ----- */
  ( "function"
    [ "method"                 (. isFunctionMethod = true; .)
    ]
    (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
    .)
    { Attribute<ref attrs> }
    NoUSIdent<out id>
    (
      [ GenericParameters<typeArgs> ]
      Formals<true, isFunctionMethod, formals, out openParen>
      ":"
      Type<out returnType>
    | "..."                    (. signatureEllipsis = t;
                                  openParen = Token.NoToken; .)
    )

  /* ----- predicate ----- */
  | "predicate"                (. isPredicate = true; .)
    [ "method"                 (. isFunctionMethod = true; .)
    ]
    (. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
    .)
    { Attribute<ref attrs> }
    NoUSIdent<out id>
    (
      [ GenericParameters<typeArgs> ]
      [ Formals<true, isFunctionMethod, formals, out openParen>
        [ ":"                  (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
        ]
      ]
    | "..."                    (. signatureEllipsis = t;
                                  openParen = Token.NoToken; .)
    )

  /* ----- copredicate ----- */
  | "copredicate"              (. isCoPredicate = true; .)
    (. if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
    .)
    { Attribute<ref attrs> }
    NoUSIdent<out id>
    (
      [ GenericParameters<typeArgs> ]
      [ Formals<true, isFunctionMethod, formals, out openParen>
        [ ":"                  (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)
        ]
      ]
    | "..."                    (. signatureEllipsis = t;
                                  openParen = Token.NoToken; .)
    )
  )

  (. decreases = isCoPredicate ? null : new List<Expression/*!*/>(); .)
  { FunctionSpec<reqs, reads, ens, decreases> }
  [ FunctionBody<out body, out bodyStart, out bodyEnd>
  ]
  (. if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {
        SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");
     }

     IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
     if (isPredicate) {
        f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);
     } else if (isCoPredicate) {
        f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, openParen, formals,
                          reqs, reads, ens, body, attrs, signatureEllipsis);
     } else {
        f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,
                         reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);
     }
     f.BodyStartTok = bodyStart;
     f.BodyEndTok = bodyEnd;
     theBuiltIns.CreateArrowTypeDecl(formals.Count);
     if (isCoPredicate) {
       // also create an arrow type for the corresponding prefix predicate
       theBuiltIns.CreateArrowTypeDecl(formals.Count);
     }
  .)
  .
FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs));
     Contract.Requires(cce.NonNullElements(reads));
     Contract.Requires(decreases == null || cce.NonNullElements(decreases));
     Expression/*!*/ e;  FrameExpression/*!*/ fe; .)
  (
    SYNC
    "requires" Expression<out e, false, true> SYNC ";"     (. reqs.Add(e); .)
  | "reads" [ PossiblyWildFrameExpression<out fe>              (. reads.Add(fe); .)
              { "," PossiblyWildFrameExpression<out fe>        (. reads.Add(fe); .)
              }
            ] SYNC ";"
  | "ensures" Expression<out e, false, true> SYNC ";"      (. ens.Add(e); .)
  | "decreases"                               (. if (decreases == null) {
                                                   SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
                                                   decreases = new List<Expression/*!*/>();
                                                 }
                                              .)
    DecreasesList<decreases, false> SYNC ";"
  )
  .

LambdaSpec<.out Expression req, List<FrameExpression> reads.>
= (. Contract.Requires(reads != null);
     Expression e; req = null;  FrameExpression fe; .)
  { ( "requires" Expression<out e, false, false>
        (. if (req == null) {
             req = e;
           } else {
             req = new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, e);
           }
        .)
    | "reads" PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
    )
  }
  .

PossiblyWildExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
     e = dummyExpr; .)
  /* A decreases clause on a loop asks that no termination check be performed.
   * Use of this feature is sound only with respect to partial correctness.
   */
  ( "*"                        (. e = new WildcardExpr(t); .)
  | Expression<out e, false, false>
  )
  .
PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)
  /* A reads clause can list a wildcard, which allows the enclosing function to
   * read anything.  In many cases, and in particular in all cases where
   * the function is defined recursively, this makes it next to impossible to make
   * any use of the function.  Nevertheless, as an experimental feature, the
   * language allows it (and it is sound).
   */
  ( "*"                        (. fe = new FrameExpression(t, new WildcardExpr(t), null); .)
  | FrameExpression<out fe>
  )
  .
FrameExpression<out FrameExpression/*!*/ fe>
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null);
     Expression/*!*/ e;
     IToken/*!*/ id;
     string fieldName = null;  IToken feTok = null;
     fe = null;
  .)
  (( Expression<out e, false, false>   (. feTok = e.tok; .)
     [ "`" Ident<out id>        (. fieldName = id.val;  feTok = id; .)
     ]
                                (. fe = new FrameExpression(feTok, e, fieldName); .)
   )
  |
   (  "`" Ident<out id>         (. fieldName = id.val; .)
                                (. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .)
  ))
  .
FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
  "{"                         (. bodyStart = t; .)
  Expression<out e, true, true>
  "}"                         (. bodyEnd = t; .)
  .
/*------------------------------------------------------------------------*/
BlockStmt<out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
     List<Statement/*!*/> body = new List<Statement/*!*/>();
  .)
  "{"                                  (. bodyStart = t; .)
  { Stmt<body>
  }
  "}"                                  (. bodyEnd = t;
                                          block = new BlockStmt(bodyStart, bodyEnd, body); .)
  .
Stmt<.List<Statement/*!*/>/*!*/ ss.>
= (. Statement/*!*/ s;
  .)
  OneStmt<out s>                                (. ss.Add(s); .)
  .
OneStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  IToken/*!*/ id;  string label = null;
     s = dummyStmt;  /* to please the compiler */
     BlockStmt bs;
     IToken bodyStart, bodyEnd;
     int breakCount;
  .)
  SYNC
  ( BlockStmt<out bs, out bodyStart, out bodyEnd>  (. s = bs; .)
  | AssertStmt<out s>
  | AssumeStmt<out s>
  | PrintStmt<out s>
  | UpdateStmt<out s>
  | VarDeclStatement<out s>
  | IfStmt<out s>
  | WhileStmt<out s>
  | MatchStmt<out s>
  | ForallStmt<out s>
  | CalcStmt<out s>
  | ModifyStmt<out s>
  | "label"                            (. x = t; .)
    NoUSIdent<out id> ":"
    OneStmt<out s>                     (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)
  | "break"                            (. x = t; breakCount = 1; label = null; .)
    ( NoUSIdent<out id>                    (. label = id.val; .)
    | { "break"                        (. breakCount++; .)
      }
    )
    SYNC
    ";"                                (. s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount); .)
  | ReturnStmt<out s>
  | SkeletonStmt<out s>
  )
  .

SkeletonStmt<out Statement s>
= (. List<IToken> names = null;
     List<Expression> exprs = null;
     IToken tok, dotdotdot, whereTok;
     Expression e; .)
  "..."                                (. dotdotdot = t; .)
  ["where"                             (. names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;.)
     Ident<out tok>                    (. names.Add(tok); .)
     {"," Ident<out tok>               (. names.Add(tok); .)
     }
     ":="
     Expression<out e, false, true>          (. exprs.Add(e); .)
     {"," Expression<out e, false, true>     (. exprs.Add(e); .)
     }
                                       (. if (exprs.Count != names.Count) {
                                            SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");
                                            names = null; exprs = null;
                                          }
                                       .)
  ]
  ";"
  (. s = new SkeletonStatement(dotdotdot, t, names, exprs); .)
  .
ReturnStmt<out Statement/*!*/ s>
= (.
   IToken returnTok = null;
   List<AssignmentRhs> rhss = null;
   AssignmentRhs r;
   bool isYield = false;
   .)
  ( "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); .)
        }
  ]
  ";"                                (. if (isYield) {
                                          s = new YieldStmt(returnTok, t, rhss);
                                        } else {
                                          s = new ReturnStmt(returnTok, t, rhss);
                                        }
                                     .)
  .
UpdateStmt<out Statement/*!*/ s>
= (. List<Expression> lhss = new List<Expression>();
     List<AssignmentRhs> rhss = new List<AssignmentRhs>();
     Expression e;  AssignmentRhs r;
     Expression lhs0;
     IToken x, endTok = Token.NoToken;
     Attributes attrs = null;
     IToken suchThatAssume = null;
     Expression suchThat = null;
  .)
  Lhs<out e>                       (. x = e.tok; .)
  ( { Attribute<ref attrs> }
    ";"                            (. endTok = t; rhss.Add(new ExprRhs(e, attrs)); .)
  |                                (. lhss.Add(e);  lhs0 = e; .)
    { "," Lhs<out e>               (. lhss.Add(e); .)
    }
    ( ":="                         (. x = t; .)
      Rhs<out r, lhs0>             (. rhss.Add(r); .)
      { "," Rhs<out r, lhs0>       (. rhss.Add(r); .)
      }
    | ":|"                         (. x = t; .)
      [ "assume"                   (. suchThatAssume = t; .)
      ]
      Expression<out suchThat, false, true>
    )
    ";"                            (. endTok = t; .)
  | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
  )
  (. if (suchThat != null) {
       s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
     } else {
       if (lhss.Count == 0 && rhss.Count == 0) {
         s = new BlockStmt(x, endTok, new List<Statement>()); // error, give empty statement
       } else {
         s = new UpdateStmt(x, endTok, lhss, rhss);
       }
     }
  .)
  .
Rhs<out AssignmentRhs r, Expression receiverForInitCall>
= (. Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);
     IToken/*!*/ x, newToken;  Expression/*!*/ e;
     Type ty = null;
     List<Expression> ee = null;
     List<Expression> args = null;
     r = dummyRhs;  // to please compiler
     Attributes attrs = null;
  .)
  ( "new"                              (. newToken = t; .)
    TypeAndToken<out x, out ty>
    [ "["                              (. ee = new List<Expression>(); .)
      Expressions<ee>
      "]"                              (. // make sure an array class with this dimensionality exists
                                          var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
                                       .)
    |                                  (. x = null; args = new List<Expression/*!*/>(); .)
      [ "." Ident<out x> ]
      "("
        [ Expressions<args> ]
      ")"
    ]
    (. if (ee != null) {
         r = new TypeRhs(newToken, ty, ee);
       } else if (args != null) {
         r = new TypeRhs(newToken, ty, x == null ? null : x.val, receiverForInitCall, args);
       } else {
         r = new TypeRhs(newToken, ty);
       }
    .)
  | "*"                                (. r = new HavocRhs(t); .)
  | Expression<out e, false, true>           (. r = new ExprRhs(e); .)
  )
  { Attribute<ref attrs> }             (. r.Attributes = attrs; .)
  .
VarDeclStatement<.out Statement/*!*/ s.>
= (. IToken x = null, assignTok = null;  bool isGhost = false;
     LocalVariable d;
     AssignmentRhs r;  IdentifierExpr lhs0;
     List<LocalVariable> lhss = new List<LocalVariable>();
     List<AssignmentRhs> rhss = new List<AssignmentRhs>();
     IToken suchThatAssume = null;
     Expression suchThat = null;
     Attributes attrs = null;
     IToken endTok;
  .)
  [ "ghost"                                 (. isGhost = true;  x = t; .)
  ]
  "var"                                     (. if (!isGhost) { x = t; } .)
  { Attribute<ref attrs> }
  LocalIdentTypeOptional<out d, isGhost>    (. lhss.Add(d); d.Attributes = attrs; attrs = null; .)
  { ","
    { Attribute<ref attrs> }
    LocalIdentTypeOptional<out d, isGhost>  (. lhss.Add(d); d.Attributes = attrs; attrs = null; .)
  }
  [ ":="                           (. assignTok = t;
                                      lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
                                   .)
    Rhs<out r, lhs0>               (. rhss.Add(r); .)
    { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)
    }
  | ":|"                           (. assignTok = t; .)
    [ "assume"                     (. suchThatAssume = t; .)
    ]
    Expression<out suchThat, false, true>
  ]
  ";"                              (. endTok = t; .)
  (. ConcreteUpdateStatement update;
     if (suchThat != null) {
       var ies = new List<Expression>();
       foreach (var lhs in lhss) {
         ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
       }
       update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume);
     } else if (rhss.Count == 0) {
       update = null;
     } else {
       var ies = new List<Expression>();
       foreach (var lhs in lhss) {
         ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
       }
       update = new UpdateStmt(assignTok, endTok, ies, rhss);
     }
     s = new VarDeclStmt(x, endTok, lhss, update);
  .)
  .
IfStmt<out Statement/*!*/ ifStmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
     Expression guard = null;  IToken guardEllipsis = null;
     BlockStmt/*!*/ thn;
     BlockStmt/*!*/ bs;
     Statement/*!*/ s;
     Statement els = null;
     IToken bodyStart, bodyEnd, endTok;
     List<GuardedAlternative> alternatives;
     ifStmt = dummyStmt;  // to please the compiler
  .)
  "if"                       (. x = t; .)
  (
    IF(IsAlternative())
    AlternativeBlock<out alternatives, out endTok>
    (. ifStmt = new AlternativeStmt(x, endTok, alternatives); .)
  |
    ( Guard<out guard>
    | "..."                  (. guardEllipsis = t; .)
    )
    BlockStmt<out thn, out bodyStart, out bodyEnd>    (. endTok = thn.EndTok; .)
    [ "else"
      ( IfStmt<out s>                                 (. els = s; endTok = s.EndTok; .)
      | BlockStmt<out bs, out bodyStart, out bodyEnd> (. els = bs; endTok = bs.EndTok; .)
      )
    ]
    (. if (guardEllipsis != null) {
         ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
       } else {
         ifStmt = new IfStmt(x, endTok, guard, thn, els);
       }
    .)
  )
  .
AlternativeBlock<.out List<GuardedAlternative> alternatives, out IToken endTok.>
= (. alternatives = new List<GuardedAlternative>();
     IToken x;
     Expression e;
     List<Statement> body;
  .)
  "{"
  { "case"                      (. x = t; .)
    Expression<out e, true, false> // NB: don't allow lambda here
    "=>"
    (. body = new List<Statement>(); .)
    { Stmt<body> }
    (. alternatives.Add(new GuardedAlternative(x, e, body)); .)
  }
  "}"                           (. endTok = t; .)
  .
WhileStmt<out Statement/*!*/ stmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
     Expression guard = null;  IToken guardEllipsis = null;
     List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
     List<Expression/*!*/> decreases = new List<Expression/*!*/>();
     Attributes decAttrs = null;
     Attributes modAttrs = null;
     List<FrameExpression/*!*/> mod = null;
     BlockStmt/*!*/ body = null;  IToken bodyEllipsis = null;
     IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken;
     List<GuardedAlternative> alternatives;
     stmt = dummyStmt;  // to please the compiler
  .)
  "while"                    (. x = t; .)
  (
    IF(IsLoopSpecOrAlternative())
    LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
    AlternativeBlock<out alternatives, out endTok>
    (. stmt = new AlternativeLoopStmt(x, endTok, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); .)
  |
    ( Guard<out guard>           (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
    | "..."                      (. guardEllipsis = t; .)
    )
    LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
    ( BlockStmt<out body, out bodyStart, out bodyEnd>  (. endTok = body.EndTok; .)
    | "..."                      (. bodyEllipsis = t; endTok = t; .)
    )
    (.
      if (guardEllipsis != null || bodyEllipsis != null) {
        if (mod != null) {
          SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
        }
        if (body == null) {
          body = new BlockStmt(x, endTok, new List<Statement>());
        }
        stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);
        stmt = new SkeletonStatement(stmt, guardEllipsis, bodyEllipsis);
      } else {
        // The following statement protects against crashes in case of parsing errors
        body = body ?? new BlockStmt(x, endTok, new List<Statement>());
        stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
      }
    .)
  )
  .
LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs.>
= (. FrameExpression/*!*/ fe;
     invariants = new List<MaybeFreeExpression/*!*/>();
     MaybeFreeExpression invariant = null;
     decreases = new List<Expression/*!*/>();
     mod = null;
  .)
  {
    Invariant<out invariant> SYNC ";"   (. invariants.Add(invariant); .)
  | SYNC "decreases"
    { IF(IsAttribute()) Attribute<ref decAttrs> }
    DecreasesList<decreases, true> SYNC ";"
  | SYNC "modifies"
    { IF(IsAttribute()) Attribute<ref modAttrs> } (. mod = mod ?? new List<FrameExpression>(); .)
    [ FrameExpression<out fe>                     (. mod.Add(fe); .)
      { "," FrameExpression<out fe>               (. mod.Add(fe); .)
      }
    ] SYNC ";"
  }
  .
Invariant<out MaybeFreeExpression/*!*/ invariant>
= (. bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; .)
    SYNC
    ["free"                            (. isFree = true; .)
    ]
    "invariant" { IF(IsAttribute()) Attribute<ref attrs> }
    Expression<out e, false, true>           (. invariant = new MaybeFreeExpression(e, isFree, attrs); .)
  .
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
  PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {
                                              SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");
                                            } else {
                                              decreases.Add(e);
                                            }
                                         .)
  { "," PossiblyWildExpression<out e>    (. if (!allowWildcard && e is WildcardExpr) {
                                              SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");
                                            } else {
                                              decreases.Add(e);
                                            }
                                         .)
  }
  .
Guard<out Expression e>   /* null represents demonic-choice */
= (. Expression/*!*/ ee;  e = null; .)
  ( "*"                             (. e = null; .)
  | IF(IsParenStar())  "(" "*" ")"  (. e = null; .)
  | Expression<out ee, true, true>        (. e = ee; .)
  )
  .
MatchStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
     Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;
     List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
     bool usesOptionalBrace = false;
  .)
  "match"                     (. x = t; .)
  Expression<out e, true, true>
  [ "{"                                     (. usesOptionalBrace = true; .)
  ]
  { CaseStatement<out c>     (. cases.Add(c); .)
  }
  ( IF(CloseOptionalBrace(usesOptionalBrace))
    "}"
  |                                         (. if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } .)
  )
  (. s = new MatchStmt(x, t, e, cases, usesOptionalBrace); .)
  .
CaseStatement<out MatchCaseStmt/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
     IToken/*!*/ x, id;
     List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
     BoundVar/*!*/ bv;
     List<Statement/*!*/> body = new List<Statement/*!*/>();
  .)
  "case"                      (. x = t; .)
  Ident<out id>
  [ "("
    IdentTypeOptional<out bv>        (. arguments.Add(bv); .)
    { "," IdentTypeOptional<out bv>  (. arguments.Add(bv); .)
    }
  ")" ]
  "=>"
    { Stmt<body> }
  (. c = new MatchCaseStmt(x, id.val, arguments, body); .)
  .
/*------------------------------------------------------------------------*/
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
     Expression e = dummyExpr; Attributes attrs = null;
     IToken dotdotdot = null;
  .)
  "assert"                                     (. x = t; .)
  { IF(IsAttribute()) Attribute<ref attrs> }
  ( Expression<out e, false, true>
  | "..."                                      (. dotdotdot = t; .)
  )
  ";"
  (. if (dotdotdot != null) {
       s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
     } else {
       s = new AssertStmt(x, t, e, attrs);
     }
  .)
  .
AssumeStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
     Expression e = dummyExpr; Attributes attrs = null;
     IToken dotdotdot = null;
  .)
  "assume"                                     (. x = t; .)
  { IF(IsAttribute()) Attribute<ref attrs> }
  ( Expression<out e, false, true>
  | "..."                                      (. dotdotdot = t; .)
  )
  ";"
  (. if (dotdotdot != null) {
       s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
     } else {
       s = new AssumeStmt(x, t, e, attrs);
     }
  .)
  .
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;
     List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
  .)
  "print"                                      (. x = t; .)
  AttributeArg<out arg, false>                 (. args.Add(arg); .)
  { "," AttributeArg<out arg, false>           (. args.Add(arg); .)
  }
  ";"                                          (. s = new PrintStmt(x, t, args); .)
  .

ForallStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
     IToken/*!*/ x = Token.NoToken;
     bool usesOptionalParen = false;
     List<BoundVar/*!*/> bvars = null;
     Attributes attrs = null;
     Expression range = null;
     var ens = new List<MaybeFreeExpression/*!*/>();
     bool isFree;
     Expression/*!*/ e;
     BlockStmt block = null;
     IToken bodyStart, bodyEnd;
     IToken tok = Token.NoToken;
  .)
  ( "forall"                                  (. x = t; tok = x; .)
  | "parallel"                                (. x = t;
                                                 errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
                                              .)
  )
  [ "("                                     (. usesOptionalParen = true; .)
  ]
  [                                         (. List<BoundVar/*!*/> bvarsX;  Attributes attrsX;  Expression rangeX; .)
    QuantifierDomain<out bvarsX, out attrsX, out rangeX>
                                            (. bvars = bvarsX; attrs = attrsX; range = rangeX;
                                            .)
  ]
                                            (. if (bvars == null) { bvars = new List<BoundVar>(); }
                                               if (range == null) { range = new LiteralExpr(x, true); }
                                            .)
  ( IF(CloseOptionalParen(usesOptionalParen))
    ")"
  |                                         (. if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } .)
  )
  {                                         (. isFree = false; .)
    [ "free"                                (. isFree = true; .)
    ]
    "ensures" Expression<out e, false, true>      (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
    ";"                                     (. tok = t; .)
  }
  [ BlockStmt<out block, out bodyStart, out bodyEnd>
  ]
  (. if (DafnyOptions.O.DisallowSoundnessCheating && block == null && 0 < ens.Count) {
        SemErr(t, "a forall statement with an ensures clause must have a body");
     }

     if (block != null) {
        tok = block.EndTok;
     }
     s = new ForallStmt(x, tok, bvars, attrs, range, ens, block);
  .)
  .

ModifyStmt<out Statement s>
= (. IToken tok;  IToken endTok = Token.NoToken;
     Attributes attrs = null;
     FrameExpression fe;  var mod = new List<FrameExpression>();
     BlockStmt body = null;  IToken bodyStart;
     IToken ellipsisToken = null;
  .)
  "modify"           (. tok = t; .)
  { IF(IsAttribute()) Attribute<ref attrs> }
  /* Note, there is an ambiguity here, because a curly brace may look like a FrameExpression and
   * may also look like a BlockStmt.  We're happy to parse the former, because if the user intended
   * the latter, then an explicit FrameExpression of {} could be given.
   */
  [ FrameExpression<out fe>         (. mod.Add(fe); .)
    { "," FrameExpression<out fe>   (. mod.Add(fe); .)
    }
  | "..."                           (. ellipsisToken = t; .)
  ]
  ( BlockStmt<out body, out bodyStart, out endTok>
  | SYNC ";"         (. endTok = t; .)
  )
  (. s = new ModifyStmt(tok, endTok, mod, attrs, body);
     if (ellipsisToken != null) {
       s = new SkeletonStatement(s, ellipsisToken, null);
     }
  .)
  .

CalcStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
     Token x;
     CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
     var lines = new List<Expression/*!*/>();
     var hints = new List<BlockStmt/*!*/>();
     CalcStmt.CalcOp stepOp;
     var stepOps = new List<CalcStmt.CalcOp>();
     CalcStmt.CalcOp maybeOp;
     Expression/*!*/ e;
     BlockStmt/*!*/ h;
     IToken opTok;
     IToken danglingOperator = null;
  .)
  "calc"                                                  (. x = t; .)
  [ CalcOp<out opTok, out calcOp>                         (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)
                                                             if (maybeOp == null) {
                                                               SemErr(opTok, "the main operator of a calculation must be transitive");
                                                             }
                                                             resOp = calcOp;
                                                          .)
  ]
  "{"
  { Expression<out e, false, true>                              (. lines.Add(e); stepOp = calcOp; danglingOperator = null; .)
    ";"
    [ CalcOp<out opTok, out op>                           (. maybeOp = resOp.ResultOp(op);
                                                             if (maybeOp == null) {
                                                               SemErr(opTok, "this operator cannot continue this calculation");
                                                             } else {
                                                               stepOp = op;
                                                               resOp = maybeOp;
                                                               danglingOperator = opTok;
                                                             }
                                                          .)
    ]                                                   (. stepOps.Add(stepOp); .)
    Hint<out h>                                         (. hints.Add(h);
                                                           if (h.Body.Count != 0) { danglingOperator = null; }
                                                        .)
  }
  "}"
  (.
    if (danglingOperator != null) {
      SemErr(danglingOperator, "a calculation cannot end with an operator");
    }
    if (lines.Count > 0) {
      // Repeat the last line to create a dummy line for the dangling hint
      lines.Add(lines[lines.Count - 1]);
    }
    s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);
  .)
  .
CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
= (. var binOp = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
     Expression k = null;
     x = null;
  .)
  ( "=="           (. x = t;  binOp = BinaryExpr.Opcode.Eq; .)
    [ "#" "[" Expression<out k, true, true> "]" ]
  | "<"            (. x = t;  binOp = BinaryExpr.Opcode.Lt; .)
  | ">"            (. x = t;  binOp = BinaryExpr.Opcode.Gt; .)
  | "<="           (. x = t;  binOp = BinaryExpr.Opcode.Le; .)
  | ">="           (. x = t;  binOp = BinaryExpr.Opcode.Ge; .)
  | "!="           (. x = t;  binOp = BinaryExpr.Opcode.Neq; .)
  | '\u2260'       (. x = t;  binOp = BinaryExpr.Opcode.Neq; .)
  | '\u2264'       (. x = t;  binOp = BinaryExpr.Opcode.Le; .)
  | '\u2265'       (. x = t;  binOp = BinaryExpr.Opcode.Ge; .)
  | EquivOp        (. x = t;  binOp = BinaryExpr.Opcode.Iff; .)
  | ImpliesOp      (. x = t;  binOp = BinaryExpr.Opcode.Imp; .)
  | ExpliesOp      (. x = t;  binOp = BinaryExpr.Opcode.Exp; .)
  )
  (.
    if (k == null) {
      op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
    } else {
      op = new Microsoft.Dafny.CalcStmt.TernaryCalcOp(k);
    }
  .)
  .
Hint<out BlockStmt s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
     var subhints = new List<Statement/*!*/>();
     IToken bodyStart, bodyEnd;
     BlockStmt/*!*/ block;
     Statement/*!*/ calc;
     Token x = la;
     IToken endTok = x;
  .)
  { BlockStmt<out block, out bodyStart, out bodyEnd>  (. endTok = block.EndTok; subhints.Add(block); .)
  | CalcStmt<out calc>                                (. endTok = calc.EndTok; subhints.Add(calc); .)
  }
  (. s = new BlockStmt(x, endTok, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
  .)
  .
/*------------------------------------------------------------------------*/
/* The "allowSemi" argument says whether or not the top-level expression
 * to be parsed is allowed to have the form S;E where S is a call to a lemma.
 * "allowSemi" should be passed in as "false" whenever the expression to
 * be parsed sits in a context that itself is terminated by a semi-colon.
 *
 * The "allowLambda" is there to be able to parse "case x => e".
 * Directly after the case keyword, you cannot do identifier-sequence-lambdas.
 */
Expression<out Expression e, bool allowSemi, bool allowLambda>
= (. Expression e0; IToken endTok; .)
  EquivExpression<out e, allowSemi, allowLambda>
  [ IF(SemiFollowsCall(allowSemi, e))
    ";"                       (. endTok = t; .)
    Expression<out e0, allowSemi, allowLambda>
    (. e = new StmtExpr(e.tok,
             new UpdateStmt(e.tok, endTok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),
             e0);
    .)
  ]
  .
/*------------------------------------------------------------------------*/
EquivExpression<out Expression e0, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
  ImpliesExpliesExpression<out e0, allowSemi, allowLambda>
  { EquivOp                                                   (. x = t; .)
    ImpliesExpliesExpression<out e1, allowSemi, allowLambda>  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
  }
  .
EquivOp = "<==>" | '\u21d4'.
/*------------------------------------------------------------------------*/
ImpliesExpliesExpression<out Expression e0, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
  LogicalExpression<out e0, allowSemi, allowLambda>
  [ ImpliesOp                                               (. x = t; .)
    ImpliesExpression<out e1, allowSemi, allowLambda>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
  | ExpliesOp                                               (. x = t; .)
    LogicalExpression<out e1, allowSemi, allowLambda>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)
    { ExpliesOp                                             (. x = t; .)
      LogicalExpression<out e1, allowSemi, allowLambda>     (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)
    }
  ]
  .
ImpliesExpression<out Expression e0, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
  LogicalExpression<out e0, allowSemi, allowLambda>
  [ ImpliesOp                                               (. x = t; .)
    ImpliesExpression<out e1, allowSemi, allowLambda>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
  ]
  .
ImpliesOp = "==>" | '\u21d2'.
ExpliesOp = "<==" | '\u21d0'.
/*------------------------------------------------------------------------*/
LogicalExpression<out Expression e0, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
  RelationalExpression<out e0, allowSemi, allowLambda>
  [ AndOp                                                   (. x = t; .)
    RelationalExpression<out e1, allowSemi, allowLambda>    (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
    { AndOp                                                 (. x = t; .)
      RelationalExpression<out e1, allowSemi, allowLambda>  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
    }
  | OrOp                                                    (. x = t; .)
    RelationalExpression<out e1, allowSemi, allowLambda>    (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
    { OrOp                                                  (. x = t; .)
      RelationalExpression<out e1, allowSemi, allowLambda>  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
    }
  ]
  .
AndOp = "&&" | '\u2227'.
OrOp = "||" | '\u2228'.
/*------------------------------------------------------------------------*/
RelationalExpression<out Expression e, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     IToken x, firstOpTok = null;  Expression e0, e1, acc = null;  BinaryExpr.Opcode op;
     List<Expression> chain = null;
     List<BinaryExpr.Opcode> ops = null;
     List<Expression/*?*/> prefixLimits = null;
     Expression k;
     int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=
                    // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=
                    // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=
                    // 3 ("illegal")     indicates illegal chain
                    // 4 ("disjoint")    indicates chain of disjoint set operators
     bool hasSeenNeq = false;
  .)
  Term<out e0, allowSemi, allowLambda>
                                   (. e = e0; .)
  [ RelOp<out x, out op, out k>    (. firstOpTok = x; .)
    Term<out e1, allowSemi, allowLambda>
                                   (. if (k == null) {
                                        e = new BinaryExpr(x, op, e0, e1);
                                        if (op == BinaryExpr.Opcode.Disjoint)
                                          acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
                                      } else {
                                        Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
                                        e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
                                      }
                                   .)
    {                              (. if (chain == null) {
                                        chain = new List<Expression>();
                                        ops = new List<BinaryExpr.Opcode>();
                                        prefixLimits = new List<Expression>();
                                        chain.Add(e0);  ops.Add(op);  prefixLimits.Add(k);  chain.Add(e1);
                                        switch (op) {
                                          case BinaryExpr.Opcode.Eq:
                                            kind = 0;  break;
                                          case BinaryExpr.Opcode.Neq:
                                            kind = 0;  hasSeenNeq = true;  break;
                                          case BinaryExpr.Opcode.Lt:
                                          case BinaryExpr.Opcode.Le:
                                            kind = 1;  break;
                                          case BinaryExpr.Opcode.Gt:
                                          case BinaryExpr.Opcode.Ge:
                                            kind = 2;  break;
                                          case BinaryExpr.Opcode.Disjoint:
                                            kind = 4;  break;
                                          default:
                                            kind = 3;  break;
                                        }
                                      }
                                      e0 = e1;
                                   .)
      RelOp<out x, out op, out k>  (. switch (op) {
                                        case BinaryExpr.Opcode.Eq:
                                          if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }
                                          break;
                                        case BinaryExpr.Opcode.Neq:
                                          if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }
                                          if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
                                          hasSeenNeq = true;  break;
                                        case BinaryExpr.Opcode.Lt:
                                        case BinaryExpr.Opcode.Le:
                                          if (kind == 0) { kind = 1; }
                                          else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
                                          break;
                                        case BinaryExpr.Opcode.Gt:
                                        case BinaryExpr.Opcode.Ge:
                                          if (kind == 0) { kind = 2; }
                                          else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
                                          break;
                                        case BinaryExpr.Opcode.Disjoint:
                                          if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
                                          break;
                                        default:
                                          SemErr(x, "this operator cannot be part of a chain");
                                          kind = 3;  break;
                                      }
                                   .)
      Term<out e1, allowSemi, allowLambda>
                                   (. ops.Add(op); prefixLimits.Add(k); chain.Add(e1);
                                      if (k != null) {
                                        Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
                                        e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
                                      } else if (op == BinaryExpr.Opcode.Disjoint) {
                                        e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
                                        acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
                                      } else {
                                        e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
                                      }
                                   .)
    }
  ]
  (. if (chain != null) {
       e = new ChainingExpression(firstOpTok, chain, ops, prefixLimits, e);
     }
  .)
  .
RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null);
     x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/;
     IToken y;
     k = null;
  .)
  ( "=="           (. x = t;  op = BinaryExpr.Opcode.Eq; .)
    [ "#" "[" Expression<out k, true, true> "]" ]
  | "<"            (. x = t;  op = BinaryExpr.Opcode.Lt; .)
  | ">"            (. x = t;  op = BinaryExpr.Opcode.Gt; .)
  | "<="           (. x = t;  op = BinaryExpr.Opcode.Le; .)
  | ">="           (. x = t;  op = BinaryExpr.Opcode.Ge; .)
  | "!="           (. x = t;  op = BinaryExpr.Opcode.Neq; .)
    [ "#" "[" Expression<out k, true, true> "]" ]
  | "in"           (. x = t;  op = BinaryExpr.Opcode.In; .)
  | notIn          (. x = t;  op = BinaryExpr.Opcode.NotIn; .)
  | /* The next operator is "!!", but we have to scan it as two "!", since the scanner is gready
       so if "!!" is a valid token, we won't be able to scan it as two "!" when needed: */
    "!"            (. x = t;  y = Token.NoToken; .)
    [ "!"          (. y = t; .)
    ]              (. if (y == Token.NoToken) {
                        SemErr(x, "invalid RelOp");
                      } else if (y.pos != x.pos + 1) {
                        SemErr(x, "invalid RelOp (perhaps you intended \"!!\" with no intervening whitespace?)");
                      } else {
                        x.val = "!!";
                        op = BinaryExpr.Opcode.Disjoint;
                      }
                   .)
  | '\u2260'       (. x = t;  op = BinaryExpr.Opcode.Neq; .)
  | '\u2264'       (. x = t;  op = BinaryExpr.Opcode.Le; .)
  | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)
  )
  .
/*------------------------------------------------------------------------*/
Term<out Expression e0, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)
  Factor<out e0, allowSemi, allowLambda>
  { AddOp<out x, out op>
    Factor<out e1, allowSemi, allowLambda> (. e0 = new BinaryExpr(x, op, e0, e1); .)
  }
  .
AddOp<out IToken x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
  ( "+"            (. x = t;  op = BinaryExpr.Opcode.Add; .)
  | "-"            (. x = t;  op = BinaryExpr.Opcode.Sub; .)
  )
  .
/*------------------------------------------------------------------------*/
Factor<out Expression e0, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)
  UnaryExpression<out e0, allowSemi, allowLambda>
  { MulOp<out x, out op>
    UnaryExpression<out e1, allowSemi, allowLambda> (. e0 = new BinaryExpr(x, op, e0, e1); .)
  }
  .
MulOp<out IToken x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
  ( "*"            (. x = t;  op = BinaryExpr.Opcode.Mul; .)
  | "/"            (. x = t;  op = BinaryExpr.Opcode.Div; .)
  | "%"            (. x = t;  op = BinaryExpr.Opcode.Mod; .)
  )
  .
/*------------------------------------------------------------------------*/
UnaryExpression<out Expression e, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; .)
  ( "-"                                        (. x = t; .)
    UnaryExpression<out e, allowSemi, allowLambda>
                                               (. e = new NegationExpression(x, e); .)
  | NegOp                                      (. x = t; .)
    UnaryExpression<out e, allowSemi, allowLambda>
                                               (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e); .)
  | EndlessExpression<out e, allowSemi, allowLambda>
  | DottedIdentifiersAndFunction<out e, allowSemi, allowLambda>
    { Suffix<ref e> }
    ApplySuffix<ref e>
  | DisplayExpr<out e>
    { Suffix<ref e> }
  | MultiSetExpr<out e>
    { Suffix<ref e> }
  | "map"                                      (. x = t; .)
    ( MapDisplayExpr<x, out e>
      { Suffix<ref e> }
    | MapComprehensionExpr<x, out e, allowSemi>
    | (. SemErr("map must be followed by literal in brackets or comprehension."); .)
    )
  | ConstAtomExpression<out e, allowSemi, allowLambda>
    { Suffix<ref e> }
  )
  .
Lhs<out Expression e>
= (. e = dummyExpr;  // the assignment is to please the compiler, the dummy value to satisfy contracts in the event of a parse error
  .)
  ( DottedIdentifiersAndFunction<out e, false, false>
    { Suffix<ref e> }
    ApplySuffix<ref e>
  | ConstAtomExpression<out e, false, false>
    Suffix<ref e>
    { Suffix<ref e> }
  )
  .
NegOp = "!" | '\u00ac'.
/* A ConstAtomExpression is never an l-value.  Also, a ConstAtomExpression is never followed by
 * an open paren (but could very well have a suffix that starts with a period or a square bracket).
 * (The "Also..." part may change if expressions in Dafny could yield functions.)
 */
ConstAtomExpression<out Expression e, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     IToken/*!*/ x;  BigInteger n;   Basetypes.BigDec d;
     e = dummyExpr;  Type toType = null;
  .)
  ( "false"                                    (. e = new LiteralExpr(t, false); .)
  | "true"                                     (. e = new LiteralExpr(t, true); .)
  | "null"                                     (. e = new LiteralExpr(t); .)
  | Nat<out n>                                 (. e = new LiteralExpr(t, n); .)
  | Dec<out d>                                 (. e = new LiteralExpr(t, d); .)
  | "this"                                     (. e = new ThisExpr(t); .)
  | "fresh"                                    (. x = t; .)
    "(" Expression<out e, true, true> ")"            (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e); .)
  | "old"                                      (. x = t; .)
    "(" Expression<out e, true, true> ")"            (. e = new OldExpr(x, e); .)
  | "|"                                        (. x = t; .)
      Expression<out e, true, true>                  (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Cardinality, e); .)
    "|"
  | ( "int"                                    (. x = t; toType = new IntType(); .)
    | "real"                                   (. x = t; toType = new RealType(); .)
    )
    "(" Expression<out e, true, true> ")"            (. e = new ConversionExpr(x, e, toType); .)
  | ParensExpression<out e, allowSemi, allowLambda>
  )
  .

LambdaArrow<out bool oneShot>
= (. oneShot = true; .)
  ( "=>" (. oneShot = false; .)
  | "->" (. oneShot = true; .)
  )
  .

ParensExpression<out Expression e, bool allowSemi, bool allowLambda>
= (. IToken x;
     Expression ee;
     e = null;
     List<Expression> args = new List<Expression>();
     List<Type> types = new List<Type>();
     Type tt;
     bool isLambda = false;
  .)
  "("                                         (. x = t; .)
    [
      OptTypedExpr<out ee, out tt, true>       (. args.Add(ee); types.Add(tt); .)
      { "," OptTypedExpr<out ee, out tt, true> (. args.Add(ee); types.Add(tt); .)
      }
    ]
  ")"
  [ IF(IsLambda(allowLambda))
    (. Expression body = null;
       Expression req = null;
       bool oneShot;
       var reads = new List<FrameExpression>();
       x = t;
    .)
    LambdaSpec<out req, reads>
    LambdaArrow<out oneShot>
    Expression<out body, allowSemi, true>
    (. List<BoundVar> bvs = new List<BoundVar>();
       for (int i = 0; i < args.Count; i++) {
         ee = args[i];
         tt = types[i];
         if (ee is IdentifierSequence) {
           IdentifierSequence ise = (IdentifierSequence)ee;
           List<IToken> idents = ise.Tokens;
           Contract.Assert(idents != null);
           Contract.Assert(idents.Count > 0);
           IToken id = idents[0];
           if (idents.Count != 1) {
             SemErr(id, "Expected variable binding.");
           }
           if (ise.Arguments != null) {
             SemErr(ise.OpenParen, "Expected variable binding.");
           }
           bvs.Add(new BoundVar(id, UnwildIdent(id.val, true), tt ?? new InferredTypeProxy()));
         } else {
           SemErr(ee.tok, "Expected variable binding.");
         }
       }
       e = new LambdaExpr(x, oneShot, bvs, req, reads, body);
       theBuiltIns.CreateArrowTypeDecl(bvs.Count);
       isLambda = true;
    .)
  ]
  (. if (!isLambda) {
       for (int i = 0; i < args.Count; i++) {
         if (types[i] != null) {
           SemErr(args[i].tok, "Type specification not allowed here, comma separator was expected.");
         }
       }
       if (args.Count == 1) {
         e = new ParensExpression(x, args[0]);
       } else {
         // make sure the corresponding tuple type exists
         var tmp = theBuiltIns.TupleType(x, args.Count, true);
         e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);
       }
     }
  .)
  [ IF(!isLambda && args.Count == 1 && la.kind == _openparen)
    (. IToken openParen; .)
    { "(" (. openParen = t; args = new List<Expression>(); .)
      [ Expressions<args> ]
      ")"
      (. e = new ApplyExpr(x, openParen, e, args); .)
    }
  ]
  .
OptTypedExpr<out Expression e, out Type tt, bool allowSemi>
= (. tt = null; .)
  Expression<out e, allowSemi, true>
  [ ":" Type<out tt> ]
  .
DisplayExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;
     e = dummyExpr;
  .)
  ( "{"                                        (. x = t;  elements = new List<Expression/*!*/>(); .)
      [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, elements);.)
    "}"
  | "["                                        (. x = t;  elements = new List<Expression/*!*/>(); .)
      [ Expressions<elements> ]                (. e = new SeqDisplayExpr(x, elements); .)
    "]"
  )
  .
MultiSetExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;
     e = dummyExpr;
  .)
  "multiset"                                   (. x = t; .)
  ( "{"                                        (. elements = new List<Expression/*!*/>(); .)
      [ Expressions<elements> ]                (. e = new MultiSetDisplayExpr(x, elements);.)
    "}"
  | "("                                        (. x = t;  elements = new List<Expression/*!*/>(); .)
      Expression<out e, true, true>                  (. e = new MultiSetFormingExpr(x, e); .)
    ")"
  | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)
  )
  .
MapDisplayExpr<IToken/*!*/ mapToken, out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
     e = dummyExpr;
  .)
  "["
    [ MapLiteralExpressions<out elements> ]  (. e = new MapDisplayExpr(mapToken, elements);.)
  "]"
  .
MapLiteralExpressions<.out List<ExpressionPair> elements.>
= (. Expression/*!*/ d, r;
     elements = new List<ExpressionPair/*!*/>(); .)
  Expression<out d, true, true> ":=" Expression<out r, true, true>       (. elements.Add(new ExpressionPair(d,r)); .)
  { "," Expression<out d, true, true> ":=" Expression<out r, true, true> (. elements.Add(new ExpressionPair(d,r)); .)
  }
  .
MapComprehensionExpr<IToken mapToken, out Expression e, bool allowSemi>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     BoundVar bv;
     List<BoundVar> bvars = new List<BoundVar>();
     Expression range = null;
     Expression body;
  .)
  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)
  [ "|" Expression<out range, true, true> ]
  QSep
  Expression<out body, allowSemi, true>
  (. e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body);
  .)
  .
EndlessExpression<out Expression e, bool allowSemi, bool allowLambda>
= (. IToken/*!*/ x;
     Expression e0, e1;
     Statement s;
     e = dummyExpr;
  .)
  ( "if"                            (. x = t; .)
    Expression<out e, true, true>
    "then" Expression<out e0, true, true>
    "else" Expression<out e1, allowSemi, allowLambda> (. e = new ITEExpr(x, e, e0, e1); .)
  | MatchExpression<out e, allowSemi, allowLambda>
  | QuantifierGuts<out e, allowSemi, allowLambda>
  | ComprehensionExpr<out e, allowSemi, allowLambda>
  | StmtInExpr<out s>
    Expression<out e, allowSemi, allowLambda>               (. e = new StmtExpr(s.Tok, s, e); .)
  | LetExpr<out e, allowSemi, allowLambda>
  | NamedExpr<out e, allowSemi, allowLambda>
  )
  .

StmtInExpr<out Statement s>
= (. s = dummyStmt; .)
  ( AssertStmt<out s>
  | AssumeStmt<out s>
  | CalcStmt<out s>
  )
  .

LetExpr<out Expression e, bool allowSemi, bool allowLambda>
= (. IToken x = null;
     bool isGhost = false;
     var letLHSs = new List<CasePattern>();
     var letRHSs = new List<Expression>();
     CasePattern pat;
     bool exact = true;
     e = dummyExpr;
  .)
    [ "ghost"                       (. isGhost = true;  x = t; .)
    ]
    "var"                           (. if (!isGhost) { x = t; } .)
    CasePattern<out pat>            (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
                                       letLHSs.Add(pat);
                                    .)
    { "," CasePattern<out pat>      (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
                                       letLHSs.Add(pat);
                                    .)
    }
    ( ":="
    | ":|"                          (. exact = false;
                                       foreach (var lhs in letLHSs) {
                                         if (lhs.Arguments != null) {
                                           SemErr(lhs.tok, "LHS of let-such-that expression must be variables, not general patterns");
                                         }
                                       }
                                    .)
    )
    Expression<out e, false, true>        (. letRHSs.Add(e); .)
    { "," Expression<out e, false, true>  (. letRHSs.Add(e); .)
    }
    ";"
    Expression<out e, allowSemi, allowLambda>    (. e = new LetExpr(x, letLHSs, letRHSs, e, exact); .)
  .

NamedExpr<out Expression e, bool allowSemi, bool allowLambda>
= (. IToken/*!*/ x, d;
     e = dummyExpr;
     Expression expr;
  .)
    "label"                          (. x = t; .)
    NoUSIdent<out d>
    ":"
    Expression<out e, allowSemi, allowLambda>     (. expr = e;
                                        e = new NamedExpr(x, d.val, expr); .)
  .

MatchExpression<out Expression e, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;
     List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
     bool usesOptionalBrace = false;
  .)
  "match"                     (. x = t; .)
  Expression<out e, allowSemi, true>
  [ "{"                                     (. usesOptionalBrace = true; .)
  ]
  /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,
     but it's okay, because we want this closer match expression to bind as much as possible--use
     parens around it to limit its scope. */
  { CaseExpression<out c, allowSemi, usesOptionalBrace || allowLambda>
                                            (. cases.Add(c); .)
  }
  ( IF(CloseOptionalBrace(usesOptionalBrace))
    "}"
  |                                         (. if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } .)
  )
  (. e = new MatchExpr(x, e, cases, usesOptionalBrace); .)
  .
CaseExpression<out MatchCaseExpr c, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
     List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
     BoundVar/*!*/ bv;
     Expression/*!*/ body;
  .)
  "case"                      (. x = t; .)
  Ident<out id>
  [ "("
    IdentTypeOptional<out bv>        (. arguments.Add(bv); .)
    { "," IdentTypeOptional<out bv>  (. arguments.Add(bv); .)
    }
  ")" ]
  "=>"
  Expression<out body, allowSemi, allowLambda>    (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
  .
CasePattern<out CasePattern pat>
= (. IToken id;  List<CasePattern> arguments;
     BoundVar bv;
     pat = null;
  .)
  ( IF(IsIdentParen())
    Ident<out id>
    "("                                (. arguments = new List<CasePattern>(); .)
      [ CasePattern<out pat>           (. arguments.Add(pat); .)
        { "," CasePattern<out pat>     (. arguments.Add(pat); .)
        }
      ]
    ")"                                (. pat = new CasePattern(id, id.val, arguments); .)

  | IdentTypeOptional<out bv>          (. // This could be a BoundVar of a parameter-less constructor and we may not know until resolution.
                                          // Nevertheless, we do put the "bv" into the CasePattern here (even though it will get thrown out
                                          // later if resolution finds the CasePattern to denote a parameter-less constructor), because this
                                          // (in particular, bv.IsGhost) is the place where a LetExpr records whether or not the "ghost"
                                          // keyword was used in the declaration.
                                          pat = new CasePattern(bv.tok, bv);
                                       .)
  )

  .
/*------------------------------------------------------------------------*/
DottedIdentifiersAndFunction<out Expression e, bool allowSemi, bool allowLambda>
= (. IToken id, idPrime;  IToken openParen = null;
     List<Expression> args = null;
     List<IToken> idents = new List<IToken>();
     e = null;
     var applyArgLists = new List<List<Expression>>();
  .)
  Ident<out id>                              (. idents.Add(id); .)
  { IdentOrDigitsSuffix<out id, out idPrime> (. idents.Add(id);
                                                if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
                                              .)
  }
  [                                     (. args = new List<Expression>(); .)
    [ "#"                               (. id.val = id.val + "#";  Expression k; .)
      "[" Expression<out k, true, true> "]"   (. args.Add(k); .)
    ]
    "("                                 (. openParen = t; .)
      [ Expressions<args> ]
    ")"
    /*
    { "("                               (. openParen = t; var argList = new List<Expression>(); .)
      [ Expressions<argList> ]
      ")"                               (. applyArgLists.Add(argList); .)
    }
    */
  ]
  // A quick-and-dirty lambda expression?
  [ IF(IsLambda(allowLambda))
    (. Expression body = null;
       Expression req = null;
       bool oneShot;
       var reads = new List<FrameExpression>();
    .)
    LambdaSpec<out req, reads>
    LambdaArrow<out oneShot>
    Expression<out body, allowSemi, true>
    (.
       if (idents.Count != 1) {
         SemErr(id, "Invalid variable binding in lambda.");
       }
       if (args != null) {
         SemErr(openParen, "Expected variable binding.");
       }
       BoundVar bv = new BoundVar(id, UnwildIdent(id.val, true),  new InferredTypeProxy());
       e = new LambdaExpr(id, oneShot, new List<BoundVar>{ bv }, req, reads, body);
       theBuiltIns.CreateArrowTypeDecl(1);
    .)
  ]
  // If it wasn't a lambda expression, then it indeed is an identifier sequence
  (. if (e == null) {
       e = new IdentifierSequence(idents, openParen, args);
       foreach (var args_ in applyArgLists) {
         e = new ApplyExpr(id, openParen, e, args_);
       }
     }
  .)
  .
Suffix<ref Expression e>
= (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x;  List<Expression/*!*/>/*!*/ args;
     Expression e0 = null;  Expression e1 = null;  Expression/*!*/ ee;  bool anyDots = false; List<Expression> multipleLengths = null; bool takeRest = false;
     List<Expression> multipleIndices = null;
     bool func = false;
  .)
  ( IdentOrDigitsSuffix<out id, out x>         (. if (x != null) {
                                                    // process id as a Suffix in its own right
                                                    e = new ExprDotName(id, e, id.val);
                                                    id = x;  // move to the next Suffix
                                                  }
                                               .)
    [                                          (. args = new List<Expression/*!*/>();  func = true; .)
      [ "#"                                    (. id.val = id.val + "#";  Expression k; .)
        "[" Expression<out k, true, true> "]"        (. args.Add(k); .)
      ]
      "("                                      (. IToken openParen = t; .)
        [ Expressions<args> ]
      ")"                                      (. e = new FunctionCallExpr(id, id.val, e, openParen, args); .)
    ]                                          (. if (!func) { e = new ExprDotName(id, e, id.val); } .)
  | "["                                        (. x = t; .)
      ( Expression<out ee, true, true>               (. e0 = ee; .)
        ( ".."                                 (. anyDots = true; .)
          [ Expression<out ee, true, true>           (. e1 = ee; .)
          ]
        | ":="
          Expression<out ee, true, true>             (. e1 = ee; .)
        | { ":"                                (. if (multipleLengths == null) {
                                                    multipleLengths = new List<Expression>();
                                                    multipleLengths.Add(e0);
                                                  }
                                                  takeRest = true;
                                               .)
            [Expression<out ee, true, true>          (. multipleLengths.Add(ee);
                                                  takeRest = false;
                                               .)
            ]
          }
        | { "," Expression<out ee, true, true>       (. if (multipleIndices == null) {
                                                    multipleIndices = new List<Expression>();
                                                    multipleIndices.Add(e0);
                                                  }
                                                  multipleIndices.Add(ee);
                                               .)
          }
        )
      | ".."                                   (. anyDots = true; .)
        [ Expression<out ee, true, true>             (. e1 = ee; .)
        ]
      )
      (. if (multipleIndices != null) {
           e = new MultiSelectExpr(x, e, multipleIndices);
           // make sure an array class with this dimensionality exists
           var tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true);
         } else {
           if (!anyDots && e0 == null) {
             /* a parsing error occurred */
             e0 = dummyExpr;
           }
           Contract.Assert(anyDots || e0 != null);
           if (anyDots) {
             //Contract.Assert(e0 != null || e1 != null);
             e = new SeqSelectExpr(x, false, e, e0, e1);
           } else if (multipleLengths != null || takeRest) {
             Expression prev = new LiteralExpr(x, 0);
             List<Expression> seqs = new List<Expression>();
             if (multipleLengths != null)
             {
               foreach (var len in multipleLengths)
               {
                 var end = new BinaryExpr(x, BinaryExpr.Opcode.Add, prev, len);
                 seqs.Add(new SeqSelectExpr(x, false, e, prev, end));
                 prev = end;
               }
             }
             if (takeRest)
             {
               seqs.Add(new SeqSelectExpr(x, false, e, prev, null));
             }
             e = new SeqDisplayExpr(x, seqs);
           } else if (e1 == null) {
             Contract.Assert(e0 != null);
             e = new SeqSelectExpr(x, true, e, e0, null);
           } else {
             Contract.Assert(e0 != null);
             e = new SeqUpdateExpr(x, e, e0, e1);
           }
         }
      .)
    "]"
  )
  ApplySuffix<ref e>
  .

ApplySuffix<ref Expression e>
= { "("                                    (. IToken openParen = t; var args = new List<Expression>(); .)
    [ Expressions<args> ]
    ")"                                    (. e = new ApplyExpr(e.tok, openParen, e, args); .)
  }
  .

/*------------------------------------------------------------------------*/
QuantifierGuts<out Expression q, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
     bool univ = false;
     List<BoundVar/*!*/> bvars;
     Attributes attrs;
     Expression range;
     Expression/*!*/ body;
  .)
  ( Forall                                     (. x = t;  univ = true; .)
  | Exists                                     (. x = t; .)
  )
  QuantifierDomain<out bvars, out attrs, out range>
  QSep
  Expression<out body, allowSemi, allowLambda>
  (. if (univ) {
       q = new ForallExpr(x, bvars, range, body, attrs);
     } else {
       q = new ExistsExpr(x, bvars, range, body, attrs);
     }
  .)
  .

Forall = "forall" | '\u2200'.
Exists = "exists" | '\u2203'.
QSep = "::" | '\u2022'.

QuantifierDomain<.out List<BoundVar> bvars, out Attributes attrs, out Expression range.>
= (.
     bvars = new List<BoundVar>();
     BoundVar/*!*/ bv;
     attrs = null;
     range = null;
  .)
  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)
  { ","
    IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)
  }
  { IF(IsAttribute()) Attribute<ref attrs> }
  [ "|"
    Expression<out range, true, true>
  ]
  .

ComprehensionExpr<out Expression q, bool allowSemi, bool allowLambda>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
     IToken x = Token.NoToken;
     BoundVar bv;
     List<BoundVar/*!*/> bvars = new List<BoundVar>();
     Expression range;
     Expression body = null;
  .)
  "set"                                        (. x = t; .)
  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)
  { ","
    IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)
  }
  "|" Expression<out range, allowSemi, allowLambda>
  [
    QSep
    Expression<out body, allowSemi, allowLambda>
  ]
  (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
     q = new SetComprehension(x, bvars, range, body);
  .)
  .
Expressions<.List<Expression/*!*/>/*!*/ args.>
= (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)
  Expression<out e, true, true>                      (. args.Add(e); .)
  { "," Expression<out e, true, true>                (. args.Add(e); .)
  }
  .
/*------------------------------------------------------------------------*/
Attribute<ref Attributes attrs>
= "{"
    AttributeBody<ref attrs>
  "}"
  .
AttributeBody<ref Attributes attrs>
= (. string aName;
     List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
     Attributes.Argument/*!*/ aArg;
  .)
  ":" ident                            (. aName = t.val; .)
  [ AttributeArg<out aArg, true>       (. aArgs.Add(aArg); .)
    { "," AttributeArg<out aArg, true> (. aArgs.Add(aArg); .)
    }
  ]                                    (. attrs = new Attributes(aName, aArgs, attrs); .)
  .
AttributeArg<out Attributes.Argument arg, bool allowSemi>
= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e;  arg = dummyAttrArg; .)
  ( string                             (. arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); .)
  | Expression<out e, allowSemi, true>       (. arg = new Attributes.Argument(t, e); .)
  )
  .
/*------------------------------------------------------------------------*/
Ident<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
  ident            (. x = t; .)
  .
// Identifier or sequence of digits
// Parse one of the following:
//      . ident
//      . digits
//      . digits . digits
// In the first two cases, x returns as the token for the ident/digits and y returns as null.
// In the third case, x and y return as the tokens for the first and second digits.
// This parser production solves a problem where the scanner might parse a real number instead
// of stopping at the decimal point.
IdentOrDigitsSuffix<out IToken x, out IToken y>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null);
     x = Token.NoToken;
     y = null;
  .)
  "."
  ( ident          (. x = t; .)
  | digits         (. x = t; .)
  | decimaldigits  (. x = t;
                      int exponent = x.val.IndexOf('e');
                      if (0 <= exponent) {
                        // this is not a legal field/destructor name
                        SemErr(x, "invalid IdentOrDigitsSuffix");
                      } else {
                        int dot = x.val.IndexOf('.');
                        if (0 <= dot) {
                          y = new Token();
                          y.pos = x.pos + dot + 1;
                          y.val = x.val.Substring(dot + 1);
                          x.val = x.val.Substring(0, dot);
                          y.col = x.col + dot + 1;
                          y.line = x.line;
                          y.filename = x.filename;
                          y.kind = x.kind;
                        }
                      }
                   .)
  | "requires"    (. x = t; .)
  | "reads"       (. x = t; .)
  )
  .
// Identifier, disallowing leading underscores
NoUSIdent<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
  ident            (. x = t;
                      if (x.val.StartsWith("_")) {
                        SemErr("cannot declare identifier beginning with underscore");
                      }
                   .)
  .

// Identifier, disallowing leading underscores, except possibly the "wildcard" identifier "_"
WildIdent<out IToken/*!*/ x, bool allowWildcardId>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
  ident            (. x = t;
                      t.val = UnwildIdent(x.val, allowWildcardId);
                   .)
  .

Nat<out BigInteger n>
= (. n = BigInteger.Zero; .)
  (digits
    (. try {
         n = BigInteger.Parse(t.val);
       } catch (System.FormatException) {
         SemErr("incorrectly formatted number");
         n = BigInteger.Zero;
       }
    .)
   |hexdigits
    (. try {
         // note: leading 0 required when parsing positive hex numbers
         n = BigInteger.Parse("0" + t.val.Substring(2), System.Globalization.NumberStyles.HexNumber);
       } catch (System.FormatException) {
         SemErr("incorrectly formatted number");
         n = BigInteger.Zero;
       }
    .)
   )
  .
Dec<out Basetypes.BigDec d>
= (. d = Basetypes.BigDec.ZERO; .)
  (decimaldigits
    (. try {
         d = Basetypes.BigDec.FromString(t.val);
       } catch (System.FormatException) {
         SemErr("incorrectly formatted number");
         d = Basetypes.BigDec.ZERO;
       }
    .)
  )
  .
END Dafny.