path: root/Source/Core/BoogiePL.atg

/*---------------------------------------------------------------------------
// BoogiePL -
//--------------------------------------------------------------------------*/

/*using System;*/
using PureCollections;
using System.Collections;
using System.Collections.Generic;
using System.IO;
using System.Text;
using Microsoft.Boogie;
using Microsoft.Basetypes;
using Bpl = Microsoft.Boogie;


COMPILER BoogiePL

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

readonly Program/*!*/ Pgm;

readonly Expr/*!*/ dummyExpr;
readonly Cmd/*!*/ dummyCmd;
readonly Block/*!*/ dummyBlock;
readonly Bpl.Type/*!*/ dummyType;
readonly Bpl.ExprSeq/*!*/ dummyExprSeq;
readonly TransferCmd/*!*/ dummyTransferCmd;
readonly StructuredCmd/*!*/ dummyStructuredCmd;

///<summary>
///Returns the number of parsing errors encountered.  If 0, "program" returns as
///the parsed program.
///</summary>
public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
  Contract.Requires(filename != null);
  Contract.Requires(cce.NonNullElements(defines,true));

  if (defines == null) {
    defines = new List<string/*!*/>();
  }

  if (filename == "stdin.bpl") {
    var s = ParserHelper.Fill(Console.In, defines);
    return Parse(s, filename, out program);
  } else {
    FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
    var s = ParserHelper.Fill(stream, defines);
    var ret = Parse(s, filename, out program);
    stream.Close();
    return ret;
  }
}


public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
  Contract.Requires(s != null);
  Contract.Requires(filename != null);

  byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));
  MemoryStream ms = new MemoryStream(buffer,false);
  Errors errors = new Errors();
  Scanner scanner = new Scanner(ms, errors, filename);

  Parser parser = new Parser(scanner, errors, false);
  parser.Parse();
  if (parser.errors.count == 0)
  {
    program = parser.Pgm;
    program.ProcessDatatypeConstructors();
    return 0;
  }
  else
  {
    program = null;
    return parser.errors.count;
  }
}

public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
 : this(scanner, errors)
{
  // initialize readonly fields
  Pgm = new Program();
  dummyExpr = new LiteralExpr(Token.NoToken, false);
  dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
  dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));
  dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
  dummyExprSeq = new ExprSeq ();
  dummyTransferCmd = new ReturnCmd(Token.NoToken);
  dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
}

// Class to represent the bounds of a bitvector expression t[a:b].
// Objects of this class only exist during parsing and are directly
// turned into BvExtract before they get anywhere else
private class BvBounds : Expr {
  public BigNum Lower;
  public BigNum Upper;
  public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
    : base(tok) {
    Contract.Requires(tok != null);
    this.Lower = lower;
    this.Upper = upper;
  }
  public override Bpl.Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Bpl.Type>() != null); return Bpl.Type.Int; } }
  public override void Resolve(ResolutionContext/*!*/ rc) {
    // Contract.Requires(rc != null);
    rc.Error(this, "bitvector bounds in illegal position");
  }
  public override void Emit(TokenTextWriter/*!*/ stream,
                            int contextBindingStrength, bool fragileContext) {
    Contract.Assert(false);throw new cce.UnreachableException();
  }
  public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
}

/*--------------------------------------------------------------------------*/
CHARACTERS
  letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
  digit = "0123456789".
  special = "'~#$^_.?`".
  glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".

  cr        = '\r'.
  lf        = '\n'.
  tab       = '\t'.
  
  space = ' '.
  quote = '"'.

  newLine = cr + lf.
  regularStringChar = ANY - quote - newLine.

  nondigit = letter + special.
  nonquote = letter + digit + space + glyph.


/*------------------------------------------------------------------------*/
TOKENS
  ident =  [ '\\' ] nondigit {nondigit | digit}.
  bvlit = digit {digit} 'b' 'v' digit {digit}.
  digits = digit {digit}.

  string = quote { regularStringChar | "\\\"" } quote.

  decimal = digit {digit} 'e' [ '-' ] digit {digit} .
  float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .

COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf

IGNORE cr + lf + tab


/*------------------------------------------------------------------------*/
PRODUCTIONS


/*------------------------------------------------------------------------*/
BoogiePL
= (. VariableSeq/*!*/ vs;
     DeclarationSeq/*!*/ ds;
     Axiom/*!*/ ax;
     List<Declaration/*!*/>/*!*/ ts;
     Procedure/*!*/ pr;
     Implementation im;
     Implementation/*!*/ nnim;
  .)
  { Consts<out vs>             (. foreach(Bpl.Variable/*!*/ v in vs){
                                    Contract.Assert(v != null);
                                    Pgm.TopLevelDeclarations.Add(v);
                                  }
                               .)
  | Function<out ds>           (. foreach(Bpl.Declaration/*!*/ d in ds){
                                    Contract.Assert(d != null);
                                    Pgm.TopLevelDeclarations.Add(d);
                                  }
                               .)
  | Axiom<out ax>              (. Pgm.TopLevelDeclarations.Add(ax); .)
  | UserDefinedTypes<out ts>   (. foreach(Declaration/*!*/ td in ts){
                                    Contract.Assert(td != null);
                                    Pgm.TopLevelDeclarations.Add(td);
                                  }
                               .)
  | GlobalVars<out vs>         (. foreach(Bpl.Variable/*!*/ v in vs){
                                    Contract.Assert(v != null);
                                    Pgm.TopLevelDeclarations.Add(v);
                                  }
                               .)
  | Procedure<out pr, out im>  (. Pgm.TopLevelDeclarations.Add(pr);
                                   if (im != null) {
                                     Pgm.TopLevelDeclarations.Add(im);
                                   }
                               .)
  | Implementation<out nnim>   (. Pgm.TopLevelDeclarations.Add(nnim); .)
  }
  EOF
  .

