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
/*--------------------------------------------------------------------------*/
static List<ModuleDecl/*!*/> theModules;
static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
static int anonymousIds = 0;
struct MemberModifiers {
  public bool IsGhost;
  public bool IsStatic;
  public bool IsUnlimited;
}
// helper routine for parsing call statements
private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)
{
Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Expression>() != null);
  FieldSelectExpr fse = e as FieldSelectExpr;
  if (fse != null && fse.Obj is ImplicitThisExpr) {
    return new IdentifierExpr(fse.tok, fse.FieldName);
  }
  return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
}
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "modules".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) /* throws System.IO.IOException */ {
  Contract.Requires(filename != null);
  Contract.Requires(cce.NonNullElements(modules));
  string s;
  if (filename == "stdin.dfy") {
    s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
    return Parse(s, filename, modules, builtIns);
  } else {
    using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
      s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
      return Parse(s, filename, modules, builtIns);
    }
  }
}
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) {
  Contract.Requires(s != null);
  Contract.Requires(filename != null);
  Contract.Requires(cce.NonNullElements(modules));
  Errors errors = new Errors();
  return Parse(s, filename, modules, builtIns, errors);
}
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
/// 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, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns,
                         Errors/*!*/ errors) {
  Contract.Requires(s != null);
  Contract.Requires(filename != null);
  Contract.Requires(cce.NonNullElements(modules));
  Contract.Requires(errors != null);
  List<ModuleDecl/*!*/> oldModules = theModules;
  theModules = modules;
  BuiltIns oldBuiltIns = builtIns;
  theBuiltIns = builtIns;
  byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
  MemoryStream ms = new MemoryStream(buffer,false);
  Scanner scanner = new Scanner(ms, errors, filename);
  Parser parser = new Parser(scanner, errors);
  parser.Parse();
  theModules = oldModules;
  theBuiltIns = oldBuiltIns;
  return parser.errors.count;
}
/*--------------------------------------------------------------------------*/
CHARACTERS
  letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
  digit = "0123456789".
  posDigit = "123456789".
  special = "'_?\\".
  glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
  cr        = '\r'.
  lf        = '\n'.
  tab       = '\t'.
  space = ' '.
  quote = '"'.
  nondigit = letter + special.
  idchar = nondigit + digit.
  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}.
  arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
  string = quote {nonquote} quote.
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
IGNORE cr + lf + tab
/*------------------------------------------------------------------------*/
PRODUCTIONS
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
     Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;
     List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
     ModuleDecl module;
     // to support multiple files, create a default module only if theModules doesn't already contain one
     DefaultModuleDecl defaultModule = null;
     foreach (ModuleDecl mdecl in theModules) {
       defaultModule = mdecl as DefaultModuleDecl;
       if (defaultModule != null) { break; }
     }
     bool defaultModuleCreatedHere = false;
     if (defaultModule == null) {
       defaultModuleCreatedHere = true;
       defaultModule = new DefaultModuleDecl();
     }
  .)
  { "module"                             (. attrs = null;  theImports = new List<string/*!*/>(); .)
    { Attribute<ref attrs> }
    Ident<out id>
    [ "imports" Idents<theImports> ]     (. module = new ModuleDecl(id, id.val, theImports, attrs); .)
    "{"                                  (. module.BodyStartTok = t; .)
      { ClassDecl<module, out c>         (. module.TopLevelDecls.Add(c); .)
      | DatatypeDecl<module, out dt>     (. module.TopLevelDecls.Add(dt); .)
      }
    "}"                                  (. module.BodyEndTok = t;
                                            theModules.Add(module); .)
  | ClassDecl<defaultModule, out c>      (. defaultModule.TopLevelDecls.Add(c); .)
  | DatatypeDecl<defaultModule, out dt>  (. defaultModule.TopLevelDecls.Add(dt); .)
  | ClassMemberDecl<membersDefaultClass, false>
  }
  (. if (defaultModuleCreatedHere) {
       defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
       theModules.Add(defaultModule);
     } else {
       // find the default class in the default module, then append membersDefaultClass to its member list
       foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
         DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
         if (defaultClass != null) {
           defaultClass.Members.AddRange(membersDefaultClass);
           break;
         }
       }
     }
  .)
  EOF
  .
ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
= (. Contract.Requires(module != null);
     Contract.Ensures(Contract.ValueAtReturn(out c) != null);
     IToken/*!*/ id;
     Attributes attrs = null;
     List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
     IToken/*!*/ idRefined;
     IToken optionalId = null;
     List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
     IToken bodyStart;
  .)
  SYNC
  "class"
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  [ "refines" Ident<out idRefined>               (. optionalId = idRefined; .)
  ]
  "{"                                            (. bodyStart = t; .)
  { ClassMemberDecl<members, true>
  }
  "}"
  (. if (optionalId == null)
       c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
     else
       c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
     c.BodyStartTok = bodyStart;
     c.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; .)
  | "unlimited"                            (. mmod.IsUnlimited = true; .)
  }
  ( FieldDecl<mmod, mm>
  | FunctionDecl<mmod, out f>                   (. mm.Add(f); .)
  | MethodDecl<mmod, allowConstructors, out m>  (. mm.Add(m); .)
  | CouplingInvDecl<mmod, mm>
  )
  .
