path: root/Dafny/Dafny.atg

/*-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------
// Dafny
// Rustan Leino, first created 25 January 2008
//--------------------------------------------------------------------------*/

using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;


COMPILER Dafny

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

static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();


static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression! dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static Scope<string>! parseVarScope = new Scope<string>();
static int anonymousIds = 0;

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

// helper routine for parsing call statements
private static void RecordCallLhs(IdentifierExpr! e,
                                  List<IdentifierExpr!>! lhs,
                                  List<AutoVarDecl!>! newVars) {
  int index = lhs.Count;
  lhs.Add(e);
  if (parseVarScope.Find(e.Name) == null) {
    AutoVarDecl d = new AutoVarDecl(e.tok, e.Name, new InferredTypeProxy(), index);
    newVars.Add(d);
    parseVarScope.Push(e.Name, e.Name);
  }
}

// helper routine for parsing call statements
private static Expression! ConvertToLocal(Expression! e)
{
  FieldSelectExpr fse = e as FieldSelectExpr;
  if (fse != null && fse.Obj is ImplicitThisExpr) {
    return new IdentifierExpr(fse.tok, fse.FieldName);
  }
  return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
}

///<summary>
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "modules".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws System.IO.IOException */ {
  if (filename == "stdin.dfy") {
    BoogiePL.Buffer.Fill(System.Console.In);
    Scanner.Init(filename);
    return Parse(modules);
  } else {
    using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
      BoogiePL.Buffer.Fill(reader);
      Scanner.Init(filename);
      return Parse(modules);
    }
  }
}

///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
public static int Parse (List<ModuleDecl!>! modules) {
  List<ModuleDecl!> oldModules = theModules;
  theModules = modules;
  Parse();
  theModules = oldModules;
  return Errors.count;
}

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

  cr        = '\r'.
  lf        = '\n'.
  tab       = '\t'.

  space = ' '.
  quote = '"'.

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


/*------------------------------------------------------------------------*/
TOKENS
  ident =  nondigit {nondigit | digit}.
  digits = digit {digit}.
  string = quote {nonquote} quote.

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

IGNORE cr + lf + tab


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

Dafny
= (. ClassDecl! c; DatatypeDecl! dt;
     Attributes attrs;  Token! id;  List<string!> theImports;

     List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();
     ModuleDecl module;
     DefaultModuleDecl defaultModule = new DefaultModuleDecl();
  .)
  { "module"                             (. attrs = null;  theImports = new List<string!>(); .)
    { Attribute<ref attrs> }
    Ident<out id>
    [ "imports" Idents<theImports> ]     (. module = new ModuleDecl(id, id.val, theImports, attrs); .)
    "{"
      { ClassDecl<module, out c>         (. module.TopLevelDecls.Add(c); .)
      | DatatypeDecl<module, out dt>     (. module.TopLevelDecls.Add(dt); .)
      }                                  (. theModules.Add(module); .)
    "}"
  | ClassDecl<defaultModule, out c>      (. defaultModule.TopLevelDecls.Add(c); .)
  | DatatypeDecl<defaultModule, out dt>  (. defaultModule.TopLevelDecls.Add(dt); .)
  | ClassMemberDecl<membersDefaultClass>
  }
  (. defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
     theModules.Add(defaultModule);
  .)
  EOF
  .

ClassDecl<ModuleDecl! module, out ClassDecl! c>
= (. Token! id;
     Attributes attrs = null;
     List<TypeParameter!> typeArgs = new List<TypeParameter!>();
     List<MemberDecl!> members = new List<MemberDecl!>();
  .)
  "class"
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  "{"
  { ClassMemberDecl<members>
  }
  "}"                                      (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); .)
  .

ClassMemberDecl<List<MemberDecl!\>! mm>
= (. Method! m;
     Function! f;
     MemberModifiers mmod = new MemberModifiers();
  .)
  { "ghost"                                (. mmod.IsGhost = true; .)
  | "static"                               (. mmod.IsStatic = true; .)
  | "unlimited"                            (. mmod.IsUnlimited = true; .)
  }
  ( FieldDecl<mmod, mm>
  | FunctionDecl<mmod, out f>              (. mm.Add(f); .)
  | MethodDecl<mmod, out m>                (. mm.Add(m); .)
  )
  .

DatatypeDecl<ModuleDecl! module, out DatatypeDecl! dt>
= (. Token! id;
     Attributes attrs = null;
     List<TypeParameter!> typeArgs = new List<TypeParameter!>();
     List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();
  .)
  "datatype"
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  "{"
  { DatatypeMemberDecl<ctors>
  }
  "}"                                      (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); .)
  .

DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>
= (. Attributes attrs = null;
     Token! id;
     List<TypeParameter!> typeArgs = new List<TypeParameter!>();
     List<Formal!> formals = new List<Formal!>();
  .)
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  (. parseVarScope.PushMarker(); .)
  [ FormalsOptionalIds<formals> ]
  (. parseVarScope.PopMarker();
     ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
  .)
  ";"
  .

FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>
= (. Attributes attrs = null;
     Token! id;  Type! ty;
  .)
  "var"
  (. if (mmod.IsUnlimited) { SemErr(token, "fields cannot be declared 'unlimited'"); }
     if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }
  .)
  { Attribute<ref attrs> }
  IdentType<out id, out ty>                         (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
  { "," IdentType<out id, out ty>                   (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
  }
  ";"
  .

GIdentType<bool allowGhost, out Token! id, out Type! ty, out bool isGhost>
/* isGhost always returns as false if allowGhost is false */
= (. isGhost = false; .)
  [ "ghost"                    (. if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); } .)
  ]
  IdentType<out id, out ty>
  .

IdentType<out Token! id, out Type! ty>
= Ident<out id>
  ":"
  Type<out ty>
  .

IdentTypeOptional<out BoundVar! var>
= (. Token! id;  Type! ty;  Type optType = null;
  .)
  Ident<out id>
  [ ":" Type<out ty>             (. optType = ty; .)
  ]
  (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
  .

TypeIdentOptional<out Token! id, out string! identName, out Type! ty, out bool isGhost>
= (. string name = null;  isGhost = false; .)
  [ "ghost"                            (. isGhost = true; .)
  ]
  TypeAndToken<out id, out ty>
  [ ":"
    (. /* try to convert ty to an identifier */
       UserDefinedType udt = ty as UserDefinedType;
       if (udt != null && udt.TypeArgs.Count == 0) {
         name = udt.Name;
       } else {
         SemErr(id, "invalid formal-parameter name in datatype constructor");
       }
    .)
    Type<out ty>
  ]
  (. if (name != null) {
       identName = name;
     } else {
       identName = "#" + anonymousIds++;
     }
  .)
  .

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

GenericParameters<List<TypeParameter!\>! typeArgs>
= (. Token! id; .)
  "<"
  Ident<out id>                       (. typeArgs.Add(new TypeParameter(id, id.val)); .)
  { "," Ident<out id>                 (. typeArgs.Add(new TypeParameter(id, id.val)); .)
  }
  ">"
  .

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

MethodDecl<MemberModifiers mmod, out Method! m>
= (. Token! id;
     Attributes attrs = null;
     List<TypeParameter!>! typeArgs = new List<TypeParameter!>();
     List<Formal!> ins = new List<Formal!>();
     List<Formal!> outs = new List<Formal!>();
     List<MaybeFreeExpression!> req = new List<MaybeFreeExpression!>();
     List<FrameExpression!> mod = new List<FrameExpression!>();
     List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
     List<Expression!> dec = new List<Expression!>();
     Statement! bb;  BlockStmt body = null;
  .)
  "method"
  (. if (mmod.IsUnlimited) { SemErr(token, "methods cannot be declared 'unlimited'"); }
  .)
  { Attribute<ref attrs> }
  Ident<out id>
  [ GenericParameters<typeArgs> ]
  (. parseVarScope.PushMarker(); .)
  Formals<true, true, ins>
  [ "returns"
    Formals<false, true, outs>
  ]

  ( ";" { MethodSpec<req, mod, ens, dec> }
  | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb>    (. body = (BlockStmt)bb; .)
  )
  
  (. parseVarScope.PopMarker();
     m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
  .)
  .

MethodSpec<List<MaybeFreeExpression!\>! req, List<FrameExpression!\>! mod, List<MaybeFreeExpression!\>! ens,
           List<Expression!\>! decreases>
= (. Expression! e;  FrameExpression! fe;  bool isFree = false;
  .)
  ( "modifies" [ FrameExpression<out fe>                     (. mod.Add(fe); .)
                 { "," FrameExpression<out fe>               (. mod.Add(fe); .)
                 }
               ] ";"
  | [ "free"                                                 (. isFree = true; .)
    ]
    ( "requires" Expression<out e> ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)
    | "ensures" Expression<out e> ";"                        (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
    )
  | "decreases" Expressions<decreases> ";"
  )
  .

Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals> 
= (. Token! id;  Type! ty;  bool isGhost; .)
  "("
  [
    GIdentType<allowGhosts, out id, out ty, out isGhost>         (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); .)
    { "," GIdentType<allowGhosts, out id, out ty, out isGhost>   (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost));  parseVarScope.Push(id.val, id.val); .)
    }
  ]
  ")"
  .

FormalsOptionalIds<List<Formal!\>! formals> 
= (. Token! id;  Type! ty;  string! name;  bool isGhost; .)
  "("
  [
    TypeIdentOptional<out id, out name, out ty, out isGhost>        (. formals.Add(new Formal(id, name, ty, true, isGhost));  parseVarScope.Push(name, name); .)
    { "," TypeIdentOptional<out id, out name, out ty, out isGhost>  (. formals.Add(new Formal(id, name, ty, true, isGhost));  parseVarScope.Push(name, name); .)
    }
  ]
  ")"
  .

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