/*------------------------------------------------------------------------*/
GlobalVars<out VariableSeq/*!*/ ds>
= (.
    Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
    QKeyValue kv = null;
    ds = new VariableSeq();
    var dsx = ds;
  .)
  "var"
  { Attribute<ref kv> }
  IdsTypeWheres<true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } > ";"
  .

LocalVars<VariableSeq/*!*/ ds>
= (.
    Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
    QKeyValue kv = null;
  .)
  "var"
  { Attribute<ref kv> }
  IdsTypeWheres<true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } > ";"
  .

ProcFormals<bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds>
= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
     ds = new VariableSeq();
     var dsx = ds;
     var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
  .)
  "("
  [ AttrsIdsTypeWheres<allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }>
  ]
  ")"
  .

BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds>
= (.
    Contract.Requires(x != null);
    Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
    TypedIdentSeq/*!*/ tyds = new TypedIdentSeq();
    ds = new VariableSeq();
    var dsx = ds;
  .)
  AttrsIdsTypeWheres<true, false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } >
  .

/*------------------------------------------------------------------------*/
/* IdsType is used with const declarations */
IdsType<out TypedIdentSeq/*!*/ tyds>
= (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty; .)
  Idents<out ids> ":" Type<out ty>
  (. tyds = new TypedIdentSeq();
     foreach(Token/*!*/ id in ids){
       Contract.Assert(id != null);
       tyds.Add(new TypedIdent(id, id.val, ty, null));
     }
  .)
  .

/* AttrsIdsTypeWheres is used with the declarations of formals and bound variables */
AttrsIdsTypeWheres<. bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
=
  AttributesIdsTypeWhere<allowAttributes, allowWhereClauses, context, action>
  { "," AttributesIdsTypeWhere<allowAttributes, allowWhereClauses, context, action> }
  .

IdsTypeWheres<. bool allowWhereClauses, string context, System.Action<TypedIdent> action .>
=
  IdsTypeWhere<allowWhereClauses, context, action>
  { "," IdsTypeWhere<allowWhereClauses, context, action> }
  .

AttributesIdsTypeWhere<. bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
= (. QKeyValue kv = null; .)
  { Attribute<ref kv>    (. if (!allowAttributes) {
                              kv = null;
                              this.SemErr("attributes are not allowed on " + context);
                            }
                         .)
  }
  IdsTypeWhere<allowWhereClauses, context, delegate(TypedIdent tyd) { action(tyd, kv); }>
  .

/* context is allowed to be null if allowWhereClauses is true */
IdsTypeWhere<. bool allowWhereClauses, string context, System.Action<TypedIdent> action .>
= (. TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty;  Expr wh = null;  Expr/*!*/ nne; .)
  Idents<out ids> ":" Type<out ty>
  [ "where" Expression<out nne>  (. if (!allowWhereClauses) {
                                      this.SemErr("where clause not allowed on " + context);
                                    } else {
                                      wh = nne;
                                    }
                                 .)
  ]
  (. foreach(Token/*!*/ id in ids){
       Contract.Assert(id != null);
       action(new TypedIdent(id, id.val, ty, wh));
     }
  .)
  .

/*------------------------------------------------------------------------*/
Type<out Bpl.Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; .)
  (
    TypeAtom<out ty>
  |
    Ident<out tok>       (. TypeSeq/*!*/ args = new TypeSeq (); .)
    [ TypeArgs<args> ]   (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .)
  |
    MapType<out ty>
  )
  .

TypeArgs<TypeSeq/*!*/ ts>
= (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .)
  (
    TypeAtom<out ty>     (. ts.Add(ty); .)
    [ TypeArgs<ts> ]
  |
    Ident<out tok>       (. TypeSeq/*!*/ args = new TypeSeq ();
                            ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); .)
    [ TypeArgs<ts> ]
  |
    MapType<out ty>      (. ts.Add(ty); .)
  )
  .

TypeAtom<out Bpl.Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; .)
  ( "int"              (. ty = new BasicType(t, SimpleType.Int); .)
  | "real"             (. ty = new BasicType(t, SimpleType.Real); .)
  | "bool"             (. ty = new BasicType(t, SimpleType.Bool); .)
  /* note: bitvectors are handled in UnresolvedTypeIdentifier */
  |
  "("
  Type<out ty>
  ")"
  )
  .

MapType<out Bpl.Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;
     IToken/*!*/ nnTok;
     TypeSeq/*!*/ arguments = new TypeSeq();
     Bpl.Type/*!*/ result;
     TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq();
   .)
  [ TypeParams<out nnTok, out typeParameters> (. tok = nnTok; .) ]
  "["                                         (.  if (tok == null) tok = t;  .)
    [ Types<arguments> ]
  "]"
  Type<out result>
  (.
    ty = new MapType(tok, typeParameters, arguments, result);
  .)
  .

TypeParams<out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams>
= (.Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); TokenSeq/*!*/ typeParamToks; .)
  "<"    (.  tok = t;  .)
    Idents<out typeParamToks>
  ">"
  (.
    typeParams = new TypeVariableSeq ();
    foreach(Token/*!*/ id in typeParamToks){
      Contract.Assert(id != null);
      typeParams.Add(new TypeVariable(id, id.val));}
   .)
  .

Types<TypeSeq/*!*/ ts>
= (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .)
  Type<out ty>                 (. ts.Add(ty); .)
  { "," Type<out ty>           (. ts.Add(ty); .)
  }
  .