DatatypeDecl<ModuleDecl/*!*/ 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
  .)
  SYNC
  "datatype"
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  "="                                      (. bodyStart = t; .)
  DatatypeMemberDecl<ctors>
  { "|" DatatypeMemberDecl<ctors> }
  SYNC ";"
  (. dt = new DatatypeDecl(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> }
  Ident<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.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
     if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
  .)
  { Attribute<ref attrs> }
  IdentType<out id, out ty>                         (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
  { "," IdentType<out id, out ty>                   (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
  }
  SYNC ";"
  .
CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
     Attributes attrs = null;
     List<IToken/*!*/> ids = new List<IToken/*!*/>();;
     IToken/*!*/ id;
     Expression/*!*/ e;
  .)
  "replaces"
  (. if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }
     if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
     if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
  .)
  { Attribute<ref attrs> }
  Ident<out id>                                     (. ids.Add(id); .)
  { "," Ident<out id>                               (. ids.Add(id); .)
  }
  "by"
  Expression<out e>
  ";"
  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)
  .
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>
  .
IdentType<out IToken/*!*/ id, out Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
  Ident<out id>
  ":"
  Type<out ty>
  .
LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
= (. IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;
  .)
  Ident<out id>
  [ ":" Type<out ty>             (. optType = ty; .)
  ]
  (. var = new VarDecl(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;
  .)
  Ident<out id>
  [ ":" 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;  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>
  ]
  (. if (name != null) {
       identName = name;
     } else {
       identName = "#" + anonymousIds++;
     }
  .)
  .
/*------------------------------------------------------------------------*/
GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
     IToken/*!*/ id; .)
  "<"
  Ident<out id>                       (. typeArgs.Add(new TypeParameter(id, id.val)); .)
  { "," Ident<out id>                 (. typeArgs.Add(new TypeParameter(id, id.val)); .)
  }
  ">"
  .
/*------------------------------------------------------------------------*/
MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
     IToken/*!*/ id;
     Attributes attrs = null;
     List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();
     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/*!*/>();
     Statement/*!*/ bb;  BlockStmt body = null;
     bool isConstructor = false;
     bool isRefinement = false;
     IToken bodyStart = Token.NoToken;
     IToken bodyEnd = Token.NoToken;
  .)
  SYNC
  ( "method"
  | "constructor"                   (. if (allowConstructor) {
                                         isConstructor = true;
                                       } else {
                                         SemErr(t, "constructors are only allowed in classes");
                                       }
                                    .)
  | "refines"                       (. isRefinement = true; .)
  )
  (. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
     if (isConstructor) {
       if (mmod.IsGhost) {
         SemErr(t, "constructors cannot be declared 'ghost'");
       }
       if (mmod.IsStatic) {
         SemErr(t, "constructors cannot be declared 'static'");
       }
     }
  .)
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  Formals<true, !mmod.IsGhost, ins>
  [ "returns"                                 (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
    Formals<false, !mmod.IsGhost, outs>
  ]
  { MethodSpec<req, mod, ens, dec> }
  [ BlockStmt<out bb, out bodyStart, out bodyEnd>    (. body = (BlockStmt)bb; .)
  ]
  (. if (isRefinement)
       m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
     else if (isConstructor)
       m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);
     else
       m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
     m.BodyStartTok = bodyStart;
     m.BodyEndTok = bodyEnd;
 .)
  .
MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
           List<Expression/*!*/>/*!*/ decreases.>
= (. 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;
  .)
  SYNC
  ( "modifies" [ FrameExpression<out fe>                     (. mod.Add(fe); .)
                 { "," FrameExpression<out fe>               (. mod.Add(fe); .)
                 }
               ] SYNC ";"
  | [ "free"                                                 (. isFree = true; .)
    ]
    ( "requires" Expression<out e> SYNC ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)
    | "ensures" Expression<out e> SYNC ";"                        (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
    )
  | "decreases" DecreasesList<decreases, false> SYNC ";"
  )
  .
Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; .)
  "("
  [
    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;
  .)
  ( "bool"                          (. tok = t; .)
  | "nat"                           (. tok = t;  ty = new NatType(); .)
  | "int"                           (. tok = t;  ty = new IntType(); .)
  | "set"                           (. tok = t;  gt = new List<Type/*!*/>(); .)
    GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                         SemErr("set type expects exactly one type argument");
                                       }
                                       ty = new SetType(gt[0]);
                                    .)
  | "multiset"                      (. tok = t;  gt = new List<Type/*!*/>(); .)
    GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                         SemErr("multiset type expects exactly one type argument");
                                       }
                                       ty = new MultiSetType(gt[0]);
                                    .)
  | "seq"                           (. tok = t;  gt = new List<Type/*!*/>(); .)
    GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                         SemErr("seq type expects exactly one type argument");
                                       }
                                       ty = new SeqType(gt[0]);
                                    .)
  | ReferenceType<out tok, out ty>
  )
  .
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;
  .)
  ( "object"                        (. tok = t;  ty = new ObjectType(); .)
  | arrayToken                      (. tok = t;  gt = new List<Type/*!*/>(); .)
    GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                         SemErr("array type expects exactly one type argument");
                                       }
                                       int dims = 1;
                                       if (tok.val.Length != 5) {
                                         dims = int.Parse(tok.val.Substring(5));
                                       }
                                       ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
                                    .)
  | Ident<out tok>                  (. gt = new List<Type/*!*/>(); .)
    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt); .)
  )
  .
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;
     List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
     List<Formal/*!*/> formals = new List<Formal/*!*/>();
     Type/*!*/ returnType;
     List<Expression/*!*/> reqs = new List<Expression/*!*/>();
     List<Expression/*!*/> ens = new List<Expression/*!*/>();
     List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
     List<Expression/*!*/> decreases = new List<Expression/*!*/>();
     Expression/*!*/ bb;  Expression body = null;
     bool isFunctionMethod = false;
     IToken bodyStart = Token.NoToken;
     IToken bodyEnd = Token.NoToken;
  .)
  "function"
  [ "method"                 (. isFunctionMethod = true; .)
  ]
  (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
  .)
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  Formals<true, isFunctionMethod, formals>
  ":"
  Type<out returnType>
  { FunctionSpec<reqs, reads, ens, decreases> }
  [ FunctionBody<out bb, out bodyStart, out bodyEnd>  (. body = bb; .)
  ]
  (. f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
     f.BodyStartTok = bodyStart;
     f.BodyEndTok = bodyEnd;
  .)
  .
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(cce.NonNullElements(decreases));
     Expression/*!*/ e;  FrameExpression/*!*/ fe; .)
  (
    SYNC
    "requires" Expression<out e> SYNC ";"      (. reqs.Add(e); .)
  | "reads" [ PossiblyWildFrameExpression<out fe>              (. reads.Add(fe); .)
              { "," PossiblyWildFrameExpression<out fe>        (. reads.Add(fe); .)
              }
            ] SYNC ";"
  | "ensures" Expression<out e> SYNC ";"      (. ens.Add(e); .)
  | "decreases" DecreasesList<decreases, false> SYNC ";"
  )
  .
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>
  )
  .
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(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; .)
  Expression<out e>
  [ "`" Ident<out id>        (. fieldName = id.val; .)
  ]
  (. fe = new FrameExpression(e, 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>
  "}"                         (. bodyEnd = t; .)
  .
/*------------------------------------------------------------------------*/
BlockStmt<out Statement/*!*/ 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, 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 */
     IToken bodyStart, bodyEnd;
     int breakCount;
  .)
  /* This list does not contain BlockStmt, see comment above in Stmt production. */
  SYNC
  ( BlockStmt<out s, out bodyStart, out bodyEnd>
  | AssertStmt<out s>
  | AssumeStmt<out s>
  | PrintStmt<out s>
  | UpdateStmt<out s>
  | VarDeclStatement<out s>
  | IfStmt<out s>
  | WhileStmt<out s>
  | MatchStmt<out s>
  | ParallelStmt<out s>
  | "label"                            (. x = t; .)
    Ident<out id> ":"
    OneStmt<out s>                     (. s.Labels = new LabelNode(x, id.val, s.Labels); .)
  | "break"                            (. x = t; breakCount = 1; label = null; .)
    ( Ident<out id>                    (. label = id.val; .)
    | { "break"                        (. breakCount++; .)
      }
    )
    SYNC
    ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
  | ReturnStmt<out s>
  )
  .
ReturnStmt<out Statement/*!*/ s>
= (.
   IToken returnTok = null;
   List<AssignmentRhs> rhss = null;
   AssignmentRhs r;
   .)
  "return"                           (. returnTok = t; .)
  [
      Rhs<out r, null>               (. rhss = new List<AssignmentRhs>(); rhss.Add(r); .)
      { "," Rhs<out r, null>         (. rhss.Add(r); .)
        }
  ]
  ";"                                (. s = new ReturnStmt(returnTok, 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;
  .)
  Lhs<out e>                       (. x = e.tok; .)
  ( ";"                            (. rhss.Add(new ExprRhs(e)); .)
  |                                (. 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); .)
    }
    ";"
  | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
  )
  (. s = new UpdateStmt(x, lhss, rhss); .)
  .