Type<out Type! ty>
= (. Token! tok; .)
  TypeAndToken<out tok, out ty>
  .

TypeAndToken<out Token! tok, out Type! ty>
= (. tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
     List<Type!>! gt;
  .)
  ( "bool"                          (. tok = token; .)
  | "int"                           (. tok = token;  ty = new IntType(); .)
  | "set"                           (. tok = token;  gt = new List<Type!>(); .)
    GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                         SemErr("set type expects exactly one type argument");
                                       }
                                       ty = new SetType(gt[0]);
                                    .)
    
  | "seq"                           (. tok = token;  gt = new List<Type!>(); .)
    GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                         SemErr("seq type expects exactly one type argument");
                                       }
                                       ty = new SeqType(gt[0]);
                                    .)
  | ReferenceType<out tok, out ty>
  )
  .

ReferenceType<out Token! tok, out Type! ty>
= (. tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/
     List<Type!>! gt;
  .)
  ( "object"                        (. tok = token;  ty = new ObjectType(); .)
  | "array"                         (. tok = token;  gt = new List<Type!>(); .)
    GenericInstantiation<gt>        (. if (gt.Count != 1) {
                                         SemErr("array type expects exactly one type argument");
                                       }
                                       ty = UserDefinedType.ArrayType(tok, gt[0]);
                                    .)
  | Ident<out tok>                  (. gt = new List<Type!>(); .)
    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt); .)
  )
  .

GenericInstantiation<List<Type!\>! gt>
= (. Type! ty; .)
  "<"
    Type<out ty>                     (. gt.Add(ty); .)
    { "," Type<out ty>               (. gt.Add(ty); .)
    }
  ">"
  .

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

FunctionDecl<MemberModifiers mmod, out Function! f>
= (. Attributes attrs = null;
     Token! id;
     List<TypeParameter!> typeArgs = new List<TypeParameter!>();
     List<Formal!> formals = new List<Formal!>();
     Type! returnType;
     List<Expression!> reqs = new List<Expression!>();
     List<FrameExpression!> reads = new List<FrameExpression!>();
     List<Expression!> decreases = new List<Expression!>();
     Expression! bb;  Expression body = null;
     bool isFunctionMethod = false;
  .)
  "function"
  [ "method"                 (. isFunctionMethod = true; .)
  ]
  (. if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); }
  .)
  { Attribute<ref attrs> }
  Ident<out id> 
  [ GenericParameters<typeArgs> ]
  (. parseVarScope.PushMarker(); .)
  Formals<true, false, formals>
  ":"
  Type<out returnType>
  ( ";"
    { FunctionSpec<reqs, reads, decreases> }
  | { FunctionSpec<reqs, reads, decreases> }
    FunctionBody<out bb>                (. body = bb; .)
  )
  (. parseVarScope.PopMarker();
     f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
  .)
  .

FunctionSpec<List<Expression!\>! reqs, List<FrameExpression!\>! reads, List<Expression!\>! decreases>
= (. Expression! e;  FrameExpression! fe; .)
  ( "requires" Expression<out e> ";"      (. reqs.Add(e); .)
  | "reads" [ PossiblyWildFrameExpression<out fe>              (. reads.Add(fe); .)
              { "," PossiblyWildFrameExpression<out fe>        (. reads.Add(fe); .)
              }
	        ] ";"
  | "decreases" Expressions<decreases> ";"
  )
  .

PossiblyWildExpression<out Expression! e>
= (. e = dummyExpr; .)
  /* A decreases clause on a loop asks that no termination check be performed.
   * Use of this feature is sound only with respect to partial correctness.
   */
  ( "*"                        (. e = new WildcardExpr(token); .)
  | Expression<out e>
  )
  .

PossiblyWildFrameExpression<out FrameExpression! fe>
= (. fe = dummyFrameExpr; .)
  /* A reads clause can list a wildcard, which allows the enclosing function to
   * read anything.  In many cases, and in particular in all cases where
   * the function is defined recursively, this makes it next to impossible to make
   * any use of the function.  Nevertheless, as an experimental feature, the
   * language allows it (and it is sound).
   */
  ( "*"                        (. fe = new FrameExpression(new WildcardExpr(token), null); .)
  | FrameExpression<out fe>
  )
  .

FrameExpression<out FrameExpression! fe>
= (. Expression! e;  Token! id;  string fieldName = null; .)
  Expression<out e>
  [ "`" Ident<out id>        (. fieldName = id.val; .)
  ]
  (. fe = new FrameExpression(e, fieldName); .)
  .

FunctionBody<out Expression! e>
= (. e = dummyExpr; .)
  "{"
  ( MatchExpression<out e>
  | Expression<out e>
  )
  "}"
  .
  
MatchExpression<out Expression! e>
= (. Token! x;  MatchCaseExpr! c;
     List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();
  .)
  "match"                     (. x = token; .)
  Expression<out e>
  { CaseExpression<out c>     (. cases.Add(c); .)
  }
  (. e = new MatchExpr(x, e, cases); .)
  .

