using PureCollections;
using System.Collections;
using System.Collections.Generic;
using Microsoft.Boogie;
using Microsoft.Basetypes;
using Bpl = Microsoft.Boogie;
using AI = Microsoft.AbstractInterpretationFramework;
using System;
using Microsoft.Contracts;

namespace BoogiePL {

public class Parser {
	const int maxT = 88;

	const bool T = true;
	const bool x = false;
	const int minErrDist = 2;
	
	static Token/*!*/ token;			// last recognized token
	static Token/*!*/ t;				// lookahead token
	static int errDist = minErrDist;

	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, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
    Buffer.Fill(reader);
    Scanner.Init(filename);
    return Parse(out program);
  }
}

///<summary>
///Returns the number of parsing errors encountered.  If 0, "program" returns as
///the parsed program.
///Note: first initialize the Scanner.
///</summary>
public static int Parse (out /*maybe null*/ Program program) {
  Pgm = new Program(); // reset the global variable
    Parse();
    if (Errors.count == 0)
    {
      program = Pgm;
      return 0;
    }
    else
    {
      program = null;
      return Errors.count;
    }
}


public static int ParseProposition (string! text, out Expr! expression)
{
  Buffer.Fill(text);
  Scanner.Init(string.Format("\"{0}\"", text));

  Errors.SynErr = new ErrorProc(SynErr);
  t = new Token();
  Get();
  Proposition(out expression);
  return 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);
    this.Lower = lower;
    this.Upper = upper;
  }
  public override Type! ShallowType { get { return Bpl.Type.Int; } }
  public override void Resolve(ResolutionContext! rc) {
    rc.Error(this, "bitvector bounds in illegal position");
  }
  public override void Emit(TokenTextWriter! stream,
                            int contextBindingStrength, bool fragileContext) {
    assert false;
  }
  public override void ComputeFreeVariables(Set! freeVars) { assert false; }
  public override AI.IExpr! IExpr { get { assert false; } }
}

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


	static void Error(int n) {
		if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);
		errDist = 0;
	}
	
	public static void SemErr(string! msg) {
		if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);
		errDist = 0;
	}

	public static void SemErr(IToken! tok, string! msg) {
		Errors.SemErr(tok.filename, tok.line, tok.col, msg);
	}

	static void Get() {
		for (;;) {
			token = t;
			t = Scanner.Scan();
			if (t.kind<=maxT) {errDist++; return;}

			t = token;
		}
	}
	
	static void Expect(int n) {
		if (t.kind==n) Get(); else Error(n);
	}
	
	static bool StartOf(int s) {
		return set[s, t.kind];
	}
	
	static void ExpectWeak(int n, int follow) {
		if (t.kind == n) Get();
		else {
			Error(n);
			while (!StartOf(follow)) Get();
		}
	}
	
	static bool WeakSeparator(int n, int syFol, int repFol) {
		bool[] s = new bool[maxT+1];
		if (t.kind == n) {Get(); return true;}
		else if (StartOf(repFol)) return false;
		else {
			for (int i=0; i <= maxT; i++) {
				s[i] = set[syFol, i] || set[repFol, i] || set[0, i];
			}
			Error(n);
			while (!s[t.kind]) Get();
			return StartOf(syFol);
		}
	}
	
	static void BoogiePL() {
		VariableSeq! vs;
		DeclarationSeq! ds;
		Axiom! ax;
		List<Declaration!>! ts;
		Procedure! pr;
		Implementation im;
		Implementation! nnim;
		
		while (StartOf(1)) {
			switch (t.kind) {
			case 19: {
				Consts(out vs);
				foreach (Bpl.Variable! v in vs) { Pgm.TopLevelDeclarations.Add(v); } 
				break;
			}
			case 23: {
				Function(out ds);
				foreach (Bpl.Declaration! d in ds) { Pgm.TopLevelDeclarations.Add(d); } 
				break;
			}
			case 27: {
				Axiom(out ax);
				Pgm.TopLevelDeclarations.Add(ax); 
				break;
			}
			case 28: {
				UserDefinedTypes(out ts);
				foreach (Declaration! td in ts) {
				     Pgm.TopLevelDeclarations.Add(td);
				   } 
				break;
			}
			case 6: {
				GlobalVars(out vs);
				foreach (Bpl.Variable! v in vs) { Pgm.TopLevelDeclarations.Add(v); } 
				break;
			}
			case 30: {
				Procedure(out pr, out im);
				Pgm.TopLevelDeclarations.Add(pr);
				if (im != null) {
				  Pgm.TopLevelDeclarations.Add(im);
				}
				
				break;
			}
			case 31: {
				Implementation(out nnim);
				Pgm.TopLevelDeclarations.Add(nnim); 
				break;
			}
			}
		}
		Expect(0);
	}

	static void Consts(out VariableSeq! ds) {
		IToken! y; TypedIdentSeq! xs;
		ds = new VariableSeq();
		bool u = false; QKeyValue kv = null;
		bool ChildrenComplete = false;
		List<ConstantParent!> Parents = null; 
		Expect(19);
		y = token; 
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		if (t.kind == 20) {
			Get();
			u = true;  
		}
		IdsType(out xs);
		if (t.kind == 21) {
			OrderSpec(out ChildrenComplete, out Parents);
		}
		bool makeClone = false;
		foreach(TypedIdent! x in xs) {
		    // ensure that no sharing is introduced
		  List<ConstantParent!> ParentsClone;
		  if (makeClone && Parents != null) {
		    ParentsClone = new List<ConstantParent!> ();
		    foreach (ConstantParent! p in Parents)
		      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));
		}
		
		Expect(7);
	}

	static void Function(out DeclarationSeq! ds) {
		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;
		
		Expect(23);
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		Ident(out z);
		if (t.kind == 17) {
			TypeParams(out typeParamTok, out typeParams);
		}
		Expect(8);
		if (StartOf(2)) {
			VarOrType(out tyd);
			arguments.Add(new Formal(tyd.tok, tyd, true)); 
			while (t.kind == 11) {
				Get();
				VarOrType(out tyd);
				arguments.Add(new Formal(tyd.tok, tyd, true)); 
			}
		}
		Expect(9);
		if (t.kind == 24) {
			Get();
			Expect(8);
			VarOrType(out tyd);
			Expect(9);
			retTyd = tyd; 
		} else if (t.kind == 10) {
			Get();
			Type(out retTy);
			retTyd = new TypedIdent(retTy.tok, "", retTy); 
		} else Error(89);
		if (t.kind == 25) {
			Get();
			Expression(out tmp);
			definition = tmp; 
			Expect(26);
		} else if (t.kind == 7) {
			Get();
		} else Error(90);
		if (retTyd == null) {
		 // construct a dummy type for the case of syntax error
		 tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));
		} else {
		  tyd = retTyd;
		}
		Function! func = new Function(z, z.val, typeParams, arguments,
		                       new Formal(tyd.tok, tyd, false), null, kv);
		ds.Add(func);
		bool allUnnamed = true;
		foreach (Formal! f in arguments) {
		  if (f.TypedIdent.Name != "") {
		    allUnnamed = false;
		break;
		     }
		   }
		   if (!allUnnamed) {
		     Type prevType = null;
		     for (int i = arguments.Length - 1; i >= 0; i--) {
		       TypedIdent! curr = ((!)arguments[i]).TypedIdent;
		       if (curr.Name == "") {
		  if (prevType == null) {
		    SemErr(curr.tok, "the type of the last parameter is unspecified");
		    break;
		  }
		  Type ty = curr.Type;
		         if (ty is UnresolvedTypeIdentifier &&
		             ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) {
		    curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;
		    curr.Type = prevType;
		  } else {
		    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) {
		         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)
		         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));
		     }
		   }
		 
	}

	static void Axiom(out Axiom! m) {
		Expr! e; QKeyValue kv = null; 
		Expect(27);
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		IToken! x = token; 
		Proposition(out e);
		Expect(7);
		m = new Axiom(x,e, null, kv); 
	}

	static void UserDefinedTypes(out List<Declaration!>! ts) {
		Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> (); 
		Expect(28);
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		UserDefinedType(out decl, kv);
		ts.Add(decl);  
		while (t.kind == 11) {
			Get();
			UserDefinedType(out decl, kv);
			ts.Add(decl);  
		}
		Expect(7);
	}

	static void GlobalVars(out VariableSeq! ds) {
		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null; 
		Expect(6);
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		IdsTypeWheres(true, tyds);
		Expect(7);
		foreach(TypedIdent! tyd in tyds) {
		 ds.Add(new GlobalVariable(tyd.tok, tyd, kv));
		}
		
	}

	static void Procedure(out Procedure! proc, out /*maybe null*/ Implementation impl) {
		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;
		
		Expect(30);
		ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
		if (t.kind == 7) {
			Get();
			while (StartOf(3)) {
				Spec(pre, mods, post);
			}
		} else if (StartOf(4)) {
			while (StartOf(3)) {
				Spec(pre, mods, post);
			}
			ImplBody(out locals, out stmtList);
			// here we attach kv only to the Procedure, not its implementation
			impl = new Implementation(x, x.val, typeParams,
			                          Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); 
			
		} else Error(91);
		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 
	}

	static void Implementation(out Implementation! impl) {
		IToken! x;
		TypeVariableSeq! typeParams;
		VariableSeq! ins, outs;
		VariableSeq! locals;
		StmtList! stmtList;
		QKeyValue kv;
		
		Expect(31);
		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); 
	}

	static void Attribute(ref QKeyValue kv) {
		Trigger trig = null; 
		AttributeOrTrigger(ref kv, ref trig);
		if (trig != null) SemErr("only attributes, not triggers, allowed here"); 
	}

	static void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) {
		IdsTypeWhere(allowWhereClauses, tyds);
		while (t.kind == 11) {
			Get();
			IdsTypeWhere(allowWhereClauses, tyds);
		}
	}

	static void LocalVars(VariableSeq! ds) {
		TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null; 
		Expect(6);
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		IdsTypeWheres(true, tyds);
		Expect(7);
		foreach(TypedIdent! tyd in tyds) {
		 ds.Add(new LocalVariable(tyd.tok, tyd, kv));
		}
		
	}

	static void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) {
		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); 
		Expect(8);
		if (t.kind == 1) {
			IdsTypeWheres(allowWhereClauses, tyds);
		}
		Expect(9);
		foreach (TypedIdent! tyd in tyds) {
		 ds.Add(new Formal(tyd.tok, tyd, incoming));
		}
		
	}

	static void BoundVars(IToken! x, out VariableSeq! ds) {
		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); 
		IdsTypeWheres(false, tyds);
		foreach (TypedIdent! tyd in tyds) {
		 ds.Add(new BoundVariable(tyd.tok, tyd));
		}
		
	}

	static void IdsType(out TypedIdentSeq! tyds) {
		TokenSeq! ids;  Bpl.Type! ty; 
		Idents(out ids);
		Expect(10);
		Type(out ty);
		tyds = new TypedIdentSeq();
		foreach (Token! id in ids) {
		  tyds.Add(new TypedIdent(id, id.val, ty, null));
		}
		
	}

	static void Idents(out TokenSeq! xs) {
		IToken! id; xs = new TokenSeq(); 
		Ident(out id);
		xs.Add(id); 
		while (t.kind == 11) {
			Get();
			Ident(out id);
			xs.Add(id); 
		}
	}

	static void Type(out Bpl.Type! ty) {
		IToken! tok; ty = dummyType; 
		if (t.kind == 8 || t.kind == 13 || t.kind == 14) {
			TypeAtom(out ty);
		} else if (t.kind == 1) {
			Ident(out tok);
			TypeSeq! args = new TypeSeq (); 
			if (StartOf(2)) {
				TypeArgs(args);
			}
			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 
		} else if (t.kind == 15 || t.kind == 17) {
			MapType(out ty);
		} else Error(92);
	}

	static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {
		TokenSeq! ids;  Bpl.Type! ty;  Expr wh = null;  Expr! nne; 
		Idents(out ids);
		Expect(10);
		Type(out ty);
		if (t.kind == 12) {
			Get();
			Expression(out nne);
			if (allowWhereClauses) {
			 wh = nne;
			} else {
			  SemErr("where clause not allowed here");
			}
			
		}
		foreach (Token! id in ids) {
		 tyds.Add(new TypedIdent(id, id.val, ty, wh));
		}
		
	}

	static void Expression(out Expr! e0) {
		IToken! x; Expr! e1; 
		ImpliesExpression(false, out e0);
		while (t.kind == 52 || t.kind == 53) {
			EquivOp();
			x = token; 
			ImpliesExpression(false, out e1);
			e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); 
		}
	}

	static void TypeAtom(out Bpl.Type! ty) {
		ty = dummyType; 
		if (t.kind == 13) {
			Get();
			ty = new BasicType(token, SimpleType.Int); 
		} else if (t.kind == 14) {
			Get();
			ty = new BasicType(token, SimpleType.Bool); 
		} else if (t.kind == 8) {
			Get();
			Type(out ty);
			Expect(9);
		} else Error(93);
	}

	static void Ident(out IToken! x) {
		Expect(1);
		x = token;
		if (x.val.StartsWith("\\"))
		  x.val = x.val.Substring(1);
		
	}

	static void TypeArgs(TypeSeq! ts) {
		IToken! tok; Type! ty; 
		if (t.kind == 8 || t.kind == 13 || t.kind == 14) {
			TypeAtom(out ty);
			ts.Add(ty); 
			if (StartOf(2)) {
				TypeArgs(ts);
			}
		} else if (t.kind == 1) {
			Ident(out tok);
			TypeSeq! args = new TypeSeq ();
			ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); 
			if (StartOf(2)) {
				TypeArgs(ts);
			}
		} else if (t.kind == 15 || t.kind == 17) {
			MapType(out ty);
			ts.Add(ty); 
		} else Error(94);
	}

	static void MapType(out Bpl.Type! ty) {
		IToken tok = null;
		IToken! nnTok;
		TypeSeq! arguments = new TypeSeq();
		Type! result;
		TypeVariableSeq! typeParameters = new TypeVariableSeq();
		
		if (t.kind == 17) {
			TypeParams(out nnTok, out typeParameters);
			tok = nnTok; 
		}
		Expect(15);
		if (tok == null) tok = token;  
		if (StartOf(2)) {
			Types(arguments);
		}
		Expect(16);
		Type(out result);
		ty = new MapType(tok, typeParameters, arguments, result);
		
	}

	static void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) {
		TokenSeq! typeParamToks; 
		Expect(17);
		tok = token;  
		Idents(out typeParamToks);
		Expect(18);
		typeParams = new TypeVariableSeq ();
		foreach (Token! id in typeParamToks)
		  typeParams.Add(new TypeVariable(id, id.val));
		
	}

	static void Types(TypeSeq! ts) {
		Bpl.Type! ty; 
		Type(out ty);
		ts.Add(ty); 
		while (t.kind == 11) {
			Get();
			Type(out ty);
			ts.Add(ty); 
		}
	}

	static void OrderSpec(out bool ChildrenComplete, out List<ConstantParent!> Parents) {
		ChildrenComplete = false;
		Parents = null;
		bool u;
		IToken! parent; 
		Expect(21);
		Parents = new List<ConstantParent!> ();
		u = false; 
		if (t.kind == 1 || t.kind == 20) {
			if (t.kind == 20) {
				Get();
				u = true; 
			}
			Ident(out parent);
			Parents.Add(new ConstantParent (
			           new IdentifierExpr(parent, parent.val), u)); 
			while (t.kind == 11) {
				Get();
				u = false; 
				if (t.kind == 20) {
					Get();
					u = true; 
				}
				Ident(out parent);
				Parents.Add(new ConstantParent (
				           new IdentifierExpr(parent, parent.val), u)); 
			}
		}
		if (t.kind == 22) {
			Get();
			ChildrenComplete = true; 
		}
	}

	static void VarOrType(out TypedIdent! tyd) {
		string! varName = ""; Bpl.Type! ty; IToken! tok; 
		Type(out ty);
		tok = ty.tok; 
		if (t.kind == 10) {
			Get();
			if (ty is UnresolvedTypeIdentifier &&
			   ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) {
			 varName = ((!)(ty as UnresolvedTypeIdentifier)).Name;
			} else {
			  SemErr("expected identifier before ':'");
			}
			
			Type(out ty);
		}
		tyd = new TypedIdent(tok, varName, ty); 
	}

	static void Proposition(out Expr! e) {
		Expression(out e);
	}

	static void UserDefinedType(out Declaration! decl, QKeyValue kv) {
		IToken! id; IToken! id2; TokenSeq! paramTokens = new TokenSeq ();
		Type! body = dummyType; bool synonym = false; 
		Ident(out id);
		if (t.kind == 1) {
			WhiteSpaceIdents(out paramTokens);
		}
		if (t.kind == 29) {
			Get();
			Type(out body);
			synonym = true; 
		}
		if (synonym) {
		 TypeVariableSeq! typeParams = new TypeVariableSeq();
		 foreach (Token! t in paramTokens)
		   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);
		}
		
	}

	static void WhiteSpaceIdents(out TokenSeq! xs) {
		IToken! id; xs = new TokenSeq(); 
		Ident(out id);
		xs.Add(id); 
		while (t.kind == 1) {
			Ident(out id);
			xs.Add(id); 
		}
	}

	static void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams,