/*------------------------------------------------------------------------*/
Consts<out VariableSeq/*!*/ ds>
= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; TypedIdentSeq/*!*/ xs;
     ds = new VariableSeq();
     bool u = false; QKeyValue kv = null;
     bool ChildrenComplete = false;
     List<ConstantParent/*!*/> Parents = null; .)
  "const"                 (. y = t; .)
  { Attribute<ref kv> }
  [ "unique"              (. u = true;  .)
  ]
  IdsType<out xs>
  [ OrderSpec<out ChildrenComplete, out Parents> ]
  (. bool makeClone = false;
     foreach(TypedIdent/*!*/ x in xs){
       Contract.Assert(x != null);

       // ensure that no sharing is introduced
       List<ConstantParent/*!*/> ParentsClone;
       if (makeClone && Parents != null) {
         ParentsClone = new List<ConstantParent/*!*/> ();
         foreach (ConstantParent/*!*/ p in Parents){
           Contract.Assert(p != null);
           ParentsClone.Add(new ConstantParent (
                            new IdentifierExpr (p.Parent.tok, p.Parent.Name),
                            p.Unique));}
       } else {
         ParentsClone = Parents;
       }
       makeClone = true;

       ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
     }
  .)
  ";"
  .

OrderSpec<.out bool ChildrenComplete, out List<ConstantParent/*!*/> Parents.>
= (.Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out Parents),true)); ChildrenComplete = false;
     Parents = null;
     bool u;
     IToken/*!*/ parent; .)
  "extends"                (. Parents = new List<ConstantParent/*!*/> ();
                              u = false; .)
  [
    [ "unique"             (. u = true; .)
    ]
    Ident<out parent>      (. Parents.Add(new ConstantParent (
                                          new IdentifierExpr(parent, parent.val), u)); .)
    {
      ","                  (. u = false; .)
      [ "unique"           (. u = true; .)
      ]
      Ident<out parent>    (. Parents.Add(new ConstantParent (
                                          new IdentifierExpr(parent, parent.val), u)); .)
    }
  ]
  [ "complete"             (. ChildrenComplete = true; .)
  ]
  .

/*------------------------------------------------------------------------*/
Function<out DeclarationSeq/*!*/ ds>
= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
     ds = new DeclarationSeq(); IToken/*!*/ z;
     IToken/*!*/ typeParamTok;
     var typeParams = new TypeVariableSeq();
     var arguments = new VariableSeq();
     TypedIdent/*!*/ tyd;
     TypedIdent retTyd = null;
     Bpl.Type/*!*/ retTy;
     QKeyValue argKv = null;
     QKeyValue kv = null;
     Expr definition = null;
     Expr/*!*/ tmp;
  .)
  "function" { Attribute<ref kv> } Ident<out z>
  [ TypeParams<out typeParamTok, out typeParams> ]
  "("
  [ VarOrType<out tyd, out argKv>      (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .)
  { "," VarOrType<out tyd, out argKv>  (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .)
  } ] ")"
  (. argKv = null; .)
  (
    "returns" "(" VarOrType<out retTyd, out argKv> ")"
    |
    ":" Type<out retTy>   (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .)
  )
  ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )
  (.
    if (retTyd == null) {
      // construct a dummy type for the case of syntax error
      retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
    }
    Function/*!*/ func = new Function(z, z.val, typeParams, arguments,
                                      new Formal(retTyd.tok, retTyd, false, argKv), null, kv);
    Contract.Assert(func != null);
    ds.Add(func);
    bool allUnnamed = true;
    foreach(Formal/*!*/ f in arguments){
      Contract.Assert(f != null);
      if (f.TypedIdent.HasName) {
        allUnnamed = false;
        break;
      }
    }
    if (!allUnnamed) {
      Bpl.Type prevType = null;
      for (int i = arguments.Length; 0 <= --i; ) {
        TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;
        if (curr.HasName) {
          // the argument was given as both an identifier and a type
          prevType = curr.Type;
        } else {
          // the argument was given as just one "thing", which syntactically parsed as a type
          if (prevType == null) {
            this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");
            break;
          }
          Bpl.Type ty = curr.Type;
          var uti = ty as UnresolvedTypeIdentifier;
          if (uti != null && uti.Arguments.Length == 0) {
            // the given "thing" was just an identifier, so let's use it as the name of the parameter
            curr.Name = uti.Name;
            curr.Type = prevType;
          } else {
            this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");
          }
        }
      }
    }
    if (definition != null) {
      // generate either an axiom or a function body
      if (QKeyValue.FindBoolAttribute(kv, "inline")) {
        func.Body = definition;
      } else {
        ds.Add(func.CreateDefinitionAxiom(definition, kv));
      }
    }
  .)
  .

VarOrType<out TypedIdent/*!*/ tyd, out QKeyValue kv>
= (.
    Contract.Ensures(Contract.ValueAtReturn(out tyd) != null);
    string/*!*/ varName = TypedIdent.NoName;
    Bpl.Type/*!*/ ty;
    IToken/*!*/ tok;
    kv = null;
  .)
  { Attribute<ref kv> }
  Type<out ty>    (. tok = ty.tok; .)
  [ ":"           (. var uti = ty as UnresolvedTypeIdentifier;
                     if (uti != null && uti.Arguments.Length == 0) {
                       varName = uti.Name;
                     } else {
                       this.SemErr("expected identifier before ':'");
                     }
                  .)
    Type<out ty>
  ]
  (. tyd = new TypedIdent(tok, varName, ty); .)
  .

/*------------------------------------------------------------------------*/
Axiom<out Axiom/*!*/ m>
= (.Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; .)
  "axiom"
   { Attribute<ref kv> }
   (. IToken/*!*/ x = t; .)
  Proposition<out e> ";"  (. m = new Axiom(x,e, null, kv); .)
  .

/*------------------------------------------------------------------------*/
UserDefinedTypes<.out List<Declaration/*!*/>/*!*/ ts.>
= (. Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> (); .)
  "type"
  { Attribute<ref kv> }
  UserDefinedType<out decl, kv>          (.  ts.Add(decl);  .)
  { "," UserDefinedType<out decl, kv>    (.  ts.Add(decl);  .) }
  ";"
  .