CaseExpression<out MatchCaseExpr! c>
= (. Token! x, id, arg;
     List<BoundVar!> arguments = new List<BoundVar!>();
     Expression! body;
  .)
  "case"                      (. x = token;  parseVarScope.PushMarker(); .)
  Ident<out id>
  [ "("
    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
                                 parseVarScope.Push(arg.val, arg.val); .)
    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
                                 parseVarScope.Push(arg.val, arg.val); .)
    }
  ")" ]
  "=>"
  Expression<out body>        (. c = new MatchCaseExpr(x, id.val, arguments, body);
                                 parseVarScope.PopMarker(); .)
  .

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

BlockStmt<out Statement! block>
= (. Token! x;
     List<Statement!> body = new List<Statement!>();
     Statement! s;
  .)
  (. parseVarScope.PushMarker(); .)
  "{"                                  (. x = token; .)
  { Stmt<body>
  }
  "}"                                  (. block = new BlockStmt(x, body); .)
  (. parseVarScope.PopMarker(); .)
  .

Stmt<List<Statement!\>! ss>
= (. Statement! s; .)
  /* By first reading a sequence of block statements, we avoid problems in the generated parser, despite
     the ambiguity in the grammar.  See Note in ConstAtomExpression production.
  */
  { BlockStmt<out s>                   (. ss.Add(s); .)
  }
  ( OneStmt<out s>                     (. ss.Add(s); .)
  | VarDeclStmts<ss>
  )
  .

OneStmt<out Statement! s>
= (. Token! x;  Token! id;  string label = null;
     s = dummyStmt;  /* to please the compiler */
  .)
  /* This list does not contain BlockStmt, see comment above in Stmt production. */
  ( AssertStmt<out s>
  | AssumeStmt<out s>
  | UseStmt<out s>
  | PrintStmt<out s>
  | AssignStmt<out s>
  | HavocStmt<out s>
  | CallStmt<out s>
  | IfStmt<out s>
  | WhileStmt<out s>
  | MatchStmt<out s>
  | ForeachStmt<out s>
  | "label"                            (. x = token; .)
    Ident<out id> ":"                  (. s = new LabelStmt(x, id.val); .)
  | "break"                            (. x = token; .)
    [ Ident<out id>                    (. label = id.val; .)
    ] ";"                              (. s = new BreakStmt(x, label); .)
  | "return"                           (. x = token; .)
    ";"                                (. s = new ReturnStmt(x); .)
  )
  .

AssignStmt<out Statement! s>
= (. Token! x;
     Expression! lhs;
     Expression rhs;
     Type ty;
     s = dummyStmt;
  .)
  LhsExpr<out lhs>
  ":="                                 (. x = token; .)
  AssignRhs<out rhs, out ty>           (. if (ty == null) {
                                            assert rhs != null;
                                            s = new AssignStmt(x, lhs, rhs);
                                          } else if (rhs == null) {
                                            s = new AssignStmt(x, lhs, ty);
                                          } else {
                                            s = new AssignStmt(x, lhs, ty, rhs);
                                          }
                                       .)
  ";"
  .

AssignRhs<out Expression e, out Type ty>
/* ensures e != null || ty != null; */
= (. Token! x;  Expression! ee;  Type! tt;
     e = null;  ty = null;
  .)
  ( "new" TypeAndToken<out x, out tt>  (. ty = tt; .)
    [ "[" Expression<out ee> "]"       (. e = ee; .)
    ]
  | Expression<out ee>                 (. e = ee; .)
  )                                    (. if (e == null && ty == null) { e = dummyExpr; } .)
  .

HavocStmt<out Statement! s>
= (. Token! x;  Expression! lhs; .)
  "havoc"                              (. x = token; .)
  LhsExpr<out lhs> ";"                 (. s = new AssignStmt(x, lhs); .)
  .

LhsExpr<out Expression! e>
= SelectExpression<out e>
  .

VarDeclStmts<List<Statement!\>! ss>
= (. VarDecl! d;  bool isGhost = false; .)
  [ "ghost"                            (. isGhost = true; .)
  ]
  "var"
  IdentTypeRhs<out d, isGhost>         (. ss.Add(d);  parseVarScope.Push(d.Name, d.Name); .)
  { "," IdentTypeRhs<out d, isGhost>   (. ss.Add(d);  parseVarScope.Push(d.Name, d.Name); .)
  }
  ";"
  .

