diff options
| -rw-r--r-- | Dafny/Dafny.atg | 22 | ||||
| -rw-r--r-- | Dafny/Parser.cs | 1250 | ||||
| -rw-r--r-- | Dafny/Scanner.cs | 219 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 4 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 9 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 4 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 4 |
7 files changed, 768 insertions, 744 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index adbad177..748b3090 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -177,11 +177,12 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl ModuleDefinition module;
ModuleDecl sm;
submodule = null; // appease compiler
+ bool opened = false;
.)
- "module"
+ ( "module"
{ Attribute<ref attrs> }
NoUSIdent<out id>
- ((
+
[ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); .)
"{" (. module.BodyStartTok = t; .)
{ (. isGhost = false; .)
@@ -199,14 +200,17 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl "}" (. module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent); .)
- ) |
- "=" QualifiedName<out idPath> ";" (. submodule = new AliasModuleDecl(idPath, id, parent); .)
- |
- ( "as" QualifiedName<out idPath>
- ["=" QualifiedName<out idAssignment> ]
- ";" (.submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment); .)
+ |
+ "import" ["opened" (.opened = true;.)]
+ ( NoUSIdent<out id> ( "=" QualifiedName<out idPath> ";"
+ (. submodule = new AliasModuleDecl(idPath, id, parent); .)
+ | ";"
+ (. idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent); .)
+ | "as" QualifiedName<out idPath> ["default" QualifiedName<out idAssignment> ] ";"
+ (.submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment); .)
+ )
)
- )
+ )
.
QualifiedName<.out List<IToken> ids.>
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 74848d52..244fe550 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -21,7 +21,7 @@ public class Parser { public const int _colon = 5;
public const int _lbrace = 6;
public const int _rbrace = 7;
- public const int maxT = 108;
+ public const int maxT = 111;
const bool T = true;
const bool x = false;
@@ -195,24 +195,24 @@ bool IsAttribute() { Get();
isGhost = true;
}
- if (la.kind == 9) {
+ if (la.kind == 9 || la.kind == 11) {
SubModuleDecl(defaultModule, isGhost, out submodule);
defaultModule.TopLevelDecls.Add(submodule);
- } else if (la.kind == 15) {
+ } else if (la.kind == 18) {
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) {
+ } else if (la.kind == 20 || la.kind == 21) {
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) {
+ } else if (la.kind == 25) {
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(109);
+ } else SynErr(112);
}
DefaultClassDecl defaultClass = null;
foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
@@ -238,13 +238,14 @@ bool IsAttribute() { ModuleDefinition module;
ModuleDecl sm;
submodule = null; // appease compiler
+ bool opened = false;
- Expect(9);
- while (la.kind == 6) {
- Attribute(ref attrs);
- }
- NoUSIdent(out id);
- if (la.kind == 6 || la.kind == 10) {
+ if (la.kind == 9) {
+ Get();
+ while (la.kind == 6) {
+ Attribute(ref attrs);
+ }
+ NoUSIdent(out id);
if (la.kind == 10) {
Get();
QualifiedName(out idRefined);
@@ -258,24 +259,24 @@ bool IsAttribute() { Get();
isGhost = true;
}
- if (la.kind == 9) {
+ if (la.kind == 9 || la.kind == 11) {
SubModuleDecl(module, isGhost, out sm);
module.TopLevelDecls.Add(sm);
- } else if (la.kind == 15) {
+ } else if (la.kind == 18) {
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) {
+ } else if (la.kind == 20 || la.kind == 21) {
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) {
+ } else if (la.kind == 25) {
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(110);
+ } else SynErr(113);
}
Expect(7);
module.BodyEndTok = t;
@@ -283,19 +284,30 @@ bool IsAttribute() { 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);
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
- QualifiedName(out idAssignment);
+ opened = true;
}
- Expect(12);
- submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment);
- } else SynErr(111);
+ NoUSIdent(out id);
+ if (la.kind == 13) {
+ Get();
+ QualifiedName(out idPath);
+ Expect(14);
+ submodule = new AliasModuleDecl(idPath, id, parent);
+ } else if (la.kind == 14) {
+ Get();
+ idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent);
+ } else if (la.kind == 15) {
+ Get();
+ QualifiedName(out idPath);
+ if (la.kind == 16) {
+ Get();
+ QualifiedName(out idAssignment);
+ }
+ Expect(14);
+ submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment);
+ } else SynErr(114);
+ } else SynErr(115);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -307,13 +319,13 @@ bool IsAttribute() { List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(112); Get();}
- Expect(15);
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(116); Get();}
+ Expect(18);
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 26) {
+ if (la.kind == 29) {
GenericParameters(typeArgs);
}
Expect(6);
@@ -338,29 +350,29 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(113); Get();}
- if (la.kind == 17) {
+ while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(117); Get();}
+ if (la.kind == 20) {
Get();
- } else if (la.kind == 18) {
+ } else if (la.kind == 21) {
Get();
co = true;
- } else SynErr(114);
+ } else SynErr(118);
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 26) {
+ if (la.kind == 29) {
GenericParameters(typeArgs);
}
- Expect(11);
+ Expect(13);
bodyStart = t;
DatatypeMemberDecl(ctors);
- while (la.kind == 19) {
+ while (la.kind == 22) {
Get();
DatatypeMemberDecl(ctors);
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(119); Get();}
+ Expect(14);
if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
} else {
@@ -376,20 +388,20 @@ bool IsAttribute() { Attributes attrs = null;
var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- Expect(22);
+ Expect(25);
while (la.kind == 6) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
- Expect(24);
- Expect(25);
+ Expect(27);
+ Expect(28);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(116); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(120); Get();}
+ Expect(14);
}
void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) {
@@ -399,7 +411,7 @@ bool IsAttribute() { MemberModifiers mmod = new MemberModifiers();
mmod.IsGhost = isAlreadyGhost;
- while (la.kind == 8 || la.kind == 16) {
+ while (la.kind == 8 || la.kind == 19) {
if (la.kind == 8) {
Get();
mmod.IsGhost = true;
@@ -408,15 +420,15 @@ bool IsAttribute() { mmod.IsStatic = true;
}
}
- if (la.kind == 20) {
+ if (la.kind == 23) {
FieldDecl(mmod, mm);
- } else if (la.kind == 45 || la.kind == 46 || la.kind == 47) {
+ } else if (la.kind == 48 || la.kind == 49 || la.kind == 50) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (la.kind == 28 || la.kind == 29) {
+ } else if (la.kind == 31 || la.kind == 32) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(117);
+ } else SynErr(121);
}
void Attribute(ref Attributes attrs) {
@@ -439,7 +451,7 @@ bool IsAttribute() { IToken id; ids = new List<IToken>();
Ident(out id);
ids.Add(id);
- while (la.kind == 14) {
+ while (la.kind == 17) {
Get();
Ident(out id);
ids.Add(id);
@@ -457,29 +469,29 @@ bool IsAttribute() { IToken/*!*/ id;
TypeParameter.EqualitySupportValue eqSupport;
- Expect(26);
+ Expect(29);
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
- Expect(24);
- Expect(25);
+ Expect(27);
+ Expect(28);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
- Expect(24);
- Expect(25);
+ Expect(27);
+ Expect(28);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
}
- Expect(27);
+ Expect(30);
}
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
@@ -487,8 +499,8 @@ bool IsAttribute() { Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 20)) {SynErr(118); Get();}
- Expect(20);
+ while (!(la.kind == 0 || la.kind == 23)) {SynErr(122); Get();}
+ Expect(23);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
while (la.kind == 6) {
@@ -496,13 +508,13 @@ bool IsAttribute() { }
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
- while (la.kind == 21) {
+ while (la.kind == 24) {
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(119); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();}
+ Expect(14);
}
void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {
@@ -524,9 +536,9 @@ bool IsAttribute() { IToken bodyEnd = Token.NoToken;
bool signatureOmitted = false;
- if (la.kind == 45) {
+ if (la.kind == 48) {
Get();
- if (la.kind == 28) {
+ if (la.kind == 31) {
Get();
isFunctionMethod = true;
}
@@ -536,22 +548,22 @@ bool IsAttribute() { Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 23 || la.kind == 26) {
- if (la.kind == 26) {
+ if (la.kind == 26 || la.kind == 29) {
+ if (la.kind == 29) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals, out openParen);
Expect(5);
Type(out returnType);
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(120);
- } else if (la.kind == 46) {
+ } else SynErr(124);
+ } else if (la.kind == 49) {
Get();
isPredicate = true;
- if (la.kind == 28) {
+ if (la.kind == 31) {
Get();
isFunctionMethod = true;
}
@@ -562,22 +574,22 @@ bool IsAttribute() { }
NoUSIdent(out id);
if (StartOf(3)) {
- if (la.kind == 26) {
+ if (la.kind == 29) {
GenericParameters(typeArgs);
}
- if (la.kind == 23) {
+ if (la.kind == 26) {
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) {
+ } else if (la.kind == 34) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(121);
- } else if (la.kind == 47) {
+ } else SynErr(125);
+ } else if (la.kind == 50) {
Get();
isCoPredicate = true;
if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
@@ -587,22 +599,22 @@ bool IsAttribute() { }
NoUSIdent(out id);
if (StartOf(3)) {
- if (la.kind == 26) {
+ if (la.kind == 29) {
GenericParameters(typeArgs);
}
- if (la.kind == 23) {
+ if (la.kind == 26) {
Formals(true, isFunctionMethod, formals, out openParen);
if (la.kind == 5) {
Get();
SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool");
}
}
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(122);
- } else SynErr(123);
+ } else SynErr(126);
+ } else SynErr(127);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(4)) {
FunctionSpec(reqs, reads, ens, decreases);
@@ -645,10 +657,10 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(124); Get();}
- if (la.kind == 28) {
+ while (!(la.kind == 0 || la.kind == 31 || la.kind == 32)) {SynErr(128); Get();}
+ if (la.kind == 31) {
Get();
- } else if (la.kind == 29) {
+ } else if (la.kind == 32) {
Get();
if (allowConstructor) {
isConstructor = true;
@@ -656,7 +668,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(125);
+ } else SynErr(129);
if (isConstructor) {
if (mmod.IsGhost) {
SemErr(t, "constructors cannot be declared 'ghost'");
@@ -670,20 +682,20 @@ bool IsAttribute() { Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 23 || la.kind == 26) {
- if (la.kind == 26) {
+ if (la.kind == 26 || la.kind == 29) {
+ if (la.kind == 29) {
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins, out openParen);
- if (la.kind == 30) {
+ if (la.kind == 33) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs, out openParen);
}
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
- } else SynErr(126);
+ } else SynErr(130);
while (StartOf(5)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
@@ -712,7 +724,7 @@ bool IsAttribute() { Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 23) {
+ if (la.kind == 26) {
FormalsOptionalIds(formals);
}
ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
@@ -720,17 +732,17 @@ bool IsAttribute() { void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
- Expect(23);
+ Expect(26);
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) {
+ while (la.kind == 24) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
- Expect(25);
+ Expect(28);
}
void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -814,22 +826,22 @@ bool IsAttribute() { List<Type/*!*/>/*!*/ gt;
switch (la.kind) {
- case 37: {
+ case 40: {
Get();
tok = t;
break;
}
- case 38: {
+ case 41: {
Get();
tok = t; ty = new NatType();
break;
}
- case 39: {
+ case 42: {
Get();
tok = t; ty = new IntType();
break;
}
- case 40: {
+ case 43: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -840,7 +852,7 @@ bool IsAttribute() { break;
}
- case 41: {
+ case 44: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -851,7 +863,7 @@ bool IsAttribute() { break;
}
- case 42: {
+ case 45: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -862,7 +874,7 @@ bool IsAttribute() { break;
}
- case 43: {
+ case 46: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -873,28 +885,28 @@ bool IsAttribute() { break;
}
- case 1: case 3: case 44: {
+ case 1: case 3: case 47: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(127); break;
+ default: SynErr(131); break;
}
}
void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
- Expect(23);
+ Expect(26);
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) {
+ while (la.kind == 24) {
Get();
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
- Expect(25);
+ Expect(28);
}
void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
@@ -902,8 +914,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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(128); Get();}
- if (la.kind == 32) {
+ while (!(StartOf(7))) {SynErr(132); Get();}
+ if (la.kind == 35) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -911,44 +923,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();}
- Expect(12);
- } else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {
- if (la.kind == 33) {
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(133); Get();}
+ Expect(14);
+ } else if (la.kind == 36 || la.kind == 37 || la.kind == 38) {
+ if (la.kind == 36) {
Get();
isFree = true;
}
- if (la.kind == 34) {
+ if (la.kind == 37) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(130); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(134); Get();}
+ Expect(14);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 35) {
+ } else if (la.kind == 38) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(135); Get();}
+ Expect(14);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(132);
- } else if (la.kind == 36) {
+ } else SynErr(136);
+ } else if (la.kind == 39) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(133); Get();}
- Expect(12);
- } else SynErr(134);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(137); Get();}
+ Expect(14);
+ } else SynErr(138);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -969,18 +981,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; fe = null;
if (StartOf(10)) {
Expression(out e);
- if (la.kind == 50) {
+ if (la.kind == 53) {
Get();
Ident(out id);
fieldName = id.val;
}
fe = new FrameExpression(e, fieldName);
- } else if (la.kind == 50) {
+ } else if (la.kind == 53) {
Get();
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(new ImplicitThisExpr(id), fieldName);
- } else SynErr(135);
+ } else SynErr(139);
}
void Expression(out Expression/*!*/ e) {
@@ -996,7 +1008,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases.Add(e);
}
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
PossiblyWildExpression(out e);
if (!allowWildcard && e is WildcardExpr) {
@@ -1010,15 +1022,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
- Expect(26);
+ Expect(29);
Type(out ty);
gt.Add(ty);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Type(out ty);
gt.Add(ty);
}
- Expect(27);
+ Expect(30);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -1027,7 +1039,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Type/*!*/>/*!*/ gt;
List<IToken> path;
- if (la.kind == 44) {
+ if (la.kind == 47) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
@@ -1047,16 +1059,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out tok);
gt = new List<Type/*!*/>();
path = new List<IToken>();
- while (la.kind == 14) {
+ while (la.kind == 17) {
path.Add(tok);
Get();
Ident(out tok);
}
- if (la.kind == 26) {
+ if (la.kind == 29) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(136);
+ } else SynErr(140);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1064,33 +1076,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- if (la.kind == 34) {
- while (!(la.kind == 0 || la.kind == 34)) {SynErr(137); Get();}
+ if (la.kind == 37) {
+ while (!(la.kind == 0 || la.kind == 37)) {SynErr(141); Get();}
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();}
+ Expect(14);
reqs.Add(e);
- } else if (la.kind == 48) {
+ } else if (la.kind == 51) {
Get();
if (StartOf(11)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(139); Get();}
- Expect(12);
- } else if (la.kind == 35) {
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(143); Get();}
+ Expect(14);
+ } else if (la.kind == 38) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(144); Get();}
+ Expect(14);
ens.Add(e);
- } else if (la.kind == 36) {
+ } else if (la.kind == 39) {
Get();
if (decreases == null) {
SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
@@ -1098,9 +1110,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(141); Get();}
- Expect(12);
- } else SynErr(142);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(145); Get();}
+ Expect(14);
+ } else SynErr(146);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1114,23 +1126,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 49) {
+ if (la.kind == 52) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(143);
+ } else SynErr(147);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 49) {
+ if (la.kind == 52) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(10)) {
Expression(out e);
- } else SynErr(144);
+ } else SynErr(148);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1147,50 +1159,50 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(12))) {SynErr(145); Get();}
+ while (!(StartOf(12))) {SynErr(149); Get();}
switch (la.kind) {
case 6: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
}
- case 69: {
+ case 72: {
AssertStmt(out s);
break;
}
- case 57: {
+ case 60: {
AssumeStmt(out s);
break;
}
- case 70: {
+ case 73: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: {
+ case 1: case 2: case 22: case 26: case 97: case 98: case 99: case 100: case 101: case 102: {
UpdateStmt(out s);
break;
}
- case 8: case 20: {
+ case 8: case 23: {
VarDeclStatement(out s);
break;
}
- case 62: {
+ case 65: {
IfStmt(out s);
break;
}
- case 66: {
+ case 69: {
WhileStmt(out s);
break;
}
- case 68: {
+ case 71: {
MatchStmt(out s);
break;
}
- case 71: {
+ case 74: {
ParallelStmt(out s);
break;
}
- case 51: {
+ case 54: {
Get();
x = t;
NoUSIdent(out id);
@@ -1199,33 +1211,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 52: {
+ case 55: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 12 || la.kind == 52) {
- while (la.kind == 52) {
+ } else if (la.kind == 14 || la.kind == 55) {
+ while (la.kind == 55) {
Get();
breakCount++;
}
- } else SynErr(146);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(147); Get();}
- Expect(12);
+ } else SynErr(150);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(151); Get();}
+ Expect(14);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 55: {
+ case 58: {
ReturnStmt(out s);
break;
}
- case 31: {
+ case 34: {
SkeletonStmt(out s);
- Expect(12);
+ Expect(14);
break;
}
- default: SynErr(148); break;
+ default: SynErr(152); break;
}
}
@@ -1233,17 +1245,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression e = null; Attributes attrs = null;
- Expect(69);
+ Expect(72);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(10)) {
Expression(out e);
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
- } else SynErr(149);
- Expect(12);
+ } else SynErr(153);
+ Expect(14);
if (e == null) {
s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
} else {
@@ -1256,39 +1268,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression e = null; Attributes attrs = null;
- Expect(57);
+ Expect(60);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(10)) {
Expression(out e);
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
- } else SynErr(150);
+ } else SynErr(154);
if (e == null) {
s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
} else {
s = new AssumeStmt(x, e, attrs);
}
- Expect(12);
+ Expect(14);
}
void PrintStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(70);
+ Expect(73);
x = t;
AttributeArg(out arg);
args.Add(arg);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
AttributeArg(out arg);
args.Add(arg);
}
- Expect(12);
+ Expect(14);
s = new PrintStmt(x, args);
}
@@ -1304,43 +1316,43 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Lhs(out e);
x = e.tok;
- if (la.kind == 6 || la.kind == 12) {
+ if (la.kind == 6 || la.kind == 14) {
while (la.kind == 6) {
Attribute(ref attrs);
}
- Expect(12);
+ Expect(14);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 21 || la.kind == 54 || la.kind == 56) {
+ } else if (la.kind == 24 || la.kind == 57 || la.kind == 59) {
lhss.Add(e); lhs0 = e;
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 54) {
+ if (la.kind == 57) {
Get();
x = t;
Rhs(out r, lhs0);
rhss.Add(r);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 56) {
+ } else if (la.kind == 59) {
Get();
x = t;
- if (la.kind == 57) {
+ if (la.kind == 60) {
Get();
suchThatAssume = t;
}
Expression(out suchThat);
- } else SynErr(151);
- Expect(12);
+ } else SynErr(155);
+ Expect(14);
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(152);
+ } else SynErr(156);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
@@ -1366,17 +1378,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
isGhost = true; x = t;
}
- Expect(20);
+ Expect(23);
if (!isGhost) { x = t; }
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 54 || la.kind == 56) {
- if (la.kind == 54) {
+ if (la.kind == 57 || la.kind == 59) {
+ if (la.kind == 57) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1384,7 +1396,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1392,14 +1404,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
Get();
assignTok = t;
- if (la.kind == 57) {
+ if (la.kind == 60) {
Get();
suchThatAssume = t;
}
Expression(out suchThat);
}
}
- Expect(12);
+ Expect(14);
ConcreteUpdateStatement update;
if (suchThat != null) {
var ies = new List<Expression>();
@@ -1431,25 +1443,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(62);
+ Expect(65);
x = t;
- if (la.kind == 23 || la.kind == 31) {
- if (la.kind == 23) {
+ if (la.kind == 26 || la.kind == 34) {
+ if (la.kind == 26) {
Guard(out guard);
} else {
Get();
guardOmitted = true;
}
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 63) {
+ if (la.kind == 66) {
Get();
- if (la.kind == 62) {
+ if (la.kind == 65) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs;
- } else SynErr(153);
+ } else SynErr(157);
}
if (guardOmitted) {
ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1460,7 +1472,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(154);
+ } else SynErr(158);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1476,10 +1488,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(66);
+ Expect(69);
x = t;
- if (la.kind == 23 || la.kind == 31) {
- if (la.kind == 23) {
+ if (la.kind == 26 || la.kind == 34) {
+ if (la.kind == 26) {
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
} else {
@@ -1489,10 +1501,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
if (la.kind == 6) {
BlockStmt(out body, out bodyStart, out bodyEnd);
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
bodyOmitted = true;
- } else SynErr(155);
+ } else SynErr(159);
if (guardOmitted || bodyOmitted) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1510,18 +1522,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives);
- } else SynErr(156);
+ } else SynErr(160);
}
void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(68);
+ Expect(71);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 64) {
+ while (la.kind == 67) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1541,9 +1553,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(71);
+ Expect(74);
x = t;
- Expect(23);
+ Expect(26);
if (la.kind == 1) {
List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX;
QuantifierDomain(out bvarsX, out attrsX, out rangeX);
@@ -1553,16 +1565,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
- Expect(25);
- while (la.kind == 33 || la.kind == 35) {
+ Expect(28);
+ while (la.kind == 36 || la.kind == 38) {
isFree = false;
- if (la.kind == 33) {
+ if (la.kind == 36) {
Get();
isFree = true;
}
- Expect(35);
+ Expect(38);
Expression(out e);
- Expect(12);
+ Expect(14);
ens.Add(new MaybeFreeExpression(e, isFree));
}
BlockStmt(out block, out bodyStart, out bodyEnd);
@@ -1574,18 +1586,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(55);
+ Expect(58);
returnTok = t;
if (StartOf(14)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Rhs(out r, null);
rhss.Add(r);
}
}
- Expect(12);
+ Expect(14);
s = new ReturnStmt(returnTok, rhss);
}
@@ -1594,22 +1606,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Expression> exprs = null;
IToken tok, dotdotdot, whereTok;
Expression e;
- Expect(31);
+ Expect(34);
dotdotdot = t;
- if (la.kind == 53) {
+ if (la.kind == 56) {
Get();
names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
names.Add(tok);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Ident(out tok);
names.Add(tok);
}
- Expect(54);
+ Expect(57);
Expression(out e);
exprs.Add(e);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Expression(out e);
exprs.Add(e);
@@ -1632,27 +1644,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = null; // to please compiler
Attributes attrs = null;
- if (la.kind == 58) {
+ if (la.kind == 61) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 14 || la.kind == 23 || la.kind == 59) {
- if (la.kind == 59) {
+ if (la.kind == 17 || la.kind == 26 || la.kind == 62) {
+ if (la.kind == 62) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(60);
+ Expect(63);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
- } else if (la.kind == 14) {
+ } else if (la.kind == 17) {
Get();
Ident(out x);
- Expect(23);
+ Expect(26);
args = new List<Expression/*!*/>();
if (StartOf(10)) {
Expressions(args);
}
- Expect(25);
+ Expect(28);
initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
} else {
Get();
@@ -1670,7 +1682,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(10)) {
Expressions(args);
}
- Expect(25);
+ Expect(28);
if (x != null) {
initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
}
@@ -1683,18 +1695,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 61) {
+ } else if (la.kind == 64) {
Get();
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 49) {
+ } else if (la.kind == 52) {
Get();
r = new HavocRhs(t);
} else if (StartOf(10)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(157);
+ } else SynErr(161);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -1706,23 +1718,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 14 || la.kind == 59) {
+ while (la.kind == 17 || la.kind == 62) {
Suffix(ref e);
}
} else if (StartOf(15)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 14 || la.kind == 59) {
+ while (la.kind == 17 || la.kind == 62) {
Suffix(ref e);
}
- } else SynErr(158);
+ } else SynErr(162);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
Expression(out e);
args.Add(e);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Expression(out e);
args.Add(e);
@@ -1731,15 +1743,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- Expect(23);
- if (la.kind == 49) {
+ Expect(26);
+ if (la.kind == 52) {
Get();
e = null;
} else if (StartOf(10)) {
Expression(out ee);
e = ee;
- } else SynErr(159);
- Expect(25);
+ } else SynErr(163);
+ Expect(28);
}
void AlternativeBlock(out List<GuardedAlternative> alternatives) {
@@ -1749,11 +1761,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Statement> body;
Expect(6);
- while (la.kind == 64) {
+ while (la.kind == 67) {
Get();
x = t;
Expression(out e);
- Expect(65);
+ Expect(68);
body = new List<Statement>();
while (StartOf(9)) {
Stmt(body);
@@ -1771,22 +1783,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null;
while (StartOf(16)) {
- if (la.kind == 33 || la.kind == 67) {
+ if (la.kind == 36 || la.kind == 70) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(160); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(164); Get();}
+ Expect(14);
invariants.Add(invariant);
- } else if (la.kind == 36) {
- while (!(la.kind == 0 || la.kind == 36)) {SynErr(161); Get();}
+ } else if (la.kind == 39) {
+ while (!(la.kind == 0 || la.kind == 39)) {SynErr(165); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(162); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(166); Get();}
+ Expect(14);
} else {
- while (!(la.kind == 0 || la.kind == 32)) {SynErr(163); Get();}
+ while (!(la.kind == 0 || la.kind == 35)) {SynErr(167); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1795,26 +1807,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(164); Get();}
- Expect(12);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(168); Get();}
+ Expect(14);
}
}
}
void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 33 || la.kind == 67)) {SynErr(165); Get();}
- if (la.kind == 33) {
+ while (!(la.kind == 0 || la.kind == 36 || la.kind == 70)) {SynErr(169); Get();}
+ if (la.kind == 36) {
Get();
isFree = true;
}
- Expect(67);
+ Expect(70);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1829,21 +1841,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(64);
+ Expect(67);
x = t;
Ident(out id);
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(25);
+ Expect(28);
}
- Expect(65);
+ Expect(68);
while (StartOf(9)) {
Stmt(body);
}
@@ -1858,7 +1870,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(10)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(166);
+ } else SynErr(170);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1869,7 +1881,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
bvars.Add(bv);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -1877,7 +1889,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 6) {
Attribute(ref attrs);
}
- if (la.kind == 19) {
+ if (la.kind == 22) {
Get();
Expression(out range);
}
@@ -1886,7 +1898,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 72 || la.kind == 73) {
+ while (la.kind == 75 || la.kind == 76) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1897,7 +1909,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 74 || la.kind == 75) {
+ if (la.kind == 77 || la.kind == 78) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1906,23 +1918,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 72) {
+ if (la.kind == 75) {
Get();
- } else if (la.kind == 73) {
+ } else if (la.kind == 76) {
Get();
- } else SynErr(167);
+ } else SynErr(171);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(17)) {
- if (la.kind == 76 || la.kind == 77) {
+ if (la.kind == 79 || la.kind == 80) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 76 || la.kind == 77) {
+ while (la.kind == 79 || la.kind == 80) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1933,7 +1945,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 78 || la.kind == 79) {
+ while (la.kind == 81 || la.kind == 82) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1944,11 +1956,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void ImpliesOp() {
- if (la.kind == 74) {
+ if (la.kind == 77) {
Get();
- } else if (la.kind == 75) {
+ } else if (la.kind == 78) {
Get();
- } else SynErr(168);
+ } else SynErr(172);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -2042,25 +2054,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 76) {
+ if (la.kind == 79) {
Get();
- } else if (la.kind == 77) {
+ } else if (la.kind == 80) {
Get();
- } else SynErr(169);
+ } else SynErr(173);
}
void OrOp() {
- if (la.kind == 78) {
+ if (la.kind == 81) {
Get();
- } else if (la.kind == 79) {
+ } else if (la.kind == 82) {
Get();
- } else SynErr(170);
+ } else SynErr(174);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 89 || la.kind == 90) {
+ while (la.kind == 92 || la.kind == 93) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2073,50 +2085,50 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken y;
switch (la.kind) {
- case 24: {
+ case 27: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
}
- case 26: {
+ case 29: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 27: {
+ case 30: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 80: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 81: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 82: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 83: {
+ case 86: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 84: {
+ case 87: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 85: {
+ case 88: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 84) {
+ if (la.kind == 87) {
Get();
y = t;
}
@@ -2131,29 +2143,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- case 86: {
+ case 89: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 87: {
+ case 90: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 88: {
+ case 91: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(171); break;
+ default: SynErr(175); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 49 || la.kind == 91 || la.kind == 92) {
+ while (la.kind == 52 || la.kind == 94 || la.kind == 95) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2162,86 +2174,86 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 89) {
+ if (la.kind == 92) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 90) {
+ } else if (la.kind == 93) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(172);
+ } else SynErr(176);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 90: {
+ case 93: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 85: case 93: {
+ case 88: case 96: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 20: case 40: case 51: case 57: case 62: case 68: case 69: case 102: case 103: case 104: case 105: {
+ case 23: case 43: case 54: case 60: case 65: case 71: case 72: case 105: case 106: case 107: case 108: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 14 || la.kind == 59) {
+ while (la.kind == 17 || la.kind == 62) {
Suffix(ref e);
}
break;
}
- case 6: case 59: {
+ case 6: case 62: {
DisplayExpr(out e);
break;
}
- case 41: {
+ case 44: {
MultiSetExpr(out e);
break;
}
- case 43: {
+ case 46: {
MapExpr(out e);
break;
}
- case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: {
+ case 2: case 22: case 26: case 97: case 98: case 99: case 100: case 101: case 102: {
ConstAtomExpression(out e);
- while (la.kind == 14 || la.kind == 59) {
+ while (la.kind == 17 || la.kind == 62) {
Suffix(ref e);
}
break;
}
- default: SynErr(173); break;
+ default: SynErr(177); break;
}
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 49) {
+ if (la.kind == 52) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 91) {
+ } else if (la.kind == 94) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 92) {
+ } else if (la.kind == 95) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(174);
+ } else SynErr(178);
}
void NegOp() {
- if (la.kind == 85) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 93) {
+ } else if (la.kind == 96) {
Get();
- } else SynErr(175);
+ } else SynErr(179);
}
void EndlessExpression(out Expression e) {
@@ -2250,56 +2262,56 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 62: {
+ case 65: {
Get();
x = t;
Expression(out e);
- Expect(100);
+ Expect(103);
Expression(out e0);
- Expect(63);
+ Expect(66);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 68: {
+ case 71: {
MatchExpression(out e);
break;
}
- case 102: case 103: case 104: case 105: {
+ case 105: case 106: case 107: case 108: {
QuantifierGuts(out e);
break;
}
- case 40: {
+ case 43: {
ComprehensionExpr(out e);
break;
}
- case 69: {
+ case 72: {
Get();
x = t;
Expression(out e0);
- Expect(12);
+ Expect(14);
Expression(out e1);
e = new AssertExpr(x, e0, e1);
break;
}
- case 57: {
+ case 60: {
Get();
x = t;
Expression(out e0);
- Expect(12);
+ Expect(14);
Expression(out e1);
e = new AssumeExpr(x, e0, e1);
break;
}
- case 20: {
+ case 23: {
LetExpr(out e);
break;
}
- case 51: {
+ case 54: {
NamedExpr(out e);
break;
}
- default: SynErr(176); break;
+ default: SynErr(180); break;
}
}
@@ -2310,18 +2322,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id);
idents.Add(id);
- while (la.kind == 14) {
+ while (la.kind == 17) {
Get();
Ident(out id);
idents.Add(id);
}
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
openParen = t; args = new List<Expression>();
if (StartOf(10)) {
Expressions(args);
}
- Expect(25);
+ Expect(28);
}
e = new IdentifierSequence(idents, openParen, args);
}
@@ -2332,38 +2344,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 14) {
+ if (la.kind == 17) {
Get();
Ident(out id);
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
IToken openParen = t; args = new List<Expression/*!*/>(); func = true;
if (StartOf(10)) {
Expressions(args);
}
- Expect(25);
+ Expect(28);
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 59) {
+ } else if (la.kind == 62) {
Get();
x = t;
if (StartOf(10)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 101) {
+ if (la.kind == 104) {
Get();
anyDots = true;
if (StartOf(10)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 54) {
+ } else if (la.kind == 57) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 21 || la.kind == 60) {
- while (la.kind == 21) {
+ } else if (la.kind == 24 || la.kind == 63) {
+ while (la.kind == 24) {
Get();
Expression(out ee);
if (multipleIndices == null) {
@@ -2373,15 +2385,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(177);
- } else if (la.kind == 101) {
+ } else SynErr(181);
+ } else if (la.kind == 104) {
Get();
anyDots = true;
if (StartOf(10)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(178);
+ } else SynErr(182);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2404,8 +2416,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(60);
- } else SynErr(179);
+ Expect(63);
+ } else SynErr(183);
}
void DisplayExpr(out Expression e) {
@@ -2421,15 +2433,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 59) {
+ } else if (la.kind == 62) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(10)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(60);
- } else SynErr(180);
+ Expect(63);
+ } else SynErr(184);
}
void MultiSetExpr(out Expression e) {
@@ -2437,7 +2449,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(41);
+ Expect(44);
x = t;
if (la.kind == 6) {
Get();
@@ -2447,15 +2459,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new MultiSetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 23) {
+ } else if (la.kind == 26) {
Get();
x = t; elements = new List<Expression/*!*/>();
Expression(out e);
e = new MultiSetFormingExpr(x, e);
- Expect(25);
+ Expect(28);
} else if (StartOf(19)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(181);
+ } else SynErr(185);
}
void MapExpr(out Expression e) {
@@ -2464,16 +2476,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<ExpressionPair/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(43);
+ Expect(46);
x = t;
- if (la.kind == 59) {
+ if (la.kind == 62) {
Get();
elements = new List<ExpressionPair/*!*/>();
if (StartOf(10)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(x, elements);
- Expect(60);
+ Expect(63);
} else if (la.kind == 1) {
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2482,14 +2494,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
bvars.Add(bv);
- Expect(19);
+ Expect(22);
Expression(out range);
QSep();
Expression(out body);
e = new MapComprehension(x, bvars, range, body);
} else if (StartOf(19)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(182);
+ } else SynErr(186);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2498,17 +2510,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 94: {
+ case 97: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 95: {
+ case 98: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 96: {
+ case 99: {
Get();
e = new LiteralExpr(t);
break;
@@ -2518,46 +2530,46 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n);
break;
}
- case 97: {
+ case 100: {
Get();
e = new ThisExpr(t);
break;
}
- case 98: {
+ case 101: {
Get();
x = t;
- Expect(23);
+ Expect(26);
Expression(out e);
- Expect(25);
+ Expect(28);
e = new FreshExpr(x, e);
break;
}
- case 99: {
+ case 102: {
Get();
x = t;
- Expect(23);
+ Expect(26);
Expression(out e);
- Expect(25);
+ Expect(28);
e = new OldExpr(x, e);
break;
}
- case 19: {
+ case 22: {
Get();
x = t;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(19);
+ Expect(22);
break;
}
- case 23: {
+ case 26: {
Get();
x = t;
Expression(out e);
e = new ParensExpression(x, e);
- Expect(25);
+ Expect(28);
break;
}
- default: SynErr(183); break;
+ default: SynErr(187); break;
}
}
@@ -2576,34 +2588,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d);
- Expect(54);
+ Expect(57);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Expression(out d);
- Expect(54);
+ Expect(57);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
}
}
void QSep() {
- if (la.kind == 106) {
+ if (la.kind == 109) {
Get();
- } else if (la.kind == 107) {
+ } else if (la.kind == 110) {
Get();
- } else SynErr(184);
+ } else SynErr(188);
}
void MatchExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(68);
+ Expect(71);
x = t;
Expression(out e);
- while (la.kind == 64) {
+ while (la.kind == 67) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2618,13 +2630,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression/*!*/ body;
- if (la.kind == 102 || la.kind == 103) {
+ if (la.kind == 105 || la.kind == 106) {
Forall();
x = t; univ = true;
- } else if (la.kind == 104 || la.kind == 105) {
+ } else if (la.kind == 107 || la.kind == 108) {
Exists();
x = t;
- } else SynErr(185);
+ } else SynErr(189);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -2644,18 +2656,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ range;
Expression body = null;
- Expect(40);
+ Expect(43);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv);
}
- Expect(19);
+ Expect(22);
Expression(out range);
- if (la.kind == 106 || la.kind == 107) {
+ if (la.kind == 109 || la.kind == 110) {
QSep();
Expression(out body);
}
@@ -2670,26 +2682,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar d;
List<BoundVar> letVars; List<Expression> letRHSs;
- Expect(20);
+ Expect(23);
x = t;
letVars = new List<BoundVar>();
letRHSs = new List<Expression>();
IdentTypeOptional(out d);
letVars.Add(d);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(54);
+ Expect(57);
Expression(out e);
letRHSs.Add(e);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
Expression(out e);
letRHSs.Add(e);
}
- Expect(12);
+ Expect(14);
Expression(out e);
e = new LetExpr(x, letVars, letRHSs, e);
}
@@ -2699,7 +2711,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
Expression expr;
- Expect(51);
+ Expect(54);
x = t;
NoUSIdent(out d);
Expect(5);
@@ -2714,39 +2726,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(64);
+ Expect(67);
x = t;
Ident(out id);
- if (la.kind == 23) {
+ if (la.kind == 26) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(25);
+ Expect(28);
}
- Expect(65);
+ Expect(68);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 102) {
+ if (la.kind == 105) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 106) {
Get();
- } else SynErr(186);
+ } else SynErr(190);
}
void Exists() {
- if (la.kind == 104) {
+ if (la.kind == 107) {
Get();
- } else if (la.kind == 105) {
+ } else if (la.kind == 108) {
Get();
- } else SynErr(187);
+ } else SynErr(191);
}
void AttributeBody(ref Attributes attrs) {
@@ -2760,7 +2772,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(20)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
- while (la.kind == 21) {
+ while (la.kind == 24) {
Get();
AttributeArg(out aArg);
aArgs.Add(aArg);
@@ -2782,27 +2794,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,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,x,T,T, T,T,T,T, 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,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, T,x,x,x, T,x,x,x, x,x,x,x, T,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,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,x,x,x, x,x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, 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,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,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,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, 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,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,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,T,T, T,T,T,T, 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, T,T,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,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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,T,x,T, x,x,x,x, x,T,T,T, x,T,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,x,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, 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, 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,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,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, 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, T,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},
- {x,x,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,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,T,T,x, x,x,T,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, x,x,T,x, x,x,x,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,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, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,x,x, x,x,x,T, T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T, x,x,x,T, x,x,x,x, x,x,x,T, T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, T,T,x,T, x,x,x,x, x,x,T,T, T,T,x,T, x,T,T,x, x,T,x,T, T,x,x,x, x,T,T,T, 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,x,x,x, x,x,x,x, x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,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,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,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,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,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,T,T,T, T,T,T,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,T, T,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,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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,T,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,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,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,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,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,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,T, 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},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, T,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, T,T,x,x, x,T,x,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
};
} // end Parser
@@ -2838,183 +2850,187 @@ public class Errors { case 8: s = "\"ghost\" expected"; break;
case 9: s = "\"module\" expected"; break;
case 10: s = "\"refines\" expected"; break;
- case 11: s = "\"=\" expected"; break;
- case 12: s = "\";\" expected"; break;
- case 13: s = "\"as\" expected"; break;
- case 14: s = "\".\" expected"; break;
- case 15: s = "\"class\" expected"; break;
- case 16: s = "\"static\" expected"; break;
- case 17: s = "\"datatype\" expected"; break;
- case 18: s = "\"codatatype\" expected"; break;
- case 19: s = "\"|\" expected"; break;
- case 20: s = "\"var\" expected"; break;
- case 21: s = "\",\" expected"; break;
- case 22: s = "\"type\" expected"; break;
- case 23: s = "\"(\" expected"; break;
- case 24: s = "\"==\" expected"; break;
- case 25: s = "\")\" expected"; break;
- case 26: s = "\"<\" expected"; break;
- case 27: s = "\">\" expected"; break;
- case 28: s = "\"method\" expected"; break;
- case 29: s = "\"constructor\" expected"; break;
- case 30: s = "\"returns\" expected"; break;
- case 31: s = "\"...\" 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 = "\"decreases\" expected"; break;
- case 37: s = "\"bool\" expected"; break;
- case 38: s = "\"nat\" expected"; break;
- case 39: s = "\"int\" expected"; break;
- case 40: s = "\"set\" expected"; break;
- case 41: s = "\"multiset\" expected"; break;
- case 42: s = "\"seq\" expected"; break;
- case 43: s = "\"map\" expected"; break;
- case 44: s = "\"object\" expected"; break;
- case 45: s = "\"function\" expected"; break;
- case 46: s = "\"predicate\" expected"; break;
- case 47: s = "\"copredicate\" expected"; break;
- case 48: s = "\"reads\" expected"; break;
- case 49: s = "\"*\" expected"; break;
- case 50: s = "\"`\" expected"; break;
- case 51: s = "\"label\" expected"; break;
- case 52: s = "\"break\" expected"; break;
- case 53: s = "\"where\" expected"; break;
- case 54: s = "\":=\" expected"; break;
- case 55: s = "\"return\" expected"; break;
- case 56: s = "\":|\" expected"; break;
- case 57: s = "\"assume\" expected"; break;
- case 58: s = "\"new\" expected"; break;
- case 59: s = "\"[\" expected"; break;
- case 60: s = "\"]\" expected"; break;
- case 61: s = "\"choose\" expected"; break;
- case 62: s = "\"if\" expected"; break;
- case 63: s = "\"else\" expected"; break;
- case 64: s = "\"case\" expected"; break;
- case 65: s = "\"=>\" expected"; break;
- case 66: s = "\"while\" expected"; break;
- case 67: s = "\"invariant\" expected"; break;
- case 68: s = "\"match\" expected"; break;
- case 69: s = "\"assert\" expected"; break;
- case 70: s = "\"print\" expected"; break;
- case 71: s = "\"parallel\" expected"; break;
- case 72: s = "\"<==>\" expected"; break;
- case 73: s = "\"\\u21d4\" expected"; break;
- case 74: s = "\"==>\" expected"; break;
- case 75: s = "\"\\u21d2\" expected"; break;
- case 76: s = "\"&&\" expected"; break;
- case 77: s = "\"\\u2227\" expected"; break;
- case 78: s = "\"||\" expected"; break;
- case 79: s = "\"\\u2228\" expected"; break;
- case 80: s = "\"<=\" expected"; break;
- case 81: s = "\">=\" expected"; break;
- case 82: s = "\"!=\" expected"; break;
- case 83: s = "\"!!\" expected"; break;
- case 84: s = "\"in\" expected"; break;
- case 85: s = "\"!\" expected"; break;
- case 86: s = "\"\\u2260\" expected"; break;
- case 87: s = "\"\\u2264\" expected"; break;
- case 88: s = "\"\\u2265\" expected"; break;
- case 89: s = "\"+\" expected"; break;
- case 90: s = "\"-\" expected"; break;
- case 91: s = "\"/\" expected"; break;
- case 92: s = "\"%\" expected"; break;
- case 93: s = "\"\\u00ac\" expected"; break;
- case 94: s = "\"false\" expected"; break;
- case 95: s = "\"true\" expected"; break;
- case 96: s = "\"null\" expected"; break;
- case 97: s = "\"this\" expected"; break;
- case 98: s = "\"fresh\" expected"; break;
- case 99: s = "\"old\" expected"; break;
- case 100: s = "\"then\" expected"; break;
- case 101: s = "\"..\" expected"; break;
- case 102: s = "\"forall\" expected"; break;
- case 103: s = "\"\\u2200\" expected"; break;
- case 104: s = "\"exists\" expected"; break;
- case 105: s = "\"\\u2203\" expected"; break;
- case 106: s = "\"::\" expected"; break;
- case 107: s = "\"\\u2022\" expected"; break;
- case 108: s = "??? expected"; break;
- case 109: s = "invalid Dafny"; break;
- case 110: s = "invalid SubModuleDecl"; break;
- case 111: s = "invalid SubModuleDecl"; break;
- case 112: s = "this symbol not expected in ClassDecl"; break;
- case 113: s = "this symbol not expected in DatatypeDecl"; break;
- case 114: s = "invalid DatatypeDecl"; break;
- case 115: s = "this symbol not expected in DatatypeDecl"; break;
- case 116: s = "this symbol not expected in ArbitraryTypeDecl"; break;
- case 117: s = "invalid ClassMemberDecl"; break;
- case 118: s = "this symbol not expected in FieldDecl"; break;
- case 119: s = "this symbol not expected in FieldDecl"; break;
- case 120: s = "invalid FunctionDecl"; break;
- case 121: s = "invalid FunctionDecl"; break;
- case 122: s = "invalid FunctionDecl"; break;
- case 123: s = "invalid FunctionDecl"; break;
- case 124: s = "this symbol not expected in MethodDecl"; break;
- case 125: s = "invalid MethodDecl"; break;
- case 126: s = "invalid MethodDecl"; break;
- case 127: s = "invalid TypeAndToken"; break;
- case 128: s = "this symbol not expected in MethodSpec"; break;
- case 129: s = "this symbol not expected in MethodSpec"; break;
- case 130: s = "this symbol not expected in MethodSpec"; break;
- case 131: s = "this symbol not expected in MethodSpec"; break;
- case 132: s = "invalid MethodSpec"; break;
+ case 11: s = "\"import\" expected"; break;
+ case 12: s = "\"opened\" expected"; break;
+ case 13: s = "\"=\" expected"; break;
+ case 14: s = "\";\" expected"; break;
+ case 15: s = "\"as\" expected"; break;
+ case 16: s = "\"default\" expected"; break;
+ case 17: s = "\".\" expected"; break;
+ case 18: s = "\"class\" expected"; break;
+ case 19: s = "\"static\" expected"; break;
+ case 20: s = "\"datatype\" expected"; break;
+ case 21: s = "\"codatatype\" expected"; break;
+ case 22: s = "\"|\" expected"; break;
+ case 23: s = "\"var\" expected"; break;
+ case 24: s = "\",\" expected"; break;
+ case 25: s = "\"type\" expected"; break;
+ case 26: s = "\"(\" expected"; break;
+ case 27: s = "\"==\" expected"; break;
+ case 28: s = "\")\" expected"; break;
+ case 29: s = "\"<\" expected"; break;
+ case 30: s = "\">\" expected"; break;
+ case 31: s = "\"method\" expected"; break;
+ case 32: s = "\"constructor\" expected"; break;
+ case 33: s = "\"returns\" expected"; break;
+ case 34: s = "\"...\" expected"; break;
+ case 35: s = "\"modifies\" expected"; break;
+ case 36: s = "\"free\" expected"; break;
+ case 37: s = "\"requires\" expected"; break;
+ case 38: s = "\"ensures\" expected"; break;
+ case 39: s = "\"decreases\" expected"; break;
+ case 40: s = "\"bool\" expected"; break;
+ case 41: s = "\"nat\" expected"; break;
+ case 42: s = "\"int\" expected"; break;
+ case 43: s = "\"set\" expected"; break;
+ case 44: s = "\"multiset\" expected"; break;
+ case 45: s = "\"seq\" expected"; break;
+ case 46: s = "\"map\" expected"; break;
+ case 47: s = "\"object\" expected"; break;
+ case 48: s = "\"function\" expected"; break;
+ case 49: s = "\"predicate\" expected"; break;
+ case 50: s = "\"copredicate\" expected"; break;
+ case 51: s = "\"reads\" expected"; break;
+ case 52: s = "\"*\" expected"; break;
+ case 53: s = "\"`\" expected"; break;
+ case 54: s = "\"label\" expected"; break;
+ case 55: s = "\"break\" expected"; break;
+ case 56: s = "\"where\" expected"; break;
+ case 57: s = "\":=\" expected"; break;
+ case 58: s = "\"return\" expected"; break;
+ case 59: s = "\":|\" expected"; break;
+ case 60: s = "\"assume\" expected"; break;
+ case 61: s = "\"new\" expected"; break;
+ case 62: s = "\"[\" expected"; break;
+ case 63: s = "\"]\" expected"; break;
+ case 64: s = "\"choose\" expected"; break;
+ case 65: s = "\"if\" expected"; break;
+ case 66: s = "\"else\" expected"; break;
+ case 67: s = "\"case\" expected"; break;
+ case 68: s = "\"=>\" expected"; break;
+ case 69: s = "\"while\" expected"; break;
+ case 70: s = "\"invariant\" expected"; break;
+ case 71: s = "\"match\" expected"; break;
+ case 72: s = "\"assert\" expected"; break;
+ case 73: s = "\"print\" expected"; break;
+ case 74: s = "\"parallel\" expected"; break;
+ case 75: s = "\"<==>\" expected"; break;
+ case 76: s = "\"\\u21d4\" expected"; break;
+ case 77: s = "\"==>\" expected"; break;
+ case 78: s = "\"\\u21d2\" expected"; break;
+ case 79: s = "\"&&\" expected"; break;
+ case 80: s = "\"\\u2227\" expected"; break;
+ case 81: s = "\"||\" expected"; break;
+ case 82: s = "\"\\u2228\" expected"; break;
+ case 83: s = "\"<=\" expected"; break;
+ case 84: s = "\">=\" expected"; break;
+ case 85: s = "\"!=\" expected"; break;
+ case 86: s = "\"!!\" expected"; break;
+ case 87: s = "\"in\" expected"; break;
+ case 88: s = "\"!\" expected"; break;
+ case 89: s = "\"\\u2260\" expected"; break;
+ case 90: s = "\"\\u2264\" expected"; break;
+ case 91: s = "\"\\u2265\" expected"; break;
+ case 92: s = "\"+\" expected"; break;
+ case 93: s = "\"-\" expected"; break;
+ case 94: s = "\"/\" expected"; break;
+ case 95: s = "\"%\" expected"; break;
+ case 96: s = "\"\\u00ac\" expected"; break;
+ case 97: s = "\"false\" expected"; break;
+ case 98: s = "\"true\" expected"; break;
+ case 99: s = "\"null\" expected"; break;
+ case 100: s = "\"this\" expected"; break;
+ case 101: s = "\"fresh\" expected"; break;
+ case 102: s = "\"old\" expected"; break;
+ case 103: s = "\"then\" expected"; break;
+ case 104: s = "\"..\" expected"; break;
+ case 105: s = "\"forall\" expected"; break;
+ case 106: s = "\"\\u2200\" expected"; break;
+ case 107: s = "\"exists\" expected"; break;
+ case 108: s = "\"\\u2203\" expected"; break;
+ case 109: s = "\"::\" expected"; break;
+ case 110: s = "\"\\u2022\" expected"; break;
+ case 111: s = "??? expected"; break;
+ case 112: s = "invalid Dafny"; break;
+ case 113: s = "invalid SubModuleDecl"; break;
+ case 114: s = "invalid SubModuleDecl"; break;
+ case 115: s = "invalid SubModuleDecl"; break;
+ case 116: s = "this symbol not expected in ClassDecl"; break;
+ case 117: s = "this symbol not expected in DatatypeDecl"; break;
+ case 118: s = "invalid DatatypeDecl"; break;
+ case 119: s = "this symbol not expected in DatatypeDecl"; break;
+ case 120: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 121: s = "invalid ClassMemberDecl"; break;
+ case 122: s = "this symbol not expected in FieldDecl"; break;
+ case 123: s = "this symbol not expected in FieldDecl"; break;
+ case 124: s = "invalid FunctionDecl"; break;
+ case 125: s = "invalid FunctionDecl"; break;
+ case 126: s = "invalid FunctionDecl"; break;
+ case 127: s = "invalid FunctionDecl"; break;
+ case 128: s = "this symbol not expected in MethodDecl"; break;
+ case 129: s = "invalid MethodDecl"; break;
+ case 130: s = "invalid MethodDecl"; break;
+ case 131: s = "invalid TypeAndToken"; break;
+ case 132: s = "this symbol not expected in MethodSpec"; break;
case 133: s = "this symbol not expected in MethodSpec"; break;
- case 134: s = "invalid MethodSpec"; break;
- case 135: s = "invalid FrameExpression"; break;
- case 136: s = "invalid ReferenceType"; break;
- case 137: s = "this symbol not expected in FunctionSpec"; break;
- case 138: s = "this symbol not expected in FunctionSpec"; break;
- case 139: s = "this symbol not expected in FunctionSpec"; break;
- case 140: s = "this symbol not expected in FunctionSpec"; break;
+ case 134: s = "this symbol not expected in MethodSpec"; break;
+ case 135: s = "this symbol not expected in MethodSpec"; break;
+ case 136: s = "invalid MethodSpec"; break;
+ case 137: s = "this symbol not expected in MethodSpec"; break;
+ case 138: s = "invalid MethodSpec"; break;
+ case 139: s = "invalid FrameExpression"; break;
+ case 140: s = "invalid ReferenceType"; break;
case 141: s = "this symbol not expected in FunctionSpec"; break;
- case 142: s = "invalid FunctionSpec"; break;
- case 143: s = "invalid PossiblyWildFrameExpression"; break;
- case 144: s = "invalid PossiblyWildExpression"; break;
- case 145: s = "this symbol not expected in OneStmt"; break;
- case 146: s = "invalid OneStmt"; break;
- case 147: s = "this symbol not expected in OneStmt"; break;
- case 148: s = "invalid OneStmt"; break;
- case 149: s = "invalid AssertStmt"; break;
- case 150: s = "invalid AssumeStmt"; break;
- case 151: s = "invalid UpdateStmt"; break;
- case 152: s = "invalid UpdateStmt"; break;
- case 153: s = "invalid IfStmt"; break;
- case 154: s = "invalid IfStmt"; break;
- case 155: s = "invalid WhileStmt"; break;
- case 156: s = "invalid WhileStmt"; break;
- case 157: s = "invalid Rhs"; break;
- case 158: s = "invalid Lhs"; break;
- case 159: s = "invalid Guard"; break;
- case 160: s = "this symbol not expected in LoopSpec"; break;
- case 161: s = "this symbol not expected in LoopSpec"; break;
- case 162: s = "this symbol not expected in LoopSpec"; break;
- case 163: s = "this symbol not expected in LoopSpec"; break;
+ case 142: s = "this symbol not expected in FunctionSpec"; break;
+ case 143: s = "this symbol not expected in FunctionSpec"; break;
+ case 144: s = "this symbol not expected in FunctionSpec"; break;
+ case 145: s = "this symbol not expected in FunctionSpec"; break;
+ case 146: s = "invalid FunctionSpec"; break;
+ case 147: s = "invalid PossiblyWildFrameExpression"; break;
+ case 148: s = "invalid PossiblyWildExpression"; break;
+ case 149: s = "this symbol not expected in OneStmt"; break;
+ case 150: s = "invalid OneStmt"; break;
+ case 151: s = "this symbol not expected in OneStmt"; break;
+ case 152: s = "invalid OneStmt"; break;
+ case 153: s = "invalid AssertStmt"; break;
+ case 154: s = "invalid AssumeStmt"; break;
+ case 155: s = "invalid UpdateStmt"; break;
+ case 156: s = "invalid UpdateStmt"; break;
+ case 157: s = "invalid IfStmt"; break;
+ case 158: s = "invalid IfStmt"; break;
+ case 159: s = "invalid WhileStmt"; break;
+ case 160: s = "invalid WhileStmt"; break;
+ case 161: s = "invalid Rhs"; break;
+ case 162: s = "invalid Lhs"; break;
+ case 163: s = "invalid Guard"; break;
case 164: s = "this symbol not expected in LoopSpec"; break;
- case 165: s = "this symbol not expected in Invariant"; break;
- case 166: s = "invalid AttributeArg"; break;
- case 167: s = "invalid EquivOp"; break;
- case 168: s = "invalid ImpliesOp"; break;
- case 169: s = "invalid AndOp"; break;
- case 170: s = "invalid OrOp"; break;
- case 171: s = "invalid RelOp"; break;
- case 172: s = "invalid AddOp"; break;
- case 173: s = "invalid UnaryExpression"; break;
- case 174: s = "invalid MulOp"; break;
- case 175: s = "invalid NegOp"; break;
- case 176: s = "invalid EndlessExpression"; break;
- case 177: s = "invalid Suffix"; break;
- case 178: s = "invalid Suffix"; break;
- case 179: s = "invalid Suffix"; break;
- case 180: s = "invalid DisplayExpr"; break;
- case 181: s = "invalid MultiSetExpr"; break;
- case 182: s = "invalid MapExpr"; break;
- case 183: s = "invalid ConstAtomExpression"; break;
- case 184: s = "invalid QSep"; break;
- case 185: s = "invalid QuantifierGuts"; break;
- case 186: s = "invalid Forall"; break;
- case 187: s = "invalid Exists"; break;
+ case 165: s = "this symbol not expected in LoopSpec"; break;
+ case 166: s = "this symbol not expected in LoopSpec"; break;
+ case 167: s = "this symbol not expected in LoopSpec"; break;
+ case 168: s = "this symbol not expected in LoopSpec"; break;
+ case 169: s = "this symbol not expected in Invariant"; break;
+ case 170: s = "invalid AttributeArg"; break;
+ case 171: s = "invalid EquivOp"; break;
+ case 172: s = "invalid ImpliesOp"; break;
+ case 173: s = "invalid AndOp"; break;
+ case 174: s = "invalid OrOp"; break;
+ case 175: s = "invalid RelOp"; break;
+ case 176: s = "invalid AddOp"; break;
+ case 177: s = "invalid UnaryExpression"; break;
+ case 178: s = "invalid MulOp"; break;
+ case 179: s = "invalid NegOp"; break;
+ case 180: s = "invalid EndlessExpression"; break;
+ case 181: s = "invalid Suffix"; break;
+ case 182: s = "invalid Suffix"; break;
+ case 183: s = "invalid Suffix"; break;
+ case 184: s = "invalid DisplayExpr"; break;
+ case 185: s = "invalid MultiSetExpr"; break;
+ case 186: s = "invalid MapExpr"; break;
+ case 187: s = "invalid ConstAtomExpression"; break;
+ case 188: s = "invalid QSep"; break;
+ case 189: s = "invalid QuantifierGuts"; break;
+ case 190: s = "invalid Forall"; break;
+ case 191: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs index 6f5e1135..a6123fbb 100644 --- a/Dafny/Scanner.cs +++ b/Dafny/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 108;
- const int noSym = 108;
+ const int maxT = 111;
+ const int noSym = 111;
[ContractInvariantMethod]
@@ -491,59 +491,62 @@ public class Scanner { case "ghost": t.kind = 8; break;
case "module": t.kind = 9; break;
case "refines": t.kind = 10; break;
- case "as": t.kind = 13; break;
- case "class": t.kind = 15; break;
- case "static": t.kind = 16; break;
- case "datatype": t.kind = 17; break;
- case "codatatype": t.kind = 18; break;
- case "var": t.kind = 20; break;
- case "type": t.kind = 22; break;
- case "method": t.kind = 28; break;
- case "constructor": t.kind = 29; break;
- case "returns": t.kind = 30; break;
- case "modifies": t.kind = 32; break;
- case "free": t.kind = 33; break;
- case "requires": t.kind = 34; break;
- case "ensures": t.kind = 35; break;
- case "decreases": t.kind = 36; break;
- case "bool": t.kind = 37; break;
- case "nat": t.kind = 38; break;
- case "int": t.kind = 39; break;
- case "set": t.kind = 40; break;
- case "multiset": t.kind = 41; break;
- case "seq": t.kind = 42; break;
- case "map": t.kind = 43; break;
- case "object": t.kind = 44; break;
- case "function": t.kind = 45; break;
- case "predicate": t.kind = 46; break;
- case "copredicate": t.kind = 47; break;
- case "reads": t.kind = 48; break;
- case "label": t.kind = 51; break;
- case "break": t.kind = 52; break;
- case "where": t.kind = 53; break;
- case "return": t.kind = 55; break;
- case "assume": t.kind = 57; break;
- case "new": t.kind = 58; break;
- case "choose": t.kind = 61; break;
- case "if": t.kind = 62; break;
- case "else": t.kind = 63; break;
- case "case": t.kind = 64; break;
- case "while": t.kind = 66; break;
- case "invariant": t.kind = 67; break;
- case "match": t.kind = 68; break;
- case "assert": t.kind = 69; break;
- case "print": t.kind = 70; break;
- case "parallel": t.kind = 71; break;
- case "in": t.kind = 84; break;
- case "false": t.kind = 94; break;
- case "true": t.kind = 95; break;
- case "null": t.kind = 96; break;
- case "this": t.kind = 97; break;
- case "fresh": t.kind = 98; break;
- case "old": t.kind = 99; break;
- case "then": t.kind = 100; break;
- case "forall": t.kind = 102; break;
- case "exists": t.kind = 104; break;
+ case "import": t.kind = 11; break;
+ case "opened": t.kind = 12; break;
+ case "as": t.kind = 15; break;
+ case "default": t.kind = 16; break;
+ case "class": t.kind = 18; break;
+ case "static": t.kind = 19; break;
+ case "datatype": t.kind = 20; break;
+ case "codatatype": t.kind = 21; break;
+ case "var": t.kind = 23; break;
+ case "type": t.kind = 25; break;
+ case "method": t.kind = 31; break;
+ case "constructor": t.kind = 32; break;
+ case "returns": t.kind = 33; break;
+ case "modifies": t.kind = 35; break;
+ case "free": t.kind = 36; break;
+ case "requires": t.kind = 37; break;
+ case "ensures": t.kind = 38; break;
+ case "decreases": t.kind = 39; break;
+ case "bool": t.kind = 40; break;
+ case "nat": t.kind = 41; break;
+ case "int": t.kind = 42; break;
+ case "set": t.kind = 43; break;
+ case "multiset": t.kind = 44; break;
+ case "seq": t.kind = 45; break;
+ case "map": t.kind = 46; break;
+ case "object": t.kind = 47; break;
+ case "function": t.kind = 48; break;
+ case "predicate": t.kind = 49; break;
+ case "copredicate": t.kind = 50; break;
+ case "reads": t.kind = 51; break;
+ case "label": t.kind = 54; break;
+ case "break": t.kind = 55; break;
+ case "where": t.kind = 56; break;
+ case "return": t.kind = 58; break;
+ case "assume": t.kind = 60; break;
+ case "new": t.kind = 61; break;
+ case "choose": t.kind = 64; break;
+ case "if": t.kind = 65; break;
+ case "else": t.kind = 66; break;
+ case "case": t.kind = 67; break;
+ case "while": t.kind = 69; break;
+ case "invariant": t.kind = 70; break;
+ case "match": t.kind = 71; break;
+ case "assert": t.kind = 72; break;
+ case "print": t.kind = 73; break;
+ case "parallel": t.kind = 74; break;
+ case "in": t.kind = 87; break;
+ case "false": t.kind = 97; break;
+ case "true": t.kind = 98; break;
+ case "null": t.kind = 99; break;
+ case "this": t.kind = 100; break;
+ case "fresh": t.kind = 101; break;
+ case "old": t.kind = 102; break;
+ case "then": t.kind = 103; break;
+ case "forall": t.kind = 105; break;
+ case "exists": t.kind = 107; break;
default: break;
}
}
@@ -649,81 +652,81 @@ public class Scanner { else if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
else {t.kind = 3; break;}
case 19:
- {t.kind = 12; break;}
+ {t.kind = 14; break;}
case 20:
- {t.kind = 21; break;}
+ {t.kind = 24; break;}
case 21:
- {t.kind = 23; break;}
+ {t.kind = 26; break;}
case 22:
- {t.kind = 25; break;}
+ {t.kind = 28; break;}
case 23:
- {t.kind = 31; break;}
+ {t.kind = 34; break;}
case 24:
- {t.kind = 49; break;}
+ {t.kind = 52; break;}
case 25:
- {t.kind = 50; break;}
+ {t.kind = 53; break;}
case 26:
- {t.kind = 54; break;}
+ {t.kind = 57; break;}
case 27:
- {t.kind = 56; break;}
- case 28:
{t.kind = 59; break;}
+ case 28:
+ {t.kind = 62; break;}
case 29:
- {t.kind = 60; break;}
+ {t.kind = 63; break;}
case 30:
- {t.kind = 65; break;}
+ {t.kind = 68; break;}
case 31:
if (ch == '>') {AddCh(); goto case 32;}
else {goto case 0;}
case 32:
- {t.kind = 72; break;}
+ {t.kind = 75; break;}
case 33:
- {t.kind = 73; break;}
+ {t.kind = 76; break;}
case 34:
- {t.kind = 74; break;}
+ {t.kind = 77; break;}
case 35:
- {t.kind = 75; break;}
+ {t.kind = 78; break;}
case 36:
if (ch == '&') {AddCh(); goto case 37;}
else {goto case 0;}
case 37:
- {t.kind = 76; break;}
+ {t.kind = 79; break;}
case 38:
- {t.kind = 77; break;}
+ {t.kind = 80; break;}
case 39:
- {t.kind = 78; break;}
+ {t.kind = 81; break;}
case 40:
- {t.kind = 79; break;}
+ {t.kind = 82; break;}
case 41:
- {t.kind = 81; break;}
+ {t.kind = 84; break;}
case 42:
- {t.kind = 82; break;}
+ {t.kind = 85; break;}
case 43:
- {t.kind = 83; break;}
- case 44:
{t.kind = 86; break;}
+ case 44:
+ {t.kind = 89; break;}
case 45:
- {t.kind = 87; break;}
+ {t.kind = 90; break;}
case 46:
- {t.kind = 88; break;}
+ {t.kind = 91; break;}
case 47:
- {t.kind = 89; break;}
+ {t.kind = 92; break;}
case 48:
- {t.kind = 90; break;}
+ {t.kind = 93; break;}
case 49:
- {t.kind = 91; break;}
+ {t.kind = 94; break;}
case 50:
- {t.kind = 92; break;}
+ {t.kind = 95; break;}
case 51:
- {t.kind = 93; break;}
+ {t.kind = 96; break;}
case 52:
- {t.kind = 103; break;}
+ {t.kind = 106; break;}
case 53:
- {t.kind = 105; break;}
+ {t.kind = 108; break;}
case 54:
- {t.kind = 106; break;}
+ {t.kind = 109; break;}
case 55:
- {t.kind = 107; break;}
+ {t.kind = 110; break;}
case 56:
recEnd = pos; recKind = 5;
if (ch == '=') {AddCh(); goto case 26;}
@@ -731,43 +734,43 @@ public class Scanner { else if (ch == ':') {AddCh(); goto case 54;}
else {t.kind = 5; break;}
case 57:
- recEnd = pos; recKind = 11;
+ recEnd = pos; recKind = 13;
if (ch == '=') {AddCh(); goto case 63;}
else if (ch == '>') {AddCh(); goto case 30;}
- else {t.kind = 11; break;}
+ else {t.kind = 13; break;}
case 58:
- recEnd = pos; recKind = 14;
+ recEnd = pos; recKind = 17;
if (ch == '.') {AddCh(); goto case 64;}
- else {t.kind = 14; break;}
+ else {t.kind = 17; break;}
case 59:
- recEnd = pos; recKind = 19;
+ recEnd = pos; recKind = 22;
if (ch == '|') {AddCh(); goto case 39;}
- else {t.kind = 19; break;}
+ else {t.kind = 22; break;}
case 60:
- recEnd = pos; recKind = 26;
+ recEnd = pos; recKind = 29;
if (ch == '=') {AddCh(); goto case 65;}
- else {t.kind = 26; break;}
+ else {t.kind = 29; break;}
case 61:
- recEnd = pos; recKind = 27;
+ recEnd = pos; recKind = 30;
if (ch == '=') {AddCh(); goto case 41;}
- else {t.kind = 27; break;}
+ else {t.kind = 30; break;}
case 62:
- recEnd = pos; recKind = 85;
+ recEnd = pos; recKind = 88;
if (ch == '=') {AddCh(); goto case 42;}
else if (ch == '!') {AddCh(); goto case 43;}
- else {t.kind = 85; break;}
+ else {t.kind = 88; break;}
case 63:
- recEnd = pos; recKind = 24;
+ recEnd = pos; recKind = 27;
if (ch == '>') {AddCh(); goto case 34;}
- else {t.kind = 24; break;}
+ else {t.kind = 27; break;}
case 64:
- recEnd = pos; recKind = 101;
+ recEnd = pos; recKind = 104;
if (ch == '.') {AddCh(); goto case 23;}
- else {t.kind = 101; break;}
+ else {t.kind = 104; break;}
case 65:
- recEnd = pos; recKind = 80;
+ recEnd = pos; recKind = 83;
if (ch == '=') {AddCh(); goto case 31;}
- else {t.kind = 80; break;}
+ else {t.kind = 83; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index e4a8c5d0..0b64a775 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -32,13 +32,13 @@ `(,(dafny-regexp-opt '(
"class" "datatype" "codatatype" "type" "function" "predicate" "copredicate"
"ghost" "var" "method" "constructor"
- "module" "imports" "static" "refines"
+ "module" "import" "default" "as" "opened" "static" "refines"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
"assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print" "where"
- "old" "forall" "exists" "new" "parallel" "in" "this" "fresh" "allocated"
+ "old" "forall" "exists" "new" "parallel" "in" "this" "fresh"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
)
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 4d8e2df1..7a124b74 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -19,7 +19,7 @@ namespace Demo this.MarkReservedWords( // NOTE: these keywords must also appear once more below
"class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",
"assert", "assume", "new", "this", "object", "refines",
- "module", "imports", "as",
+ "module", "import", "as", "default", "opened",
"if", "then", "else", "while", "invariant",
"break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
@@ -28,7 +28,7 @@ namespace Demo "in", "forall", "exists",
"seq", "set", "map", "multiset", "array", "array2", "array3",
"match", "case",
- "fresh", "allocated", "old", "choose", "where"
+ "fresh", "old", "choose", "where"
);
StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);
@@ -276,7 +276,9 @@ namespace Demo | "object"
| "refines"
| "module"
- | "imports"
+ | "import"
+ | "default"
+ | "opened"
| "as"
| "if"
| "then"
@@ -318,7 +320,6 @@ namespace Demo | "match"
| "case"
| "fresh"
- | "allocated"
| "old"
| "choose"
| "where"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 74bfa65a..9ce6c3e1 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -8,10 +8,10 @@ morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,map%
function,predicate,copredicate,
ghost,var,static,refines,
- method,constructor,returns,module,imports,in,
+ method,constructor,returns,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
- match,case,false,true,null,old,fresh,allocated,choose,this,
+ match,case,false,true,null,old,fresh,choose,this,
% statements
assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,parallel,where
},
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 37ec7be0..6023830c 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -6,14 +6,14 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate method constructor -syntax keyword dafnyTypeDef class datatype codatatype type +syntax keyword dafnyTypeDef class datatype codatatype type module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel syntax keyword dafnyStatement havoc assume assert return new print break label where syntax keyword dafnyKeyword var ghost returns null static this refines syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant -syntax keyword dafnyOperator forall exists old fresh allocated choose +syntax keyword dafnyOperator forall exists old fresh choose syntax keyword dafnyBoolean true false syntax region dafnyString start=/"/ skip=/\\"/ end=/"/ |