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;
using AI = Microsoft.AbstractInterpretationFramework;


COMPILER BoogiePL

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

static Program/*!*/ Pgm = new Program();

static Expr/*!*/ dummyExpr = new LiteralExpr(Token.NoToken, false);
static Cmd/*!*/ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
static Block/*!*/ dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(),
                                     new ReturnCmd(Token.NoToken));
static Bpl.Type/*!*/ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
static Bpl.ExprSeq/*!*/ dummyExprSeq = new ExprSeq ();
static TransferCmd/*!*/ dummyTransferCmd = new ReturnCmd(Token.NoToken);
static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);

///<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);
  Pgm = new Program(); // reset the global variable
    parser.Parse();
    if (parser.errors.count == 0)
    {
      program = Pgm;
      program.ProcessDatatypeConstructors();
      return 0;
    }
    else
    {
      program = null;
      return parser.errors.count;
    }
}

// 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){//BASEMOVE
    Contract.Requires(tok != null);
    //:base(tok);
    this.Lower = lower;
    this.Upper = upper;
  }
  public override Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<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.Requires(stream != null);
    {Contract.Assert(false);throw new cce.UnreachableException();}
  }
  public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
  public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {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.

  float = digit {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); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null; .)
  "var"
  { Attribute<ref kv> }
  IdsTypeWheres<true, tyds> ";"
  (. foreach(TypedIdent/*!*/ tyd in tyds){
       Contract.Assert(tyd != null);
       ds.Add(new GlobalVariable(tyd.tok, tyd, kv));
     }
  .)
  .

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

ProcFormals<bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds>
= (.Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); .)
  "("
  [ IdsTypeWheres<allowWhereClauses, tyds> ]
  ")"
  (. foreach(TypedIdent/*!*/ tyd in tyds){
       Contract.Assert(tyd != null);
       ds.Add(new Formal(tyd.tok, tyd, incoming));
     }
  .)
  .

BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds>
= (. Contract.Requires(x != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); .)
  IdsTypeWheres<false, tyds>
  (. foreach(TypedIdent/*!*/ tyd in tyds){
       Contract.Assert(tyd != null);
       ds.Add(new BoundVariable(tyd.tok, tyd));
     }
  .)
  .

/*------------------------------------------------------------------------*/
/* 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));
     }
  .)
  .

/* IdsTypeWheres is used with the declarations of global and local variables,
   procedure parameters, and quantifier bound variables. */
IdsTypeWheres<bool allowWhereClauses, TypedIdentSeq/*!*/ tyds>
=(.Contract.Requires(tyds != null);.)
  IdsTypeWhere<allowWhereClauses, tyds>
  { "," IdsTypeWhere<allowWhereClauses, tyds> }
  .

IdsTypeWhere<bool allowWhereClauses, TypedIdentSeq/*!*/ tyds>
= (.Contract.Requires(tyds != null); TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty;  Expr wh = null;  Expr/*!*/ nne; .)
  Idents<out ids> ":" Type<out ty>
  [ "where" Expression<out nne>  (. if (allowWhereClauses) {
                                      wh = nne;
                                    } else {
                                      this.SemErr("where clause not allowed here");
                                    }
                                 .)
  ]
  (. foreach(Token/*!*/ id in ids){
       Contract.Assert(id != null);
       tyds.Add(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; 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); .)
  | "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();
     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;
     TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();
     VariableSeq arguments = new VariableSeq();
     TypedIdent/*!*/ tyd;
     TypedIdent retTyd = null;
     Type/*!*/ retTy;
     QKeyValue kv = null;
     Expr definition = null;
     Expr/*!*/ tmp;
  .)
  "function" { Attribute<ref kv> } Ident<out z>
  [ TypeParams<out typeParamTok, out typeParams> ]
  "("
  [ VarOrType<out tyd>      (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)
  { "," VarOrType<out tyd>  (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)
  } ] ")"
  (
    "returns" "(" VarOrType<out tyd> ")" (. retTyd = tyd; .)
    |
    ":" Type<out retTy>   (. retTyd = new TypedIdent(retTy.tok, "", retTy); .)
  )
  ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )
  (.
    if (retTyd == null) {
      // construct a dummy type for the case of syntax error
      tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int));
    } else {
      tyd = retTyd;
    }
    Function/*!*/ func = new Function(z, z.val, typeParams, arguments,
                           new Formal(tyd.tok, tyd, false), null, kv);
    Contract.Assert(func != null);
    ds.Add(func);
    bool allUnnamed = true;
    foreach(Formal/*!*/ f in arguments){
      Contract.Assert(f != null);
      if (f.TypedIdent.Name != "") {
        allUnnamed = false;
	break;
      }
    }
    if (!allUnnamed) {
      Type prevType = null;
      for (int i = arguments.Length - 1; i >= 0; i--) {
        TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;
        if (curr.Name == "") {
	  if (prevType == null) {
	    this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");
	    break;
	  }
	  Type ty = curr.Type;
          if (ty is UnresolvedTypeIdentifier &&
              cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {
	    curr.Name = cce.NonNull(ty as UnresolvedTypeIdentifier).Name;
	    curr.Type = prevType;
	  } else {
	    this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");
	  }
	} else {
	  prevType = curr.Type;
	}
      }
    }
    if (definition != null) {
      // generate either an axiom or a function body
      if (QKeyValue.FindBoolAttribute(kv, "inline")) {
        func.Body = definition;
      } else {
        VariableSeq dummies = new VariableSeq();
        ExprSeq callArgs = new ExprSeq();
        int i = 0;
        foreach(Formal/*!*/ f in arguments){
          Contract.Assert(f != null);
          string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;
          dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));
          callArgs.Add(new IdentifierExpr(f.tok, nm));
          i++;
        }
        TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();
        foreach(TypeVariable/*!*/ t in typeParams){
          Contract.Assert(t != null);
          quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));
        }

        Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);
        // specify the type of the function, because it might be that
        // type parameters only occur in the output type
        call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());
        Expr def = Expr.Eq(call, definition);
        if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {
          def = new ForallExpr(z, quantifiedTypeVars, dummies,
                               kv,
                               new Trigger(z, true, new ExprSeq(call), null),
                               def);
        }
        ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));
      }
    }
  .)
  .