IdentTypeRhs<out VarDecl! d, bool isGhost>
= (. Token! id;  Type! ty;  Expression! e;
     Expression rhs = null;  Type newType = null;
     Type optionalType = null;  DeterminedAssignmentRhs optionalRhs = null;
  .)
  Ident<out id>
  [ ":" Type<out ty>                   (. optionalType = ty; .)
  ]
  [ ":="
    AssignRhs<out rhs, out newType>
  ]
  (. if (newType == null && rhs != null) {
       optionalRhs = new ExprRhs(rhs);
     } else if (newType != null) {
       if (rhs == null) {
         optionalRhs = new TypeRhs(newType);
       } else {
         optionalRhs = new TypeRhs(newType, rhs);
       }
     } else if (optionalType == null) {
       optionalType = new InferredTypeProxy();
     }
     d = new VarDecl(id, id.val, optionalType, isGhost, optionalRhs);
  .)
  .

IfStmt<out Statement! ifStmt>
= (. Token! x;
     Expression guard;
     Statement! thn;
     Statement! s;
     Statement els = null;
  .)
  "if"                       (. x = token; .)
  Guard<out guard>
  BlockStmt<out thn>
  [ "else"
    ( IfStmt<out s>          (. els = s; .)
    | BlockStmt<out s>       (. els = s; .)
    )
  ]
  (. ifStmt = new IfStmt(x, guard, thn, els); .)
  .