Rhs<out AssignmentRhs r, Expression receiverForInitCall>
= (. IToken/*!*/ x, newToken;  Expression/*!*/ e;
     List<Expression> ee = null;
     Type ty = null;
     CallStmt initCall = null;
     List<Expression> args;
     r = null;  // to please compiler
  .)
  ( "new"                              (. newToken = t; .)
    TypeAndToken<out x, out ty>
    [ "["                              (. ee = new List<Expression>(); .)
      Expressions<ee>
      "]"                              (. // make sure an array class with this dimensionality exists
                                          UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
                                       .)
    | "." Ident<out x>
      "("                              (. args = new List<Expression/*!*/>(); .)
        [ Expressions<args> ]
      ")"                              (. initCall = new CallStmt(x, new List<Expression>(),
                                                                  receiverForInitCall, x.val, args); .)
    ]
    (. if (ee != null) {
         r = new TypeRhs(newToken, ty, ee);
       } else {
         r = new TypeRhs(newToken, ty, initCall);
       }
    .)
  /* One day, the choose expression should be treated just as a special case of a method call. */
  | "choose"                           (. x = t; .)
    Expression<out e>                  (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)
  | "*"                                (. r = new HavocRhs(t); .)
  | Expression<out e>                  (. r = new ExprRhs(e); .)
  )
  .