VarOrType<out TypedIdent/*!*/ tyd>
= (.Contract.Ensures(Contract.ValueAtReturn(out tyd) != null); string/*!*/ varName = ""; Bpl.Type/*!*/ ty; IToken/*!*/ tok; .)
  Type<out ty>    (. tok = ty.tok; .)
  [ ":"           (. if (ty is UnresolvedTypeIdentifier &&
                         cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {
                       varName = cce.NonNull(ty as UnresolvedTypeIdentifier).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 ();
     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; .)
  )
  .

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

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; IToken/*!*/ first; IToken p;
     List<IdentifierExpr>/*!*/ ids = new List<IdentifierExpr>();
     List<Expr>/*!*/ es = new List<Expr>();
     QKeyValue kv = null;
     Expr en;  List<Expr> args;
     c = dummyCmd;
     bool isFree = false;
  .)
  [ "free"          (. isFree = true;  .)
  ]
  "call"                          (. x = t; .)
  { Attribute<ref kv> }
  ( Ident<out first>
    ( "("
      [ CallForallArg<out en>       (. es.Add(en); .)
        { "," CallForallArg<out en> (. es.Add(en); .)
        }
      ]
      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
    |
                                  (. ids.Add(new IdentifierExpr(first, first.val)); .)
      [ "," CallOutIdent<out p>  (.
                                     if (p==null) {
                                        ids.Add(null);
                                     } else {
                                        ids.Add(new IdentifierExpr(p, p.val));
                                     }
                                  .)
        { "," CallOutIdent<out p>  (.
                                     if (p==null) {
                                        ids.Add(null);
                                     } else {
                                        ids.Add(new IdentifierExpr(p, p.val));
                                     }
                                  .)
        }
      ] ":="
      Ident<out first> "("
      [ CallForallArg<out en>       (. es.Add(en); .)
        { "," CallForallArg<out en> (. es.Add(en); .)
        }
      ]
      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
    )
  | "forall"
    Ident<out first> "("              (. args = new List<Expr>(); .)
    [ CallForallArg<out en>       (. args.Add(en); .)
      { "," CallForallArg<out en> (. args.Add(en); .)
      }
    ]
    ")"                           (. c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree; .)
  | "*"
                                  (. ids.Add(null); .)
      [ "," CallOutIdent<out p>  (.
                                     if (p==null) {
                                        ids.Add(null);
                                     } else {
                                        ids.Add(new IdentifierExpr(p, p.val));
                                     }
                                  .)
        { "," CallOutIdent<out p>  (.
                                     if (p==null) {
                                        ids.Add(null);
                                     } else {
                                        ids.Add(new IdentifierExpr(p, p.val));
                                     }
                                  .)
        }
      ] ":="
      Ident<out first> "("
      [ CallForallArg<out en>       (. es.Add(en); .)
        { "," CallForallArg<out en> (. es.Add(en); .)
        }
      ]
      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
  )
  .

CallOutIdent<out IToken id>
= (. id = null;
     IToken/*!*/ p;
  .)
  ( "*"
  | Ident<out p>                   (. id = p; .)
  )
  .

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

/*------------------------------------------------------------------------*/
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; .)
  UnaryExpression<out e0>
  { MulOp<out x, out op>
    UnaryExpression<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; .)
  | "/"            (. x = t; op=BinaryOperator.Opcode.Div; .)
  | "%"            (. x = t; op=BinaryOperator.Opcode.Mod; .)
  )
  .

/*------------------------------------------------------------------------*/
UnaryExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
     e = dummyExpr;
  .)
  ( "-"                        (. x = t; .)
    UnaryExpression<out e>     (. e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), 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;
     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;
     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); .)
  | 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); .)

  | "(" ( 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;
     }
  .)
  .

/*------------------------------------------------------------------------*/
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.