WhileStmt<out Statement! stmt>
= (. Token! x;
     Expression guard;
     bool isFree;  Expression! e;
     List<MaybeFreeExpression!> invariants = new List<MaybeFreeExpression!>();
     List<Expression!> decreases = new List<Expression!>();
     Statement! body;
  .)
  "while"                    (. x = token; .)
  Guard<out guard>           (. assume guard == null || Owner.None(guard); .)
  {                          (. isFree = false; .)
     [ "free"                (. isFree = true; .)
     ]
     "invariant"
     Expression<out e>       (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
     ";"
   | "decreases"
     PossiblyWildExpression<out e>          (. decreases.Add(e); .)
     { "," PossiblyWildExpression<out e>    (. decreases.Add(e); .)
     }
     ";"
  }
  BlockStmt<out body>        (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
  .

Guard<out Expression e>   /* null represents demonic-choice */
= (. Expression! ee;  e = null; .)
  "("
  ( "*"                      (. e = null; .)
  | Expression<out ee>       (. e = ee; .)
  )
  ")"
  .

MatchStmt<out Statement! s>
= (. Token x;  Expression! e;  MatchCaseStmt! c;
     List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>(); .)
  "match"                     (. x = token; .)
  Expression<out e>
  "{"
  { CaseStatement<out c>     (. cases.Add(c); .)
  }
  "}"
  (. s = new MatchStmt(x, e, cases); .)
  .

CaseStatement<out MatchCaseStmt! c>
= (. Token! x, id, arg;
     List<BoundVar!> arguments = new List<BoundVar!>();
     List<Statement!> body = new List<Statement!>();
  .)
  "case"                      (. x = token;  parseVarScope.PushMarker(); .)
  Ident<out id>
  [ "("
    Ident<out arg>            (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
                                 parseVarScope.Push(arg.val, arg.val); .)
    { "," Ident<out arg>      (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
                                 parseVarScope.Push(arg.val, arg.val); .)
    }
  ")" ]
  "=>"
    (. parseVarScope.PushMarker(); .)
    { Stmt<body> }
    (. parseVarScope.PopMarker(); .)
  (. c = new MatchCaseStmt(x, id.val, arguments, body); .)
  (. parseVarScope.PopMarker(); .)
  .

CallStmt<out Statement! s>
= (. Token! x, id;
     Expression! e;
     List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
     List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
  .)
  "call"                       (. x = token; .)
  CallStmtSubExpr<out e>
  
  [ ","                        /* call a,b,c,... := ... */
                               (. e = ConvertToLocal(e);
                                  if (e is IdentifierExpr) {
                                    RecordCallLhs((IdentifierExpr)e, lhs, newVars);
                                  } else if (e is FieldSelectExpr) {
                                    SemErr(e.tok, "each LHS of call statement must be a variable, not a field");
                                  } else {
                                    SemErr(e.tok, "each LHS of call statement must be a variable");
                                  }
                               .)
    Ident<out id>              (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)
    { "," Ident<out id>        (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)
    }
    ":="
    CallStmtSubExpr<out e>

  | ":="                       /* call a := ... */
                               (. e = ConvertToLocal(e);
                                  if (e is IdentifierExpr) {
                                    RecordCallLhs((IdentifierExpr)e, lhs, newVars);
                                  } else if (e is FieldSelectExpr) {
                                    SemErr(e.tok, "each LHS of call statement must be a variable, not a field");
                                  } else {
                                    SemErr(e.tok, "each LHS of call statement must be a variable");
                                  }
                               .)
    CallStmtSubExpr<out e>
  ]
  ";"

  /* "e" has now been parsed as one of: IdentifierExpr, FunctionCallExpr, FieldSelectExpr.
     It denotes the RHS, so to be legal it must be a FunctionCallExpr.  */
  (. if (e is FunctionCallExpr) {
       FunctionCallExpr fce = (FunctionCallExpr)e;
       s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args
     } else {
       SemErr("RHS of call statement must denote a method invocation");
       s = new CallStmt(x, newVars, lhs, dummyExpr, "dummyMethodName", new List<Expression!>());
     }
  .)
  .

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

ForeachStmt<out Statement! s>
= (. Token! x, boundVar;
     Type! ty;
     Expression! collection;
     Expression! range;
     List<PredicateStmt!> bodyPrefix = new List<PredicateStmt!>();
     AssignStmt bodyAssign = null;
  .)
  (. parseVarScope.PushMarker(); .)
  "foreach"                                    (. x = token;
                                                  range = new LiteralExpr(x, true);
                                                  ty = new InferredTypeProxy();
                                               .)
  "(" Ident<out boundVar>
      [ ":" Type<out ty> ]
      "in" Expression<out collection>
                                               (. parseVarScope.Push(boundVar.val, boundVar.val); .)
      [ "|" Expression<out range> ]
  ")"
  "{"
    { AssertStmt<out s>                        (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
    | AssumeStmt<out s>                        (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
    | UseStmt<out s>                           (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
    }
    ( AssignStmt<out s>                        (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
    | HavocStmt<out s>                         (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
    )
  "}"                                          (. if (bodyAssign != null) {
                                                    s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
                                                  } else {
                                                    s = dummyStmt;  // some error occurred in parsing the bodyAssign
                                                  }
                                               .)
  (. parseVarScope.PopMarker(); .)
  .

AssertStmt<out Statement! s>
= (. Token! x;  Expression! e; .)
  "assert"                                     (. x = token; .)
  Expression<out e> ";"                        (. s = new AssertStmt(x, e); .)
  .

AssumeStmt<out Statement! s>
= (. Token! x;  Expression! e; .)
  "assume"                                     (. x = token; .)
  Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)
  .

UseStmt<out Statement! s>
= (. Token! x;  Expression! e; .)
  "use"                                        (. x = token; .)
  Expression<out e> ";"                        (. s = new UseStmt(x, e); .)
  .

PrintStmt<out Statement! s>
= (. Token! x;  Attributes.Argument! arg;
     List<Attributes.Argument!> args = new List<Attributes.Argument!>();
  .)
  "print"                                      (. x = token; .)
  AttributeArg<out arg>                        (. args.Add(arg); .)
  { "," AttributeArg<out arg>                  (. args.Add(arg); .)
  }
  ";"                                          (. s = new PrintStmt(x, args); .)
  .

/*------------------------------------------------------------------------*/
Expression<out Expression! e>
= (. Token! x;  Expression! e0;  Expression! e1 = dummyExpr;
     e = dummyExpr;
  .)
  ( "if"                               (. x = token; .)
    Expression<out e>
    "then" Expression<out e0>
    "else" Expression<out e1>          (. e = new ITEExpr(x, e, e0, e1); .)
  | EquivExpression<out e>
  )
  .

/*------------------------------------------------------------------------*/
EquivExpression<out Expression! e0>
= (. Token! x;  Expression! e1; .)
  ImpliesExpression<out e0>
  { EquivOp                                    (. x = token; .)
    ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
  }
  .

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

/*------------------------------------------------------------------------*/
ImpliesExpression<out Expression! e0>
= (. Token! x;  Expression! e1; .)
  LogicalExpression<out e0>
  [ ImpliesOp                                  (. x = token; .)
    ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
  ]
  .

ImpliesOp = "==>" | '\u21d2'.

/*------------------------------------------------------------------------*/
LogicalExpression<out Expression! e0>
= (. Token! x;  Expression! e1; .)
  RelationalExpression<out e0>
  [ AndOp                                      (. x = token; .)
    RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
    { AndOp                                    (. x = token; .)
      RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
    }
  | OrOp                                       (. x = token; .)
    RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
    { OrOp                                     (. x = token; .)
      RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
    }
  ]
  .

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

/*------------------------------------------------------------------------*/
RelationalExpression<out Expression! e0>
= (. Token! x;  Expression! e1;  BinaryExpr.Opcode op; .)
  Term<out e0>
  [ RelOp<out x, out op>
    Term<out e1>                               (. e0 = new BinaryExpr(x, op, e0, e1); .)
  ]
  .

RelOp<out Token! x, out BinaryExpr.Opcode op>
=                  (. x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
  ( "=="           (. x = token;  op = BinaryExpr.Opcode.Eq; .)
  | "<"            (. x = token;  op = BinaryExpr.Opcode.Lt; .)
  | ">"            (. x = token;  op = BinaryExpr.Opcode.Gt; .)
  | "<="           (. x = token;  op = BinaryExpr.Opcode.Le; .)
  | ">="           (. x = token;  op = BinaryExpr.Opcode.Ge; .)
  | "!="           (. x = token;  op = BinaryExpr.Opcode.Neq; .)
  | "!!"           (. x = token;  op = BinaryExpr.Opcode.Disjoint; .)
  | "in"           (. x = token;  op = BinaryExpr.Opcode.In; .)
  | "!in"          (. x = token;  op = BinaryExpr.Opcode.NotIn; .)
  | '\u2260'       (. x = token;  op = BinaryExpr.Opcode.Neq; .)
  | '\u2264'       (. x = token;  op = BinaryExpr.Opcode.Le; .)
  | '\u2265'       (. x = token;  op = BinaryExpr.Opcode.Ge; .)
  )
  .

/*------------------------------------------------------------------------*/
Term<out Expression! e0>
= (. Token! x;  Expression! e1;  BinaryExpr.Opcode op; .)
  Factor<out e0>
  { AddOp<out x, out op>
    Factor<out e1>                             (. e0 = new BinaryExpr(x, op, e0, e1); .)
  }
  .

AddOp<out Token! x, out BinaryExpr.Opcode op>
=                  (. x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
  ( "+"            (. x = token;  op = BinaryExpr.Opcode.Add; .)
  | "-"            (. x = token;  op = BinaryExpr.Opcode.Sub; .)
  )
  .

/*------------------------------------------------------------------------*/
Factor<out Expression! e0>
= (. Token! x;  Expression! e1;  BinaryExpr.Opcode op; .)
  UnaryExpression<out e0>
  { MulOp<out x, out op>
    UnaryExpression<out e1>                    (. e0 = new BinaryExpr(x, op, e0, e1); .)
  }
  .

MulOp<out Token! x, out BinaryExpr.Opcode op>
=                  (. x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
  ( "*"            (. x = token;  op = BinaryExpr.Opcode.Mul; .)
  | "/"            (. x = token;  op = BinaryExpr.Opcode.Div; .)
  | "%"            (. x = token;  op = BinaryExpr.Opcode.Mod; .)
  )
  .

/*------------------------------------------------------------------------*/
UnaryExpression<out Expression! e>
= (. Token! x;  e = dummyExpr; .)
  ( "-"                                        (. x = token; .)
    UnaryExpression<out e>                     (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)
  | NegOp                                      (. x = token; .)
    UnaryExpression<out e>                     (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
  | SelectExpression<out e>
  | ConstAtomExpression<out e>
  )
  .

NegOp = "!" | '\u00ac'.

ConstAtomExpression<out Expression! e>            
= (. Token! x, dtName, id;  BigInteger n;  List<Expression!>! elements;
     e = dummyExpr;  
  .)
  ( "false"                                    (. e = new LiteralExpr(token, false); .)
  | "true"                                     (. e = new LiteralExpr(token, true); .)
  | "null"                                     (. e = new LiteralExpr(token); .)
  | Nat<out n>                                 (. e = new LiteralExpr(token, n); .)
  | "#"                                        (. x = token; .)
    Ident<out dtName>
    "."
    Ident<out id>                              (. elements = new List<Expression!>(); .)
    [ "("
      [ Expressions<elements> ]
    ")" ]                                      (. e = new DatatypeValue(token, dtName.val, id.val, elements); .)
  | "fresh"                                    (. x = token; .)
    "(" Expression<out e> ")"                  (. e = new FreshExpr(x, e); .)
  | "|"                                        (. x = token; .)
      Expression<out e>                        (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
    "|"
  | "{"                                        (. x = token;  elements = new List<Expression!>(); .)
      [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, elements); .)
    "}"
  | "["                                        (. x = token;  elements = new List<Expression!>(); .)
      [ Expressions<elements> ]                (. e = new SeqDisplayExpr(x, elements); .)
    "]"
  )
  .

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

/* returns one of:
   -- IdentifierExpr
   -- FunctionCallExpr
   -- FieldSelectExpr
*/
CallStmtSubExpr<out Expression! e>
= (. e = dummyExpr; .)
  ( IdentOrFuncExpression<out e>
  | ObjectExpression<out e>
    SelectOrCallSuffix<ref e>
  )
  { SelectOrCallSuffix<ref e> }
  .

SelectExpression<out Expression! e>
= (. Token! id;  e = dummyExpr; .)
  ( IdentOrFuncExpression<out e>
  | ObjectExpression<out e>
  )
  { SelectOrCallSuffix<ref e> }
  .

IdentOrFuncExpression<out Expression! e>
= (. Token! id;  e = dummyExpr;  List<Expression!>! args; .)
  Ident<out id>
  [ "("                                      (. args = new List<Expression!>(); .)
      [ Expressions<args> ]
    ")"                                      (. e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args); .)
  ]                                          (. if (e == dummyExpr) {
                                                  if (parseVarScope.Find(id.val) != null) {
                                                    e = new IdentifierExpr(id, id.val);
                                                  } else {
                                                    e = new FieldSelectExpr(id, new ImplicitThisExpr(id), id.val);
                                                  }
                                                }
                                             .)
  .

SelectOrCallSuffix<ref Expression! e>
= (. Token! id, x;  List<Expression!>! args;
     Expression e0 = null;  Expression e1 = null;  Expression! ee;  bool anyDots = false;
     bool func = false;
  .)
  ( "."
    Ident<out id>
    [ "("                                      (. args = new List<Expression!>();  func = true; .)
        [ Expressions<args> ]
      ")"                                      (. e = new FunctionCallExpr(id, id.val, e, args); .)
    ]                                          (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)
    
  | "["                                        (. x = token; .)
      ( Expression<out ee>                     (. e0 = ee; .)
        [ ".."                                 (. anyDots = true; .)
          [ Expression<out ee>                 (. e1 = ee; .)
          ]
        | ":="
          Expression<out ee>                   (. e1 = ee; .)
        ]
      | ".." Expression<out ee>                (. anyDots = true;  e1 = ee; .)
      )                                        (. if (!anyDots && e0 == null) {
                                                    /* a parsing error occurred */
                                                    e0 = dummyExpr;
                                                  }
                                                  assert !anyDots ==> e0 != null;
                                                  if (anyDots) {
                                                    assert e0 != null || e1 != null;
                                                    e = new SeqSelectExpr(x, false, e, e0, e1);
                                                  } else if (e1 == null) {
                                                    assert e0 != null;
                                                    e = new SeqSelectExpr(x, true, e, e0, null);
                                                  } else {
                                                    assert e0 != null;
                                                    e = new SeqUpdateExpr(x, e, e0, e1);
                                                  }
                                               .)
    "]"
  )
  .

/* ObjectExpression represents those expressions E that could possibly be used in E.f
   or E(...), except Ident.  Since the lookahead is just 1, quantifier expressions are also
   parsed here.  The expression returned is never an lvalue.
*/
ObjectExpression<out Expression! e>
= (. Token! x;  e = dummyExpr; .)
  ( "this"                                     (. e = new ThisExpr(token); .)
  | "old"                                      (. x = token; .)
    "("
      Expression<out e>
    ")"                                        (. e = new OldExpr(x, e); .)
  | "(" ( QuantifierGuts<out e>
        | Expression<out e>
        )
    ")"
  )
  .

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

QuantifierGuts<out Expression! q>
= (. Token! x = Token.NoToken;
     bool univ = false;
     BoundVar! bv;
     List<BoundVar!> bvars = new List<BoundVar!>();
     Token! tok;  Expr! e;  ExprSeq! es;
     Attributes attrs = null;
     Triggers trigs = null;
     Expression! body;
  .)
  ( Forall                                     (. x = token;  univ = true; .)
  | Exists                                     (. x = token; .)
  )
  (. parseVarScope.PushMarker(); .)
  IdentTypeOptional<out bv>                    (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)
  { ","
    IdentTypeOptional<out bv>                  (. bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); .)
  }
  { AttributeOrTrigger<ref attrs, ref trigs> }
  QSep
  Expression<out body>
  (. if (univ) {
       q = new ForallExpr(x, bvars, body, trigs, attrs);
     } else {
       q = new ExistsExpr(x, bvars, body, trigs, attrs);
     }
     parseVarScope.PopMarker();
  .)
  .

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

Expressions<List<Expression!\>! args>
= (. Expression! e; .)
  Expression<out e>                            (. args.Add(e); .)
  { "," Expression<out e>                      (. args.Add(e); .)
  }
  .

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

Attribute<ref Attributes attrs>
= "{"
    AttributeBody<ref attrs>
  "}"
  .

AttributeBody<ref Attributes attrs>
= (. string aName;
     List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();
     Attributes.Argument! aArg;
  .)
  ":" ident                            (. aName = token.val; .)
  [ AttributeArg<out aArg>             (. aArgs.Add(aArg); .)
    { "," AttributeArg<out aArg>       (. aArgs.Add(aArg); .)
    }
  ]                                    (. attrs = new Attributes(aName, aArgs, attrs); .)
  .

AttributeArg<out Attributes.Argument! arg>
= (. Expression! e;  arg = dummyAttrArg; .)
  ( string                             (. arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2)); .)
  | Expression<out e>                  (. arg = new Attributes.Argument(e); .)
  )
  .

AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
= (. List<Expression!> es = new List<Expression!>();
  .)
  "{"
    ( AttributeBody<ref attrs>
    |                                  (. es = new List<Expression!>(); .)
      Expressions<es>                  (. trigs = new Triggers(es, trigs); .)
    )
  "}"
  .

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

Idents<List<string!\>! ids>
= (. Token! id; .)
  Ident<out id>                            (. ids.Add(id.val); .)
  { "," Ident<out id>                      (. ids.Add(id.val); .)
  }
  .

Ident<out Token! x>
=
  ident            (. x = token; .)
  .                                  

Nat<out BigInteger n>
=
  digits
  (. try {
       n = BigInteger.Parse(token.val);
     } catch (System.FormatException) {
       SemErr("incorrectly formatted number");
       n = BigInteger.Zero;
     }
  .) 
  .

END Dafny.