UserDefinedType<out Declaration/*!*/ decl, QKeyValue kv>
= (. Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; TokenSeq/*!*/ paramTokens = new TokenSeq ();
     Bpl.Type/*!*/ body = dummyType; bool synonym = false; .)
  Ident<out id>
  [ WhiteSpaceIdents<out paramTokens> ]
  [
    "=" Type<out body>
    (. synonym = true; .)
  ]
  (.
     if (synonym) {
       TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();
       foreach(Token/*!*/ t in paramTokens){
         Contract.Assert(t != null);
         typeParams.Add(new TypeVariable(t, t.val));}
       decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);
     } else {
       decl = new TypeCtorDecl(id, id.val, paramTokens.Length, kv);
     }
   .)
  .


/*------------------------------------------------------------------------*/
Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
= (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
     TypeVariableSeq/*!*/ typeParams;
     VariableSeq/*!*/ ins, outs;
     RequiresSeq/*!*/ pre = new RequiresSeq();
     IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();
     EnsuresSeq/*!*/ post = new EnsuresSeq();

     VariableSeq/*!*/ locals = new VariableSeq();
     StmtList/*!*/ stmtList;
     QKeyValue kv = null;
     impl = null;
  .)

  "procedure"
  ProcSignature<true, out x, out typeParams, out ins, out outs, out kv>
  ( ";"
    { Spec<pre, mods, post> }
  | { Spec<pre, mods, post> }
    ImplBody<out locals, out stmtList>
    (.
      impl = new Implementation(x, x.val, typeParams,
                                Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
    .)
  )
  (. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)
  .


Implementation<out Implementation/*!*/ impl>
= (. Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x;
     TypeVariableSeq/*!*/ typeParams;
     VariableSeq/*!*/ ins, outs;
     VariableSeq/*!*/ locals;
     StmtList/*!*/ stmtList;
     QKeyValue kv;
  .)

  "implementation"
  ProcSignature<false, out x, out typeParams, out ins, out outs, out kv>
  ImplBody<out locals, out stmtList>
    (. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); .)
  .


ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVariableSeq/*!*/ typeParams,
              out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv>
= (. Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);
     IToken/*!*/ typeParamTok; typeParams = new TypeVariableSeq();
     outs = new VariableSeq(); kv = null; .)
  { Attribute<ref kv> }
  Ident<out name>
  [ TypeParams<out typeParamTok, out typeParams> ]
  ProcFormals<true, allowWhereClausesOnFormals, out ins>
  [ "returns" ProcFormals<false, allowWhereClausesOnFormals, out outs> ]
  .


Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>
= (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .)
  ( "modifies"
    [ Idents<out ms>        (. foreach(IToken/*!*/ m in ms){
                                 Contract.Assert(m != null);
                                 mods.Add(new IdentifierExpr(m, m.val));
                               }
                            .)
    ] ";"
  | "free" SpecPrePost<true, pre, post>
  | SpecPrePost<false, pre, post>
  )
  .

SpecPrePost<bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post>
= (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .)
  ( "requires"              (. tok = t; .)
    { Attribute<ref kv> }
    Proposition<out e> ";"  (. pre.Add(new Requires(tok, free, e, null, kv)); .)
  | "ensures"               (. tok = t; .)
    { Attribute<ref kv> }
    Proposition<out e> ";"  (. post.Add(new Ensures(tok, free, e, null, kv)); .)
  )
  .

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

ImplBody<out VariableSeq/*!*/ locals, out StmtList/*!*/ stmtList>
= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new VariableSeq(); .)
  "{"
  { LocalVars<locals> }
  StmtList<out stmtList>
  .

/* the StmtList also reads the final curly brace */
StmtList<out StmtList/*!*/ stmtList>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List<BigBlock/*!*/> bigblocks = new List<BigBlock/*!*/>();
     /* built-up state for the current BigBlock: */
     IToken startToken = null;  string currentLabel = null;
     CmdSeq cs = null;  /* invariant: startToken != null ==> cs != null */
     /* temporary variables: */
     IToken label;  Cmd c;  BigBlock b;
     StructuredCmd ec = null;  StructuredCmd/*!*/ ecn;
     TransferCmd tc = null;  TransferCmd/*!*/ tcn;
  .)

  {
  ( LabelOrCmd<out c, out label>
    (. if (c != null) {
         // LabelOrCmd read a Cmd
         Contract.Assert(label == null);
         if (startToken == null) { startToken = c.tok;  cs = new CmdSeq(); }
         Contract.Assert(cs != null);
         cs.Add(c);
       } else {
         // LabelOrCmd read a label
         Contract.Assert(label != null);
         if (startToken != null) {
           Contract.Assert(cs != null);
           // dump the built-up state into a BigBlock
           b = new BigBlock(startToken, currentLabel, cs, null, null);
           bigblocks.Add(b);
           cs = null;
         }
         startToken = label;
         currentLabel = label.val;
         cs = new CmdSeq();
       }
    .)

  | StructuredCmd<out ecn>
    (. ec = ecn;
       if (startToken == null) { startToken = ec.tok;  cs = new CmdSeq(); }
       Contract.Assert(cs != null);
       b = new BigBlock(startToken, currentLabel, cs, ec, null);
       bigblocks.Add(b);
       startToken = null;  currentLabel = null;  cs = null;
    .)

  | TransferCmd<out tcn>
    (. tc = tcn;
       if (startToken == null) { startToken = tc.tok;  cs = new CmdSeq(); }
       Contract.Assert(cs != null);
       b = new BigBlock(startToken, currentLabel, cs, null, tc);
       bigblocks.Add(b);
       startToken = null;  currentLabel = null;  cs = null;
    .)

  )
  }
  "}"
  (. IToken/*!*/ endCurly = t;
     if (startToken == null && bigblocks.Count == 0) {
       startToken = t;  cs = new CmdSeq();
     }
     if (startToken != null) {
       Contract.Assert(cs != null);
       b = new BigBlock(startToken, currentLabel, cs, null, null);
       bigblocks.Add(b);
     }

     stmtList = new StmtList(bigblocks, endCurly);
  .)
  .