out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
		IToken! typeParamTok; typeParams = new TypeVariableSeq();
		outs = new VariableSeq(); kv = null; 
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		Ident(out name);
		if (t.kind == 17) {
			TypeParams(out typeParamTok, out typeParams);
		}
		ProcFormals(true, allowWhereClausesOnFormals, out ins);
		if (t.kind == 24) {
			Get();
			ProcFormals(false, allowWhereClausesOnFormals, out outs);
		}
	}

	static void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) {
		TokenSeq! ms; 
		if (t.kind == 32) {
			Get();
			if (t.kind == 1) {
				Idents(out ms);
				foreach (IToken! m in ms) {
				 mods.Add(new IdentifierExpr(m, m.val));
				}
				
			}
			Expect(7);
		} else if (t.kind == 33) {
			Get();
			SpecPrePost(true, pre, post);
		} else if (t.kind == 34 || t.kind == 35) {
			SpecPrePost(false, pre, post);
		} else Error(95);
	}

	static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {
		locals = new VariableSeq(); 
		Expect(25);
		while (t.kind == 6) {
			LocalVars(locals);
		}
		StmtList(out stmtList);
	}

	static void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) {
		Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; 
		if (t.kind == 34) {
			Get();
			tok = token; 
			while (t.kind == 25) {
				Attribute(ref kv);
			}
			if (StartOf(5)) {
				Proposition(out e);
				Expect(7);
				pre.Add(new Requires(tok, free, e, null, kv)); 
			} else if (t.kind == 36) {
				SpecBody(out locals, out blocks);
				Expect(7);
				pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); 
			} else Error(96);
		} else if (t.kind == 35) {
			Get();
			tok = token; 
			while (t.kind == 25) {
				Attribute(ref kv);
			}
			if (StartOf(5)) {
				Proposition(out e);
				Expect(7);
				post.Add(new Ensures(tok, free, e, null, kv)); 
			} else if (t.kind == 36) {
				SpecBody(out locals, out blocks);
				Expect(7);
				post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); 
			} else Error(97);
		} else Error(98);
	}

	static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {
		locals = new VariableSeq(); Block! b; 
		Expect(36);
		while (t.kind == 6) {
			LocalVars(locals);
		}
		SpecBlock(out b);
		blocks = new BlockSeq(b); 
		while (t.kind == 1) {
			SpecBlock(out b);
			blocks.Add(b); 
		}
		Expect(37);
	}

	static void SpecBlock(out Block! b) {
		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);
		Expect(10);
		while (StartOf(6)) {
			LabelOrCmd(out c, out label);
			if (c != null) {
			 assert label == null;
			 cs.Add(c);
			} else {
			  assert label != null;
			  SemErr("SpecBlock's can only have one label");
			}
			
		}
		if (t.kind == 38) {
			Get();
			y = token; 
			Idents(out xs);
			foreach (IToken! s in xs) { ss.Add(s.val); }
			b = new Block(x,x.val,cs,new GotoCmd(y,ss));
			
		} else if (t.kind == 39) {
			Get();
			Expression(out e);
			b = new Block(x,x.val,cs,new ReturnExprCmd(token,e)); 
		} else Error(99);
		Expect(7);
	}

	static void LabelOrCmd(out Cmd c, out IToken label) {
		IToken! x; Expr! e;
		TokenSeq! xs;
		IdentifierExprSeq ids;
		c = dummyCmd;  label = null;
		Cmd! cn;
		QKeyValue kv = null;
		
		if (t.kind == 1) {
			LabelOrAssign(out c, out label);
		} else if (t.kind == 46) {
			Get();
			x = token; 
			while (t.kind == 25) {
				Attribute(ref kv);
			}
			Proposition(out e);
			c = new AssertCmd(x,e, kv); 
			Expect(7);
		} else if (t.kind == 47) {
			Get();
			x = token; 
			Proposition(out e);
			c = new AssumeCmd(x,e); 
			Expect(7);
		} else if (t.kind == 48) {
			Get();
			x = token; 
			Idents(out xs);
			Expect(7);
			ids = new IdentifierExprSeq();
			foreach (IToken! y in xs) {
			  ids.Add(new IdentifierExpr(y, y.val));
			}
			c = new HavocCmd(x,ids);
			
		} else if (t.kind == 50) {
			CallCmd(out cn);
			Expect(7);
			c = cn; 
		} else Error(100);
	}

	static void StmtList(out StmtList! stmtList) {
		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;
		
		while (StartOf(7)) {
			if (StartOf(6)) {
				LabelOrCmd(out c, out label);
				if (c != null) {
				 // LabelOrCmd read a Cmd
				 assert label == null;
				 if (startToken == null) { startToken = c.tok;  cs = new CmdSeq(); }
				 assert cs != null;
				 cs.Add(c);
				} else {
				  // LabelOrCmd read a label
				  assert label != null;
				  if (startToken != null) {
				    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();
				}
				
			} else if (t.kind == 40 || t.kind == 42 || t.kind == 45) {
				StructuredCmd(out ecn);
				ec = ecn;
				if (startToken == null) { startToken = ec.tok;  cs = new CmdSeq(); }
				assert cs != null;
				b = new BigBlock(startToken, currentLabel, cs, ec, null);
				bigblocks.Add(b);
				startToken = null;  currentLabel = null;  cs = null;
				
			} else {
				TransferCmd(out tcn);
				tc = tcn;
				if (startToken == null) { startToken = tc.tok;  cs = new CmdSeq(); }
				assert cs != null;
				b = new BigBlock(startToken, currentLabel, cs, null, tc);
				bigblocks.Add(b);
				startToken = null;  currentLabel = null;  cs = null;
				
			}
		}
		Expect(26);
		IToken! endCurly = token;
		if (startToken == null && bigblocks.Count == 0) {
		  startToken = token;  cs = new CmdSeq();
		}
		if (startToken != null) {
		  assert cs != null;
		  b = new BigBlock(startToken, currentLabel, cs, null, null);
		  bigblocks.Add(b);
		}
		  stmtList = new StmtList(bigblocks, endCurly);
		
	}

	static void StructuredCmd(out StructuredCmd! ec) {
		ec = dummyStructuredCmd;  assume ec.IsPeerConsistent;
		IfCmd! ifcmd;  WhileCmd! wcmd;  BreakCmd! bcmd;
		
		if (t.kind == 40) {
			IfCmd(out ifcmd);
			ec = ifcmd; 
		} else if (t.kind == 42) {
			WhileCmd(out wcmd);
			ec = wcmd; 
		} else if (t.kind == 45) {
			BreakCmd(out bcmd);
			ec = bcmd; 
		} else Error(101);
	}

	static void TransferCmd(out TransferCmd! tc) {
		tc = dummyTransferCmd;
		Token y;  TokenSeq! xs;
		StringSeq ss = new StringSeq();
		
		if (t.kind == 38) {
			Get();
			y = token; 
			Idents(out xs);
			foreach (IToken! s in xs) { ss.Add(s.val); }
			tc = new GotoCmd(y, ss);
			
		} else if (t.kind == 39) {
			Get();
			tc = new ReturnCmd(token); 
		} else Error(102);
		Expect(7);
	}

	static void IfCmd(out IfCmd! ifcmd) {
		IToken! x;
		Expr guard;
		StmtList! thn;
		IfCmd! elseIf;  IfCmd elseIfOption = null;
		StmtList! els;  StmtList elseOption = null;
		
		Expect(40);
		x = token; 
		Guard(out guard);
		Expect(25);
		StmtList(out thn);
		if (t.kind == 41) {
			Get();
			if (t.kind == 40) {
				IfCmd(out elseIf);
				elseIfOption = elseIf; 
			} else if (t.kind == 25) {
				Get();
				StmtList(out els);
				elseOption = els; 
			} else Error(103);
		}
		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 
	}

	static void WhileCmd(out WhileCmd! wcmd) {
		IToken! x;  Token z;
		Expr guard;  Expr! e;  bool isFree;
		List<PredicateCmd!> invariants = new List<PredicateCmd!>();
		StmtList! body;
		
		Expect(42);
		x = token; 
		Guard(out guard);
		assume guard == null || Owner.None(guard); 
		while (t.kind == 33 || t.kind == 43) {
			isFree = false; z = t/*lookahead token*/; 
			if (t.kind == 33) {
				Get();
				isFree = true;  
			}
			Expect(43);
			Expression(out e);
			if (isFree) {
			 invariants.Add(new AssumeCmd(z, e));
			} else {
			  invariants.Add(new AssertCmd(z, e));
			}
			
			Expect(7);
		}
		Expect(25);
		StmtList(out body);
		wcmd = new WhileCmd(x, guard, invariants, body); 
	}

	static void BreakCmd(out BreakCmd! bcmd) {
		IToken! x;  IToken! y;
		string breakLabel = null;
		
		Expect(45);
		x = token; 
		if (t.kind == 1) {
			Ident(out y);
			breakLabel = y.val; 
		}
		Expect(7);
		bcmd = new BreakCmd(x, breakLabel); 
	}

	static void Guard(out Expr e) {
		Expr! ee;  e = null; 
		Expect(8);
		if (t.kind == 44) {
			Get();
			e = null; 
		} else if (StartOf(5)) {
			Expression(out ee);
			e = ee; 
		} else Error(104);
		Expect(9);
	}

	static void LabelOrAssign(out Cmd c, out IToken label) {
		IToken! id; IToken! x; Expr! e, e0;
		c = dummyCmd;  label = null;
		AssignLhs! lhs;
		List<AssignLhs!>! lhss;
		List<Expr!>! rhss;
		
		Ident(out id);
		x = token; 
		if (t.kind == 10) {
			Get();
			c = null;  label = x; 
		} else if (t.kind == 11 || t.kind == 15 || t.kind == 49) {
			MapAssignIndexes(id, out lhs);
			lhss = new List<AssignLhs!> ();
			lhss.Add(lhs); 
			while (t.kind == 11) {
				Get();
				Ident(out id);
				MapAssignIndexes(id, out lhs);
				lhss.Add(lhs); 
			}
			Expect(49);
			x = token; /* use location of := */ 
			Expression(out e0);
			rhss = new List<Expr!> ();
			rhss.Add(e0); 
			while (t.kind == 11) {
				Get();
				Expression(out e0);
				rhss.Add(e0); 
			}
			Expect(7);
			c = new AssignCmd(x, lhss, rhss); 
		} else Error(105);
	}

	static void CallCmd(out Cmd! c) {
		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;
		
		Expect(50);
		x = token; 
		while (t.kind == 25) {
			Attribute(ref kv);
		}
		if (t.kind == 1) {
			Ident(out first);
			if (t.kind == 8) {
				Get();
				if (StartOf(8)) {
					CallForallArg(out en);
					es.Add(en); 
					while (t.kind == 11) {
						Get();
						CallForallArg(out en);
						es.Add(en); 
					}
				}
				Expect(9);
				c = new CallCmd(x, first.val, es, ids, kv); 
			} else if (t.kind == 11 || t.kind == 49) {
				ids.Add(new IdentifierExpr(first, first.val)); 
				if (t.kind == 11) {
					Get();
					CallOutIdent(out p);
					if (p==null) {
					  ids.Add(null);
					} else {
					   ids.Add(new IdentifierExpr(p, p.val));
					}
					
					while (t.kind == 11) {
						Get();
						CallOutIdent(out p);
						if (p==null) {
						  ids.Add(null);
						} else {
						   ids.Add(new IdentifierExpr(p, p.val));
						}
						
					}
				}
				Expect(49);
				Ident(out first);
				Expect(8);
				if (StartOf(8)) {
					CallForallArg(out en);
					es.Add(en); 
					while (t.kind == 11) {
						Get();
						CallForallArg(out en);
						es.Add(en); 
					}
				}
				Expect(9);
				c = new CallCmd(x, first.val, es, ids, kv); 
			} else Error(106);
		} else if (t.kind == 51) {
			Get();
			Ident(out first);
			Expect(8);
			args = new List<Expr>(); 
			if (StartOf(8)) {
				CallForallArg(out en);
				args.Add(en); 
				while (t.kind == 11) {
					Get();
					CallForallArg(out en);
					args.Add(en); 
				}
			}
			Expect(9);
			c = new CallForallCmd(x, first.val, args, kv); 
		} else if (t.kind == 44) {
			Get();
			ids.Add(null); 
			if (t.kind == 11) {
				Get();
				CallOutIdent(out p);
				if (p==null) {
				  ids.Add(null);
				} else {
				   ids.Add(new IdentifierExpr(p, p.val));
				}
				
				while (t.kind == 11) {
					Get();
					CallOutIdent(out p);
					if (p==null) {
					  ids.Add(null);
					} else {
					   ids.Add(new IdentifierExpr(p, p.val));
					}
					
				}
			}
			Expect(49);
			Ident(out first);
			Expect(8);
			if (StartOf(8)) {
				CallForallArg(out en);
				es.Add(en); 
				while (t.kind == 11) {
					Get();
					CallForallArg(out en);
					es.Add(en); 
				}
			}
			Expect(9);
			c = new CallCmd(x, first.val, es, ids, kv); 
		} else Error(107);
	}

	static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {
		IToken! x;
		AssignLhs! runningLhs =
		  new SimpleAssignLhs(assignedVariable,
		                      new IdentifierExpr(assignedVariable, assignedVariable.val));
		List<Expr!>! indexes;
		Expr! e0;
		
		while (t.kind == 15) {
			Get();
			x = token;
			indexes = new List<Expr!> (); 
			if (StartOf(5)) {
				Expression(out e0);
				indexes.Add(e0); 
				while (t.kind == 11) {
					Get();
					Expression(out e0);
					indexes.Add(e0); 
				}
			}
			Expect(16);
			runningLhs =
			 new MapAssignLhs (x, runningLhs, indexes);  
		}
		lhs = runningLhs; 
	}

	static void CallForallArg(out Expr exprOptional) {
		exprOptional = null;
		Expr! e;
		
		if (t.kind == 44) {
			Get();
		} else if (StartOf(5)) {
			Expression(out e);
			exprOptional = e; 
		} else Error(108);
	}

	static void CallOutIdent(out IToken id) {
		id = null;
		IToken! p;
		
		if (t.kind == 44) {
			Get();
		} else if (t.kind == 1) {
			Ident(out p);
			id = p; 
		} else Error(109);
	}

	static void Expressions(out ExprSeq! es) {
		Expr! e; es = new ExprSeq(); 
		Expression(out e);
		es.Add(e); 
		while (t.kind == 11) {
			Get();
			Expression(out e);
			es.Add(e); 
		}
	}

	static void ImpliesExpression(bool noExplies, out Expr! e0) {
		IToken! x; Expr! e1; 
		LogicalExpression(out e0);
		if (StartOf(9)) {
			if (t.kind == 54 || t.kind == 55) {
				ImpliesOp();
				x = token; 
				ImpliesExpression(true, out e1);
				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); 
			} else {
				ExpliesOp();
				if (noExplies)
				 SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");
				x = token; 
				LogicalExpression(out e1);
				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 
				while (t.kind == 56 || t.kind == 57) {
					ExpliesOp();
					x = token; 
					LogicalExpression(out e1);
					e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 
				}
			}
		}
	}

	static void EquivOp() {
		if (t.kind == 52) {
			Get();
		} else if (t.kind == 53) {
			Get();
		} else Error(110);
	}

	static void LogicalExpression(out Expr! e0) {
		IToken! x; Expr! e1; BinaryOperator.Opcode op; 
		RelationalExpression(out e0);
		if (StartOf(10)) {
			if (t.kind == 58 || t.kind == 59) {
				AndOp();
				x = token; 
				RelationalExpression(out e1);
				e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 
				while (t.kind == 58 || t.kind == 59) {
					AndOp();
					x = token; 
					RelationalExpression(out e1);
					e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 
				}
			} else {
				OrOp();
				x = token; 
				RelationalExpression(out e1);
				e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 
				while (t.kind == 60 || t.kind == 61) {
					OrOp();
					x = token; 
					RelationalExpression(out e1);
					e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 
				}
			}
		}
	}

	static void ImpliesOp() {
		if (t.kind == 54) {
			Get();
		} else if (t.kind == 55) {
			Get();
		} else Error(111);
	}

	static void ExpliesOp() {
		if (t.kind == 56) {
			Get();
		} else if (t.kind == 57) {
			Get();
		} else Error(112);
	}

	static void RelationalExpression(out Expr! e0) {
		IToken! x; Expr! e1; BinaryOperator.Opcode op; 
		BvTerm(out e0);
		if (StartOf(11)) {
			RelOp(out x, out op);
			BvTerm(out e1);
			e0 = Expr.Binary(x, op, e0, e1); 
		}
	}

	static void AndOp() {
		if (t.kind == 58) {
			Get();
		} else if (t.kind == 59) {
			Get();
		} else Error(113);
	}

	static void OrOp() {
		if (t.kind == 60) {
			Get();
		} else if (t.kind == 61) {
			Get();
		} else Error(114);
	}

	static void BvTerm(out Expr! e0) {
		IToken! x; Expr! e1; 
		Term(out e0);
		while (t.kind == 70) {
			Get();
			x = token; 
			Term(out e1);
			e0 = new BvConcatExpr(x, e0, e1); 
		}
	}

	static void RelOp(out IToken! x, out BinaryOperator.Opcode op) {
		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
		switch (t.kind) {
		case 62: {
			Get();
			x = token; op=BinaryOperator.Opcode.Eq; 
			break;
		}
		case 17: {
			Get();
			x = token; op=BinaryOperator.Opcode.Lt; 
			break;
		}
		case 18: {
			Get();
			x = token; op=BinaryOperator.Opcode.Gt; 
			break;
		}
		case 63: {
			Get();
			x = token; op=BinaryOperator.Opcode.Le; 
			break;
		}
		case 64: {
			Get();
			x = token; op=BinaryOperator.Opcode.Ge; 
			break;
		}
		case 65: {
			Get();
			x = token; op=BinaryOperator.Opcode.Neq; 
			break;
		}
		case 66: {
			Get();
			x = token; op=BinaryOperator.Opcode.Subtype; 
			break;
		}
		case 67: {
			Get();
			x = token; op=BinaryOperator.Opcode.Neq; 
			break;
		}
		case 68: {
			Get();
			x = token; op=BinaryOperator.Opcode.Le; 
			break;
		}
		case 69: {
			Get();
			x = token; op=BinaryOperator.Opcode.Ge; 
			break;
		}
		default: Error(115); break;
		}
	}

	static void Term(out Expr! e0) {
		IToken! x; Expr! e1; BinaryOperator.Opcode op; 
		Factor(out e0);
		while (t.kind == 71 || t.kind == 72) {
			AddOp(out x, out op);
			Factor(out e1);
			e0 = Expr.Binary(x, op, e0, e1); 
		}
	}

	static void Factor(out Expr! e0) {
		IToken! x; Expr! e1; BinaryOperator.Opcode op; 
		UnaryExpression(out e0);
		while (t.kind == 44 || t.kind == 73 || t.kind == 74) {
			MulOp(out x, out op);
			UnaryExpression(out e1);
			e0 = Expr.Binary(x, op, e0, e1); 
		}
	}

	static void AddOp(out IToken! x, out BinaryOperator.Opcode op) {
		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
		if (t.kind == 71) {
			Get();
			x = token; op=BinaryOperator.Opcode.Add; 
		} else if (t.kind == 72) {
			Get();
			x = token; op=BinaryOperator.Opcode.Sub; 
		} else Error(116);
	}

	static void UnaryExpression(out Expr! e) {
		IToken! x;
		e = dummyExpr;
		
		if (t.kind == 72) {
			Get();
			x = token; 
			UnaryExpression(out e);
			e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); 
		} else if (t.kind == 75 || t.kind == 76) {
			NegOp();
			x = token; 
			UnaryExpression(out e);
			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 
		} else if (StartOf(12)) {
			CoercionExpression(out e);
		} else Error(117);
	}

	static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {
		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
		if (t.kind == 44) {
			Get();
			x = token; op=BinaryOperator.Opcode.Mul; 
		} else if (t.kind == 73) {
			Get();
			x = token; op=BinaryOperator.Opcode.Div; 
		} else if (t.kind == 74) {
			Get();
			x = token; op=BinaryOperator.Opcode.Mod; 
		} else Error(118);
	}

	static void NegOp() {
		if (t.kind == 75) {
			Get();
		} else if (t.kind == 76) {
			Get();
		} else Error(119);
	}

	static void CoercionExpression(out Expr! e) {
		IToken! x;
		Type! coercedTo;
		BigNum bn;
		
		ArrayExpression(out e);
		while (t.kind == 10) {
			Get();
			x = token; 
			if (StartOf(2)) {
				Type(out coercedTo);
				e = Expr.CoerceType(x, e, coercedTo); 
			} else if (t.kind == 3) {
				Nat(out bn);
				if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {
				 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);
				}
				
			} else Error(120);
		}
	}

	static void ArrayExpression(out Expr! e) {
		IToken! x;
		Expr! index0 = dummyExpr; Expr! e1;
		bool store; bool bvExtract;
		ExprSeq! allArgs = dummyExprSeq;
		
		AtomExpression(out e);
		while (t.kind == 15) {
			Get();
			x = token; allArgs = new ExprSeq ();
			allArgs.Add(e);
			store = false; bvExtract = false; 
			if (StartOf(13)) {
				if (StartOf(5)) {
					Expression(out index0);
					if (index0 is BvBounds)
					 bvExtract = true;
					else
					  allArgs.Add(index0);
					
					while (t.kind == 11) {
						Get();
						Expression(out e1);
						if (bvExtract || e1 is BvBounds)
						 SemErr("bitvectors only have one dimension");
						allArgs.Add(e1);
						
					}
					if (t.kind == 49) {
						Get();
						Expression(out e1);
						if (bvExtract || e1 is BvBounds)
						 SemErr("assignment to bitvectors is not possible");
						allArgs.Add(e1); store = true;
						
					}
				} else {
					Get();
					Expression(out e1);
					allArgs.Add(e1); store = true; 
				}
			}
			Expect(16);
			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); 
			
		}
	}

	static void Nat(out BigNum n) {
		Expect(3);
		try {
		 n = BigNum.FromString(token.val);
		} catch (FormatException) {
		  SemErr("incorrectly formatted number");
		  n = BigNum.ZERO;
		}
		
	}

	static void AtomExpression(out Expr! e) {
		IToken! x; int n; BigNum bn;
		ExprSeq! es;  VariableSeq! ds;  Trigger trig;
		TypeVariableSeq! typeParams;
		IdentifierExpr! id;
		Bpl.Type! ty;
		QKeyValue kv;
		e = dummyExpr;
		
		switch (t.kind) {
		case 77: {
			Get();
			e = new LiteralExpr(token, false); 
			break;
		}
		case 78: {
			Get();
			e = new LiteralExpr(token, true); 
			break;
		}
		case 3: {
			Nat(out bn);
			e = new LiteralExpr(token, bn); 
			break;
		}
		case 2: {
			BvLit(out bn, out n);
			e = new LiteralExpr(token, bn, n); 
			break;
		}
		case 1: {
			Ident(out x);
			id = new IdentifierExpr(x, x.val);  e = id; 
			if (t.kind == 8) {
				Get();
				if (StartOf(5)) {
					Expressions(out es);
					e = new NAryExpr(x, new FunctionCall(id), es); 
				} else if (t.kind == 9) {
					e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); 
				} else Error(121);
				Expect(9);
			}
			break;
		}
		case 79: {
			Get();
			x = token; 
			Expect(8);
			Expression(out e);
			Expect(9);
			e = new OldExpr(x, e); 
			break;
		}
		case 8: {
			Get();
			if (StartOf(5)) {
				Expression(out e);
				if (e is BvBounds)
				 SemErr("parentheses around bitvector bounds " +
				        "are not allowed"); 
			} else if (t.kind == 51 || t.kind == 81) {
				Forall();
				x = token; 
				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); 
			} else if (t.kind == 82 || t.kind == 83) {
				Exists();
				x = token; 
				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); 
			} else if (t.kind == 84 || t.kind == 85) {
				Lambda();
				x = token; 
				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); 
			} else Error(122);
			Expect(9);
			break;
		}
		case 40: {
			IfThenElseExpression(out e);
			break;
		}
		default: Error(123); break;
		}
	}

	static void BvLit(out BigNum n, out int m) {
		Expect(2);
		int pos = token.val.IndexOf("bv");
		string a = token.val.Substring(0, pos);
		string b = token.val.Substring(pos + 2);
		try {
		  n = BigNum.FromString(a);
		  m = Convert.ToInt32(b);
		} catch (FormatException) {
		  SemErr("incorrectly formatted bitvector");
		  n = BigNum.ZERO;
		  m = 0;
		}
		
	}

	static void Forall() {
		if (t.kind == 51) {
			Get();
		} else if (t.kind == 81) {
			Get();
		} else Error(124);
	}

	static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,