VarDeclStatement<.out Statement/*!*/ s.>
= (. IToken x = null, assignTok = null;  bool isGhost = false;
     VarDecl/*!*/ d;
     AssignmentRhs r;  IdentifierExpr lhs0;
     List<VarDecl> lhss = new List<VarDecl>();
     List<AssignmentRhs> rhss = new List<AssignmentRhs>();
  .)
  [ "ghost"                                 (. isGhost = true;  x = t; .)
  ]
  "var"                                     (. if (!isGhost) { x = t; } .)
  LocalIdentTypeOptional<out d, isGhost>    (. lhss.Add(d); .)
  { ","
    LocalIdentTypeOptional<out d, isGhost>  (. lhss.Add(d); .)
  }
  [ ":="                           (. assignTok = t;
                                      lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
                                      lhs0.Var = lhss[0];  lhs0.Type = lhss[0].OptionalType;  // resolve here
                                   .)
    Rhs<out r, lhs0>               (. rhss.Add(r); .)
    { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)
    }
  ]
  ";"
  (. UpdateStmt update;
     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, ies, rhss);
     }
     s = new VarDeclStmt(x, lhss, update);
  .)
  .
IfStmt<out Statement/*!*/ ifStmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
     Expression guard;
     Statement/*!*/ thn;
     Statement/*!*/ s;
     Statement els = null;
     IToken bodyStart, bodyEnd;
     List<GuardedAlternative> alternatives;
     ifStmt = dummyStmt;  // to please the compiler
  .)
  "if"                       (. x = t; .)
  (
    Guard<out guard>
    BlockStmt<out thn, out bodyStart, out bodyEnd>
    [ "else"
      ( IfStmt<out s>                                 (. els = s; .)
      | BlockStmt<out s, out bodyStart, out bodyEnd>  (. els = s; .)
      )
    ]
    (. ifStmt = new IfStmt(x, guard, thn, els); .)
  |
    AlternativeBlock<out alternatives>
    (. ifStmt = new AlternativeStmt(x, alternatives); .)
  )
  .
AlternativeBlock<.out List<GuardedAlternative> alternatives.>
= (. alternatives = new List<GuardedAlternative>();
     IToken x;
     Expression e;
     List<Statement> body;
  .)
  "{"
  { "case"                      (. x = t; .)
    Expression<out e>
    "=>"
    (. body = new List<Statement>(); .)
    { Stmt<body> }
    (. alternatives.Add(new GuardedAlternative(x, e, body)); .)
  }
  "}"
  .
WhileStmt<out Statement/*!*/ stmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
     Expression guard;
     List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
     List<Expression/*!*/> decreases = new List<Expression/*!*/>();
     List<FrameExpression/*!*/> mod = null;
     Statement/*!*/ body;
     IToken bodyStart, bodyEnd;
     List<GuardedAlternative> alternatives;
     stmt = dummyStmt;  // to please the compiler
  .)
  "while"                    (. x = t; .)
  (
    Guard<out guard>           (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
    LoopSpec<out invariants, out decreases, out mod>
    BlockStmt<out body, out bodyStart, out bodyEnd>
    (. stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); .)
  |
    LoopSpec<out invariants, out decreases, out mod>
    AlternativeBlock<out alternatives>
    (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)
  )
  .
LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
= (. FrameExpression/*!*/ fe;
     invariants = new List<MaybeFreeExpression/*!*/>();
     MaybeFreeExpression invariant = null;
     decreases = new List<Expression/*!*/>();
     mod = null;
  .)
  {
    Invariant<out invariant> SYNC ";"   (. invariants.Add(invariant); .)
  | SYNC "decreases" DecreasesList<decreases, true> SYNC ";"
  | SYNC "modifies" (. 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; invariant = null; .)
    SYNC
    ["free"                                 (. isFree = true; .)
    ]
    "invariant" Expression<out e>           (. invariant = new MaybeFreeExpression(e, isFree); .)
  .
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
  PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {
                                              SemErr(e.tok, "'decreases *' is only allowed on loops");
                                            } else {
                                              decreases.Add(e);
                                            }
                                         .)
  { "," PossiblyWildExpression<out e>    (. if (!allowWildcard && e is WildcardExpr) {
                                              SemErr(e.tok, "'decreases *' is only allowed on loops");
                                            } else {
                                              decreases.Add(e);
                                            }
                                         .)
  }
  .