TransferCmd<out TransferCmd/*!*/ tc>
= (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;
     Token y;  TokenSeq/*!*/ xs;
     StringSeq ss = new StringSeq();
  .)
  ( "goto"             (. y = t; .)
    Idents<out xs>     (. foreach(IToken/*!*/ s in xs){
                            Contract.Assert(s != null);
                            ss.Add(s.val); }
                          tc = new GotoCmd(y, ss);
                       .)
  | "return"           (. tc = new ReturnCmd(t); .)
  ) ";"
  .

StructuredCmd<out StructuredCmd/*!*/ ec>
= (. Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd;  Contract.Assume(cce.IsPeerConsistent(ec));
     IfCmd/*!*/ ifcmd;  WhileCmd/*!*/ wcmd;  BreakCmd/*!*/ bcmd;
  .)
  ( IfCmd<out ifcmd>    (. ec = ifcmd; .)
  | WhileCmd<out wcmd>  (. ec = wcmd; .)
  | BreakCmd<out bcmd>  (. ec = bcmd; .)
  )
  .

IfCmd<out IfCmd/*!*/ ifcmd>
= (. Contract.Ensures(Contract.ValueAtReturn(out ifcmd) != null); IToken/*!*/ x;
     Expr guard;
     StmtList/*!*/ thn;
     IfCmd/*!*/ elseIf;  IfCmd elseIfOption = null;
     StmtList/*!*/ els;  StmtList elseOption = null;
  .)
  "if"                       (. x = t; .)
  Guard<out guard>
  "{" StmtList<out thn>
  [ "else"
    ( IfCmd<out elseIf>      (. elseIfOption = elseIf; .)
    | "{"
      StmtList<out els>      (. elseOption = els; .)
    )
  ]
  (. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); .)
  .

