diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 2 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 3 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 9 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 26 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 1019 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 3 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 112 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 171 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 543 | ||||
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 1 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 44 | ||||
| -rw-r--r-- | Test/dafny0/CoinductiveProofs.dfy | 152 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 6 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 3 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 3 |
17 files changed, 1270 insertions, 832 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 342b72c1..c23e8a7e 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -471,6 +471,8 @@ function DatatypeCtorId(DatatypeType): DtCtorId; function DtRank(DatatypeType): int;
+function CoDatatypeCertificate#Equal(DatatypeType, DatatypeType): bool;
+
// ---------------------------------------------------------------
// -- Axiom contexts ---------------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 340683f6..8fc0db0a 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -527,6 +527,9 @@ namespace Microsoft.Dafny if (m is Constructor) {
return new Constructor(Tok(m.tok), m.Name, tps, ins,
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), false);
+ } else if (m is CoMethod) {
+ return new CoMethod(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ req, mod, ens, decreases, body, CloneAttributes(m.Attributes), false);
} else {
return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), false);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index fa8cd9b2..774d800a 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -480,12 +480,14 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> Attributes modAttrs = null;
BlockStmt body = null;
bool isConstructor = false;
+ bool isCoMethod = false;
bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
SYNC
( "method"
+ | "comethod" (. isCoMethod = true; .)
| "constructor" (. if (allowConstructor) {
isConstructor = true;
} else {
@@ -500,6 +502,10 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> if (mmod.IsStatic) {
SemErr(t, "constructors cannot be declared 'static'");
}
+ } else if (isCoMethod) {
+ if (mmod.IsGhost) {
+ SemErr(t, "comethods cannot be declared 'ghost'");
+ }
}
.)
{ Attribute<ref attrs> }
@@ -526,6 +532,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> (. if (isConstructor) {
m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
+ } else if (isCoMethod) {
+ m = new CoMethod(id, id.val, mmod.IsStatic, typeArgs, ins, outs,
+ req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
} else {
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 3550ddb2..cec40977 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1126,7 +1126,7 @@ namespace Microsoft.Dafny { // TODO: One could imagine having a precondition on datatype constructors
public DatatypeDecl EnclosingDatatype; // filled in during resolution
public SpecialField QueryField; // filled in during resolution
- public List<SpecialField/*may be null*/> Destructors = new List<SpecialField/*may be null*/>(); // contents filled in during resolution
+ public List<SpecialField> Destructors = new List<SpecialField>(); // contents filled in during resolution; includes both implicit (not mentionable in source) and explicit destructors
public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Formal/*!*/>/*!*/ formals, Attributes attributes)
: base(tok, name, attributes) {
@@ -1794,6 +1794,30 @@ namespace Microsoft.Dafny { }
}
+ public class CoMethod : Method
+ {
+ public CoMethod(IToken tok, string name,
+ bool isStatic,
+ List<TypeParameter/*!*/>/*!*/ typeArgs,
+ List<Formal/*!*/>/*!*/ ins, [Captured] List<Formal/*!*/>/*!*/ outs,
+ List<MaybeFreeExpression/*!*/>/*!*/ req, [Captured] Specification<FrameExpression>/*!*/ mod,
+ List<MaybeFreeExpression/*!*/>/*!*/ ens,
+ Specification<Expression>/*!*/ decreases,
+ BlockStmt body,
+ Attributes attributes, bool signatureOmitted)
+ : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureOmitted) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(ins));
+ Contract.Requires(cce.NonNullElements(outs));
+ Contract.Requires(cce.NonNullElements(req));
+ Contract.Requires(mod != null);
+ Contract.Requires(cce.NonNullElements(ens));
+ Contract.Requires(decreases != null);
+ }
+ }
+
// ------------------------------------------------------------------------------------------------------
public abstract class Statement {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 1217ae48..8982750d 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/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 = 115;
+ public const int maxT = 116;
const bool T = true;
const bool x = false;
@@ -234,11 +234,11 @@ bool IsAttribute() { defaultModule.TopLevelDecls.Add(iter);
break;
}
- case 8: case 19: case 23: case 34: case 35: case 52: case 53: case 54: {
+ case 8: case 19: case 23: case 34: case 35: case 36: case 53: case 54: case 55: {
ClassMemberDecl(membersDefaultClass, isGhost, false);
break;
}
- default: SynErr(116); break;
+ default: SynErr(117); break;
}
}
DefaultClassDecl defaultClass = null;
@@ -316,11 +316,11 @@ bool IsAttribute() { module.TopLevelDecls.Add(iter);
break;
}
- case 8: case 19: case 23: case 34: case 35: case 52: case 53: case 54: {
+ case 8: case 19: case 23: case 34: case 35: case 36: case 53: case 54: case 55: {
ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);
break;
}
- default: SynErr(117); break;
+ default: SynErr(118); break;
}
}
Expect(7);
@@ -351,8 +351,8 @@ bool IsAttribute() { }
Expect(14);
submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened);
- } else SynErr(118);
- } else SynErr(119);
+ } else SynErr(119);
+ } else SynErr(120);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -364,7 +364,7 @@ bool IsAttribute() { List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(120); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(121); Get();}
Expect(18);
while (la.kind == 6) {
Attribute(ref attrs);
@@ -395,13 +395,13 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(121); Get();}
+ while (!(la.kind == 0 || la.kind == 20 || la.kind == 21)) {SynErr(122); Get();}
if (la.kind == 20) {
Get();
} else if (la.kind == 21) {
Get();
co = true;
- } else SynErr(122);
+ } else SynErr(123);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -416,7 +416,7 @@ bool IsAttribute() { Get();
DatatypeMemberDecl(ctors);
}
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(124); Get();}
Expect(14);
if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
@@ -445,7 +445,7 @@ bool IsAttribute() { eqSupport = TypeParameter.EqualitySupportValue.Required;
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(124); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(125); Get();}
Expect(14);
}
@@ -473,7 +473,7 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 29)) {SynErr(125); Get();}
+ while (!(la.kind == 0 || la.kind == 29)) {SynErr(126); Get();}
Expect(29);
while (la.kind == 6) {
Attribute(ref attrs);
@@ -491,7 +491,7 @@ bool IsAttribute() { } else if (la.kind == 31) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
- } else SynErr(126);
+ } else SynErr(127);
while (StartOf(3)) {
IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
}
@@ -527,13 +527,13 @@ bool IsAttribute() { }
if (la.kind == 23) {
FieldDecl(mmod, mm);
- } else if (la.kind == 52 || la.kind == 53 || la.kind == 54) {
+ } else if (la.kind == 53 || la.kind == 54 || la.kind == 55) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (la.kind == 34 || la.kind == 35) {
+ } else if (la.kind == 34 || la.kind == 35 || la.kind == 36) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(127);
+ } else SynErr(128);
}
void Attribute(ref Attributes attrs) {
@@ -604,7 +604,7 @@ bool IsAttribute() { Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 23)) {SynErr(128); Get();}
+ while (!(la.kind == 0 || la.kind == 23)) {SynErr(129); Get();}
Expect(23);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -618,7 +618,7 @@ bool IsAttribute() { IdentType(out id, out ty, false);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(129); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(130); Get();}
Expect(14);
}
@@ -641,7 +641,7 @@ bool IsAttribute() { IToken bodyEnd = Token.NoToken;
bool signatureOmitted = false;
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
if (la.kind == 34) {
Get();
@@ -664,8 +664,8 @@ bool IsAttribute() { Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(130);
- } else if (la.kind == 53) {
+ } else SynErr(131);
+ } else if (la.kind == 54) {
Get();
isPredicate = true;
if (la.kind == 34) {
@@ -693,8 +693,8 @@ bool IsAttribute() { Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(131);
- } else if (la.kind == 54) {
+ } else SynErr(132);
+ } else if (la.kind == 55) {
Get();
isCoPredicate = true;
if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
@@ -718,8 +718,8 @@ bool IsAttribute() { Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(132);
- } else SynErr(133);
+ } else SynErr(133);
+ } else SynErr(134);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(5)) {
FunctionSpec(reqs, reads, ens, decreases);
@@ -759,22 +759,26 @@ bool IsAttribute() { Attributes modAttrs = null;
BlockStmt body = null;
bool isConstructor = false;
+ bool isCoMethod = false;
bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 34 || la.kind == 35)) {SynErr(134); Get();}
+ while (!(StartOf(6))) {SynErr(135); Get();}
if (la.kind == 34) {
Get();
} else if (la.kind == 35) {
Get();
+ isCoMethod = true;
+ } else if (la.kind == 36) {
+ Get();
if (allowConstructor) {
isConstructor = true;
} else {
SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(135);
+ } else SynErr(136);
keywordToken = t;
if (isConstructor) {
if (mmod.IsGhost) {
@@ -783,6 +787,10 @@ bool IsAttribute() { if (mmod.IsStatic) {
SemErr(t, "constructors cannot be declared 'static'");
}
+ } else if (isCoMethod) {
+ if (mmod.IsGhost) {
+ SemErr(t, "comethods cannot be declared 'ghost'");
+ }
}
while (la.kind == 6) {
@@ -804,7 +812,7 @@ bool IsAttribute() { GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins, out openParen);
- if (la.kind == 36) {
+ if (la.kind == 37) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs, out openParen);
@@ -812,8 +820,8 @@ bool IsAttribute() { } else if (la.kind == 31) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
- } else SynErr(136);
- while (StartOf(6)) {
+ } else SynErr(137);
+ while (StartOf(7)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
if (la.kind == 6) {
@@ -822,6 +830,9 @@ bool IsAttribute() { if (isConstructor) {
m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
+ } else if (isCoMethod) {
+ m = new CoMethod(id, id.val, mmod.IsStatic, typeArgs, ins, outs,
+ req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
} else {
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
@@ -850,7 +861,7 @@ bool IsAttribute() { void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
Expect(26);
- if (StartOf(7)) {
+ if (StartOf(8)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
while (la.kind == 24) {
@@ -957,22 +968,22 @@ bool IsAttribute() { List<Type/*!*/>/*!*/ gt;
switch (la.kind) {
- case 44: {
+ case 45: {
Get();
tok = t;
break;
}
- case 45: {
+ case 46: {
Get();
tok = t; ty = new NatType();
break;
}
- case 46: {
+ case 47: {
Get();
tok = t; ty = new IntType();
break;
}
- case 47: {
+ case 48: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -983,7 +994,7 @@ bool IsAttribute() { break;
}
- case 48: {
+ case 49: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -994,7 +1005,7 @@ bool IsAttribute() { break;
}
- case 49: {
+ case 50: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -1005,7 +1016,7 @@ bool IsAttribute() { break;
}
- case 50: {
+ case 51: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -1016,11 +1027,11 @@ bool IsAttribute() { break;
}
- case 1: case 3: case 51: {
+ case 1: case 3: case 52: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(137); break;
+ default: SynErr(138); break;
}
}
@@ -1046,13 +1057,13 @@ List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!* ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
- while (!(StartOf(8))) {SynErr(138); Get();}
- if (la.kind == 42) {
+ while (!(StartOf(9))) {SynErr(139); Get();}
+ if (la.kind == 43) {
Get();
while (IsAttribute()) {
Attribute(ref readsAttrs);
}
- if (StartOf(9)) {
+ if (StartOf(10)) {
FrameExpression(out fe);
reads.Add(fe);
while (la.kind == 24) {
@@ -1061,14 +1072,14 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(139); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(140); Get();}
Expect(14);
- } else if (la.kind == 37) {
+ } else if (la.kind == 38) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
}
- if (StartOf(9)) {
+ if (StartOf(10)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 24) {
@@ -1077,21 +1088,21 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(140); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(141); Get();}
Expect(14);
- } else if (StartOf(10)) {
- if (la.kind == 38) {
+ } else if (StartOf(11)) {
+ if (la.kind == 39) {
Get();
isFree = true;
}
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
isYield = true;
}
- if (la.kind == 39) {
+ if (la.kind == 40) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(141); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();}
Expect(14);
if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
@@ -1099,13 +1110,13 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { req.Add(new MaybeFreeExpression(e, isFree));
}
- } else if (la.kind == 40) {
+ } else if (la.kind == 41) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(142); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(143); Get();}
Expect(14);
if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
@@ -1113,16 +1124,16 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
- } else SynErr(143);
- } else if (la.kind == 41) {
+ } else SynErr(144);
+ } else if (la.kind == 42) {
Get();
while (IsAttribute()) {
Attribute(ref decrAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(144); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(145); Get();}
Expect(14);
- } else SynErr(145);
+ } else SynErr(146);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -1131,7 +1142,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expect(6);
bodyStart = t;
- while (StartOf(11)) {
+ while (StartOf(12)) {
Stmt(body);
}
Expect(7);
@@ -1144,13 +1155,13 @@ 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(12))) {SynErr(146); Get();}
- if (la.kind == 37) {
+ while (!(StartOf(13))) {SynErr(147); Get();}
+ if (la.kind == 38) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
}
- if (StartOf(9)) {
+ if (StartOf(10)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 24) {
@@ -1159,38 +1170,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(147); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(148); Get();}
Expect(14);
- } else if (la.kind == 38 || la.kind == 39 || la.kind == 40) {
- if (la.kind == 38) {
+ } else if (la.kind == 39 || la.kind == 40 || la.kind == 41) {
+ if (la.kind == 39) {
Get();
isFree = true;
}
- if (la.kind == 39) {
+ if (la.kind == 40) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(148); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(149); Get();}
Expect(14);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 40) {
+ } else if (la.kind == 41) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(149); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(150); Get();}
Expect(14);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(150);
- } else if (la.kind == 41) {
+ } else SynErr(151);
+ } else if (la.kind == 42) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(151); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(152); Get();}
Expect(14);
- } else SynErr(152);
+ } else SynErr(153);
}
void FrameExpression(out FrameExpression/*!*/ fe) {
@@ -1200,21 +1211,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo string fieldName = null; IToken feTok = null;
fe = null;
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expression(out e);
feTok = e.tok;
- if (la.kind == 56) {
+ if (la.kind == 57) {
Get();
Ident(out id);
fieldName = id.val; feTok = id;
}
fe = new FrameExpression(feTok, e, fieldName);
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
- } else SynErr(153);
+ } else SynErr(154);
}
void Expression(out Expression/*!*/ e) {
@@ -1261,7 +1272,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Type/*!*/>/*!*/ gt;
List<IToken> path;
- if (la.kind == 51) {
+ if (la.kind == 52) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
@@ -1290,7 +1301,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(154);
+ } else SynErr(155);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1298,16 +1309,16 @@ 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 == 39) {
- while (!(la.kind == 0 || la.kind == 39)) {SynErr(155); Get();}
+ if (la.kind == 40) {
+ while (!(la.kind == 0 || la.kind == 40)) {SynErr(156); Get();}
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(156); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(157); Get();}
Expect(14);
reqs.Add(e);
- } else if (la.kind == 42) {
+ } else if (la.kind == 43) {
Get();
- if (StartOf(14)) {
+ if (StartOf(15)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
while (la.kind == 24) {
@@ -1316,15 +1327,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(157); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(158); Get();}
Expect(14);
- } else if (la.kind == 40) {
+ } else if (la.kind == 41) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(158); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(159); Get();}
Expect(14);
ens.Add(e);
- } else if (la.kind == 41) {
+ } else if (la.kind == 42) {
Get();
if (decreases == null) {
SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
@@ -1332,9 +1343,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(159); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(160); Get();}
Expect(14);
- } else SynErr(160);
+ } else SynErr(161);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1348,23 +1359,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 == 55) {
+ if (la.kind == 56) {
Get();
fe = new FrameExpression(t, new WildcardExpr(t), null);
- } else if (StartOf(9)) {
+ } else if (StartOf(10)) {
FrameExpression(out fe);
- } else SynErr(161);
+ } else SynErr(162);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
e = new WildcardExpr(t);
- } else if (StartOf(13)) {
+ } else if (StartOf(14)) {
Expression(out e);
- } else SynErr(162);
+ } else SynErr(163);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1381,26 +1392,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(15))) {SynErr(163); Get();}
+ while (!(StartOf(16))) {SynErr(164); Get();}
switch (la.kind) {
case 6: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
}
- case 75: {
+ case 76: {
AssertStmt(out s);
break;
}
- case 63: {
+ case 64: {
AssumeStmt(out s);
break;
}
- case 76: {
+ case 77: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 22: case 26: case 101: case 102: case 103: case 104: case 105: case 106: {
+ case 1: case 2: case 22: case 26: case 102: case 103: case 104: case 105: case 106: case 107: {
UpdateStmt(out s);
break;
}
@@ -1408,27 +1419,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s);
break;
}
- case 68: {
+ case 69: {
IfStmt(out s);
break;
}
- case 72: {
+ case 73: {
WhileStmt(out s);
break;
}
- case 74: {
+ case 75: {
MatchStmt(out s);
break;
}
- case 77: {
+ case 78: {
ParallelStmt(out s);
break;
}
- case 78: {
+ case 79: {
CalcStmt(out s);
break;
}
- case 57: {
+ case 58: {
Get();
x = t;
NoUSIdent(out id);
@@ -1437,24 +1448,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 58: {
+ case 59: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 14 || la.kind == 58) {
- while (la.kind == 58) {
+ } else if (la.kind == 14 || la.kind == 59) {
+ while (la.kind == 59) {
Get();
breakCount++;
}
- } else SynErr(164);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(165); Get();}
+ } else SynErr(165);
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(166); Get();}
Expect(14);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 43: case 61: {
+ case 44: case 62: {
ReturnStmt(out s);
break;
}
@@ -1463,7 +1474,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(14);
break;
}
- default: SynErr(166); break;
+ default: SynErr(167); break;
}
}
@@ -1471,16 +1482,16 @@ 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(75);
+ Expect(76);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expression(out e);
} else if (la.kind == 31) {
Get();
- } else SynErr(167);
+ } else SynErr(168);
Expect(14);
if (e == null) {
s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
@@ -1494,16 +1505,16 @@ 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(63);
+ Expect(64);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expression(out e);
} else if (la.kind == 31) {
Get();
- } else SynErr(168);
+ } else SynErr(169);
if (e == null) {
s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
} else {
@@ -1517,7 +1528,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(76);
+ Expect(77);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1548,14 +1559,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(14);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 24 || la.kind == 60 || la.kind == 62) {
+ } else if (la.kind == 24 || la.kind == 61 || la.kind == 63) {
lhss.Add(e); lhs0 = e;
while (la.kind == 24) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 60) {
+ if (la.kind == 61) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1565,20 +1576,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 62) {
+ } else if (la.kind == 63) {
Get();
x = t;
- if (la.kind == 63) {
+ if (la.kind == 64) {
Get();
suchThatAssume = t;
}
Expression(out suchThat);
- } else SynErr(169);
+ } else SynErr(170);
Expect(14);
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(170);
+ } else SynErr(171);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
@@ -1613,8 +1624,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 60 || la.kind == 62) {
- if (la.kind == 60) {
+ if (la.kind == 61 || la.kind == 63) {
+ if (la.kind == 61) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1630,7 +1641,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
Get();
assignTok = t;
- if (la.kind == 63) {
+ if (la.kind == 64) {
Get();
suchThatAssume = t;
}
@@ -1669,7 +1680,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(68);
+ Expect(69);
x = t;
if (la.kind == 26 || la.kind == 31) {
if (la.kind == 26) {
@@ -1679,15 +1690,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo guardOmitted = true;
}
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
- if (la.kind == 68) {
+ if (la.kind == 69) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs;
- } else SynErr(171);
+ } else SynErr(172);
}
if (guardOmitted) {
ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1698,7 +1709,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(172);
+ } else SynErr(173);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1714,7 +1725,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(72);
+ Expect(73);
x = t;
if (la.kind == 26 || la.kind == 31) {
if (la.kind == 26) {
@@ -1730,7 +1741,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 31) {
Get();
bodyOmitted = true;
- } else SynErr(173);
+ } else SynErr(174);
if (guardOmitted || bodyOmitted) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1746,22 +1757,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
- } else if (StartOf(16)) {
+ } else if (StartOf(17)) {
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(174);
+ } else SynErr(175);
}
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(74);
+ Expect(75);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 70) {
+ while (la.kind == 71) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1781,7 +1792,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(77);
+ Expect(78);
x = t;
Expect(26);
if (la.kind == 1) {
@@ -1794,13 +1805,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (range == null) { range = new LiteralExpr(x, true); }
Expect(28);
- while (la.kind == 38 || la.kind == 40) {
+ while (la.kind == 39 || la.kind == 41) {
isFree = false;
- if (la.kind == 38) {
+ if (la.kind == 39) {
Get();
isFree = true;
}
- Expect(40);
+ Expect(41);
Expression(out e);
Expect(14);
ens.Add(new MaybeFreeExpression(e, isFree));
@@ -1821,9 +1832,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ h;
IToken opTok;
- Expect(78);
+ Expect(79);
x = t;
- if (StartOf(17)) {
+ if (StartOf(18)) {
CalcOp(out opTok, out calcOp);
maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(calcOp, calcOp); // guard against non-trasitive calcOp (like !=)
if (maybeOp == null) {
@@ -1833,14 +1844,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(6);
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expression(out e);
lines.Add(e);
Expect(14);
- while (StartOf(18)) {
+ while (StartOf(19)) {
Hint(out h);
hints.Add(h);
- if (StartOf(17)) {
+ if (StartOf(18)) {
CalcOp(out opTok, out op);
maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
if (maybeOp == null) {
@@ -1851,9 +1862,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo resOp = (BinaryExpr.Opcode)maybeOp;
}
- } else if (StartOf(13)) {
+ } else if (StartOf(14)) {
customOps.Add(null);
- } else SynErr(175);
+ } else SynErr(176);
Expression(out e);
lines.Add(e);
Expect(14);
@@ -1869,14 +1880,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssignmentRhs r;
bool isYield = false;
- if (la.kind == 61) {
+ if (la.kind == 62) {
Get();
returnTok = t;
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
returnTok = t; isYield = true;
- } else SynErr(176);
- if (StartOf(19)) {
+ } else SynErr(177);
+ if (StartOf(20)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 24) {
@@ -1901,7 +1912,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e;
Expect(31);
dotdotdot = t;
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
@@ -1911,7 +1922,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out tok);
names.Add(tok);
}
- Expect(60);
+ Expect(61);
Expression(out e);
exprs.Add(e);
while (la.kind == 24) {
@@ -1937,16 +1948,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = dummyRhs; // to please compiler
Attributes attrs = null;
- if (la.kind == 64) {
+ if (la.kind == 65) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 17 || la.kind == 26 || la.kind == 65) {
- if (la.kind == 65) {
+ if (la.kind == 17 || la.kind == 26 || la.kind == 66) {
+ if (la.kind == 66) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(66);
+ Expect(67);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
@@ -1956,7 +1967,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out x);
}
Expect(26);
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expressions(args);
}
Expect(28);
@@ -1970,18 +1981,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty);
}
- } else if (la.kind == 67) {
+ } else if (la.kind == 68) {
Get();
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 55) {
+ } else if (la.kind == 56) {
Get();
r = new HavocRhs(t);
- } else if (StartOf(13)) {
+ } else if (StartOf(14)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(177);
+ } else SynErr(178);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -1993,16 +2004,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 17 || la.kind == 65) {
+ while (la.kind == 17 || la.kind == 66) {
Suffix(ref e);
}
- } else if (StartOf(20)) {
+ } else if (StartOf(21)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 17 || la.kind == 65) {
+ while (la.kind == 17 || la.kind == 66) {
Suffix(ref e);
}
- } else SynErr(178);
+ } else SynErr(179);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -2019,13 +2030,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
Expect(26);
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
e = null;
- } else if (StartOf(13)) {
+ } else if (StartOf(14)) {
Expression(out ee);
e = ee;
- } else SynErr(179);
+ } else SynErr(180);
Expect(28);
}
@@ -2036,13 +2047,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Statement> body;
Expect(6);
- while (la.kind == 70) {
+ while (la.kind == 71) {
Get();
x = t;
Expression(out e);
- Expect(71);
+ Expect(72);
body = new List<Statement>();
- while (StartOf(11)) {
+ while (StartOf(12)) {
Stmt(body);
}
alternatives.Add(new GuardedAlternative(x, e, body));
@@ -2057,29 +2068,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(21)) {
- if (la.kind == 38 || la.kind == 73) {
+ while (StartOf(22)) {
+ if (la.kind == 39 || la.kind == 74) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(180); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(181); Get();}
Expect(14);
invariants.Add(invariant);
- } else if (la.kind == 41) {
- while (!(la.kind == 0 || la.kind == 41)) {SynErr(181); Get();}
+ } else if (la.kind == 42) {
+ while (!(la.kind == 0 || la.kind == 42)) {SynErr(182); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(182); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(183); Get();}
Expect(14);
} else {
- while (!(la.kind == 0 || la.kind == 37)) {SynErr(183); Get();}
+ while (!(la.kind == 0 || la.kind == 38)) {SynErr(184); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
}
mod = mod ?? new List<FrameExpression>();
- if (StartOf(9)) {
+ if (StartOf(10)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 24) {
@@ -2088,7 +2099,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 14)) {SynErr(184); Get();}
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(185); Get();}
Expect(14);
}
}
@@ -2096,12 +2107,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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 == 38 || la.kind == 73)) {SynErr(185); Get();}
- if (la.kind == 38) {
+ while (!(la.kind == 0 || la.kind == 39 || la.kind == 74)) {SynErr(186); Get();}
+ if (la.kind == 39) {
Get();
isFree = true;
}
- Expect(73);
+ Expect(74);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -2116,7 +2127,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(70);
+ Expect(71);
x = t;
Ident(out id);
if (la.kind == 26) {
@@ -2130,8 +2141,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(28);
}
- Expect(71);
- while (StartOf(11)) {
+ Expect(72);
+ while (StartOf(12)) {
Stmt(body);
}
c = new MatchCaseStmt(x, id.val, arguments, body);
@@ -2142,10 +2153,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 4) {
Get();
arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2));
- } else if (StartOf(13)) {
+ } else if (StartOf(14)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(186);
+ } else SynErr(187);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -2191,47 +2202,47 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 85: case 86: {
+ case 86: case 87: {
EquivOp();
x = t; op = BinaryExpr.Opcode.Iff;
break;
}
- case 87: case 88: {
+ case 88: case 89: {
ImpliesOp();
x = t; op = BinaryExpr.Opcode.Imp;
break;
}
- default: SynErr(187); break;
+ default: SynErr(188); break;
}
}
@@ -2243,7 +2254,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Statement/*!*/ calc;
Token x = la;
- while (la.kind == 6 || la.kind == 78) {
+ while (la.kind == 6 || la.kind == 79) {
if (la.kind == 6) {
BlockStmt(out block, out bodyStart, out bodyEnd);
subhints.Add(block);
@@ -2257,25 +2268,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 85) {
+ if (la.kind == 86) {
Get();
- } else if (la.kind == 86) {
+ } else if (la.kind == 87) {
Get();
- } else SynErr(188);
+ } else SynErr(189);
}
void ImpliesOp() {
- if (la.kind == 87) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 88) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(189);
+ } else SynErr(190);
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 85 || la.kind == 86) {
+ while (la.kind == 86 || la.kind == 87) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -2286,7 +2297,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 == 87 || la.kind == 88) {
+ if (la.kind == 88 || la.kind == 89) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -2297,13 +2308,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(22)) {
- if (la.kind == 89 || la.kind == 90) {
+ if (StartOf(23)) {
+ if (la.kind == 90 || la.kind == 91) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 89 || la.kind == 90) {
+ while (la.kind == 90 || la.kind == 91) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -2314,7 +2325,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 == 91 || la.kind == 92) {
+ while (la.kind == 92 || la.kind == 93) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -2338,7 +2349,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Term(out e0);
e = e0;
- if (StartOf(23)) {
+ if (StartOf(24)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
@@ -2346,7 +2357,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (op == BinaryExpr.Opcode.Disjoint)
acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
- while (StartOf(23)) {
+ while (StartOf(24)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -2415,25 +2426,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 89) {
+ if (la.kind == 90) {
Get();
- } else if (la.kind == 90) {
+ } else if (la.kind == 91) {
Get();
- } else SynErr(190);
+ } else SynErr(191);
}
void OrOp() {
- if (la.kind == 91) {
+ if (la.kind == 92) {
Get();
- } else if (la.kind == 92) {
+ } else if (la.kind == 93) {
Get();
- } else SynErr(191);
+ } else SynErr(192);
}
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 == 96 || la.kind == 97) {
+ while (la.kind == 97 || la.kind == 98) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2461,35 +2472,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 93: {
+ case 94: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 94: {
+ case 95: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 95: {
+ case 96: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 94) {
+ if (la.kind == 95) {
Get();
y = t;
}
@@ -2504,29 +2515,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(192); break;
+ default: SynErr(193); 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 == 55 || la.kind == 98 || la.kind == 99) {
+ while (la.kind == 56 || la.kind == 99 || la.kind == 100) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2535,103 +2546,103 @@ 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 == 96) {
+ if (la.kind == 97) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 97) {
+ } else if (la.kind == 98) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(193);
+ } else SynErr(194);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 97: {
+ case 98: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 95: case 100: {
+ case 96: case 101: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 23: case 47: case 57: case 63: case 68: case 74: case 75: case 109: case 110: case 111: case 112: {
+ case 23: case 48: case 58: case 64: case 69: case 75: case 76: case 110: case 111: case 112: case 113: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 17 || la.kind == 65) {
+ while (la.kind == 17 || la.kind == 66) {
Suffix(ref e);
}
break;
}
- case 6: case 65: {
+ case 6: case 66: {
DisplayExpr(out e);
- while (la.kind == 17 || la.kind == 65) {
+ while (la.kind == 17 || la.kind == 66) {
Suffix(ref e);
}
break;
}
- case 48: {
+ case 49: {
MultiSetExpr(out e);
- while (la.kind == 17 || la.kind == 65) {
+ while (la.kind == 17 || la.kind == 66) {
Suffix(ref e);
}
break;
}
- case 50: {
+ case 51: {
Get();
x = t;
- if (la.kind == 65) {
+ if (la.kind == 66) {
MapDisplayExpr(x, out e);
- while (la.kind == 17 || la.kind == 65) {
+ while (la.kind == 17 || la.kind == 66) {
Suffix(ref e);
}
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e);
- } else if (StartOf(24)) {
+ } else if (StartOf(25)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(194);
+ } else SynErr(195);
break;
}
- case 2: case 22: case 26: case 101: case 102: case 103: case 104: case 105: case 106: {
+ case 2: case 22: case 26: case 102: case 103: case 104: case 105: case 106: case 107: {
ConstAtomExpression(out e);
- while (la.kind == 17 || la.kind == 65) {
+ while (la.kind == 17 || la.kind == 66) {
Suffix(ref e);
}
break;
}
- default: SynErr(195); break;
+ default: SynErr(196); 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 == 55) {
+ if (la.kind == 56) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 98) {
+ } else if (la.kind == 99) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 99) {
+ } else if (la.kind == 100) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(196);
+ } else SynErr(197);
}
void NegOp() {
- if (la.kind == 95) {
+ if (la.kind == 96) {
Get();
- } else if (la.kind == 100) {
+ } else if (la.kind == 101) {
Get();
- } else SynErr(197);
+ } else SynErr(198);
}
void EndlessExpression(out Expression e) {
@@ -2640,30 +2651,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 68: {
+ case 69: {
Get();
x = t;
Expression(out e);
- Expect(107);
+ Expect(108);
Expression(out e0);
- Expect(69);
+ Expect(70);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 74: {
+ case 75: {
MatchExpression(out e);
break;
}
- case 109: case 110: case 111: case 112: {
+ case 110: case 111: case 112: case 113: {
QuantifierGuts(out e);
break;
}
- case 47: {
+ case 48: {
ComprehensionExpr(out e);
break;
}
- case 75: {
+ case 76: {
Get();
x = t;
Expression(out e0);
@@ -2672,7 +2683,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AssertExpr(x, e0, e1);
break;
}
- case 63: {
+ case 64: {
Get();
x = t;
Expression(out e0);
@@ -2685,11 +2696,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LetExpr(out e);
break;
}
- case 57: {
+ case 58: {
NamedExpr(out e);
break;
}
- default: SynErr(198); break;
+ default: SynErr(199); break;
}
}
@@ -2708,7 +2719,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 26) {
Get();
openParen = t; args = new List<Expression>();
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expressions(args);
}
Expect(28);
@@ -2728,31 +2739,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 26) {
Get();
IToken openParen = t; args = new List<Expression/*!*/>(); func = true;
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expressions(args);
}
Expect(28);
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 65) {
+ } else if (la.kind == 66) {
Get();
x = t;
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 108) {
+ if (la.kind == 109) {
Get();
anyDots = true;
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 60) {
+ } else if (la.kind == 61) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 24 || la.kind == 66) {
+ } else if (la.kind == 24 || la.kind == 67) {
while (la.kind == 24) {
Get();
Expression(out ee);
@@ -2763,15 +2774,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(199);
- } else if (la.kind == 108) {
+ } else SynErr(200);
+ } else if (la.kind == 109) {
Get();
anyDots = true;
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(200);
+ } else SynErr(201);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2794,8 +2805,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(66);
- } else SynErr(201);
+ Expect(67);
+ } else SynErr(202);
}
void DisplayExpr(out Expression e) {
@@ -2806,20 +2817,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 6) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 65) {
+ } else if (la.kind == 66) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(66);
- } else SynErr(202);
+ Expect(67);
+ } else SynErr(203);
}
void MultiSetExpr(out Expression e) {
@@ -2827,12 +2838,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(48);
+ Expect(49);
x = t;
if (la.kind == 6) {
Get();
elements = new List<Expression/*!*/>();
- if (StartOf(13)) {
+ if (StartOf(14)) {
Expressions(elements);
}
e = new MultiSetDisplayExpr(x, elements);
@@ -2843,9 +2854,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e);
e = new MultiSetFormingExpr(x, e);
Expect(28);
- } else if (StartOf(25)) {
+ } else if (StartOf(26)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(203);
+ } else SynErr(204);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -2853,12 +2864,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
e = dummyExpr;
- Expect(65);
- if (StartOf(13)) {
+ Expect(66);
+ if (StartOf(14)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(mapToken, elements);
- Expect(66);
+ Expect(67);
}
void MapComprehensionExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -2886,17 +2897,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 101: {
+ case 102: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 102: {
+ case 103: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 103: {
+ case 104: {
Get();
e = new LiteralExpr(t);
break;
@@ -2906,12 +2917,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n);
break;
}
- case 104: {
+ case 105: {
Get();
e = new ThisExpr(t);
break;
}
- case 105: {
+ case 106: {
Get();
x = t;
Expect(26);
@@ -2920,7 +2931,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FreshExpr(x, e);
break;
}
- case 106: {
+ case 107: {
Get();
x = t;
Expect(26);
@@ -2945,7 +2956,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(28);
break;
}
- default: SynErr(204); break;
+ default: SynErr(205); break;
}
}
@@ -2964,34 +2975,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d);
- Expect(60);
+ Expect(61);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 24) {
Get();
Expression(out d);
- Expect(60);
+ Expect(61);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
}
}
void QSep() {
- if (la.kind == 113) {
+ if (la.kind == 114) {
Get();
- } else if (la.kind == 114) {
+ } else if (la.kind == 115) {
Get();
- } else SynErr(205);
+ } else SynErr(206);
}
void MatchExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(74);
+ Expect(75);
x = t;
Expression(out e);
- while (la.kind == 70) {
+ while (la.kind == 71) {
CaseExpression(out c);
cases.Add(c);
}
@@ -3006,13 +3017,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression/*!*/ body;
- if (la.kind == 109 || la.kind == 110) {
+ if (la.kind == 110 || la.kind == 111) {
Forall();
x = t; univ = true;
- } else if (la.kind == 111 || la.kind == 112) {
+ } else if (la.kind == 112 || la.kind == 113) {
Exists();
x = t;
- } else SynErr(206);
+ } else SynErr(207);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -3032,7 +3043,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ range;
Expression body = null;
- Expect(47);
+ Expect(48);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -3043,7 +3054,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(22);
Expression(out range);
- if (la.kind == 113 || la.kind == 114) {
+ if (la.kind == 114 || la.kind == 115) {
QSep();
Expression(out body);
}
@@ -3069,7 +3080,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(60);
+ Expect(61);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 24) {
@@ -3087,7 +3098,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
Expression expr;
- Expect(57);
+ Expect(58);
x = t;
NoUSIdent(out d);
Expect(5);
@@ -3102,7 +3113,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(70);
+ Expect(71);
x = t;
Ident(out id);
if (la.kind == 26) {
@@ -3116,25 +3127,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(28);
}
- Expect(71);
+ Expect(72);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 109) {
+ if (la.kind == 110) {
Get();
- } else if (la.kind == 110) {
+ } else if (la.kind == 111) {
Get();
- } else SynErr(207);
+ } else SynErr(208);
}
void Exists() {
- if (la.kind == 111) {
+ if (la.kind == 112) {
Get();
- } else if (la.kind == 112) {
+ } else if (la.kind == 113) {
Get();
- } else SynErr(208);
+ } else SynErr(209);
}
void AttributeBody(ref Attributes attrs) {
@@ -3145,7 +3156,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(5);
Expect(1);
aName = t.val;
- if (StartOf(26)) {
+ if (StartOf(27)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 24) {
@@ -3170,33 +3181,34 @@ 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, x,x,T,x, x,x,T,x, T,T,T,T, x,x,T,x, x,T,x,T, x,x,T,T, x,T,T,T, T,T,T,T, 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,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,T,x,x, x,x,T,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x, x,x,T,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x, T,x,T,T, x,x,x,T, T,T,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, 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, 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,x, x,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,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,x, x,x,x,T, T,x,T,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,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,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,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,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,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,T,T,x, x,T,x,T, x,x,x,x, T,x,x,x, T,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, 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,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,x, x,x,x,T, T,x,T,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,x, x,x,x,T, 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,x, x,x,x,T, T,x,T,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,x, x,x,x,T, 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,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,T,T,x, x,T,x,T, x,x,x,x, T,x,x,x, T,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,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,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, 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, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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, 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,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,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,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,T, 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,x, x,x,x,T, T,x,T,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,x, x,x,x,T, 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,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,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, 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,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,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,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,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, T,x,x,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,x,T,x, x,T,T,T, x,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,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,T,x, T,x,x,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,T,x, x,T,T,T, x,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,x, x,x,x,T, T,x,T,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,x, x,x,x,T, 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,T,x,T, x,x,T,T, T,x,T,T, T,T,T,T, T,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,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,T,x,x, x,x,T,T, T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x, x,x,T,T, T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x, T,x,T,T, T,x,x,x, T,T,T,T, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {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,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,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,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, 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,x, x,x,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,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,x, x,x,x,x, T,T,x,T, 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, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,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,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, 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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,T, 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,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,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,T,T, T,T,T,T, 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,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,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,x, x,x,x,x, T,T,x,T, 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, x,x,x,x, T,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,x, x,x,x,x, T,T,x,T, 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, x,x,x,x, T,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,T, 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,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,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,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,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,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, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,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,T, x,x,x,x, T,T,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,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, T,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,x, x,x,x,x, T,T,x,T, 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, x,x,x,x, T,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,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,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,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,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,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,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,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, T,x,x,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,x,T, x,x,T,T, T,x,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,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,T,x, T,x,x,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,T, x,x,T,T, T,x,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,x, x,x,x,x, T,T,x,T, 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, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
@@ -3256,180 +3268,181 @@ public class Errors { case 32: s = "\"<\" expected"; break;
case 33: s = "\">\" expected"; break;
case 34: s = "\"method\" expected"; break;
- case 35: s = "\"constructor\" expected"; break;
- case 36: s = "\"returns\" expected"; break;
- case 37: s = "\"modifies\" expected"; break;
- case 38: s = "\"free\" expected"; break;
- case 39: s = "\"requires\" expected"; break;
- case 40: s = "\"ensures\" expected"; break;
- case 41: s = "\"decreases\" expected"; break;
- case 42: s = "\"reads\" expected"; break;
- case 43: s = "\"yield\" expected"; break;
- case 44: s = "\"bool\" expected"; break;
- case 45: s = "\"nat\" expected"; break;
- case 46: s = "\"int\" expected"; break;
- case 47: s = "\"set\" expected"; break;
- case 48: s = "\"multiset\" expected"; break;
- case 49: s = "\"seq\" expected"; break;
- case 50: s = "\"map\" expected"; break;
- case 51: s = "\"object\" expected"; break;
- case 52: s = "\"function\" expected"; break;
- case 53: s = "\"predicate\" expected"; break;
- case 54: s = "\"copredicate\" expected"; break;
- case 55: s = "\"*\" expected"; break;
- case 56: s = "\"`\" expected"; break;
- case 57: s = "\"label\" expected"; break;
- case 58: s = "\"break\" expected"; break;
- case 59: s = "\"where\" expected"; break;
- case 60: s = "\":=\" expected"; break;
- case 61: s = "\"return\" expected"; break;
- case 62: s = "\":|\" expected"; break;
- case 63: s = "\"assume\" expected"; break;
- case 64: s = "\"new\" expected"; break;
- case 65: s = "\"[\" expected"; break;
- case 66: s = "\"]\" expected"; break;
- case 67: s = "\"choose\" expected"; break;
- case 68: s = "\"if\" expected"; break;
- case 69: s = "\"else\" expected"; break;
- case 70: s = "\"case\" expected"; break;
- case 71: s = "\"=>\" expected"; break;
- case 72: s = "\"while\" expected"; break;
- case 73: s = "\"invariant\" expected"; break;
- case 74: s = "\"match\" expected"; break;
- case 75: s = "\"assert\" expected"; break;
- case 76: s = "\"print\" expected"; break;
- case 77: s = "\"parallel\" expected"; break;
- case 78: s = "\"calc\" expected"; break;
- case 79: s = "\"<=\" expected"; break;
- case 80: s = "\">=\" expected"; break;
- case 81: s = "\"!=\" expected"; break;
- case 82: s = "\"\\u2260\" expected"; break;
- case 83: s = "\"\\u2264\" expected"; break;
- case 84: s = "\"\\u2265\" expected"; break;
- case 85: s = "\"<==>\" expected"; break;
- case 86: s = "\"\\u21d4\" expected"; break;
- case 87: s = "\"==>\" expected"; break;
- case 88: s = "\"\\u21d2\" expected"; break;
- case 89: s = "\"&&\" expected"; break;
- case 90: s = "\"\\u2227\" expected"; break;
- case 91: s = "\"||\" expected"; break;
- case 92: s = "\"\\u2228\" expected"; break;
- case 93: s = "\"!!\" expected"; break;
- case 94: s = "\"in\" expected"; break;
- case 95: s = "\"!\" expected"; break;
- case 96: s = "\"+\" expected"; break;
- case 97: s = "\"-\" expected"; break;
- case 98: s = "\"/\" expected"; break;
- case 99: s = "\"%\" expected"; break;
- case 100: s = "\"\\u00ac\" expected"; break;
- case 101: s = "\"false\" expected"; break;
- case 102: s = "\"true\" expected"; break;
- case 103: s = "\"null\" expected"; break;
- case 104: s = "\"this\" expected"; break;
- case 105: s = "\"fresh\" expected"; break;
- case 106: s = "\"old\" expected"; break;
- case 107: s = "\"then\" expected"; break;
- case 108: s = "\"..\" expected"; break;
- case 109: s = "\"forall\" expected"; break;
- case 110: s = "\"\\u2200\" expected"; break;
- case 111: s = "\"exists\" expected"; break;
- case 112: s = "\"\\u2203\" expected"; break;
- case 113: s = "\"::\" expected"; break;
- case 114: s = "\"\\u2022\" expected"; break;
- case 115: s = "??? expected"; break;
- case 116: s = "invalid Dafny"; break;
- case 117: s = "invalid SubModuleDecl"; break;
+ case 35: s = "\"comethod\" expected"; break;
+ case 36: s = "\"constructor\" expected"; break;
+ case 37: s = "\"returns\" expected"; break;
+ case 38: s = "\"modifies\" expected"; break;
+ case 39: s = "\"free\" expected"; break;
+ case 40: s = "\"requires\" expected"; break;
+ case 41: s = "\"ensures\" expected"; break;
+ case 42: s = "\"decreases\" expected"; break;
+ case 43: s = "\"reads\" expected"; break;
+ case 44: s = "\"yield\" expected"; break;
+ case 45: s = "\"bool\" expected"; break;
+ case 46: s = "\"nat\" expected"; break;
+ case 47: s = "\"int\" expected"; break;
+ case 48: s = "\"set\" expected"; break;
+ case 49: s = "\"multiset\" expected"; break;
+ case 50: s = "\"seq\" expected"; break;
+ case 51: s = "\"map\" expected"; break;
+ case 52: s = "\"object\" expected"; break;
+ case 53: s = "\"function\" expected"; break;
+ case 54: s = "\"predicate\" expected"; break;
+ case 55: s = "\"copredicate\" expected"; break;
+ case 56: s = "\"*\" expected"; break;
+ case 57: s = "\"`\" expected"; break;
+ case 58: s = "\"label\" expected"; break;
+ case 59: s = "\"break\" expected"; break;
+ case 60: s = "\"where\" expected"; break;
+ case 61: s = "\":=\" expected"; break;
+ case 62: s = "\"return\" expected"; break;
+ case 63: s = "\":|\" expected"; break;
+ case 64: s = "\"assume\" expected"; break;
+ case 65: s = "\"new\" expected"; break;
+ case 66: s = "\"[\" expected"; break;
+ case 67: s = "\"]\" expected"; break;
+ case 68: s = "\"choose\" expected"; break;
+ case 69: s = "\"if\" expected"; break;
+ case 70: s = "\"else\" expected"; break;
+ case 71: s = "\"case\" expected"; break;
+ case 72: s = "\"=>\" expected"; break;
+ case 73: s = "\"while\" expected"; break;
+ case 74: s = "\"invariant\" expected"; break;
+ case 75: s = "\"match\" expected"; break;
+ case 76: s = "\"assert\" expected"; break;
+ case 77: s = "\"print\" expected"; break;
+ case 78: s = "\"parallel\" expected"; break;
+ case 79: s = "\"calc\" expected"; break;
+ case 80: s = "\"<=\" expected"; break;
+ case 81: s = "\">=\" expected"; break;
+ case 82: s = "\"!=\" expected"; break;
+ case 83: s = "\"\\u2260\" expected"; break;
+ case 84: s = "\"\\u2264\" expected"; break;
+ case 85: s = "\"\\u2265\" expected"; break;
+ case 86: s = "\"<==>\" expected"; break;
+ case 87: s = "\"\\u21d4\" expected"; break;
+ case 88: s = "\"==>\" expected"; break;
+ case 89: s = "\"\\u21d2\" expected"; break;
+ case 90: s = "\"&&\" expected"; break;
+ case 91: s = "\"\\u2227\" expected"; break;
+ case 92: s = "\"||\" expected"; break;
+ case 93: s = "\"\\u2228\" expected"; break;
+ case 94: s = "\"!!\" expected"; break;
+ case 95: s = "\"in\" expected"; break;
+ case 96: s = "\"!\" expected"; break;
+ case 97: s = "\"+\" expected"; break;
+ case 98: s = "\"-\" expected"; break;
+ case 99: s = "\"/\" expected"; break;
+ case 100: s = "\"%\" expected"; break;
+ case 101: s = "\"\\u00ac\" expected"; break;
+ case 102: s = "\"false\" expected"; break;
+ case 103: s = "\"true\" expected"; break;
+ case 104: s = "\"null\" expected"; break;
+ case 105: s = "\"this\" expected"; break;
+ case 106: s = "\"fresh\" expected"; break;
+ case 107: s = "\"old\" expected"; break;
+ case 108: s = "\"then\" expected"; break;
+ case 109: s = "\"..\" expected"; break;
+ case 110: s = "\"forall\" expected"; break;
+ case 111: s = "\"\\u2200\" expected"; break;
+ case 112: s = "\"exists\" expected"; break;
+ case 113: s = "\"\\u2203\" expected"; break;
+ case 114: s = "\"::\" expected"; break;
+ case 115: s = "\"\\u2022\" expected"; break;
+ case 116: s = "??? expected"; break;
+ case 117: s = "invalid Dafny"; break;
case 118: s = "invalid SubModuleDecl"; break;
case 119: s = "invalid SubModuleDecl"; break;
- case 120: s = "this symbol not expected in ClassDecl"; break;
- case 121: s = "this symbol not expected in DatatypeDecl"; break;
- case 122: s = "invalid DatatypeDecl"; break;
- case 123: s = "this symbol not expected in DatatypeDecl"; break;
- case 124: s = "this symbol not expected in ArbitraryTypeDecl"; break;
- case 125: s = "this symbol not expected in IteratorDecl"; break;
- case 126: s = "invalid IteratorDecl"; break;
- case 127: s = "invalid ClassMemberDecl"; break;
- case 128: s = "this symbol not expected in FieldDecl"; break;
+ case 120: s = "invalid SubModuleDecl"; break;
+ case 121: s = "this symbol not expected in ClassDecl"; break;
+ case 122: s = "this symbol not expected in DatatypeDecl"; break;
+ case 123: s = "invalid DatatypeDecl"; break;
+ case 124: s = "this symbol not expected in DatatypeDecl"; break;
+ case 125: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 126: s = "this symbol not expected in IteratorDecl"; break;
+ case 127: s = "invalid IteratorDecl"; break;
+ case 128: s = "invalid ClassMemberDecl"; break;
case 129: s = "this symbol not expected in FieldDecl"; break;
- case 130: s = "invalid FunctionDecl"; break;
+ case 130: s = "this symbol not expected in FieldDecl"; break;
case 131: s = "invalid FunctionDecl"; break;
case 132: s = "invalid FunctionDecl"; break;
case 133: s = "invalid FunctionDecl"; break;
- case 134: s = "this symbol not expected in MethodDecl"; break;
- case 135: s = "invalid MethodDecl"; break;
+ case 134: s = "invalid FunctionDecl"; break;
+ case 135: s = "this symbol not expected in MethodDecl"; break;
case 136: s = "invalid MethodDecl"; break;
- case 137: s = "invalid TypeAndToken"; break;
- case 138: s = "this symbol not expected in IteratorSpec"; break;
+ case 137: s = "invalid MethodDecl"; break;
+ case 138: s = "invalid TypeAndToken"; break;
case 139: s = "this symbol not expected in IteratorSpec"; break;
case 140: s = "this symbol not expected in IteratorSpec"; break;
case 141: s = "this symbol not expected in IteratorSpec"; break;
case 142: s = "this symbol not expected in IteratorSpec"; break;
- case 143: s = "invalid IteratorSpec"; break;
- case 144: s = "this symbol not expected in IteratorSpec"; break;
- case 145: s = "invalid IteratorSpec"; break;
- case 146: s = "this symbol not expected in MethodSpec"; break;
+ case 143: s = "this symbol not expected in IteratorSpec"; break;
+ case 144: s = "invalid IteratorSpec"; break;
+ case 145: s = "this symbol not expected in IteratorSpec"; break;
+ case 146: s = "invalid IteratorSpec"; break;
case 147: s = "this symbol not expected in MethodSpec"; break;
case 148: s = "this symbol not expected in MethodSpec"; break;
case 149: s = "this symbol not expected in MethodSpec"; break;
- case 150: s = "invalid MethodSpec"; break;
- case 151: s = "this symbol not expected in MethodSpec"; break;
- case 152: s = "invalid MethodSpec"; break;
- case 153: s = "invalid FrameExpression"; break;
- case 154: s = "invalid ReferenceType"; break;
- case 155: s = "this symbol not expected in FunctionSpec"; break;
+ case 150: s = "this symbol not expected in MethodSpec"; break;
+ case 151: s = "invalid MethodSpec"; break;
+ case 152: s = "this symbol not expected in MethodSpec"; break;
+ case 153: s = "invalid MethodSpec"; break;
+ case 154: s = "invalid FrameExpression"; break;
+ case 155: s = "invalid ReferenceType"; break;
case 156: s = "this symbol not expected in FunctionSpec"; break;
case 157: s = "this symbol not expected in FunctionSpec"; break;
case 158: s = "this symbol not expected in FunctionSpec"; break;
case 159: s = "this symbol not expected in FunctionSpec"; break;
- case 160: s = "invalid FunctionSpec"; break;
- case 161: s = "invalid PossiblyWildFrameExpression"; break;
- case 162: s = "invalid PossiblyWildExpression"; break;
- case 163: s = "this symbol not expected in OneStmt"; break;
- case 164: s = "invalid OneStmt"; break;
- case 165: s = "this symbol not expected in OneStmt"; break;
- case 166: s = "invalid OneStmt"; break;
- case 167: s = "invalid AssertStmt"; break;
- case 168: s = "invalid AssumeStmt"; break;
- case 169: s = "invalid UpdateStmt"; break;
+ case 160: s = "this symbol not expected in FunctionSpec"; break;
+ case 161: s = "invalid FunctionSpec"; break;
+ case 162: s = "invalid PossiblyWildFrameExpression"; break;
+ case 163: s = "invalid PossiblyWildExpression"; break;
+ case 164: s = "this symbol not expected in OneStmt"; break;
+ case 165: s = "invalid OneStmt"; break;
+ case 166: s = "this symbol not expected in OneStmt"; break;
+ case 167: s = "invalid OneStmt"; break;
+ case 168: s = "invalid AssertStmt"; break;
+ case 169: s = "invalid AssumeStmt"; break;
case 170: s = "invalid UpdateStmt"; break;
- case 171: s = "invalid IfStmt"; break;
+ case 171: s = "invalid UpdateStmt"; break;
case 172: s = "invalid IfStmt"; break;
- case 173: s = "invalid WhileStmt"; break;
+ case 173: s = "invalid IfStmt"; break;
case 174: s = "invalid WhileStmt"; break;
- case 175: s = "invalid CalcStmt"; break;
- case 176: s = "invalid ReturnStmt"; break;
- case 177: s = "invalid Rhs"; break;
- case 178: s = "invalid Lhs"; break;
- case 179: s = "invalid Guard"; break;
- case 180: s = "this symbol not expected in LoopSpec"; break;
+ case 175: s = "invalid WhileStmt"; break;
+ case 176: s = "invalid CalcStmt"; break;
+ case 177: s = "invalid ReturnStmt"; break;
+ case 178: s = "invalid Rhs"; break;
+ case 179: s = "invalid Lhs"; break;
+ case 180: s = "invalid Guard"; break;
case 181: s = "this symbol not expected in LoopSpec"; break;
case 182: s = "this symbol not expected in LoopSpec"; break;
case 183: s = "this symbol not expected in LoopSpec"; break;
case 184: s = "this symbol not expected in LoopSpec"; break;
- case 185: s = "this symbol not expected in Invariant"; break;
- case 186: s = "invalid AttributeArg"; break;
- case 187: s = "invalid CalcOp"; break;
- case 188: s = "invalid EquivOp"; break;
- case 189: s = "invalid ImpliesOp"; break;
- case 190: s = "invalid AndOp"; break;
- case 191: s = "invalid OrOp"; break;
- case 192: s = "invalid RelOp"; break;
- case 193: s = "invalid AddOp"; break;
- case 194: s = "invalid UnaryExpression"; break;
+ case 185: s = "this symbol not expected in LoopSpec"; break;
+ case 186: s = "this symbol not expected in Invariant"; break;
+ case 187: s = "invalid AttributeArg"; break;
+ case 188: s = "invalid CalcOp"; break;
+ case 189: s = "invalid EquivOp"; break;
+ case 190: s = "invalid ImpliesOp"; break;
+ case 191: s = "invalid AndOp"; break;
+ case 192: s = "invalid OrOp"; break;
+ case 193: s = "invalid RelOp"; break;
+ case 194: s = "invalid AddOp"; break;
case 195: s = "invalid UnaryExpression"; break;
- case 196: s = "invalid MulOp"; break;
- case 197: s = "invalid NegOp"; break;
- case 198: s = "invalid EndlessExpression"; break;
- case 199: s = "invalid Suffix"; break;
+ case 196: s = "invalid UnaryExpression"; break;
+ case 197: s = "invalid MulOp"; break;
+ case 198: s = "invalid NegOp"; break;
+ case 199: s = "invalid EndlessExpression"; break;
case 200: s = "invalid Suffix"; break;
case 201: s = "invalid Suffix"; break;
- case 202: s = "invalid DisplayExpr"; break;
- case 203: s = "invalid MultiSetExpr"; break;
- case 204: s = "invalid ConstAtomExpression"; break;
- case 205: s = "invalid QSep"; break;
- case 206: s = "invalid QuantifierGuts"; break;
- case 207: s = "invalid Forall"; break;
- case 208: s = "invalid Exists"; break;
+ case 202: s = "invalid Suffix"; break;
+ case 203: s = "invalid DisplayExpr"; break;
+ case 204: s = "invalid MultiSetExpr"; break;
+ case 205: s = "invalid ConstAtomExpression"; break;
+ case 206: s = "invalid QSep"; break;
+ case 207: s = "invalid QuantifierGuts"; break;
+ case 208: s = "invalid Forall"; break;
+ case 209: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 03f8faad..d045426d 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -532,6 +532,9 @@ namespace Microsoft.Dafny if (m is Constructor) {
return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), false);
+ } else if (m is CoMethod) {
+ return new CoMethod(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
+ req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), false);
} else {
return new Method(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), false);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 573cdfa7..2486f337 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -696,15 +696,15 @@ namespace Microsoft.Dafny // add deconstructors now (that is, after the query methods have been added)
foreach (DatatypeCtor ctor in dt.Ctors) {
foreach (var formal in ctor.Formals) {
- SpecialField dtor = null;
- if (formal.HasName) {
- if (members.ContainsKey(formal.Name)) {
- Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
- } else {
- dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
- dtor.EnclosingClass = dt; // resolve here
- members.Add(formal.Name, dtor);
- }
+ bool nameError = false;
+ if (formal.HasName && members.ContainsKey(formal.Name)) {
+ Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
+ nameError = true;
+ }
+ var dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
+ dtor.EnclosingClass = dt; // resolve here
+ if (!nameError && formal.HasName) {
+ members.Add(formal.Name, dtor);
}
ctor.Destructors.Add(dtor);
}
@@ -864,6 +864,9 @@ namespace Microsoft.Dafny if (m is Constructor) {
return new Constructor(m.tok, m.Name, tps, ins,
req, mod, ens, decreases, null, null, false);
+ } else if (m is CoMethod) {
+ return new CoMethod(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ req, mod, ens, decreases, null, null, false);
} else {
return new Method(m.tok, m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, null, null, false);
@@ -1346,10 +1349,23 @@ namespace Microsoft.Dafny }
}
}
- // Check that copredicates are not recursive with non-copredicate functions.
- foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {
- if (fn.Body != null && (fn is CoPredicate || fn.IsRecursive)) {
- CoPredicateChecks(fn.Body, fn, CallingPosition.Positive);
+ // Check that copredicates are not recursive with non-copredicate functions, and
+ // check that comethods are not recursive with non-comethod methods.
+ foreach (var d in declarations) {
+ if (d is ClassDecl) {
+ foreach (var member in ((ClassDecl)d).Members) {
+ if (member is CoPredicate) {
+ var fn = (CoPredicate)member;
+ if (fn.Body != null) {
+ CoPredicateChecks(fn.Body, fn, CallingPosition.Positive);
+ }
+ } else if (member is CoMethod) {
+ var m = (CoMethod)member;
+ if (m.Body != null) {
+ CoMethodChecks(m.Body, m);
+ }
+ }
+ }
}
}
}
@@ -1531,7 +1547,7 @@ namespace Microsoft.Dafny }
}
- void CoPredicateChecks(Expression expr, Function context, CallingPosition cp) {
+ void CoPredicateChecks(Expression expr, CoPredicate context, CallingPosition cp) {
Contract.Requires(expr != null);
Contract.Requires(context != null);
if (expr is ConcreteSyntaxExpression) {
@@ -1544,14 +1560,12 @@ namespace Microsoft.Dafny var moduleCallee = e.Function.EnclosingClass.Module;
if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {
// we're looking at a recursive call
- if (context is CoPredicate) {
- if (!(e.Function is CoPredicate)) {
- Error(e, "a recursive call from a copredicate can go only to other copredicates");
- } else if (cp != CallingPosition.Positive) {
- Error(e, "a recursive copredicate call can only be done in positive positions");
- }
- } else if (e.Function is CoPredicate) {
- Error(e, "a recursive call from a non-copredicate can go only to other non-copredicates");
+ if (!(e.Function is CoPredicate)) {
+ Error(e, "a recursive call from a copredicate can go only to other copredicates");
+ } else if (cp != CallingPosition.Positive) {
+ Error(e, "a recursive copredicate call can only be done in positive positions");
+ } else {
+ e.CoCall = FunctionCallExpr.CoCallResolution.Yes;
}
}
// fall through to do the subexpressions
@@ -1601,6 +1615,27 @@ namespace Microsoft.Dafny expr.SubExpressions.Iter(ee => CoPredicateChecks(ee, context, CallingPosition.Neither));
}
+ void CoMethodChecks(Statement stmt, CoMethod context) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(context != null);
+ if (stmt is CallStmt) {
+ var s = (CallStmt)stmt;
+ if (s.Method is CoMethod) {
+ // all is cool
+ } else {
+ // the call goes from a comethod context to a non-comethod callee
+ var moduleCaller = context.EnclosingClass.Module;
+ var moduleCallee = s.Method.EnclosingClass.Module;
+ if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {
+ // we're looking at a recursive call (to a non-comethod)
+ Error(s, "a recursive call from a comethod can go only to other comethods");
+ }
+ }
+ } else {
+ stmt.SubStatements.Iter(ss => CoMethodChecks(ss, context));
+ }
+ }
+
void CheckEqualityTypes_Stmt(Statement stmt) {
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
@@ -4390,6 +4425,32 @@ namespace Microsoft.Dafny return null;
}
+ /// <summary>
+ /// Returns a resolved FieldSelectExpr.
+ /// </summary>
+ public static FieldSelectExpr NewFieldSelectExpr(IToken tok, Expression obj, Field field, Dictionary<TypeParameter, Type> typeSubstMap) {
+ Contract.Requires(tok != null);
+ Contract.Requires(obj != null);
+ Contract.Requires(field != null);
+ Contract.Requires(obj.Type != null); // "obj" is required to be resolved
+ Contract.Requires(typeSubstMap != null);
+ var e = new FieldSelectExpr(tok, obj, field.Name);
+ e.Field = field; // resolve here
+ e.Type = SubstType(field.Type, typeSubstMap); // resolve here
+ return e;
+ }
+
+ public static Dictionary<TypeParameter, Type> TypeSubstitutionMap(List<TypeParameter> formals, List<Type> actuals) {
+ Contract.Requires(formals != null);
+ Contract.Requires(actuals != null);
+ Contract.Requires(formals.Count == actuals.Count);
+ var subst = new Dictionary<TypeParameter, Type>();
+ for (int i = 0; i < formals.Count; i++) {
+ subst.Add(formals[i], actuals[i]);
+ }
+ return subst;
+ }
+
public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/, Type/*!*/>/*!*/ subst) {
Contract.Requires(type != null);
Contract.Requires(cce.NonNullDictionaryAndValues(subst));
@@ -4640,10 +4701,7 @@ namespace Microsoft.Dafny Error(expr, "a field must be selected via an object, not just a class name");
}
// build the type substitution map
- Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
- for (int i = 0; i < ctype.TypeArgs.Count; i++) {
- subst.Add(ctype.ResolvedClass.TypeArgs[i], ctype.TypeArgs[i]);
- }
+ var subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs);
e.Type = SubstType(e.Field.Type, subst);
}
@@ -6292,7 +6350,7 @@ namespace Microsoft.Dafny /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if
/// resolution of the binary expression failed. If so, an arbitrary resolved opcode is returned.
/// </summary>
- BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type operandType) {
+ public static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type operandType) {
Contract.Requires(operandType != null);
switch (op) {
case BinaryExpr.Opcode.Iff: return BinaryExpr.ResolvedOpcode.Iff;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index b23931b6..2c456766 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/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 = 115;
- const int noSym = 115;
+ const int maxT = 116;
+ const int noSym = 116;
[ContractInvariantMethod]
@@ -504,53 +504,54 @@ public class Scanner { case "iterator": t.kind = 29; break;
case "yields": t.kind = 30; break;
case "method": t.kind = 34; break;
- case "constructor": t.kind = 35; break;
- case "returns": t.kind = 36; break;
- case "modifies": t.kind = 37; break;
- case "free": t.kind = 38; break;
- case "requires": t.kind = 39; break;
- case "ensures": t.kind = 40; break;
- case "decreases": t.kind = 41; break;
- case "reads": t.kind = 42; break;
- case "yield": t.kind = 43; break;
- case "bool": t.kind = 44; break;
- case "nat": t.kind = 45; break;
- case "int": t.kind = 46; break;
- case "set": t.kind = 47; break;
- case "multiset": t.kind = 48; break;
- case "seq": t.kind = 49; break;
- case "map": t.kind = 50; break;
- case "object": t.kind = 51; break;
- case "function": t.kind = 52; break;
- case "predicate": t.kind = 53; break;
- case "copredicate": t.kind = 54; break;
- case "label": t.kind = 57; break;
- case "break": t.kind = 58; break;
- case "where": t.kind = 59; break;
- case "return": t.kind = 61; break;
- case "assume": t.kind = 63; break;
- case "new": t.kind = 64; break;
- case "choose": t.kind = 67; break;
- case "if": t.kind = 68; break;
- case "else": t.kind = 69; break;
- case "case": t.kind = 70; break;
- case "while": t.kind = 72; break;
- case "invariant": t.kind = 73; break;
- case "match": t.kind = 74; break;
- case "assert": t.kind = 75; break;
- case "print": t.kind = 76; break;
- case "parallel": t.kind = 77; break;
- case "calc": t.kind = 78; break;
- case "in": t.kind = 94; break;
- case "false": t.kind = 101; break;
- case "true": t.kind = 102; break;
- case "null": t.kind = 103; break;
- case "this": t.kind = 104; break;
- case "fresh": t.kind = 105; break;
- case "old": t.kind = 106; break;
- case "then": t.kind = 107; break;
- case "forall": t.kind = 109; break;
- case "exists": t.kind = 111; break;
+ case "comethod": t.kind = 35; break;
+ case "constructor": t.kind = 36; break;
+ case "returns": t.kind = 37; break;
+ case "modifies": t.kind = 38; break;
+ case "free": t.kind = 39; break;
+ case "requires": t.kind = 40; break;
+ case "ensures": t.kind = 41; break;
+ case "decreases": t.kind = 42; break;
+ case "reads": t.kind = 43; break;
+ case "yield": t.kind = 44; break;
+ case "bool": t.kind = 45; break;
+ case "nat": t.kind = 46; break;
+ case "int": t.kind = 47; break;
+ case "set": t.kind = 48; break;
+ case "multiset": t.kind = 49; break;
+ case "seq": t.kind = 50; break;
+ case "map": t.kind = 51; break;
+ case "object": t.kind = 52; break;
+ case "function": t.kind = 53; break;
+ case "predicate": t.kind = 54; break;
+ case "copredicate": t.kind = 55; break;
+ case "label": t.kind = 58; break;
+ case "break": t.kind = 59; break;
+ case "where": t.kind = 60; break;
+ case "return": t.kind = 62; break;
+ case "assume": t.kind = 64; break;
+ case "new": t.kind = 65; break;
+ case "choose": t.kind = 68; break;
+ case "if": t.kind = 69; break;
+ case "else": t.kind = 70; break;
+ case "case": t.kind = 71; break;
+ case "while": t.kind = 73; break;
+ case "invariant": t.kind = 74; break;
+ case "match": t.kind = 75; break;
+ case "assert": t.kind = 76; break;
+ case "print": t.kind = 77; break;
+ case "parallel": t.kind = 78; break;
+ case "calc": t.kind = 79; break;
+ case "in": t.kind = 95; break;
+ case "false": t.kind = 102; break;
+ case "true": t.kind = 103; break;
+ case "null": t.kind = 104; break;
+ case "this": t.kind = 105; break;
+ case "fresh": t.kind = 106; break;
+ case "old": t.kind = 107; break;
+ case "then": t.kind = 108; break;
+ case "forall": t.kind = 110; break;
+ case "exists": t.kind = 112; break;
default: break;
}
}
@@ -666,71 +667,71 @@ public class Scanner { case 23:
{t.kind = 31; break;}
case 24:
- {t.kind = 55; break;}
- case 25:
{t.kind = 56; break;}
+ case 25:
+ {t.kind = 57; break;}
case 26:
- {t.kind = 60; break;}
+ {t.kind = 61; break;}
case 27:
- {t.kind = 62; break;}
+ {t.kind = 63; break;}
case 28:
- {t.kind = 65; break;}
- case 29:
{t.kind = 66; break;}
+ case 29:
+ {t.kind = 67; break;}
case 30:
- {t.kind = 71; break;}
+ {t.kind = 72; break;}
case 31:
- {t.kind = 80; break;}
- case 32:
{t.kind = 81; break;}
- case 33:
+ case 32:
{t.kind = 82; break;}
- case 34:
+ case 33:
{t.kind = 83; break;}
- case 35:
+ case 34:
{t.kind = 84; break;}
+ case 35:
+ {t.kind = 85; break;}
case 36:
if (ch == '>') {AddCh(); goto case 37;}
else {goto case 0;}
case 37:
- {t.kind = 85; break;}
- case 38:
{t.kind = 86; break;}
- case 39:
+ case 38:
{t.kind = 87; break;}
- case 40:
+ case 39:
{t.kind = 88; break;}
+ case 40:
+ {t.kind = 89; break;}
case 41:
if (ch == '&') {AddCh(); goto case 42;}
else {goto case 0;}
case 42:
- {t.kind = 89; break;}
- case 43:
{t.kind = 90; break;}
- case 44:
+ case 43:
{t.kind = 91; break;}
- case 45:
+ case 44:
{t.kind = 92; break;}
- case 46:
+ case 45:
{t.kind = 93; break;}
+ case 46:
+ {t.kind = 94; break;}
case 47:
- {t.kind = 96; break;}
- case 48:
{t.kind = 97; break;}
- case 49:
+ case 48:
{t.kind = 98; break;}
- case 50:
+ case 49:
{t.kind = 99; break;}
- case 51:
+ case 50:
{t.kind = 100; break;}
+ case 51:
+ {t.kind = 101; break;}
case 52:
- {t.kind = 110; break;}
+ {t.kind = 111; break;}
case 53:
- {t.kind = 112; break;}
- case 54:
{t.kind = 113; break;}
- case 55:
+ case 54:
{t.kind = 114; break;}
+ case 55:
+ {t.kind = 115; break;}
case 56:
recEnd = pos; recKind = 5;
if (ch == '=') {AddCh(); goto case 26;}
@@ -759,22 +760,22 @@ public class Scanner { if (ch == '=') {AddCh(); goto case 31;}
else {t.kind = 33; break;}
case 62:
- recEnd = pos; recKind = 95;
+ recEnd = pos; recKind = 96;
if (ch == '=') {AddCh(); goto case 32;}
else if (ch == '!') {AddCh(); goto case 46;}
- else {t.kind = 95; break;}
+ else {t.kind = 96; break;}
case 63:
recEnd = pos; recKind = 27;
if (ch == '>') {AddCh(); goto case 39;}
else {t.kind = 27; break;}
case 64:
- recEnd = pos; recKind = 108;
+ recEnd = pos; recKind = 109;
if (ch == '.') {AddCh(); goto case 23;}
- else {t.kind = 108; break;}
+ else {t.kind = 109; break;}
case 65:
- recEnd = pos; recKind = 79;
+ recEnd = pos; recKind = 80;
if (ch == '=') {AddCh(); goto case 36;}
- else {t.kind = 79; break;}
+ else {t.kind = 80; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8785e2cd..e6ea7bd9 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -300,21 +300,6 @@ namespace Microsoft.Dafny { } else {
return prelude;
}
-/*
- List<string!> defines = new List<string!>();
- using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))
- {
- BoogiePL.Buffer.Fill(new System.IO.StreamReader(stream), defines);
- //BoogiePL.Scanner.Init("<DafnyPrelude.bpl>");
- Bpl.Program prelude;
- int errorCount = BoogiePL.Parser.Parse(out prelude);
- if (prelude == null || errorCount > 0) {
- return null;
- } else {
- return prelude;
- }
- }
-*/
}
public Bpl.Program Translate(Program p) {
@@ -468,20 +453,13 @@ namespace Microsoft.Dafny { sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
// Add injectivity axioms:
+ Contract.Assert(ctor.Formals.Count == ctor.Destructors.Count); // even nameless destructors are included in ctor.Destructors
i = 0;
foreach (Formal arg in ctor.Formals) {
// function ##dt.ctor#i(DatatypeType) returns (Ti);
var sf = ctor.Destructors[i];
- if (sf != null) {
- fn = GetReadonlyField(sf);
- } else {
- Contract.Assert(!arg.HasName);
- argTypes = new Bpl.VariableSeq();
- argTypes.Add(new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true));
- resType = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), false);
- string nm = "#" + ctor.FullName + "#" + i;
- fn = new Bpl.Function(ctor.tok, nm, argTypes, resType);
- }
+ Contract.Assert(sf != null);
+ fn = GetReadonlyField(sf);
sink.TopLevelDeclarations.Add(fn);
// axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i);
CreateBoundVariables(ctor.Formals, out bvs, out args);
@@ -632,33 +610,34 @@ namespace Microsoft.Dafny { }
AddFrameAxiom(f);
AddWellformednessCheck(f);
+#if OLD_COINDUCTION_PRINCIPLE
if (f is CoPredicate) {
AddCoinductionPrinciple((CoPredicate)f);
}
+#endif
} else if (member is Method) {
Method m = (Method)member;
bool isRefinementMethod = RefinementToken.IsInherited(m.tok, m.EnclosingClass.Module);
// wellformedness check for method specification
- Bpl.Procedure proc = AddMethod(m, 0, isRefinementMethod);
+ Bpl.Procedure proc = AddMethod(m, MethodTranslationKind.SpecWellformedness);
sink.TopLevelDeclarations.Add(proc);
if (m.EnclosingClass is IteratorDecl && m == ((IteratorDecl)m.EnclosingClass).Member_MoveNext) {
// skip the well-formedness check, because it has already been done for the iterator
} else {
AddMethodImpl(m, proc, true);
}
- // the method itself
- proc = AddMethod(m, 1, isRefinementMethod);
- sink.TopLevelDeclarations.Add(proc);
- if (isRefinementMethod) {
- proc = AddMethod(m, 2, isRefinementMethod);
- sink.TopLevelDeclarations.Add(proc);
- proc = AddMethod(m, 3, isRefinementMethod);
- sink.TopLevelDeclarations.Add(proc);
+ // the method spec itself
+ sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.InterModuleCall));
+ sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.IntraModuleCall));
+ if (m is CoMethod) {
+ sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.CoCall));
}
if (m.Body != null) {
// ...and its implementation
+ proc = AddMethod(m, MethodTranslationKind.Implementation);
+ sink.TopLevelDeclarations.Add(proc);
AddMethodImpl(m, proc, false);
}
@@ -738,7 +717,7 @@ namespace Microsoft.Dafny { if (kind == 2 && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this precondition was inherited into this module, so just ignore it
} else {
- req.Add(Requires(s.E.tok, s.IsFree, s.E, null, null));
+ req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, null));
// the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
}
}
@@ -754,7 +733,7 @@ namespace Microsoft.Dafny { if (kind == 3 && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this postcondition was inherited into this module, so just ignore it
} else {
- ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
+ ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, null, null));
}
}
}
@@ -1481,7 +1460,7 @@ namespace Microsoft.Dafny { Bpl.StmtList stmts;
if (!wellformednessProc) {
- if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0) {
+ if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoMethod)) {
var posts = new List<Expression>();
m.Ens.ForEach(mfe => posts.Add(mfe.E));
var allIns = new List<Formal>();
@@ -1955,10 +1934,10 @@ namespace Microsoft.Dafny { foreach (Expression p in f.Ens) {
var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f);
var splits = new List<SplitExprInfo>();
- bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, etran);
+ bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, false, etran);
foreach (var s in splits) {
- if (!s.IsFree && !RefinementToken.IsInherited(s.E.tok, currentModule)) {
- ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
+ if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule)) {
+ ens.Add(Ensures(s.E.tok, false, s.E, null, null));
}
}
}
@@ -2500,7 +2479,7 @@ namespace Microsoft.Dafny { } else if (b == Bpl.Expr.True) {
return a;
} else {
- return Bpl.Expr.And(a, b);
+ return Bpl.Expr.Binary(a.tok, BinaryOperator.Opcode.And, a, b);
}
}
@@ -2514,7 +2493,7 @@ namespace Microsoft.Dafny { } else if (b == Bpl.Expr.False) {
return a;
} else {
- return Bpl.Expr.Or(a, b);
+ return Bpl.Expr.Binary(a.tok, BinaryOperator.Opcode.Or, a, b);
}
}
@@ -2932,7 +2911,7 @@ namespace Microsoft.Dafny { builder.Add(Assert(e.Guard.tok, etran.TrExpr(e.Guard), "condition in assert expression might not hold"));
} else {
foreach (var split in ss) {
- if (!split.IsFree) {
+ if (split.IsChecked) {
builder.Add(AssertNS(split.E.tok, split.E, "condition in assert expression might not hold"));
}
}
@@ -3389,6 +3368,9 @@ namespace Microsoft.Dafny { sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 0), args, res));
sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 2), args, res));
}
+ if (f is CoPredicate) {
+ sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, f.FullCompileName + "#cert", args, res));
+ }
res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullCompileName + "#canCall", args, res);
@@ -3396,23 +3378,43 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// This method is expected to be called at most 4 times for each procedure in the program:
- /// * once with kind==0, which says to create a procedure for the wellformedness check of the
- /// method's specification
- /// * once with kind==1, which says to create the ordinary procedure for the method, always
- /// suitable for inter-module callers, and for non-refinement methods also suitable for
- /// the implementation and intra-module callers of the method
- /// * possibly once with kind==2 (allowed only if isRefinementMethod), which says to create
- /// a procedure suitable for intra-module callers of a refinement method
- /// * possibly once with kind==3 (allowed only if isRefinementMethod), which says to create
- /// a procedure suitable for the implementation of a refinement method
+ /// A method can have several translations, suitable for different purposes.
+ /// SpecWellformedness
+ /// This procedure is suitable for the wellformedness check of the
+ /// method's specification.
+ /// This means the pre- and postconditions are not filled in, since the
+ /// body of the procedure is going to check that these are well-formed in
+ /// the first place.
+ /// InterModuleCall
+ /// This procedure is suitable for inter-module callers.
+ /// This means that predicate definitions are not inlined.
+ /// IntraModuleCall
+ /// This procedure is suitable for non-co-call intra-module callers.
+ /// This means that predicates can be inlined in the usual way.
+ /// CoCall
+ /// This procedure is suitable for (intra-module) co-calls.
+ /// In these calls, some uses of copredicates may be replaced by
+ /// proof certificates. Note, unless the method is a comethod, there
+ /// is no reason to include a procedure for co-calls.
+ /// Implementation
+ /// This procedure is suitable for checking the implementation of the
+ /// method.
+ /// If the method has no body, there is no reason to include this kind
+ /// of procedure.
+ ///
+ /// Note that SpecWellformedness and Implementation have procedure implementations
+ /// but no callers, and vice versa for InterModuleCall, IntraModuleCall, and CoCall.
+ /// </summary>
+ enum MethodTranslationKind { SpecWellformedness, InterModuleCall, IntraModuleCall, CoCall, Implementation }
+
+ /// <summary>
+ /// This method is expected to be called at most once for each parameter combination, and in particular
+ /// at most once for each value of "kind".
/// </summary>
- Bpl.Procedure AddMethod(Method m, int kind, bool isRefinementMethod)
+ Bpl.Procedure AddMethod(Method m, MethodTranslationKind kind)
{
Contract.Requires(m != null);
Contract.Requires(m.EnclosingClass != null);
- Contract.Requires(0 <= kind && kind < 4);
- Contract.Requires(isRefinementMethod || kind < 2);
Contract.Requires(predef != null);
Contract.Requires(currentModule == null && codeContext == null);
Contract.Ensures(currentModule == null && codeContext == null);
@@ -3429,7 +3431,8 @@ namespace Microsoft.Dafny { Bpl.RequiresSeq req = new Bpl.RequiresSeq();
Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();
- if (kind == 0 || (kind == 1 && !isRefinementMethod) || kind == 3) { // the other cases have no need for a free precondition
+ // FREE PRECONDITIONS
+ if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation) { // the other cases have no need for a free precondition
// free requires mh == ModuleContextHeight && InMethodContext;
Bpl.Expr context = Bpl.Expr.And(
Bpl.Expr.Eq(Bpl.Expr.Literal(m.EnclosingClass.Module.Height), etran.ModuleContextHeight()),
@@ -3439,18 +3442,19 @@ namespace Microsoft.Dafny { mod.Add((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr);
mod.Add(etran.Tick());
- if (kind != 0) {
+ if (kind != MethodTranslationKind.SpecWellformedness) {
+ // USER-DEFINED SPECIFICATIONS
string comment = "user-defined preconditions";
foreach (MaybeFreeExpression p in m.Req) {
- if ((p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) || kind == 3) { // kind==3 never has callers, so no reason to bother splitting
+ if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
- if (kind == 2 && RefinementToken.IsInherited(s.E.tok, currentModule)) {
+ if ((kind == MethodTranslationKind.IntraModuleCall || kind == MethodTranslationKind.CoCall) && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this precondition was inherited into this module, so just ignore it
} else {
- req.Add(Requires(s.E.tok, s.IsFree, s.E, null, null));
+ req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, null));
// the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
}
}
@@ -3459,15 +3463,16 @@ namespace Microsoft.Dafny { }
comment = "user-defined postconditions";
foreach (MaybeFreeExpression p in m.Ens) {
- if ((p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) || (kind == 1 && isRefinementMethod) || kind == 2) { // for refinement methods, kind==1 has no implementations, and kind==2 never has implementations
- ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
+ var certEtran = kind == MethodTranslationKind.CoCall ? etran.WithCoCallCertificates : etran;
+ if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
+ ens.Add(Ensures(p.E.tok, true, certEtran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
- if (kind == 3 && RefinementToken.IsInherited(s.E.tok, currentModule)) {
+ foreach (var s in TrSplitExpr(p.E, certEtran, out splitHappened)) {
+ if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this postcondition was inherited into this module, so just ignore it
} else {
- ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
+ ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, null, null));
}
}
}
@@ -3479,14 +3484,7 @@ namespace Microsoft.Dafny { }
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
- string name;
- switch (kind) {
- case 0: name = "CheckWellformed$$" + m.FullCompileName; break;
- case 1: name = m.FullCompileName; break;
- case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;
- case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;
- default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected kind
- }
+ string name = MethodName(m, kind);
Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);
currentModule = null;
@@ -3495,6 +3493,36 @@ namespace Microsoft.Dafny { return proc;
}
+ static string MethodName(Method m, MethodTranslationKind kind) {
+ Contract.Requires(m != null);
+ switch (kind) {
+ case MethodTranslationKind.SpecWellformedness:
+ return "CheckWellformed$$" + m.FullCompileName;
+ case MethodTranslationKind.InterModuleCall:
+ return "InterModuleCall$$" + m.FullCompileName;
+ case MethodTranslationKind.IntraModuleCall:
+ return "IntraModuleCall$$" + m.FullCompileName;
+ case MethodTranslationKind.CoCall:
+ return "CoCall$$" + m.FullCompileName;
+ case MethodTranslationKind.Implementation:
+ return "Impl$$" + m.FullCompileName;
+ default:
+ Contract.Assert(false); // unexpected kind
+ throw new cce.UnreachableException();
+ }
+ }
+
+ /// <summary>
+ /// Return an expression that is like "expr", but where all atomic formulas in positive positions have been replaced
+ /// by "true", except for co-recursive copredicate calls and equality operations on codatatypes which have been
+ /// replaced by BoogieWrapper's containing "certEtran" translations of the positively occurring formulas.
+ /// </summary>
+ Expression CoMethodTrim(Expression expr, ExpressionTranslator certEtran) {
+ Contract.Requires(expr != null);
+ Contract.Requires(certEtran != null);
+ return new BoogieWrapper(certEtran.TrExpr(expr), expr.Type); // TODO
+ }
+
private void AddMethodRefinementCheck(MethodCheck methodCheck) {
// First, we generate the declaration of the procedure. This procedure has the same
@@ -3527,14 +3555,14 @@ namespace Microsoft.Dafny { } else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
- req.Add(Requires(s.E.tok, s.IsFree, s.E, null, null));
+ req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, null));
}
}
}
foreach (MaybeFreeExpression p in m.Ens) {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
- ens.Add(Ensures(s.E.tok, s.IsFree, s.E, "Error: postcondition of refined method may be violated", null));
+ ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, "Error: postcondition of refined method may be violated", null));
}
}
foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, etran.Old, etran, etran.Old)) {
@@ -3700,8 +3728,8 @@ namespace Microsoft.Dafny { foreach (Expression p in f.Ens) {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p, etran, out splitHappened)) {
- if (!s.IsFree) {
- ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
+ if (s.IsChecked) {
+ ens.Add(Ensures(s.E.tok, false, s.E, null, null));
}
}
}
@@ -4118,7 +4146,7 @@ namespace Microsoft.Dafny { builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok));
} else {
foreach (var split in ss) {
- if (!split.IsFree) {
+ if (split.IsChecked) {
var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.E.tok);
builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok));
}
@@ -4192,7 +4220,7 @@ namespace Microsoft.Dafny { foreach (var split in ss) {
if (RefinementToken.IsInherited(split.E.tok, currentModule)) {
// this postcondition was inherited into this module, so just ignore it
- } else if (!split.IsFree) {
+ } else if (split.IsChecked) {
var yieldToken = new NestedToken(s.Tok, split.E.tok);
builder.Add(AssertNS(yieldToken, split.E, "possible violation of yield-ensures condition", stmt.Tok));
}
@@ -4452,7 +4480,7 @@ namespace Microsoft.Dafny { b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));
} else {
foreach (var split in ss) {
- if (!split.IsFree) {
+ if (split.IsChecked) {
b.Add(AssertNS(s.Lines[i + 1].tok, split.E, "the calculation step between the previous line and this line might not hold"));
}
}
@@ -5027,7 +5055,7 @@ namespace Microsoft.Dafny { if (!ens.IsFree) {
bool splitHappened; // we actually don't care
foreach (var split in TrSplitExpr(ens.E, etran, out splitHappened)) {
- if (!split.IsFree) {
+ if (split.IsChecked) {
definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of parallel statement"));
}
}
@@ -5164,10 +5192,10 @@ namespace Microsoft.Dafny { } else {
foreach (var split in ss) {
var wInv = Bpl.Expr.Binary(split.E.tok, BinaryOperator.Opcode.Imp, w, split.E);
- if (split.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(split.E.tok, wInv));
- } else {
+ if (split.IsChecked) {
invariants.Add(Assert(split.E.tok, wInv, "loop invariant violation")); // TODO: it would be fine to have this use {:subsumption 0}
+ } else {
+ invariants.Add(new Bpl.AssumeCmd(split.E.tok, wInv));
}
}
}
@@ -5430,13 +5458,17 @@ namespace Microsoft.Dafny { // Check termination
ModuleDefinition module = method.EnclosingClass.Module;
+ bool isRecursiveCall = false;
if (module == currentModule) {
var caller = codeContext is Method ? (Method)codeContext : ((IteratorDecl)codeContext).Member_MoveNext;
if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(caller)) {
- bool contextDecrInferred, calleeDecrInferred;
- List<Expression> contextDecreases = MethodDecreasesWithDefault(caller, out contextDecrInferred);
- List<Expression> calleeDecreases = MethodDecreasesWithDefault(method, out calleeDecrInferred);
- CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred, null);
+ isRecursiveCall = true;
+ if (!(method is CoMethod)) {
+ bool contextDecrInferred, calleeDecrInferred;
+ List<Expression> contextDecreases = MethodDecreasesWithDefault(caller, out contextDecrInferred);
+ List<Expression> calleeDecreases = MethodDecreasesWithDefault(method, out calleeDecrInferred);
+ CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred, null);
+ }
}
}
@@ -5460,13 +5492,15 @@ namespace Microsoft.Dafny { }
// Make the call
- string name;
- if (RefinementToken.IsInherited(method.tok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
- name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName);
+ MethodTranslationKind kind;
+ if (isRecursiveCall && method is CoMethod) {
+ kind = MethodTranslationKind.CoCall;
+ } else if (RefinementToken.IsInherited(method.tok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
+ kind = MethodTranslationKind.IntraModuleCall;
} else {
- name = method.FullCompileName;
+ kind = MethodTranslationKind.InterModuleCall;
}
- Bpl.CallCmd call = new Bpl.CallCmd(tok, name, ins, outs);
+ Bpl.CallCmd call = new Bpl.CallCmd(tok, MethodName(method, kind), ins, outs);
builder.Add(call);
// Unbox results as needed
@@ -6459,6 +6493,7 @@ namespace Microsoft.Dafny { readonly Function applyLimited_CurrentFunction;
public readonly int layerOffset = 0;
public int Statistics_CustomLayerFunctionCount = 0;
+ public readonly bool ProducingCoCertificates = false;
[ContractInvariantMethod]
void ObjectInvariant()
{
@@ -6477,7 +6512,7 @@ namespace Microsoft.Dafny { /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.
/// </summary>
ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,
- Function applyLimited_CurrentFunction, int layerOffset, string modifiesFrame) {
+ Function applyLimited_CurrentFunction, int layerOffset, string modifiesFrame, bool produceCoCertificates) {
Contract.Requires(translator != null);
Contract.Requires(predef != null);
@@ -6493,6 +6528,7 @@ namespace Microsoft.Dafny { this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
this.layerOffset = layerOffset;
this.modifiesFrame = modifiesFrame;
+ this.ProducingCoCertificates = produceCoCertificates;
}
public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken)
@@ -6523,7 +6559,7 @@ namespace Microsoft.Dafny { }
public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar)
- : this(translator, predef, heap, thisVar, null, 0, "$_Frame") {
+ : this(translator, predef, heap, thisVar, null, 0, "$_Frame", false) {
Contract.Requires(translator != null);
Contract.Requires(predef != null);
Contract.Requires(heap != null);
@@ -6531,7 +6567,7 @@ namespace Microsoft.Dafny { }
public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)
- : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerOffset, modifiesFrame) {
+ : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerOffset, modifiesFrame, etran.ProducingCoCertificates) {
Contract.Requires(etran != null);
Contract.Requires(modifiesFrame != null);
}
@@ -6542,7 +6578,7 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
if (oldEtran == null) {
- oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);
+ oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerOffset, modifiesFrame, ProducingCoCertificates);
oldEtran.oldEtran = oldEtran;
}
return oldEtran;
@@ -6555,11 +6591,18 @@ namespace Microsoft.Dafny { }
}
+ public ExpressionTranslator WithCoCallCertificates {
+ get {
+ // don't bother caching it
+ return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset, modifiesFrame, true);
+ }
+ }
+
public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction) {
Contract.Requires(applyLimited_CurrentFunction != null);
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
- return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);
+ return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset, modifiesFrame, ProducingCoCertificates);
}
public ExpressionTranslator LayerOffset(int offset) {
@@ -6567,9 +6610,9 @@ namespace Microsoft.Dafny { Contract.Requires(layerOffset + offset <= 1);
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
- var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);
+ var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame, ProducingCoCertificates);
if (this.oldEtran != null) {
- var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);
+ var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame, ProducingCoCertificates);
etOld.oldEtran = etOld;
et.oldEtran = etOld;
}
@@ -6786,23 +6829,7 @@ namespace Microsoft.Dafny { } else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
- int offsetToUse = e.Function.IsRecursive ? this.layerOffset : 0;
- if (e.Function.IsRecursive) {
- Statistics_CustomLayerFunctionCount++;
- }
- string nm = FunctionName(e.Function, 1 + offsetToUse);
- if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive) {
- ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;
- if (module == cce.NonNull(applyLimited_CurrentFunction.EnclosingClass).Module) {
- if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {
- nm = FunctionName(e.Function, 0 + offsetToUse);
- }
- }
- }
- Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType(cce.NonNull(e.Type)));
- Bpl.ExprSeq args = FunctionInvocationArguments(e);
- Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);
- return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);
+ return TrFunctionCallExpr(e, ProducingCoCertificates);
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
@@ -6857,12 +6884,12 @@ namespace Microsoft.Dafny { return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);
} else if (e.E.Type.IsDatatype) {
Bpl.Expr alloc = translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);
- return Bpl.Expr.Not(alloc);
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, alloc);
} else {
// generate: x != null && !old($Heap)[x]
Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null);
Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));
- return Bpl.Expr.And(oNull, oIsFresh);
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And, oNull, oIsFresh);
}
} else if (expr is UnaryExpr) {
@@ -6914,6 +6941,9 @@ namespace Microsoft.Dafny { bOpcode = BinaryOperator.Opcode.Or; break;
case BinaryExpr.ResolvedOpcode.EqCommon:
+ if (ProducingCoCertificates && e.E0.Type.IsCoDatatype) {
+ return translator.FunctionCall(e.tok, BuiltinFunction.CoCallCertificateEq, null, e0, e1);
+ }
bOpcode = BinaryOperator.Opcode.Eq; break;
case BinaryExpr.ResolvedOpcode.NeqCommon:
bOpcode = BinaryOperator.Opcode.Neq; break;
@@ -7157,6 +7187,29 @@ namespace Microsoft.Dafny { }
}
+ public Bpl.Expr TrFunctionCallExpr(FunctionCallExpr e, bool useCertificateName) {
+ Contract.Requires(e != null);
+ int offsetToUse = e.Function.IsRecursive ? this.layerOffset : 0;
+ if (e.Function.IsRecursive) {
+ Statistics_CustomLayerFunctionCount++;
+ }
+ string nm = FunctionName(e.Function, 1 + offsetToUse);
+ if (useCertificateName && e.Function is CoPredicate) {
+ nm = e.Function.FullCompileName + "#cert";
+ } else if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive) {
+ ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;
+ if (module == cce.NonNull(applyLimited_CurrentFunction.EnclosingClass).Module) {
+ if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {
+ nm = FunctionName(e.Function, 0 + offsetToUse);
+ }
+ }
+ }
+ Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(e.tok, nm, translator.TrType(cce.NonNull(e.Type)));
+ Bpl.ExprSeq args = FunctionInvocationArguments(e);
+ Bpl.Expr result = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);
+ return CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type);
+ }
+
public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars) {
return TrBoundVariables(boundVars, bvars, false);
}
@@ -7414,9 +7467,9 @@ namespace Microsoft.Dafny { BinaryExpr bin = (BinaryExpr)s;
switch (bin.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.MultiSetUnion:
- return Bpl.Expr.Or(TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
+ return Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Or, TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
case BinaryExpr.ResolvedOpcode.MultiSetIntersection:
- return Bpl.Expr.And(TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
+ return Bpl.Expr.Binary(tok, BinaryOperator.Opcode.And, TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
default:
break;
}
@@ -7593,6 +7646,8 @@ namespace Microsoft.Dafny { MapUnion,
MapGlue,
+ CoCallCertificateEq,
+
IndexField,
MultiIndexField,
@@ -7793,6 +7848,11 @@ namespace Microsoft.Dafny { Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Map#Disjoint", typeInstantiation, args);
+ case BuiltinFunction.CoCallCertificateEq:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "CoDatatypeCertificate#Equal", typeInstantiation, args);
+
case BuiltinFunction.IndexField:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
@@ -7920,22 +7980,26 @@ namespace Microsoft.Dafny { public class SplitExprInfo
{
- public readonly bool IsFree;
+ public enum K { Free, Checked, Both }
+ public K Kind;
+ public bool IsOnlyFree { get { return Kind == K.Free; } }
+ public bool IsChecked { get { return Kind != K.Free; } }
public readonly Bpl.Expr E;
- public SplitExprInfo(bool isFree, Bpl.Expr e) {
- Contract.Requires(e != null);
- IsFree = isFree;
+ public SplitExprInfo(K kind, Bpl.Expr e) {
+ Contract.Requires(e != null && e.tok != null);
+ // TODO: Contract.Requires(kind == K.Free || e.tok.IsValid);
+ Kind = kind;
E = e;
}
}
- internal List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, out bool splitHappened) {
+ List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, out bool splitHappened) {
Contract.Requires(expr != null);
Contract.Requires(etran != null);
Contract.Ensures(Contract.Result<List<SplitExprInfo>>() != null);
var splits = new List<SplitExprInfo>();
- splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, etran);
+ splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, codeContext is CoMethod, etran);
return splits;
}
@@ -7943,8 +8007,29 @@ namespace Microsoft.Dafny { /// Tries to split the expression into tactical conjuncts (if "position") or disjuncts (if "!position").
/// If a (necessarily boolean) function call appears as a top-level conjunct, then inline the function if
/// if it declared in the current module and its height is less than "heightLimit".
+ ///
+ /// If "inCoContext", then any copredicate P(s) appearing in a positive position is interpreted as
+ /// a proof certificate P'(s) for P(s), and similarly an equality A==B on co-datatype values is interpreted as
+ /// a proof certificate A~~B for the equality. These certificate interpretations have an effect on inlining.
+ /// In particular, where P(s) would inline into:
+ /// check P(s) \/ H(s)
+ /// check P(s) \/ P(s.tail)
+ /// free P(s)
+ /// P'(s) inlines into:
+ /// check P(s) \/ H(s)
+ /// check P(s) \/ P'(s.tail)
+ /// free P'(s)
+ /// Analogously, it would be possible to inline an equality A==B into:
+ /// check A==B \/ A.head==B.head
+ /// check A==B \/ A.tail==B.tail
+ /// free A==B
+ /// but that's not done (because equalities are not ordinarily inlined). However, a proof certificate A~~B
+ /// is inline:
+ /// check A==B \/ A.head==B.head
+ /// check A==B \/ A.tail~~B.tail
+ /// free A~~B
/// </summary>
- internal bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, ExpressionTranslator etran) {
+ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, bool inCoContext, ExpressionTranslator etran) {
Contract.Requires(expr != null);
Contract.Requires(expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType));
Contract.Requires(splits != null);
@@ -7953,28 +8038,28 @@ namespace Microsoft.Dafny { if (expr is BoxingCastExpr) {
var bce = (BoxingCastExpr)expr;
var ss = new List<SplitExprInfo>();
- if (TrSplitExpr(bce.E, ss, position, heightLimit, etran)) {
+ if (TrSplitExpr(bce.E, ss, position, heightLimit, inCoContext, etran)) {
foreach (var s in ss) {
- splits.Add(new SplitExprInfo(s.IsFree, etran.CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType)));
+ splits.Add(new SplitExprInfo(s.Kind, etran.CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType)));
}
return true;
}
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
- return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, etran);
+ return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, inCoContext, etran);
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
- return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, etran);
+ return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, inCoContext, etran);
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
if (e.Op == UnaryExpr.Opcode.Not) {
var ss = new List<SplitExprInfo>();
- if (TrSplitExpr(e.E, ss, !position, heightLimit, etran)) {
+ if (TrSplitExpr(e.E, ss, !position, heightLimit, inCoContext, etran)) {
foreach (var s in ss) {
- splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));
+ splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));
}
return true;
}
@@ -7983,13 +8068,13 @@ namespace Microsoft.Dafny { } else if (expr is BinaryExpr) {
var bin = (BinaryExpr)expr;
if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
- TrSplitExpr(bin.E0, splits, position, heightLimit, etran);
- TrSplitExpr(bin.E1, splits, position, heightLimit, etran);
+ TrSplitExpr(bin.E0, splits, position, heightLimit, inCoContext, etran);
+ TrSplitExpr(bin.E1, splits, position, heightLimit, inCoContext, etran);
return true;
} else if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {
- TrSplitExpr(bin.E0, splits, position, heightLimit, etran);
- TrSplitExpr(bin.E1, splits, position, heightLimit, etran);
+ TrSplitExpr(bin.E0, splits, position, heightLimit, inCoContext, etran);
+ TrSplitExpr(bin.E1, splits, position, heightLimit, inCoContext, etran);
return true;
} else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
@@ -7997,21 +8082,57 @@ namespace Microsoft.Dafny { if (position) {
var lhs = etran.TrExpr(bin.E0);
var ss = new List<SplitExprInfo>();
- TrSplitExpr(bin.E1, ss, position, heightLimit, etran);
+ TrSplitExpr(bin.E1, ss, position, heightLimit, inCoContext, etran);
foreach (var s in ss) {
// as the source location in the following implication, use that of the translated "s"
- splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E)));
+ splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E)));
}
} else {
var ss = new List<SplitExprInfo>();
- TrSplitExpr(bin.E0, ss, !position, heightLimit, etran);
- var lhs = etran.TrExpr(bin.E1);
+ TrSplitExpr(bin.E0, ss, !position, heightLimit, inCoContext, etran);
+ var rhs = etran.TrExpr(bin.E1);
foreach (var s in ss) {
// as the source location in the following implication, use that of the translated "s"
- splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, lhs)));
+ splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));
}
}
return true;
+ } else if (inCoContext && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) {
+ var udt = (UserDefinedType)bin.E0.Type; // cast is justified by the IsCoDatatype in the guard
+ var cotype = (CoDatatypeDecl)udt.ResolvedClass; // ditto
+ // "inline" the equality, and add appropriate certificate-equality operators.
+ // For example, for possibly infinite lists:
+ // codatatype SList<T> = Nil | SCons(head: T, tail: SList<T>);
+ // produce:
+ // free A ~~ B
+ // checked A == B || (A.Nil? ==> B.Nil?)
+ // checked A == B || (A.Cons? ==> B.Cons? && A.head ~~ B.head && A.tail ~~ B.tail)
+ // where ~~ stands for either ordinary equality or, for codatatypes, certificate-equality
+
+ var certEtran = etran.WithCoCallCertificates;
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, certEtran.TrExpr(bin)));
+ // We want to use the regular etran translation for bin.E0 and bin.E1, but use the etran.WithCoCallCertificates
+ // translation for the equalities, so translate the operands here and stuff them into a BoogieWrapper.
+ var A = new BoogieWrapper(etran.TrExpr(bin.E0), bin.E0.Type);
+ var B = new BoogieWrapper(etran.TrExpr(bin.E1), bin.E1.Type);
+ var typeSubstMap = Resolver.TypeSubstitutionMap(cotype.TypeArgs, udt.TypeArgs);
+ var eq = etran.TrExpr(bin);
+ foreach (var ctor in cotype.Ctors) {
+ var a = Resolver.NewFieldSelectExpr(bin.tok, A, ctor.QueryField, typeSubstMap);
+ var b = Resolver.NewFieldSelectExpr(bin.tok, B, ctor.QueryField, typeSubstMap);
+ var lhs = certEtran.TrExpr(a);
+ var rhs = certEtran.TrExpr(b);
+ foreach (var dtor in ctor.Destructors) { // note, ctor.Destructors has a field for every constructor parameter, whether or not the parameter was named in the source
+ a = Resolver.NewFieldSelectExpr(bin.tok, A, dtor, typeSubstMap);
+ b = Resolver.NewFieldSelectExpr(bin.tok, B, dtor, typeSubstMap);
+ var q = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Eq, a, b);
+ q.ResolvedOp = Resolver.ResolveOp(q.Op, a.Type); // resolve here
+ q.Type = Type.Bool; // resolve here
+ rhs = Bpl.Expr.And(rhs, certEtran.TrExpr(q));
+ }
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, Bpl.Expr.Binary(new NestedToken(bin.tok, ctor.tok), BinaryOperator.Opcode.Or, eq, Bpl.Expr.Imp(lhs, rhs))));
+ }
+ return true;
}
} else if (expr is ITEExpr) {
@@ -8020,18 +8141,18 @@ namespace Microsoft.Dafny { var ssThen = new List<SplitExprInfo>();
var ssElse = new List<SplitExprInfo>();
// Note: The following lines intentionally uses | instead of ||, because we need both calls to TrSplitExpr
- if (TrSplitExpr(ite.Thn, ssThen, position, heightLimit, etran) | TrSplitExpr(ite.Els, ssElse, position, heightLimit, etran)) {
+ if (TrSplitExpr(ite.Thn, ssThen, position, heightLimit, inCoContext, etran) | TrSplitExpr(ite.Els, ssElse, position, heightLimit, inCoContext, etran)) {
var op = position ? BinaryOperator.Opcode.Imp : BinaryOperator.Opcode.And;
var test = etran.TrExpr(ite.Test);
foreach (var s in ssThen) {
// as the source location in the following implication, use that of the translated "s"
- splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, op, test, s.E)));
+ splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, op, test, s.E)));
}
var negatedTest = Bpl.Expr.Not(test);
foreach (var s in ssElse) {
// as the source location in the following implication, use that of the translated "s"
- splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, op, negatedTest, s.E)));
+ splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, op, negatedTest, s.E)));
}
return true;
@@ -8045,88 +8166,101 @@ namespace Microsoft.Dafny { if (position) {
var guard = etran.TrExpr(e.Guard);
var ss = new List<SplitExprInfo>();
- TrSplitExpr(e.Body, ss, position, heightLimit, etran);
+ TrSplitExpr(e.Body, ss, position, heightLimit, inCoContext, etran);
foreach (var s in ss) {
// as the source location in the following implication, use that of the translated "s"
- splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, guard, s.E)));
+ splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, guard, s.E)));
}
} else {
var ss = new List<SplitExprInfo>();
- TrSplitExpr(e.Guard, ss, !position, heightLimit, etran);
+ TrSplitExpr(e.Guard, ss, !position, heightLimit, inCoContext, etran);
var rhs = etran.TrExpr(e.Body);
foreach (var s in ss) {
// as the source location in the following implication, use that of the translated "s"
- splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));
+ splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));
}
}
return true;
} else if (expr is OldExpr) {
var e = (OldExpr)expr;
- return TrSplitExpr(e.E, splits, position, heightLimit, etran.Old);
+ return TrSplitExpr(e.E, splits, position, heightLimit, inCoContext, etran.Old);
} else if (expr is FunctionCallExpr) {
- if (position) {
- var fexp = (FunctionCallExpr)expr;
+ var fexp = (FunctionCallExpr)expr;
+ if (position && !etran.ProducingCoCertificates) {
var f = fexp.Function;
Contract.Assert(f != null); // filled in during resolution
var module = f.EnclosingClass.Module;
var functionHeight = module.CallGraph.GetSCCRepresentativeId(f);
- if (module == currentModule && functionHeight < heightLimit) {
- if (f.Body != null && !(f.Body.Resolved is MatchExpr)) {
- if (RefinementToken.IsInherited(fexp.tok, currentModule) &&
- f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition &&
- (codeContext == null || !codeContext.MustReverify)) {
- // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything
- // that needed to be proved about the function was proved already in the previous module, even without the body definition).
+ if (module == currentModule && functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) {
+ if (RefinementToken.IsInherited(fexp.tok, currentModule) &&
+ f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition &&
+ (codeContext == null || !codeContext.MustReverify)) {
+ // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything
+ // that needed to be proved about the function was proved already in the previous module, even without the body definition).
+ } else {
+ // inline this body
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ Contract.Assert(fexp.Args.Count == f.Formals.Count);
+ for (int i = 0; i < f.Formals.Count; i++) {
+ Formal p = f.Formals[i];
+ Expression arg = fexp.Args[i];
+ arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);
+ arg.Type = p.Type; // resolve here
+ substMap.Add(p, arg);
+ }
+ Expression body = Substitute(f.Body, fexp.Receiver, substMap);
+
+ // Produce, for a "body" split into b0, b1, b2:
+ // free F#canCall(args) && F(args) && (b0 && b1 && b2)
+ // checked F#canCall(args) ==> F(args) || b0
+ // checked F#canCall(args) ==> F(args) || b1
+ // checked F#canCall(args) ==> F(args) || b2
+ // For "inCoContext", split into:
+ // free F#canCall(args) && F'(args)
+ // checked F#canCall(args) ==> F(args) || b0'
+ // checked F#canCall(args) ==> F(args) || b1'
+ // checked F#canCall(args) ==> F(args) || b2'
+ // where the primes indicate certificate translations.
+
+ // F#canCall(args)
+ Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
+ ExprSeq args = etran.FunctionInvocationArguments(fexp);
+ Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
+
+ if (inCoContext && f is CoPredicate) {
+ // F'(args)
+ var fargs = etran.TrFunctionCallExpr(fexp, true);
+ // F#canCall(args) && F'(args)
+ var fr = Bpl.Expr.And(canCall, fargs);
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));
} else {
- // inline this body
- Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
- Contract.Assert(fexp.Args.Count == f.Formals.Count);
- for (int i = 0; i < f.Formals.Count; i++) {
- Formal p = f.Formals[i];
- Expression arg = fexp.Args[i];
- arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);
- arg.Type = p.Type; // resolve here
- substMap.Add(p, arg);
- }
- Expression body = Substitute(f.Body, fexp.Receiver, substMap);
-
- // Produce, for a "body" split into b0, b1, b2:
- // free F#canCall(args) && F(args) && (b0 && b1 && b2)
- // checked F#canCall(args) ==> F(args) || b0
- // checked F#canCall(args) ==> F(args) || b1
- // checked F#canCall(args) ==> F(args) || b2
- // Note that "body" does not contain limited calls.
-
- // F#canCall(args)
- Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
- ExprSeq args = etran.FunctionInvocationArguments(fexp);
- Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
-
// F(args)
- Bpl.Expr fargs = etran.TrExpr(fexp);
-
+ var fargs = etran.TrExpr(fexp);
// body
- Bpl.Expr trBody = etran.TrExpr(body);
+ var trBody = etran.TrExpr(body);
trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);
+ // F#canCall(args) && F(args) && (b0 && b1 && b2)
+ var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody));
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));
+ }
- // here goes the free piece:
- splits.Add(new SplitExprInfo(true, Bpl.Expr.Binary(trBody.tok, BinaryOperator.Opcode.And, canCall, BplAnd(fargs, trBody))));
-
- // recurse on body
- var ss = new List<SplitExprInfo>();
- TrSplitExpr(body, ss, position, functionHeight, etran);
- foreach (var s in ss) {
+ // recurse on body
+ var fargsOriginalFunction = etran.TrFunctionCallExpr(fexp, false);
+ var ss = new List<SplitExprInfo>();
+ TrSplitExpr(body, ss, position, functionHeight, inCoContext, inCoContext && f is CoPredicate ? etran.WithCoCallCertificates : etran);
+ foreach (var s in ss) {
+ if (s.IsChecked) {
var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);
- var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);
+ var bodyOrConjunct = Bpl.Expr.Or(fargsOriginalFunction, unboxedConjunct);
var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);
- splits.Add(new SplitExprInfo(s.IsFree, p));
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));
}
-
- return true;
}
+
+ return true;
}
}
}
@@ -8207,11 +8341,11 @@ namespace Microsoft.Dafny { } else {
q = new Bpl.ExistsExpr(kase.tok, bvars, Bpl.Expr.And(ante, bdy));
}
- splits.Add(new SplitExprInfo(false, q));
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, q));
}
// Finally, assume the original quantifier (forall/exists n :: P(n))
- splits.Add(new SplitExprInfo(true, etran.TrExpr(expr)));
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etran.TrExpr(expr)));
return true;
}
}
@@ -8235,7 +8369,7 @@ namespace Microsoft.Dafny { translatedExpression.tok = new ForceCheckToken(expr.tok);
splitHappened = true; // count this as a split, so this translated expression is not ignored
}
- splits.Add(new SplitExprInfo(false, translatedExpression));
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, translatedExpression));
return splitHappened;
}
@@ -8548,6 +8682,7 @@ namespace Microsoft.Dafny { }
}
+#if OLD_COINDUCTION_PRINCIPLE
void AddCoinductionPrinciple(CoPredicate coPredicate) {
Contract.Requires(coPredicate != null);
if (coPredicate.Body == null) {
@@ -8774,6 +8909,7 @@ namespace Microsoft.Dafny { return F;
}
}
+#endif
/// <summary>
/// Returns true iff 'v' occurs as a free variable in 'expr'.
@@ -8823,6 +8959,7 @@ namespace Microsoft.Dafny { return s.Substitute(expr);
}
+#if OLD_COINDUCTION_PRINCIPLE
public class CoinductionSubstituter : Substituter
{
CoPredicate coPredicate;
@@ -8995,6 +9132,7 @@ namespace Microsoft.Dafny { // TODO: in the following substitution, it may be that we also need to update the types of the resulting subexpressions (is this true for all Substitute calls?)
return Substitute(fce.Function.Body, fce.Receiver, substMap);
}
+#endif
public class FunctionCallSubstituter : Substituter
{
public readonly Function A, B;
@@ -9101,6 +9239,7 @@ namespace Microsoft.Dafny { if (receiver != e.Receiver || newArgs != e.Args) {
FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);
newFce.Function = e.Function; // resolve on the fly (and set newFce.Type below, at end)
+ newFce.CoCall = e.CoCall; // also copy the co-call status
newExpr = newFce;
}
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 2f295429..f3c158ac 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -237,6 +237,7 @@ namespace DafnyLanguage case "choose":
case "class":
case "codatatype":
+ case "comethod":
case "constructor":
case "copredicate":
case "datatype":
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e7fda470..0dd78b1e 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1327,14 +1327,44 @@ Execution trace: Dafny program verifier finished with 5 verified, 2 errors
--------------------- CoPredicates.dfy --------------------
-CoPredicates.dfy(45,1): Error BP5003: A postcondition might not hold on this return path.
-CoPredicates.dfy(44,11): Related location: This is the postcondition that might not hold.
-CoPredicates.dfy(30,22): Related location: Related location
+-------------------- CoinductiveProofs.dfy --------------------
+CoinductiveProofs.dfy(26,12): Error: assertion violation
+CoinductiveProofs.dfy(10,17): Related location: Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+CoinductiveProofs.dfy(47,1): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(46,11): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(42,3): Related location: Related location
+Execution trace:
+ (0,0): anon0
+CoinductiveProofs.dfy(79,1): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(78,11): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(68,3): Related location: Related location
+Execution trace:
+ (0,0): anon0
+CoinductiveProofs.dfy(88,12): Error: assertion violation
+CoinductiveProofs.dfy(68,3): Related location: Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+CoinductiveProofs.dfy(99,1): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(98,11): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(94,3): Related location: Related location
+Execution trace:
+ (0,0): anon0
+CoinductiveProofs.dfy(144,1): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(143,22): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(1,24): Related location: Related location
+Execution trace:
+ (0,0): anon0
+CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(1,24): Related location: Related location
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 12 verified, 1 error
+Dafny program verifier finished with 33 verified, 7 errors
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
@@ -1753,7 +1783,7 @@ Dafny program verifier finished with 38 verified, 11 errors Verifying CheckWellformed$$_0_M0.C.M ...
[0 proof obligations] verified
-Verifying _0_M0.C.M ...
+Verifying Impl$$_0_M0.C.M ...
[4 proof obligations] verified
Verifying CheckWellformed$$_0_M0.C.P ...
@@ -1776,7 +1806,7 @@ Execution trace: Verifying CheckWellformed$$_1_M1.C.M ...
[0 proof obligations] verified
-Verifying RefinementImpl_M1$$_1_M1.C.M ...
+Verifying Impl$$_1_M1.C.M ...
[0 proof obligations] verified
Verifying CheckWellformed$$_1_M1.C.P ...
diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy new file mode 100644 index 00000000..c555bc99 --- /dev/null +++ b/Test/dafny0/CoinductiveProofs.dfy @@ -0,0 +1,152 @@ +codatatype Stream<T> = Cons(head: T, tail: Stream);
+
+function Upward(n: int): Stream<int>
+{
+ Cons(n, Upward(n + 1))
+}
+
+copredicate Pos(s: Stream<int>)
+{
+ 0 < s.head && Pos(s.tail)
+}
+
+comethod PosLemma0(n: int)
+ requires 1 <= n;
+ ensures Pos(Upward(n));
+{
+ PosLemma0(n + 1); // this completes the proof
+}
+
+comethod PosLemma1(n: int)
+ requires 1 <= n;
+ ensures Pos(Upward(n));
+{
+ PosLemma1(n + 1);
+ if (*) {
+ assert Pos(Upward(n + 1)); // error: cannot conclude this here
+ }
+}
+
+comethod OutsideCaller_PosLemma(n: int)
+ requires 1 <= n;
+ ensures Pos(Upward(n));
+{
+ assert Upward(n).tail == Upward(n + 1); // follows from one unrolling of the definition of Upward
+ PosLemma0(n + 1);
+ assert Pos(Upward(n+1)); // this follows directly from the previous line, but it's not a recursive call
+}
+
+
+copredicate X(s: Stream) // this is equivalent to always returning 'true'
+{
+ X(s)
+}
+
+comethod AlwaysLemma_X0(s: Stream)
+ ensures X(s); // prove that X(s) really is always 'true'
+{ // error: this is not the right proof
+ AlwaysLemma_X0(s.tail);
+}
+
+comethod AlwaysLemma_X1(s: Stream)
+ ensures X(s); // prove that X(s) really is always 'true'
+{
+ AlwaysLemma_X1(s); // this is the right proof
+}
+
+comethod AlwaysLemma_X2(s: Stream)
+ ensures X(s);
+{
+ AlwaysLemma_X2(s);
+ if (*) {
+ assert X(s); // actually, we can conclude this here, because the X(s) we're trying to prove gets expanded
+ }
+}
+
+copredicate Y(s: Stream) // this is equivalent to always returning 'true'
+{
+ Y(s.tail)
+}
+
+comethod AlwaysLemma_Y0(s: Stream)
+ ensures Y(s); // prove that Y(s) really is always 'true'
+{
+ AlwaysLemma_Y0(s.tail); // this is a correct proof
+}
+
+comethod AlwaysLemma_Y1(s: Stream)
+ ensures Y(s);
+{ // error: this is not the right proof
+ AlwaysLemma_Y1(s);
+}
+
+comethod AlwaysLemma_Y2(s: Stream)
+ ensures Y(s);
+{
+ AlwaysLemma_Y2(s.tail);
+ if (*) {
+ assert Y(s.tail); // error: not provable here
+ }
+}
+
+copredicate Z(s: Stream)
+{
+ false
+}
+
+comethod AlwaysLemma_Z(s: Stream)
+ ensures Z(s); // says, perversely, that Z(s) is always 'true'
+{ // error: this had better not lead to a proof
+ AlwaysLemma_Z(s);
+}
+
+function Doubles(n: int): Stream<int>
+{
+ Cons(2*n, Doubles(n + 1))
+}
+
+copredicate Even(s: Stream<int>)
+{
+ s.head % 2 == 0 && Even(s.tail)
+}
+
+comethod Lemma0(n: int)
+ ensures Even(Doubles(n));
+{
+ Lemma0(n+1);
+}
+
+function UpwardBy2(n: int): Stream<int>
+{
+ Cons(n, UpwardBy2(n + 2))
+}
+
+comethod Lemma1(n: int)
+ ensures Even(UpwardBy2(2*n));
+{
+ Lemma1(n+1);
+}
+
+comethod BadTheorem(s: Stream<int>)
+//TODO: ensures false;
+{ // error: cannot establish postcondition 'false', despite the recursive call (this works because CoCall's drop all positive formulas except certificate-based ones)
+ BadTheorem(s.tail);
+}
+
+comethod ProveEquality(n: int)
+ ensures Doubles(n) == UpwardBy2(2*n);
+{
+ ProveEquality(n+1);
+}
+
+comethod BadEquality0(n: int)
+ ensures Doubles(n) == UpwardBy2(n); // error: postcondition does not hold
+{
+ BadEquality0(n+1);
+}
+
+comethod BadEquality1(n: int)
+ ensures Doubles(n) == UpwardBy2(n+1); // error: postcondition does not hold
+{
+ BadEquality1(n+1);
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 4613b085..0f63b9dc 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
TypeParameters.dfy Datatypes.dfy
- Coinductive.dfy Corecursion.dfy CoPredicates.dfy
+ Coinductive.dfy Corecursion.dfy CoinductiveProofs.dfy
TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 1ba6186b..035703cf 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -30,9 +30,9 @@ ]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "codatatype" "type" "function" "predicate" "copredicate"
- "iterator"
- "ghost" "var" "method" "constructor"
+ "class" "datatype" "codatatype" "type" "iterator"
+ "function" "predicate" "copredicate"
+ "ghost" "var" "method" "constructor" "comethod"
"module" "import" "default" "as" "opened" "static" "refines"
"returns" "yields" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index ac1b755c..2c3a650e 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -17,7 +17,7 @@ namespace Demo StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
this.MarkReservedWords( // NOTE: these keywords must also appear once more below
- "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype",
+ "class", "ghost", "static", "var", "method", "constructor", "comethod", "datatype", "codatatype",
"iterator", "type",
"assert", "assume", "new", "this", "object", "refines",
"module", "import", "as", "default", "opened",
@@ -267,6 +267,7 @@ namespace Demo | "var"
| "method"
| "constructor"
+ | "comethod"
| "datatype"
| "codatatype"
| "type"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 879b90cb..8ac9defe 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -9,7 +9,8 @@ bool,nat,int,object,set,multiset,seq,array,array2,array3,map,
function,predicate,copredicate,
ghost,var,static,refines,
- method,constructor,returns,yields,module,import,default,opened,as,in,
+ method,constructor,comethod,
+ returns,yields,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,choose,this,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 45afbcf0..fc98156a 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -5,7 +5,8 @@ syntax clear syntax case match -syntax keyword dafnyFunction function predicate copredicate method constructor +syntax keyword dafnyFunction function predicate copredicate +syntax keyword method constructor comethod syntax keyword dafnyTypeDef class datatype codatatype type iterator syntax keyword module import opened as default syntax keyword dafnyConditional if then else match case |