Guard<out Expression e>   /* null represents demonic-choice */
= (. Expression/*!*/ ee;  e = null; .)
  "("
  ( "*"                      (. e = null; .)
  | Expression<out ee>       (. 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/*!*/>(); .)
  "match"                     (. x = t; .)
  Expression<out e>
  "{"
  { CaseStatement<out c>     (. cases.Add(c); .)
  }
  "}"
  (. s = new MatchStmt(x, e, cases); .)
  .
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; .)
  "assert"                                     (. x = t; .)
  Expression<out e> ";"                        (. s = new AssertStmt(x, e); .)
  .
AssumeStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)
  "assume"                                     (. x = t; .)
  Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)
  .
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>                        (. args.Add(arg); .)
  { "," AttributeArg<out arg>                  (. args.Add(arg); .)
  }
  ";"                                          (. s = new PrintStmt(x, args); .)
  .

ParallelStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
     IToken/*!*/ x;
     List<BoundVar/*!*/> bvars;
     Attributes attrs;
     Expression range;
     var ens = new List<MaybeFreeExpression/*!*/>();
     bool isFree;
     Expression/*!*/ e;
     Statement/*!*/ block;
     IToken bodyStart, bodyEnd;
  .)
  "parallel"                                (. x = t; .)
  "("
  QuantifierDomain<out bvars, out attrs, out range>
                                            (. if (range == null) { range = new LiteralExpr(x, true); } .)
  ")"
  {                                         (. isFree = false; .)
    [ "free"                                (. isFree = true; .)
    ]
    "ensures" Expression<out e> ";"         (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
  }
  BlockStmt<out block, out bodyStart, out bodyEnd>
  (. s = new ParallelStmt(x, bvars, attrs, range, ens, block); .)
  .
/*------------------------------------------------------------------------*/
Expression<out Expression/*!*/ e>
=
  EquivExpression<out e>
  .
/*------------------------------------------------------------------------*/
EquivExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
  ImpliesExpression<out e0>
  { EquivOp                                    (. x = t; .)
    ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
  }
  .
EquivOp = "<==>" | '\u21d4'.
/*------------------------------------------------------------------------*/
ImpliesExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
  LogicalExpression<out e0>
  [ ImpliesOp                                  (. x = t; .)
    ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
  ]
  .
ImpliesOp = "==>" | '\u21d2'.
/*------------------------------------------------------------------------*/
LogicalExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
  RelationalExpression<out e0>
  [ AndOp                                      (. x = t; .)
    RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
    { AndOp                                    (. x = t; .)
      RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
    }
  | OrOp                                       (. x = t; .)
    RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
    { OrOp                                     (. x = t; .)
      RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
    }
  ]
  .
AndOp = "&&" | '\u2227'.
OrOp = "||" | '\u2228'.
/*------------------------------------------------------------------------*/
RelationalExpression<out Expression/*!*/ e>
= (. 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;
     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>                     (. e = e0; .)
  [ RelOp<out x, out op>           (. firstOpTok = x; .)
    Term<out e1>                   (. 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.
                                   .)
    {                              (. if (chain == null) {
                                        chain = new List<Expression>();
                                        ops = new List<BinaryExpr.Opcode>();
                                        chain.Add(e0);  ops.Add(op);  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>         (. 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>                 (. ops.Add(op); chain.Add(e1);
                                      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, e);
     }
  .)
  .
RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null);
     x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/;
     IToken y;
  .)
  ( "=="           (. x = t;  op = BinaryExpr.Opcode.Eq; .)
  | "<"            (. x = t;  op = BinaryExpr.Opcode.Lt; .)
  | ">"            (. x = t;  op = BinaryExpr.Opcode.Gt; .)
  | "<="           (. x = t;  op = BinaryExpr.Opcode.Le; .)
  | ">="           (. x = t;  op = BinaryExpr.Opcode.Ge; .)
  | "!="           (. x = t;  op = BinaryExpr.Opcode.Neq; .)
  | "!!"           (. x = t;  op = BinaryExpr.Opcode.Disjoint; .)
  | "in"           (. x = t;  op = BinaryExpr.Opcode.In; .)
  | /* The next operator is "!in", but Coco evidently parses "!in" even when it is a prefix of, say, "!initialized".
     * The reason for this seems to be that the first character of "!in" is not a letter.  So, here is the workaround:
     */
    "!"            (. x = t;  y = Token.NoToken; .)
    [ "in"         (. y = t; .)
    ]              (. if (y == Token.NoToken) {
                        SemErr(x, "invalid RelOp");
                      } else if (y.pos != x.pos + 1) {
                        SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");
                      } else {
                        x.val = "!in";
                        op = BinaryExpr.Opcode.NotIn;
                      }
                   .)
  | '\u2260'       (. x = t;  op = BinaryExpr.Opcode.Neq; .)
  | '\u2264'       (. x = t;  op = BinaryExpr.Opcode.Le; .)
  | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)
  )
  .
/*------------------------------------------------------------------------*/
Term<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)
  Factor<out e0>
  { AddOp<out x, out op>
    Factor<out e1>                             (. e0 = new BinaryExpr(x, op, e0, e1); .)
  }
  .
AddOp<out 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>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)
  UnaryExpression<out e0>
  { MulOp<out x, out op>
    UnaryExpression<out e1>                    (. e0 = new BinaryExpr(x, op, e0, e1); .)
  }
  .