WhileCmd<out WhileCmd/*!*/ wcmd>
= (. Contract.Ensures(Contract.ValueAtReturn(out wcmd) != null); IToken/*!*/ x;  Token z;
     Expr guard;  Expr/*!*/ e;  bool isFree;
     List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();
     StmtList/*!*/ body;
     QKeyValue kv = null;
  .)
  "while"             (. x = t; .)
  Guard<out guard>    (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
  {                   (. isFree = false; z = la/*lookahead token*/; .)
    [ "free"          (. isFree = true;  .)
    ]
    "invariant"
    { Attribute<ref kv> }
    Expression<out e> (. if (isFree) {
                           invariants.Add(new AssumeCmd(z, e, kv));
                         } else {
                           invariants.Add(new AssertCmd(z, e, kv));
                         }
                      .)
    ";"
  }
  "{"
  StmtList<out body>  (. wcmd = new WhileCmd(x, guard, invariants, body); .)
  .

Guard<out Expr e>
= (. Expr/*!*/ ee;  e = null; .)
  "("
  ( "*"                   (. e = null; .)
  | Expression<out ee>    (. e = ee; .)
  )
  ")"
  .

BreakCmd<out BreakCmd/*!*/ bcmd>
= (.Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x;  IToken/*!*/ y;
     string breakLabel = null;
  .)
  "break"             (. x = t; .)
  [ Ident<out y>      (. breakLabel = y.val; .)
  ] ";"               (. bcmd = new BreakCmd(x, breakLabel); .)
  .

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

LabelOrCmd<out Cmd c, out IToken label>
/* ensures (c == null) != (label != null) */
= (. IToken/*!*/ x; Expr/*!*/ e;
     TokenSeq/*!*/ xs;
     IdentifierExprSeq ids;
     c = dummyCmd;  label = null;
     Cmd/*!*/ cn;
     QKeyValue kv = null;
  .)
  ( LabelOrAssign<out c, out label>
  | "assert"              (. x = t; .)
    { Attribute<ref kv> }
    Proposition<out e>    (. c = new AssertCmd(x, e, kv); .)
    ";"
  | "assume"              (. x = t; .)
    { Attribute<ref kv> }
    Proposition<out e>    (. c = new AssumeCmd(x, e, kv); .)
    ";"
  | "havoc"               (. x = t; .)
    Idents<out xs> ";"    (. ids = new IdentifierExprSeq();
                             foreach(IToken/*!*/ y in xs){
                               Contract.Assert(y != null);
                               ids.Add(new IdentifierExpr(y, y.val));
                             }
                             c = new HavocCmd(x,ids);
                          .)
  | CallCmd<out cn> ";"   (. c = cn; .)
  | "yield"               (. x = t; .)
    ";"                   (. c = new YieldCmd(x); .)
  )
  .

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

LabelOrAssign<out Cmd c, out IToken label>
/* ensures (c == null) != (label != null) */
= (. IToken/*!*/ id; IToken/*!*/ x, y; Expr/*!*/ e0;
     c = dummyCmd;  label = null;
     AssignLhs/*!*/ lhs;
     List<AssignLhs/*!*/>/*!*/ lhss;
     List<Expr/*!*/>/*!*/ rhss;
     List<Expr/*!*/>/*!*/ indexes;
  .)
  Ident<out id>              (. x = t; .)
  ( ":"                      (. c = null;  label = x; .)

  | (. lhss = new List<AssignLhs/*!*/>(); .)
    (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)

    { MapAssignIndex<out y, out indexes>    (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
    (. lhss.Add(lhs); .)

    { ","
      Ident<out id>
      (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
      { MapAssignIndex<out y, out indexes>    (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
      (. lhss.Add(lhs); .)
    }

    ":="                     (. x = t; /* use location of := */ .)
    Expression<out e0>       (. rhss = new List<Expr/*!*/> ();
                                rhss.Add(e0); .)
    { ","
      Expression<out e0>     (. rhss.Add(e0); .)
    }
    ";"                      (. c = new AssignCmd(x, lhss, rhss); .)
  )
  .

MapAssignIndex<.out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes.>
= (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
     Expr/*!*/ e;
  .)
  "["                        (. x = t; .)
    [
      Expression<out e>      (. indexes.Add(e); .)
      { ","
        Expression<out e>    (. indexes.Add(e); .)
      }
    ]
  "]"
  .

/*------------------------------------------------------------------------*/
CallCmd<out Cmd c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); 
     IToken x; 
     bool isAsync = false;
     bool isFree = false;
     QKeyValue kv = null;
     c = null;
  .)
  [ "async"          (. isAsync = true;  .)
  ]
  [ "free"          (. isFree = true;  .)
  ]
  "call"                          (. x = t; .)
  { Attribute<ref kv> }
  CallParams<isAsync, isFree, kv, x, ref c> (. .) 
  { "|" CallParams<isAsync, isFree, kv, x, ref c> (. .) 
  }
  .

CallParams<bool isAsync, bool isFree, QKeyValue kv, IToken x, ref Cmd c>
= (. 
    List<IdentifierExpr> ids = new List<IdentifierExpr>();
    List<Expr> es = new List<Expr>();
    Expr en;
    IToken first; 
    IToken p;
  .)
  Ident<out first>
    ( "("
      [ Expression<out en>       (. es.Add(en); .)
        { "," Expression<out en> (. es.Add(en); .)
        }
      ]
      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
    |
                                  (. ids.Add(new IdentifierExpr(first, first.val)); .)
      [ "," Ident<out p>  (. ids.Add(new IdentifierExpr(p, p.val)); .)
        { "," Ident<out p>  (. ids.Add(new IdentifierExpr(p, p.val)); .)
        }
      ] ":="
      Ident<out first> "("
      [ Expression<out en>       (. es.Add(en); .)
        { "," Expression<out en> (. es.Add(en); .)
        }
      ]
      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
    )
  .

/*------------------------------------------------------------------------*/
Proposition<out Expr/*!*/ e>
=(.Contract.Ensures(Contract.ValueAtReturn(out e) != null);.)
  Expression<out e>
  .

/*------------------------------------------------------------------------*/
Idents<out TokenSeq/*!*/ xs>
= (.Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq(); .)
  Ident<out id>                 (. xs.Add(id); .)
  { "," Ident<out id>           (. xs.Add(id); .)
  }
  .

/*------------------------------------------------------------------------*/
WhiteSpaceIdents<out TokenSeq/*!*/ xs>
= (. Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq(); .)
  Ident<out id>                 (. xs.Add(id); .)
  { Ident<out id>               (. xs.Add(id); .)
  }
  .

/*------------------------------------------------------------------------*/
Expressions<out ExprSeq/*!*/ es>
= (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq(); .)
  Expression<out e>             (. es.Add(e); .)
  { "," Expression<out e>       (. es.Add(e); .)
  }
  .

/*------------------------------------------------------------------------*/
Expression<out Expr/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
  ImpliesExpression<false, out e0>
  { EquivOp        (. x = t; .)
    ImpliesExpression<false, out e1>
                   (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .)
  }
  .

EquivOp = "<==>" | '\u21d4'.

/*------------------------------------------------------------------------*/
ImpliesExpression<bool noExplies, out Expr/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
  LogicalExpression<out e0>
  [
    ImpliesOp      (. x = t; .)
    /* recurse because implication is right-associative */
    ImpliesExpression<true, out e1>
                   (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); .)
  |
    ExpliesOp      (. if (noExplies)
                        this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");
                      x = t; .)
    LogicalExpression<out e1>
                   (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)
    /* loop because explies is left-associative */
    {
      ExpliesOp    (. x = t; .)
      LogicalExpression<out e1>
                   (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)
    }
  ]
  .

ImpliesOp = "==>" | '\u21d2'.
ExpliesOp = "<==" | '\u21d0'.

/*------------------------------------------------------------------------*/
LogicalExpression<out Expr/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
  RelationalExpression<out e0>
  [ AndOp          (. x = t; .)
    RelationalExpression<out e1>
    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
    { AndOp        (. x = t; .)
      RelationalExpression<out e1>
      (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
    }
  | OrOp           (. x = t; .)
    RelationalExpression<out e1>
    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
    { OrOp         (. x = t; .)
      RelationalExpression<out e1>
      (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
    }
  ]
  .

AndOp = "&&" | '\u2227'.
OrOp = "||" | '\u2228'.

/*------------------------------------------------------------------------*/
RelationalExpression<out Expr/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
  BvTerm<out e0>
  [ RelOp<out x, out op>
    BvTerm<out e1>            (. e0 = Expr.Binary(x, op, e0, e1); .)
  ]
  .

RelOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
=                  (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
  ( "=="           (. x = t; op=BinaryOperator.Opcode.Eq; .)
  | "<"            (. x = t; op=BinaryOperator.Opcode.Lt; .)
  | ">"            (. x = t; op=BinaryOperator.Opcode.Gt; .)
  | "<="           (. x = t; op=BinaryOperator.Opcode.Le; .)
  | ">="           (. x = t; op=BinaryOperator.Opcode.Ge; .)
  | "!="           (. x = t; op=BinaryOperator.Opcode.Neq; .)
  | "<:"           (. x = t; op=BinaryOperator.Opcode.Subtype; .)
  | '\u2260'       (. x = t; op=BinaryOperator.Opcode.Neq; .)
  | '\u2264'       (. x = t; op=BinaryOperator.Opcode.Le; .)
  | '\u2265'       (. x = t; op=BinaryOperator.Opcode.Ge; .)
  )
  .

/*------------------------------------------------------------------------*/
BvTerm<out Expr/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
  Term<out e0>
  { "++"                  (. x = t; .)
    Term<out e1>          (. e0 = new BvConcatExpr(x, e0, e1); .)
  }
  .


/*------------------------------------------------------------------------*/
Term<out Expr/*!*/ e0>
= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
  Factor<out e0>
  { AddOp<out x, out op>
    Factor<out e1>          (. e0 = Expr.Binary(x, op, e0, e1); .)
  }
  .

AddOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
=                  (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
  ( "+"            (. x = t; op=BinaryOperator.Opcode.Add; .)
  | "-"            (. x = t; op=BinaryOperator.Opcode.Sub; .)
  )
  .

/*------------------------------------------------------------------------*/
Factor<out Expr/*!*/ e0>
= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
  Power<out e0>
  { MulOp<out x, out op>
    Power<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
  }
  .

MulOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
=                  (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
  ( "*"            (. x = t; op=BinaryOperator.Opcode.Mul; .)
  | "div"          (. x = t; op=BinaryOperator.Opcode.Div; .)
  | "mod"          (. x = t; op=BinaryOperator.Opcode.Mod; .)
  | "/"            (. x = t; op=BinaryOperator.Opcode.RealDiv; .)
  )
  .

/*------------------------------------------------------------------------*/
Power<out Expr/*!*/ e0>
= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
  UnaryExpression<out e0>
  [
    "**"           (. x = t; .)
    /* recurse because exponentation is right-associative */
    Power<out e1>  (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); .)
  ]
  .

/*------------------------------------------------------------------------*/
UnaryExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
     e = dummyExpr;
  .)
  ( "-"                        (. x = t; .)
    UnaryExpression<out e>     (. e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); .)
  | NegOp                      (. x = t; .)
    UnaryExpression<out e>     (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .)
  | CoercionExpression<out e>
  )
  .

NegOp = "!" | '\u00ac'.

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

/* This production creates ambiguities, because types can start with "<"
   (polymorphic map types), but can also be followed by "<" (inequalities).
   Coco deals with these ambiguities in a reasonable way by preferring to read
   further types (type arguments) over relational symbols. E.g., "5 : C < 0"
   will cause a parse error because "<" is treated as the beginning of a
   map type. */

CoercionExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
     Bpl.Type/*!*/ coercedTo;
     BigNum bn;
    .)
  ArrayExpression<out e>
  { ":"                     (. x = t; .)
    (
      Type<out coercedTo>   (. e = Expr.CoerceType(x, e, coercedTo); .)
    |
      Nat<out bn>           /* This means that we really look at a bitvector
                               expression t[a:b] */
                            (. if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {
                                 this.SemErr("arguments of extract need to be integer literals");
                                 e = new BvBounds(x, bn, BigNum.ZERO);
                               } else {
                                 e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
                               }
                             .)
    )
  }
  .

/*------------------------------------------------------------------------*/
ArrayExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
     Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1;
     bool store; bool bvExtract;
     ExprSeq/*!*/ allArgs = dummyExprSeq;
  .)
  AtomExpression<out e>
  { "["        (. x = t; allArgs = new ExprSeq ();
                  allArgs.Add(e);
                  store = false; bvExtract = false; .)
      [
        Expression<out index0>
               (. if (index0 is BvBounds)
                    bvExtract = true;
                  else
                    allArgs.Add(index0);
               .)
        { "," Expression<out e1>
               (. if (bvExtract || e1 is BvBounds)
                    this.SemErr("bitvectors only have one dimension");
                  allArgs.Add(e1);
               .)
        }
        [ ":=" Expression<out e1>
               (. if (bvExtract || e1 is BvBounds)
                    this.SemErr("assignment to bitvectors is not possible");
                  allArgs.Add(e1); store = true;
               .)
        ]
      | ":=" Expression<out e1>       (. allArgs.Add(e1); store = true; .)
      ]
    "]"
    (. if (store)
         e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);
       else if (bvExtract)
         e = new BvExtractExpr(x, e,
                               ((BvBounds)index0).Upper.ToIntSafe,
                               ((BvBounds)index0).Lower.ToIntSafe);
       else
         e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
    .)
  }
  .


/*------------------------------------------------------------------------*/
AtomExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
     ExprSeq/*!*/ es;  VariableSeq/*!*/ ds;  Trigger trig;
     TypeVariableSeq/*!*/ typeParams;
     IdentifierExpr/*!*/ id;
     QKeyValue kv;
     e = dummyExpr;
     VariableSeq/*!*/ locals;
     List<Block/*!*/>/*!*/ blocks;
  .)
  ( "false"           (. e = new LiteralExpr(t, false); .)
  | "true"            (. e = new LiteralExpr(t, true); .)
  | Nat<out bn>            (. e = new LiteralExpr(t, bn); .)
  | Dec<out bd>            (. e = new LiteralExpr(t, bd); .)
  | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)

  | Ident<out x>            (. id = new IdentifierExpr(x, x.val);  e = id; .)
    [ "("
      ( Expressions<out es> (. e = new NAryExpr(x, new FunctionCall(id), es); .)
      | /* empty */         (. e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); .)
      )
      ")"
    ]

  | "old"                   (. x = t; .)
    "("
    Expression<out e>
    ")"                     (. e = new OldExpr(x, e); .)

  | "int"                   (. x = t; .)
    "("
    Expression<out e>
    ")"                     (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); .)

  | "real"                  (. x = t; .)
    "("
    Expression<out e>
    ")"                     (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); .)

  | "(" ( Expression<out e>                 (. if (e is BvBounds)
                                                 this.SemErr("parentheses around bitvector bounds " +
                                                        "are not allowed"); .)
        | Forall                            (. x = t; .)
          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>
                                            (. if (typeParams.Length + ds.Length > 0)
                                                 e = new ForallExpr(x, typeParams, ds, kv, trig, e); .)
        | Exists                            (. x = t; .)
          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>
                                            (. if (typeParams.Length + ds.Length > 0)
                                                 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .)
        | Lambda                            (. x = t; .)
          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>
                                            (. if (trig != null)
                                                 SemErr("triggers not allowed in lambda expressions");
                                               if (typeParams.Length + ds.Length > 0)
                                                 e = new LambdaExpr(x, typeParams, ds, kv, e); .)
        )
    ")"
  | IfThenElseExpression<out e>
  | CodeExpression<out locals, out blocks> (. e = new CodeExpr(locals, blocks); .)
  )
  .

