using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
using System.Text;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Dafny {
public class Parser {
public const int _EOF = 0;
public const int _ident = 1;
public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
public const int _colon = 5;
public const int _lbrace = 6;
public const int _rbrace = 7;
public const int maxT = 107;
const bool T = true;
const bool x = false;
const int minErrDist = 2;
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
public Token/*!*/ t; // last recognized token
public Token/*!*/ la; // lookahead token
int errDist = minErrDist;
static ModuleDecl theModule;
static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
static int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
}
// helper routine for parsing call statements
///
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(module != null);
string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List());
return Parse(s, filename, module, builtIns);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List());
return Parse(s, filename, module, builtIns);
}
}
}
///
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(module != null);
Errors errors = new Errors();
return Parse(s, filename, module, builtIns, errors);
}
///
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner with the given Errors sink.
///
public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,
Errors/*!*/ errors) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(module != null);
Contract.Requires(errors != null);
var oldModule = theModule;
theModule = module;
BuiltIns oldBuiltIns = builtIns;
theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Scanner scanner = new Scanner(ms, errors, filename);
Parser parser = new Parser(scanner, errors);
parser.Parse();
theModule = oldModule;
theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
bool IsAttribute() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.kind == _colon;
}
/*--------------------------------------------------------------------------*/
public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {
this.scanner = scanner;
this.errors = errors;
Token/*!*/ tok = new Token();
tok.val = "";
this.la = tok;
this.t = new Token(); // just to satisfy its non-null constraint
}
void SynErr (int n) {
if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);
errDist = 0;
}
public void SemErr (string/*!*/ msg) {
Contract.Requires(msg != null);
if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
Contract.Requires(tok != null);
Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
void Get () {
for (;;) {
t = la;
la = scanner.Scan();
if (la.kind <= maxT) { ++errDist; break; }
la = t;
}
}
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
bool StartOf (int s) {
return set[s, la.kind];
}
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
SynErr(n);
while (!StartOf(follow)) Get();
}
}
bool WeakSeparator(int n, int syFol, int repFol) {
int kind = la.kind;
if (kind == n) {Get(); return true;}
else if (StartOf(repFol)) {return false;}
else {
SynErr(n);
while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {
Get();
kind = la.kind;
}
return StartOf(syFol);
}
}
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;
List membersDefaultClass = new List();
ModuleDecl submodule;
// to support multiple files, create a default module only if theModule is null
DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
// theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
Contract.Assert(defaultModule != null);
bool isGhost;
while (StartOf(1)) {
isGhost = false;
if (la.kind == 8) {
Get();
isGhost = true;
}
if (la.kind == 9) {
SubModuleDecl(defaultModule, isGhost, out submodule);
defaultModule.TopLevelDecls.Add(submodule);
} else if (la.kind == 15) {
if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); }
ClassDecl(defaultModule, out c);
defaultModule.TopLevelDecls.Add(c);
} else if (la.kind == 17 || la.kind == 18) {
if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); }
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
} else if (la.kind == 22) {
if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); }
ArbitraryTypeDecl(defaultModule, out at);
defaultModule.TopLevelDecls.Add(at);
} else if (StartOf(2)) {
ClassMemberDecl(membersDefaultClass, isGhost, false);
} else SynErr(108);
}
DefaultClassDecl defaultClass = null;
foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
defaultClass = topleveldecl as DefaultClassDecl;
if (defaultClass != null) {
defaultClass.Members.AddRange(membersDefaultClass);
break;
}
}
if (defaultClass == null) { // create the default class here, because it wasn't found
defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);
defaultModule.TopLevelDecls.Add(defaultClass);
}
Expect(0);
}
void SubModuleDecl(ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule) {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;
Attributes attrs = null; IToken/*!*/ id;
List namedModuleDefaultClassMembers = new List();;
List idRefined = null, idPath = null;
bool isGhost = false;
ModuleDefinition module;
ModuleDecl sm;
submodule = null; // appease compiler
Expect(9);
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 6 || la.kind == 10) {
if (la.kind == 10) {
Get();
QualifiedName(out idRefined);
}
module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false);
Expect(6);
module.BodyStartTok = t;
while (StartOf(1)) {
isGhost = false;
if (la.kind == 8) {
Get();
isGhost = true;
}
if (la.kind == 9) {
SubModuleDecl(module, isGhost, out sm);
module.TopLevelDecls.Add(sm);
} else if (la.kind == 15) {
if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); }
ClassDecl(module, out c);
module.TopLevelDecls.Add(c);
} else if (la.kind == 17 || la.kind == 18) {
if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); }
DatatypeDecl(module, out dt);
module.TopLevelDecls.Add(dt);
} else if (la.kind == 22) {
if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); }
ArbitraryTypeDecl(module, out at);
module.TopLevelDecls.Add(at);
} else if (StartOf(2)) {
ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);
} else SynErr(109);
}
Expect(7);
module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent);
} else if (la.kind == 11) {
Get();
QualifiedName(out idPath);
Expect(12);
submodule = new AliasModuleDecl(idPath, id, parent);
} else if (la.kind == 13) {
Get();
QualifiedName(out idPath);
Expect(12);
submodule = new AbstractModuleDecl(idPath, id, parent);
} else SynErr(110);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
Attributes attrs = null;
List typeArgs = new List();
List members = new List();
IToken bodyStart;
while (!(la.kind == 0 || la.kind == 15)) {SynErr(111); Get();}
Expect(15);
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 26) {
GenericParameters(typeArgs);
}
Expect(6);
bodyStart = t;
while (StartOf(2)) {
ClassMemberDecl(members, false, true);
}
Expect(7);
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
}
void DatatypeDecl(ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt) {
Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
IToken/*!*/ id;
Attributes attrs = null;
List typeArgs = new List();
List ctors = new List();
IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(112); Get();}
if (la.kind == 17) {
Get();
} else if (la.kind == 18) {
Get();
co = true;
} else SynErr(113);
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 26) {
GenericParameters(typeArgs);
}
Expect(11);
bodyStart = t;
DatatypeMemberDecl(ctors);
while (la.kind == 19) {
Get();
DatatypeMemberDecl(ctors);
}
while (!(la.kind == 0 || la.kind == 12)) {SynErr(114); Get();}
Expect(12);
if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
} else {
dt = new IndDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
}
dt.BodyStartTok = bodyStart;
dt.BodyEndTok = t;
}
void ArbitraryTypeDecl(ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at) {
IToken/*!*/ id;
Attributes attrs = null;
var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
Expect(22);
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 23) {
Get();
Expect(24);
Expect(25);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();}
Expect(12);
}
void ClassMemberDecl(List/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) {
Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
mmod.IsGhost = isAlreadyGhost;
while (la.kind == 8 || la.kind == 16) {
if (la.kind == 8) {
Get();
mmod.IsGhost = true;
} else {
Get();
mmod.IsStatic = true;
}
}
if (la.kind == 20) {
FieldDecl(mmod, mm);
} else if (la.kind == 45 || la.kind == 46) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (la.kind == 28 || la.kind == 29) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
} else SynErr(116);
}
void Attribute(ref Attributes attrs) {
Expect(6);
AttributeBody(ref attrs);
Expect(7);
}
void NoUSIdent(out IToken/*!*/ x) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
x = t;
if (x.val.Length > 0 && x.val.StartsWith("_")) {
SemErr("cannot declare identifier beginning with underscore");
}
}
void QualifiedName(out List ids) {
IToken id; ids = new List();
Ident(out id);
ids.Add(id);
while (la.kind == 14) {
Get();
Ident(out id);
ids.Add(id);
}
}
void Ident(out IToken/*!*/ x) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
x = t;
}
void GenericParameters(List/*!*/ typeArgs) {
Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id;
TypeParameter.EqualitySupportValue eqSupport;
Expect(26);
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
if (la.kind == 23) {
Get();
Expect(24);
Expect(25);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
while (la.kind == 21) {
Get();
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
if (la.kind == 23) {
Get();
Expect(24);
Expect(25);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
}
Expect(27);
}
void FieldDecl(MemberModifiers mmod, List/*!*/ mm) {
Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
while (!(la.kind == 0 || la.kind == 20)) {SynErr(117); Get();}
Expect(20);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
while (la.kind == 6) {
Attribute(ref attrs);
}
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
while (la.kind == 21) {
Get();
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
while (!(la.kind == 0 || la.kind == 12)) {SynErr(118); Get();}
Expect(12);
}
void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {
Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
Attributes attrs = null;
IToken/*!*/ id = Token.NoToken; // to please compiler
List typeArgs = new List();
List formals = new List();
Type/*!*/ returnType = new BoolType();
List reqs = new List();
List ens = new List();
List reads = new List();
List decreases = new List();
Expression body = null;
bool isPredicate = false;
bool isFunctionMethod = false;
IToken openParen = null;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
bool signatureOmitted = false;
if (la.kind == 45) {
Get();
if (la.kind == 28) {
Get();
isFunctionMethod = true;
}
if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 23 || la.kind == 26) {
if (la.kind == 26) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals, out openParen);
Expect(5);
Type(out returnType);
} else if (la.kind == 31) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
} else SynErr(119);
} else if (la.kind == 46) {
Get();
isPredicate = true;
if (la.kind == 28) {
Get();
isFunctionMethod = true;
}
if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (StartOf(3)) {
if (la.kind == 26) {
GenericParameters(typeArgs);
}
if (la.kind == 23) {
Formals(true, isFunctionMethod, formals, out openParen);
if (la.kind == 5) {
Get();
SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
}
}
} else if (la.kind == 31) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
} else SynErr(120);
} else SynErr(121);
while (StartOf(4)) {
FunctionSpec(reqs, reads, ens, decreases);
}
if (la.kind == 6) {
FunctionBody(out body, out bodyStart, out bodyEnd);
}
if (isPredicate) {
f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
reqs, reads, ens, new Specification(decreases, null), body, false, attrs, signatureOmitted);
} else {
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,
reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureOmitted);
}
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
}
void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) {
Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id;
Attributes attrs = null;
List/*!*/ typeArgs = new List();
IToken openParen;
List ins = new List();
List outs = new List();
List req = new List();
List mod = new List();
List ens = new List();
List dec = new List();
Attributes decAttrs = null;
Attributes modAttrs = null;
BlockStmt body = null;
bool isConstructor = false;
bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(122); Get();}
if (la.kind == 28) {
Get();
} else if (la.kind == 29) {
Get();
if (allowConstructor) {
isConstructor = true;
} else {
SemErr(t, "constructors are only allowed in classes");
}
} else SynErr(123);
if (isConstructor) {
if (mmod.IsGhost) {
SemErr(t, "constructors cannot be declared 'ghost'");
}
if (mmod.IsStatic) {
SemErr(t, "constructors cannot be declared 'static'");
}
}
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 23 || la.kind == 26) {
if (la.kind == 26) {
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins, out openParen);
if (la.kind == 30) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs, out openParen);
}
} else if (la.kind == 31) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
} else SynErr(124);
while (StartOf(5)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
if (la.kind == 6) {
BlockStmt(out body, out bodyStart, out bodyEnd);
}
if (isConstructor) {
m = new Constructor(id, id.val, typeArgs, ins,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureOmitted);
} else {
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureOmitted);
}
m.BodyStartTok = bodyStart;
m.BodyEndTok = bodyEnd;
}
void DatatypeMemberDecl(List/*!*/ ctors) {
Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
IToken/*!*/ id;
List formals = new List();
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 23) {
FormalsOptionalIds(formals);
}
ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
}
void FormalsOptionalIds(List/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
Expect(23);
if (StartOf(6)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
while (la.kind == 21) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
Expect(25);
}
void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
NoUSIdent(out id);
Expect(5);
Type(out ty);
}
void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false;
if (la.kind == 8) {
Get();
if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
IdentType(out id, out ty);
}
void Type(out Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
TypeAndToken(out tok, out ty);
}
void LocalIdentTypeOptional(out VarDecl/*!*/ var, bool isGhost) {
IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
NoUSIdent(out id);
if (la.kind == 5) {
Get();
Type(out ty);
optType = ty;
}
var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost);
}
void IdentTypeOptional(out BoundVar/*!*/ var) {
Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
NoUSIdent(out id);
if (la.kind == 5) {
Get();
Type(out ty);
optType = ty;
}
var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType);
}
void TypeIdentOptional(out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost) {
Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
string name = null; isGhost = false;
if (la.kind == 8) {
Get();
isGhost = true;
}
TypeAndToken(out id, out ty);
if (la.kind == 5) {
Get();
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++;
}
}
void TypeAndToken(out IToken/*!*/ tok, out Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List/*!*/ gt;
switch (la.kind) {
case 37: {
Get();
tok = t;
break;
}
case 38: {
Get();
tok = t; ty = new NatType();
break;
}
case 39: {
Get();
tok = t; ty = new IntType();
break;
}
case 40: {
Get();
tok = t; gt = new List();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("set type expects exactly one type argument");
}
ty = new SetType(gt[0]);
break;
}
case 41: {
Get();
tok = t; gt = new List();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("multiset type expects exactly one type argument");
}
ty = new MultiSetType(gt[0]);
break;
}
case 42: {
Get();
tok = t; gt = new List();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
}
ty = new SeqType(gt[0]);
break;
}
case 43: {
Get();
tok = t; gt = new List();
GenericInstantiation(gt);
if (gt.Count != 2) {
SemErr("map type expects exactly two type arguments");
}
else { ty = new MapType(gt[0], gt[1]); }
break;
}
case 1: case 3: case 44: {
ReferenceType(out tok, out ty);
break;
}
default: SynErr(125); break;
}
}
void Formals(bool incoming, bool allowGhostKeyword, List/*!*/ formals, out IToken openParen) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
Expect(23);
openParen = t;
if (la.kind == 1 || la.kind == 8) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
while (la.kind == 21) {
Get();
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
Expect(25);
}
void MethodSpec(List/*!*/ req, List/*!*/ mod, List/*!*/ ens,
List/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs) {
Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
while (!(StartOf(7))) {SynErr(126); Get();}
if (la.kind == 32) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
}
if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 21) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
while (!(la.kind == 0 || la.kind == 12)) {SynErr(127); Get();}
Expect(12);
} else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {
if (la.kind == 33) {
Get();
isFree = true;
}
if (la.kind == 34) {
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 12)) {SynErr(128); Get();}
Expect(12);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 35) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e);
while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();}
Expect(12);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
} else SynErr(130);
} else if (la.kind == 36) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, false);
while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}
Expect(12);
} else SynErr(132);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List body = new List();
Expect(6);
bodyStart = t;
while (StartOf(9)) {
Stmt(body);
}
Expect(7);
bodyEnd = t;
block = new BlockStmt(bodyStart, body);
}
void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
if (la.kind == 49) {
Get();
Ident(out id);
fieldName = id.val;
}
fe = new FrameExpression(e, fieldName);
}
void Expression(out Expression/*!*/ e) {
EquivExpression(out e);
}
void DecreasesList(List decreases, bool allowWildcard) {
Expression/*!*/ e;
PossiblyWildExpression(out e);
if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is only allowed on loops");
} else {
decreases.Add(e);
}
while (la.kind == 21) {
Get();
PossiblyWildExpression(out e);
if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is only allowed on loops");
} else {
decreases.Add(e);
}
}
}
void GenericInstantiation(List/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
Expect(26);
Type(out ty);
gt.Add(ty);
while (la.kind == 21) {
Get();
Type(out ty);
gt.Add(ty);
}
Expect(27);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
IToken moduleName = null;
List/*!*/ gt;
if (la.kind == 44) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
Get();
tok = t; gt = new List();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
int dims = 1;
if (tok.val.Length != 5) {
dims = int.Parse(tok.val.Substring(5));
}
ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
} else if (la.kind == 1) {
Ident(out tok);
gt = new List();
if (la.kind == 14) {
moduleName = tok;
Get();
Ident(out tok);
}
if (la.kind == 26) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, moduleName);
} else SynErr(133);
}
void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 34) {
while (!(la.kind == 0 || la.kind == 34)) {SynErr(134); Get();}
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();}
Expect(12);
reqs.Add(e);
} else if (la.kind == 47) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
while (la.kind == 21) {
Get();
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
}
}
while (!(la.kind == 0 || la.kind == 12)) {SynErr(136); Get();}
Expect(12);
} else if (la.kind == 35) {
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();}
Expect(12);
ens.Add(e);
} else if (la.kind == 36) {
Get();
DecreasesList(decreases, false);
while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}
Expect(12);
} else SynErr(139);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
Expect(6);
bodyStart = t;
Expression(out e);
Expect(7);
bodyEnd = t;
}
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
if (la.kind == 48) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
} else SynErr(140);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
if (la.kind == 48) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
} else SynErr(141);
}
void Stmt(List/*!*/ ss) {
Statement/*!*/ s;
OneStmt(out s);
ss.Add(s);
}
void OneStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
BlockStmt bs;
IToken bodyStart, bodyEnd;
int breakCount;
while (!(StartOf(11))) {SynErr(142); Get();}
switch (la.kind) {
case 6: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
}
case 67: {
AssertStmt(out s);
break;
}
case 55: {
AssumeStmt(out s);
break;
}
case 68: {
PrintStmt(out s);
break;
}
case 1: case 2: case 19: case 23: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
UpdateStmt(out s);
break;
}
case 8: case 20: {
VarDeclStatement(out s);
break;
}
case 60: {
IfStmt(out s);
break;
}
case 64: {
WhileStmt(out s);
break;
}
case 66: {
MatchStmt(out s);
break;
}
case 69: {
ParallelStmt(out s);
break;
}
case 50: {
Get();
x = t;
NoUSIdent(out id);
Expect(5);
OneStmt(out s);
s.Labels = new LList