MulOp<out 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>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; .)
  ( "-"                                        (. x = t; .)
    UnaryExpression<out e>                     (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)
  | NegOp                                      (. x = t; .)
    UnaryExpression<out e>                     (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
  | EndlessExpression<out e>     /* these have no further suffix */
  | DottedIdentifiersAndFunction<out e>
    { Suffix<ref e> }
  | DisplayExpr<out e>
  | MultiSetExpr<out e>
  | ConstAtomExpression<out e>
    { Suffix<ref e> }
  )
  .
Lhs<out Expression e>
= (. e = null;  // to please the compiler
  .)
  ( DottedIdentifiersAndFunction<out e>
    { Suffix<ref e> }
  | ConstAtomExpression<out e>
    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>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     IToken/*!*/ x;  BigInteger n;
     e = dummyExpr;
  .)
  ( "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); .)
  | "this"                                     (. e = new ThisExpr(t); .)
  | "fresh"                                    (. x = t; .)
    "(" Expression<out e> ")"                  (. e = new FreshExpr(x, e); .)
  | "allocated"                                (. x = t; .)
    "(" Expression<out e> ")"                  (. e = new AllocatedExpr(x, e); .)
  | "old"                                      (. x = t; .)
    "(" Expression<out e> ")"                  (. e = new OldExpr(x, e); .)
  | "|"                                        (. x = t; .)
      Expression<out e>                        (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
    "|"
  | "("                                        (. x = t; .)
      Expression<out e>                        (. e = new ParensExpression(x, e); .)
    ")"
  )
  .
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>                        (. e = new MultiSetFormingExpr(x, e); .)
    ")"
  | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)
  )
  .
EndlessExpression<out Expression e>
= (. IToken/*!*/ x;
     Expression e0, e1;
     e = dummyExpr;
     BoundVar d;
     List<BoundVar> letVars;  List<Expression> letRHSs;
  .)
  ( "if"                            (. x = t; .)
    Expression<out e>
    "then" Expression<out e0>
    "else" Expression<out e1>       (. e = new ITEExpr(x, e, e0, e1); .)
  | MatchExpression<out e>
  | QuantifierGuts<out e>
  | ComprehensionExpr<out e>
  | "assert"                        (. x = t; .)
    Expression<out e0> ";"
    Expression<out e1>              (. e = new AssertExpr(x, e0, e1); .)
  | "assume"                        (. x = t; .)
    Expression<out e0> ";"
    Expression<out e1>              (. e = new AssumeExpr(x, e0, e1); .)
  | "var"                           (. x = t;
                                       letVars = new List<BoundVar>();
                                       letRHSs = new List<Expression>(); .)
    IdentTypeOptional<out d>        (. letVars.Add(d); .)
    { "," IdentTypeOptional<out d>  (. letVars.Add(d); .)
    }
    ":="
    Expression<out e>               (. letRHSs.Add(e); .)
    { "," Expression<out e>         (. letRHSs.Add(e); .)
    }
    ";"
    Expression<out e>               (. e = new LetExpr(x, letVars, letRHSs, e); .)
  )
  .
MatchExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;
     List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
  .)
  "match"                     (. x = t; .)
  Expression<out e>
  /* 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>     (. cases.Add(c); .)
  }
  (. e = new MatchExpr(x, e, cases); .)
  .
CaseExpression<out MatchCaseExpr/*!*/ c>
= (. 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>       (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
  .
/*------------------------------------------------------------------------*/
DottedIdentifiersAndFunction<out Expression e>
= (. IToken id;  IToken openParen = null;
     List<Expression> args = null;
     List<IToken> idents = new List<IToken>();
  .)
  Ident<out id>                        (. idents.Add(id); .)
  { "."
    Ident<out id>                      (. idents.Add(id); .)
  }
  [ "("                                (. openParen = t;  args = new List<Expression>(); .)
      [ Expressions<args> ]
    ")"
  ]
  (. e = new IdentifierSequence(idents, openParen, 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> multipleIndices = null;
     bool func = false;
  .)
  ( "."
    Ident<out id>
    [ "("                                      (. args = new List<Expression/*!*/>();  func = true; .)
        [ Expressions<args> ]
      ")"                                      (. e = new FunctionCallExpr(id, id.val, e, args); .)
    ]                                          (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)
  | "["                                        (. x = t; .)
      ( Expression<out ee>                     (. e0 = ee; .)
        ( ".."                                 (. anyDots = true; .)
          [ Expression<out ee>                 (. e1 = ee; .)
          ]
        | ":="
          Expression<out ee>                   (. e1 = ee; .)
        | { "," Expression<out ee>             (. if (multipleIndices == null) {
                                                    multipleIndices = new List<Expression>();
                                                    multipleIndices.Add(e0);
                                                  }
                                                  multipleIndices.Add(ee);
                                               .)
          }
        )
      | ".."                                   (. anyDots = true; .)
        [ Expression<out ee>                   (. e1 = ee; .)
        ]
      )
      (. if (multipleIndices != null) {
           e = new MultiSelectExpr(x, e, multipleIndices);
           // make sure an array class with this dimensionality exists
           UserDefinedType tmp = theBuiltIns.ArrayType(x, 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 (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);
           }
         }
      .)
    "]"
  )
  .
/*------------------------------------------------------------------------*/
QuantifierGuts<out Expression/*!*/ q>
= (. 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>
  (. 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); .)
  }
  { Attribute<ref attrs> }
  [ "|"
    Expression<out range>
  ]
  .

ComprehensionExpr<out Expression/*!*/ q>
= (. 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>
  [
    QSep
    Expression<out body>
  ]
  (. 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>                            (. args.Add(e); .)
  { "," Expression<out e>                      (. 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>             (. aArgs.Add(aArg); .)
    { "," AttributeArg<out aArg>       (. aArgs.Add(aArg); .)
    }
  ]                                    (. attrs = new Attributes(aName, aArgs, attrs); .)
  .
AttributeArg<out Attributes.Argument/*!*/ arg>
= (. 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>                  (. arg = new Attributes.Argument(t, e); .)
  )
  .
/*------------------------------------------------------------------------*/
Idents<.List<string/*!*/>/*!*/ ids.>
= (. IToken/*!*/ id; .)
  Ident<out id>                            (. ids.Add(id.val); .)
  { "," Ident<out id>                      (. ids.Add(id.val); .)
  }
  .
Ident<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
  ident            (. x = t; .)
  .
Nat<out BigInteger n>
=
  digits
  (. try {
       n = BigInteger.Parse(t.val);
     } catch (System.FormatException) {
       SemErr("incorrectly formatted number");
       n = BigInteger.Zero;
     }
  .)
  .
END Dafny.