CodeExpression<.out VariableSeq/*!*/ locals, out List<Block/*!*/>/*!*/ blocks.>
= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new VariableSeq(); Block/*!*/ b;
     blocks = new List<Block/*!*/>();
  .)
  "|{"
  { LocalVars<locals> }
  SpecBlock<out b>          (. blocks.Add(b); .)
  { SpecBlock<out b>        (. blocks.Add(b); .)
  }
  "}|"
  .

SpecBlock<out Block/*!*/ b>
= (. Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;
     Cmd c;  IToken label;
     CmdSeq cs = new CmdSeq();
     TokenSeq/*!*/ xs;
     StringSeq ss = new StringSeq();
     b = dummyBlock;
     Expr/*!*/ e;
  .)
  Ident<out x> ":"
  { LabelOrCmd<out c, out label>
                       (. if (c != null) {
                            Contract.Assert(label == null);
                            cs.Add(c);
                          } else {
                            Contract.Assert(label != null);
                            SemErr("SpecBlock's can only have one label");
                          }
                       .)
  }
  ( "goto"             (. y = t; .)
    Idents<out xs>     (. foreach(IToken/*!*/ s in xs){
                            Contract.Assert(s != null);
                            ss.Add(s.val); }
                          b = new Block(x,x.val,cs,new GotoCmd(y,ss));
                       .)
  | "return" Expression<out e>
                       (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)
  )
  ";"
  .