out QKeyValue kv, out Trigger trig, out Expr! body) {
		trig = null; typeParams = new TypeVariableSeq ();
		IToken! tok;  Expr! e;  ExprSeq! es;
		kv = null;  string key;  string value;
		ds = new VariableSeq ();
		
		if (t.kind == 17) {
			TypeParams(out tok, out typeParams);
			if (t.kind == 1) {
				BoundVars(q, out ds);
			}
		} else if (t.kind == 1) {
			BoundVars(q, out ds);
		} else Error(125);
		QSep();
		while (t.kind == 25) {
			AttributeOrTrigger(ref kv, ref trig);
		}
		Expression(out body);
	}

	static void Exists() {
		if (t.kind == 82) {
			Get();
		} else if (t.kind == 83) {
			Get();
		} else Error(126);
	}

	static void Lambda() {
		if (t.kind == 84) {
			Get();
		} else if (t.kind == 85) {
			Get();
		} else Error(127);
	}

	static void IfThenElseExpression(out Expr! e) {
		IToken! tok;
		Expr! e0, e1, e2; 
		e = dummyExpr; 
		Expect(40);
		tok = token; 
		Expression(out e0);
		Expect(80);
		Expression(out e1);
		Expect(41);
		Expression(out e2);
		e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); 
	}

	static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
		IToken! tok;  Expr! e;  ExprSeq! es;
		string key;  string value;
		List<object!> parameters;  object! param;
		
		Expect(25);
		tok = token; 
		if (t.kind == 10) {
			Get();
			Expect(1);
			key = token.val;  parameters = new List<object!>(); 
			if (StartOf(14)) {
				AttributeParameter(out param);
				parameters.Add(param); 
				while (t.kind == 11) {
					Get();
					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 {
			   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));
			  }
			}
			
		} else if (StartOf(5)) {
			Expression(out e);
			es = new ExprSeq(e); 
			while (t.kind == 11) {
				Get();
				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));
			}
			
		} else Error(128);
		Expect(26);
	}

	static void AttributeParameter(out object! o) {
		o = "error";
		Expr! e;
		
		if (t.kind == 4) {
			Get();
			o = token.val.Substring(1, token.val.Length-2); 
		} else if (StartOf(5)) {
			Expression(out e);
			o = e; 
		} else Error(129);
	}

	static void QSep() {
		if (t.kind == 86) {
			Get();
		} else if (t.kind == 87) {
			Get();
		} else Error(130);
	}



	public static void Parse() {
		Errors.SynErr = new ErrorProc(SynErr);
		t = new Token();
		Get();
		BoogiePL();

	}

	[Microsoft.Contracts.Verify(false)]
	static void SynErr(int n, string filename, int line, int col) {
		Errors.count++;
		Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);
		string s;
		switch (n) {
			case 0: s = "EOF expected"; break;
			case 1: s = "ident expected"; break;
			case 2: s = "bvlit expected"; break;
			case 3: s = "digits expected"; break;
			case 4: s = "string expected"; break;
			case 5: s = "float expected"; break;
			case 6: s = "var expected"; break;
			case 7: s = "; expected"; break;
			case 8: s = "( expected"; break;
			case 9: s = ") expected"; break;
			case 10: s = ": expected"; break;
			case 11: s = ", expected"; break;
			case 12: s = "where expected"; break;
			case 13: s = "int expected"; break;
			case 14: s = "bool expected"; break;
			case 15: s = "[ expected"; break;
			case 16: s = "] expected"; break;
			case 17: s = "< expected"; break;
			case 18: s = "> expected"; break;
			case 19: s = "const expected"; break;
			case 20: s = "unique expected"; break;
			case 21: s = "extends expected"; break;
			case 22: s = "complete expected"; break;
			case 23: s = "function expected"; break;
			case 24: s = "returns expected"; break;
			case 25: s = "{ expected"; break;
			case 26: s = "} expected"; break;
			case 27: s = "axiom expected"; break;
			case 28: s = "type expected"; break;
			case 29: s = "= expected"; break;
			case 30: s = "procedure expected"; break;
			case 31: s = "implementation expected"; break;
			case 32: s = "modifies expected"; break;
			case 33: s = "free expected"; break;
			case 34: s = "requires expected"; break;
			case 35: s = "ensures expected"; break;
			case 36: s = "{{ expected"; break;
			case 37: s = "}} expected"; break;
			case 38: s = "goto expected"; break;
			case 39: s = "return expected"; break;
			case 40: s = "if expected"; break;
			case 41: s = "else expected"; break;
			case 42: s = "while expected"; break;
			case 43: s = "invariant expected"; break;
			case 44: s = "* expected"; break;
			case 45: s = "break expected"; break;
			case 46: s = "assert expected"; break;
			case 47: s = "assume expected"; break;
			case 48: s = "havoc expected"; break;
			case 49: s = ":= expected"; break;
			case 50: s = "call expected"; break;
			case 51: s = "forall expected"; break;
			case 52: s = "<==> expected"; break;
			case 53: s = "\\u21d4 expected"; break;
			case 54: s = "==> expected"; break;
			case 55: s = "\\u21d2 expected"; break;
			case 56: s = "<== expected"; break;
			case 57: s = "\\u21d0 expected"; break;
			case 58: s = "&& expected"; break;
			case 59: s = "\\u2227 expected"; break;
			case 60: s = "|| expected"; break;
			case 61: s = "\\u2228 expected"; break;
			case 62: s = "== expected"; break;
			case 63: s = "<= expected"; break;
			case 64: s = ">= expected"; break;
			case 65: s = "!= expected"; break;
			case 66: s = "<: expected"; break;
			case 67: s = "\\u2260 expected"; break;
			case 68: s = "\\u2264 expected"; break;
			case 69: s = "\\u2265 expected"; break;
			case 70: s = "++ expected"; break;
			case 71: s = "+ expected"; break;
			case 72: s = "- expected"; break;
			case 73: s = "/ expected"; break;
			case 74: s = "% expected"; break;
			case 75: s = "! expected"; break;
			case 76: s = "\\u00ac expected"; break;
			case 77: s = "false expected"; break;
			case 78: s = "true expected"; break;
			case 79: s = "old expected"; break;
			case 80: s = "then expected"; break;
			case 81: s = "\\u2200 expected"; break;
			case 82: s = "exists expected"; break;
			case 83: s = "\\u2203 expected"; break;
			case 84: s = "lambda expected"; break;
			case 85: s = "\\u03bb expected"; break;
			case 86: s = ":: expected"; break;
			case 87: s = "\\u2022 expected"; break;
			case 88: s = "??? expected"; break;
			case 89: s = "invalid Function"; break;
			case 90: s = "invalid Function"; break;
			case 91: s = "invalid Procedure"; break;
			case 92: s = "invalid Type"; break;
			case 93: s = "invalid TypeAtom"; break;
			case 94: s = "invalid TypeArgs"; break;
			case 95: s = "invalid Spec"; break;
			case 96: s = "invalid SpecPrePost"; break;
			case 97: s = "invalid SpecPrePost"; break;
			case 98: s = "invalid SpecPrePost"; break;
			case 99: s = "invalid SpecBlock"; break;
			case 100: s = "invalid LabelOrCmd"; break;
			case 101: s = "invalid StructuredCmd"; break;
			case 102: s = "invalid TransferCmd"; break;
			case 103: s = "invalid IfCmd"; break;
			case 104: s = "invalid Guard"; break;
			case 105: s = "invalid LabelOrAssign"; break;
			case 106: s = "invalid CallCmd"; break;
			case 107: s = "invalid CallCmd"; break;
			case 108: s = "invalid CallForallArg"; break;
			case 109: s = "invalid CallOutIdent"; break;
			case 110: s = "invalid EquivOp"; break;
			case 111: s = "invalid ImpliesOp"; break;
			case 112: s = "invalid ExpliesOp"; break;
			case 113: s = "invalid AndOp"; break;
			case 114: s = "invalid OrOp"; break;
			case 115: s = "invalid RelOp"; break;
			case 116: s = "invalid AddOp"; break;
			case 117: s = "invalid UnaryExpression"; break;
			case 118: s = "invalid MulOp"; break;
			case 119: s = "invalid NegOp"; break;
			case 120: s = "invalid CoercionExpression"; break;
			case 121: s = "invalid AtomExpression"; break;
			case 122: s = "invalid AtomExpression"; break;
			case 123: s = "invalid AtomExpression"; break;
			case 124: s = "invalid Forall"; break;
			case 125: s = "invalid QuantifierBody"; break;
			case 126: s = "invalid Exists"; break;
			case 127: s = "invalid Lambda"; break;
			case 128: s = "invalid AttributeOrTrigger"; break;
			case 129: s = "invalid AttributeParameter"; break;
			case 130: s = "invalid QSep"; break;

			default: s = "error " + n; break;
		}
		Console.WriteLine(s);
	}

	static bool[,]! set = {
	{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x},
	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
	{x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}

	};

	[Microsoft.Contracts.Verify(false)]
	static Parser() {}
} // end Parser

} // end namespace