Attribute<ref QKeyValue kv>
= (. Trigger trig = null; .)
  AttributeOrTrigger<ref kv, ref trig> (.  if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .)
.

AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
= (. IToken/*!*/ tok;  Expr/*!*/ e;  ExprSeq/*!*/ es;
     string key;
     List<object/*!*/> parameters;  object/*!*/ param;
  .)
  "{"                                         (. tok = t; .)
     (
       ":" ident                              (. key = t.val;  parameters = new List<object/*!*/>(); .)
       [ AttributeParameter<out param>        (. parameters.Add(param); .)
         { "," AttributeParameter<out param>  (. parameters.Add(param); .)
         }
       ]
       (. if (key == "nopats") {
            if (parameters.Count == 1 && parameters[0] is Expr) {
              e = (Expr)parameters[0];
              if(trig==null){
                trig = new Trigger(tok, false, new ExprSeq(e), null);
              } else {
                trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null));
              }
            } else {
              this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");
            }
          } else {
            if (kv==null) {
              kv = new QKeyValue(tok, key, parameters, null);
            } else {
              kv.AddLast(new QKeyValue(tok, key, parameters, null));
            }
          }
       .)
     |
       Expression<out e>       (. es = new ExprSeq(e); .)
       { "," Expression<out e> (. es.Add(e); .)
       }                       (. if (trig==null) {
                                    trig = new Trigger(tok, true, es, null);
                                  } else {
                                    trig.AddLast(new Trigger(tok, true, es, null));
                                  }
                               .)
     )
  "}"
  .

AttributeParameter<out object/*!*/ o>
= (. Contract.Ensures(Contract.ValueAtReturn(out o) != null);
     o = "error";
     Expr/*!*/ e;
  .)
  ( string                (. o = t.val.Substring(1, t.val.Length-2); .)
  | Expression<out e>     (. o = e; .)
  )
  .

IfThenElseExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
     IToken/*!*/ tok;
     Expr/*!*/ e0, e1, e2;
     e = dummyExpr; .)
  "if" (. tok = t; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>
  (. e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); .)
  .


QuantifierBody<IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out VariableSeq/*!*/ ds,
               out QKeyValue kv, out Trigger trig, out Expr/*!*/ body>
= (. Contract.Requires(q != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); Contract.Ensures(Contract.ValueAtReturn(out body) != null);
     trig = null; typeParams = new TypeVariableSeq ();
     IToken/*!*/ tok;
     kv = null;
     ds = new VariableSeq ();
  .)
  (
     TypeParams<out tok, out typeParams>
     [ BoundVars<q, out ds> ]
  |
     BoundVars<q, out ds>
  )
  QSep
  { AttributeOrTrigger<ref kv, ref trig> }
  Expression<out body>
  .

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

/*------------------------------------------------------------------------*/
Ident<out IToken/*!*/ x>
=(.Contract.Ensures(Contract.ValueAtReturn(out x) != null);.)
  ident            (.  x = t;
                       if (x.val.StartsWith("\\"))
                         x.val = x.val.Substring(1);
                    .)
  .

/*------------------------------------------------------------------------*/
Nat<out BigNum n>
=
  digits
  (. try {
       n = BigNum.FromString(t.val);
     } catch (FormatException) {
       this.SemErr("incorrectly formatted number");
       n = BigNum.ZERO;
     }
  .)
  .

/*------------------------------------------------------------------------*/
Dec<out BigDec n>
= (. string s = ""; .)
  (
    decimal   (. s = t.val; .)
  |
    float     (. s = t.val; .)
  )
  (. try {
       n = BigDec.FromString(s);
     } catch (FormatException) {
       this.SemErr("incorrectly formatted number");
       n = BigDec.ZERO;
     }
  .)
  .

/*------------------------------------------------------------------------*/
BvLit<out BigNum n, out int m>
=
  bvlit
  (.
     int pos = t.val.IndexOf("bv");
     string a = t.val.Substring(0, pos);
     string b = t.val.Substring(pos + 2);
     try {
       n = BigNum.FromString(a);
       m = Convert.ToInt32(b);
     } catch (FormatException) {
       this.SemErr("incorrectly formatted bitvector");
       n = BigNum.ZERO;
       m = 0;
     }
  .)
  .
END BoogiePL.