summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-01-10 13:23:20 -0800
committerGravatar Rustan Leino <leino@microsoft.com>2012-01-10 13:23:20 -0800
commitae8ba23b193e160d0e6363558482a8f955034775 (patch)
tree070689560ebef9cdf7168dc3ffecc5993bc928c0
parent8973c639509884d7493e1fe3f70bf3b0de8fa277 (diff)
Dafny: added predicates
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg21
-rw-r--r--Source/Dafny/DafnyAst.cs13
-rw-r--r--Source/Dafny/Parser.cs749
-rw-r--r--Source/Dafny/Printer.cs9
-rw-r--r--Source/Dafny/RefinementTransformer.cs54
-rw-r--r--Source/Dafny/Scanner.cs135
-rw-r--r--Test/dafny0/Answer9
-rw-r--r--Test/dafny0/Predicates.dfy31
-rw-r--r--Test/dafny0/runtest.bat3
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs3
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs1
-rw-r--r--Util/latex/dafny.sty2
-rw-r--r--Util/vim/syntax/dafny.vim2
14 files changed, 571 insertions, 463 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index f072747c..a6ae3855 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -518,31 +518,40 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
IToken/*!*/ id;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<Formal/*!*/> formals = new List<Formal/*!*/>();
- Type/*!*/ returnType;
+ Type/*!*/ returnType = new BoolType();
List<Expression/*!*/> reqs = new List<Expression/*!*/>();
List<Expression/*!*/> ens = new List<Expression/*!*/>();
List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
Expression/*!*/ bb; Expression body = null;
+ bool isPredicate = false;
bool isFunctionMethod = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
- "function"
+ ( "function"
+ | "predicate" (. isPredicate = true; .)
+ )
[ "method" (. isFunctionMethod = true; .)
]
- (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
+ (. if (mmod.IsGhost) { SemErr(t, (isPredicate ? "predicate" : "function") + "s cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
Formals<true, isFunctionMethod, formals>
- ":"
- Type<out returnType>
+ ( ":" (. if (isPredicate) { SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); } .)
+ Type<out returnType>
+ | (. if (!isPredicate) { SemErr(la, "functions must declare a return type; expecting \":\""); } .)
+ )
{ FunctionSpec<reqs, reads, ens, decreases> }
[ FunctionBody<out bb, out bodyStart, out bodyEnd> (. body = bb; .)
]
- (. f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);
+ (. if (isPredicate) {
+ f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);
+ } else {
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);
+ }
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
.)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 9e69b432..927191e7 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1066,7 +1066,6 @@ namespace Microsoft.Dafny {
Contract.Invariant(Decreases != null);
}
-
public Function(IToken tok, string name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter/*!*/>/*!*/ typeArgs,
[Captured] List<Formal/*!*/>/*!*/ formals, Type/*!*/ resultType, List<Expression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ reads,
List<Expression/*!*/>/*!*/ ens, Specification<Expression>/*!*/ decreases, Expression body, Attributes attributes)
@@ -1094,7 +1093,17 @@ namespace Microsoft.Dafny {
}
}
- public class Method : MemberDecl, TypeParameter.ParentType {
+ public class Predicate : Function
+ {
+ public Predicate(IToken tok, string name, bool isStatic, bool isGhost, bool isUnlimited, List<TypeParameter> typeArgs,
+ List<Formal> formals, List<Expression> req, List<FrameExpression> reads,
+ List<Expression> ens, Specification<Expression> decreases, Expression body, Attributes attributes)
+ : base(tok, name, isStatic, isGhost, isUnlimited, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes) {
+ }
+ }
+
+ public class Method : MemberDecl, TypeParameter.ParentType
+ {
public readonly bool IsGhost;
public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;
public readonly List<Formal/*!*/>/*!*/ Ins;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index cc87bdab..46d93902 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 = 103;
+ public const int maxT = 104;
const bool T = true;
const bool x = false;
@@ -305,7 +305,7 @@ bool IsAttribute() {
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 11)) {SynErr(104); Get();}
+ while (!(la.kind == 0 || la.kind == 11)) {SynErr(105); Get();}
Expect(11);
while (la.kind == 6) {
Attribute(ref attrs);
@@ -335,7 +335,7 @@ bool IsAttribute() {
List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
IToken bodyStart = Token.NoToken; // dummy assignment
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(105); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(106); Get();}
Expect(15);
while (la.kind == 6) {
Attribute(ref attrs);
@@ -351,7 +351,7 @@ bool IsAttribute() {
Get();
DatatypeMemberDecl(ctors);
}
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(106); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(107); Get();}
Expect(18);
dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
@@ -369,7 +369,7 @@ bool IsAttribute() {
}
Ident(out id);
at = new ArbitraryTypeDecl(id, id.val, module, attrs);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(107); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(108); Get();}
Expect(18);
}
@@ -393,13 +393,13 @@ bool IsAttribute() {
}
if (la.kind == 19) {
FieldDecl(mmod, mm);
- } else if (la.kind == 41) {
+ } else if (la.kind == 41 || la.kind == 42) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (la.kind == 24 || la.kind == 25) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(108);
+ } else SynErr(109);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -421,7 +421,7 @@ bool IsAttribute() {
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 19)) {SynErr(109); Get();}
+ while (!(la.kind == 0 || la.kind == 19)) {SynErr(110); Get();}
Expect(19);
if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -436,7 +436,7 @@ bool IsAttribute() {
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(110); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(111); Get();}
Expect(18);
}
@@ -446,22 +446,28 @@ bool IsAttribute() {
IToken/*!*/ id;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<Formal/*!*/> formals = new List<Formal/*!*/>();
- Type/*!*/ returnType;
+ Type/*!*/ returnType = new BoolType();
List<Expression/*!*/> reqs = new List<Expression/*!*/>();
List<Expression/*!*/> ens = new List<Expression/*!*/>();
List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
Expression/*!*/ bb; Expression body = null;
+ bool isPredicate = false;
bool isFunctionMethod = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- Expect(41);
+ if (la.kind == 41) {
+ Get();
+ } else if (la.kind == 42) {
+ Get();
+ isPredicate = true;
+ } else SynErr(112);
if (la.kind == 24) {
Get();
isFunctionMethod = true;
}
- if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
+ if (mmod.IsGhost) { SemErr(t, (isPredicate ? "predicate" : "function") + "s cannot be declared 'ghost' (they are ghost by default)"); }
while (la.kind == 6) {
Attribute(ref attrs);
@@ -471,16 +477,25 @@ bool IsAttribute() {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals);
- Expect(5);
- Type(out returnType);
- while (StartOf(3)) {
+ if (la.kind == 5) {
+ Get();
+ if (isPredicate) { SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); }
+ Type(out returnType);
+ } else if (StartOf(3)) {
+ if (!isPredicate) { SemErr(la, "functions must declare a return type; expecting \":\""); }
+ } else SynErr(113);
+ while (StartOf(4)) {
FunctionSpec(reqs, reads, ens, decreases);
}
if (la.kind == 6) {
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
}
- f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);
+ if (isPredicate) {
+ f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);
+ } else {
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);
+ }
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
@@ -504,7 +519,7 @@ bool IsAttribute() {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(111); Get();}
+ while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(114); Get();}
if (la.kind == 24) {
Get();
} else if (la.kind == 25) {
@@ -515,7 +530,7 @@ bool IsAttribute() {
SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(112);
+ } else SynErr(115);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
if (mmod.IsGhost) {
@@ -539,7 +554,7 @@ bool IsAttribute() {
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs);
}
- while (StartOf(4)) {
+ while (StartOf(5)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
if (la.kind == 6) {
@@ -574,7 +589,7 @@ bool IsAttribute() {
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
Expect(32);
- if (StartOf(5)) {
+ if (StartOf(6)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
while (la.kind == 20) {
@@ -719,7 +734,7 @@ bool IsAttribute() {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(113); break;
+ default: SynErr(116); break;
}
}
@@ -743,13 +758,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(6))) {SynErr(114); Get();}
+ while (!(StartOf(7))) {SynErr(117); Get();}
if (la.kind == 27) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
}
- if (StartOf(7)) {
+ if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 20) {
@@ -758,7 +773,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(115); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(118); Get();}
Expect(18);
} else if (la.kind == 28 || la.kind == 29 || la.kind == 30) {
if (la.kind == 28) {
@@ -768,7 +783,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 29) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(116); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(119); Get();}
Expect(18);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 30) {
@@ -777,19 +792,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Attribute(ref ensAttrs);
}
Expression(out e);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(117); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(120); Get();}
Expect(18);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(118);
+ } else SynErr(121);
} else if (la.kind == 31) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(119); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(122); Get();}
Expect(18);
- } else SynErr(120);
+ } else SynErr(123);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -798,7 +813,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(6);
bodyStart = t;
- while (StartOf(8)) {
+ while (StartOf(9)) {
Stmt(body);
}
Expect(7);
@@ -809,7 +824,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
- if (la.kind == 44) {
+ if (la.kind == 45) {
Get();
Ident(out id);
fieldName = id.val;
@@ -883,22 +898,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(121);
+ } else SynErr(124);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 29) {
- while (!(la.kind == 0 || la.kind == 29)) {SynErr(122); Get();}
+ while (!(la.kind == 0 || la.kind == 29)) {SynErr(125); Get();}
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(123); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();}
Expect(18);
reqs.Add(e);
- } else if (la.kind == 42) {
+ } else if (la.kind == 43) {
Get();
- if (StartOf(9)) {
+ if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
while (la.kind == 20) {
@@ -907,20 +922,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(124); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(127); Get();}
Expect(18);
} else if (la.kind == 30) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(128); Get();}
Expect(18);
ens.Add(e);
} else if (la.kind == 31) {
Get();
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(129); Get();}
Expect(18);
- } else SynErr(127);
+ } else SynErr(130);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -934,23 +949,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 == 43) {
+ if (la.kind == 44) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(128);
+ } else SynErr(131);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
e = new WildcardExpr(t);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
- } else SynErr(129);
+ } else SynErr(132);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -966,25 +981,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(10))) {SynErr(130); Get();}
+ while (!(StartOf(11))) {SynErr(133); Get();}
switch (la.kind) {
case 6: {
BlockStmt(out s, out bodyStart, out bodyEnd);
break;
}
- case 61: {
+ case 62: {
AssertStmt(out s);
break;
}
- case 62: {
+ case 63: {
AssumeStmt(out s);
break;
}
- case 63: {
+ case 64: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 17: case 32: case 88: case 89: case 90: case 91: case 92: case 93: case 94: {
+ case 1: case 2: case 17: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
UpdateStmt(out s);
break;
}
@@ -992,23 +1007,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
VarDeclStatement(out s);
break;
}
- case 54: {
+ case 55: {
IfStmt(out s);
break;
}
- case 58: {
+ case 59: {
WhileStmt(out s);
break;
}
- case 60: {
+ case 61: {
MatchStmt(out s);
break;
}
- case 64: {
+ case 65: {
ParallelStmt(out s);
break;
}
- case 45: {
+ case 46: {
Get();
x = t;
Ident(out id);
@@ -1017,34 +1032,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s.Labels = new LabelNode(x, id.val, s.Labels);
break;
}
- case 46: {
+ case 47: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- } else if (la.kind == 18 || la.kind == 46) {
- while (la.kind == 46) {
+ } else if (la.kind == 18 || la.kind == 47) {
+ while (la.kind == 47) {
Get();
breakCount++;
}
- } else SynErr(131);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(132); Get();}
+ } else SynErr(134);
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();}
Expect(18);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 47: {
+ case 48: {
ReturnStmt(out s);
break;
}
- default: SynErr(133); break;
+ default: SynErr(136); break;
}
}
void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; Attributes attrs = null;
- Expect(61);
+ Expect(62);
x = t; s = null;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1056,7 +1071,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(62);
+ Expect(63);
x = t;
Expression(out e);
Expect(18);
@@ -1067,7 +1082,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(63);
+ Expect(64);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1096,14 +1111,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(18);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 20 || la.kind == 48) {
+ } else if (la.kind == 20 || la.kind == 49) {
lhss.Add(e); lhs0 = e;
while (la.kind == 20) {
Get();
Lhs(out e);
lhss.Add(e);
}
- Expect(48);
+ Expect(49);
x = t;
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1116,7 +1131,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(134);
+ } else SynErr(137);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1140,7 +1155,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1179,26 +1194,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(54);
+ Expect(55);
x = t;
if (la.kind == 32) {
Guard(out guard);
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
- if (la.kind == 54) {
+ if (la.kind == 55) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(135);
+ } else SynErr(138);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 6) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(136);
+ } else SynErr(139);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1214,7 +1229,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(58);
+ Expect(59);
x = t;
if (la.kind == 32) {
Guard(out guard);
@@ -1222,22 +1237,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
BlockStmt(out body, out bodyStart, out bodyEnd);
stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
- } else if (StartOf(11)) {
+ } else if (StartOf(12)) {
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(137);
+ } else SynErr(140);
}
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(60);
+ Expect(61);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 56) {
+ while (la.kind == 57) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1257,7 +1272,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Statement/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(64);
+ Expect(65);
x = t;
Expect(32);
QuantifierDomain(out bvars, out attrs, out range);
@@ -1283,9 +1298,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(47);
+ Expect(48);
returnTok = t;
- if (StartOf(12)) {
+ if (StartOf(13)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 20) {
@@ -1307,16 +1322,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = null; // to please compiler
Attributes attrs = null;
- if (la.kind == 49) {
+ if (la.kind == 50) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 50 || la.kind == 52) {
- if (la.kind == 50) {
+ if (la.kind == 51 || la.kind == 53) {
+ if (la.kind == 51) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(51);
+ Expect(52);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
@@ -1324,7 +1339,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out x);
Expect(32);
args = new List<Expression/*!*/>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(33);
@@ -1338,18 +1353,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
r = new HavocRhs(t);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(138);
+ } else SynErr(141);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1361,16 +1376,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
- } else if (StartOf(13)) {
+ } else if (StartOf(14)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
- } else SynErr(139);
+ } else SynErr(142);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1387,13 +1402,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
Expect(32);
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
e = null;
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(140);
+ } else SynErr(143);
Expect(33);
}
@@ -1404,13 +1419,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Statement> body;
Expect(6);
- while (la.kind == 56) {
+ while (la.kind == 57) {
Get();
x = t;
Expression(out e);
- Expect(57);
+ Expect(58);
body = new List<Statement>();
- while (StartOf(8)) {
+ while (StartOf(9)) {
Stmt(body);
}
alternatives.Add(new GuardedAlternative(x, e, body));
@@ -1425,29 +1440,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(14)) {
- if (la.kind == 28 || la.kind == 59) {
+ while (StartOf(15)) {
+ if (la.kind == 28 || la.kind == 60) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(141); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(144); Get();}
Expect(18);
invariants.Add(invariant);
} else if (la.kind == 31) {
- while (!(la.kind == 0 || la.kind == 31)) {SynErr(142); Get();}
+ while (!(la.kind == 0 || la.kind == 31)) {SynErr(145); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(143); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(146); Get();}
Expect(18);
} else {
- while (!(la.kind == 0 || la.kind == 27)) {SynErr(144); Get();}
+ while (!(la.kind == 0 || la.kind == 27)) {SynErr(147); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
}
mod = mod ?? new List<FrameExpression>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 20) {
@@ -1456,7 +1471,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(145); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(148); Get();}
Expect(18);
}
}
@@ -1464,12 +1479,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 == 28 || la.kind == 59)) {SynErr(146); Get();}
+ while (!(la.kind == 0 || la.kind == 28 || la.kind == 60)) {SynErr(149); Get();}
if (la.kind == 28) {
Get();
isFree = true;
}
- Expect(59);
+ Expect(60);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1484,7 +1499,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(56);
+ Expect(57);
x = t;
Ident(out id);
if (la.kind == 32) {
@@ -1498,8 +1513,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(33);
}
- Expect(57);
- while (StartOf(8)) {
+ Expect(58);
+ while (StartOf(9)) {
Stmt(body);
}
c = new MatchCaseStmt(x, id.val, arguments, body);
@@ -1510,10 +1525,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(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(147);
+ } else SynErr(150);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1541,7 +1556,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 65 || la.kind == 66) {
+ while (la.kind == 66 || la.kind == 67) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1552,7 +1567,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 == 67 || la.kind == 68) {
+ if (la.kind == 68 || la.kind == 69) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1561,23 +1576,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void EquivOp() {
- if (la.kind == 65) {
+ if (la.kind == 66) {
Get();
- } else if (la.kind == 66) {
+ } else if (la.kind == 67) {
Get();
- } else SynErr(148);
+ } else SynErr(151);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(15)) {
- if (la.kind == 69 || la.kind == 70) {
+ if (StartOf(16)) {
+ if (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 69 || la.kind == 70) {
+ while (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1588,7 +1603,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 == 71 || la.kind == 72) {
+ while (la.kind == 72 || la.kind == 73) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1599,11 +1614,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void ImpliesOp() {
- if (la.kind == 67) {
+ if (la.kind == 68) {
Get();
- } else if (la.kind == 68) {
+ } else if (la.kind == 69) {
Get();
- } else SynErr(149);
+ } else SynErr(152);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1620,7 +1635,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Term(out e0);
e = e0;
- if (StartOf(16)) {
+ if (StartOf(17)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
@@ -1628,7 +1643,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(16)) {
+ while (StartOf(17)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1697,25 +1712,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void AndOp() {
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
- } else if (la.kind == 70) {
+ } else if (la.kind == 71) {
Get();
- } else SynErr(150);
+ } else SynErr(153);
}
void OrOp() {
- if (la.kind == 71) {
+ if (la.kind == 72) {
Get();
- } else if (la.kind == 72) {
+ } else if (la.kind == 73) {
Get();
- } else SynErr(151);
+ } else SynErr(154);
}
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 == 83 || la.kind == 84) {
+ while (la.kind == 84 || la.kind == 85) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1728,7 +1743,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken y;
switch (la.kind) {
- case 73: {
+ case 74: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1743,35 +1758,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 74: {
+ case 75: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 75: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 76: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 77: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 78: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 78) {
+ if (la.kind == 79) {
Get();
y = t;
}
@@ -1786,29 +1801,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(152); break;
+ default: SynErr(155); 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 == 43 || la.kind == 85 || la.kind == 86) {
+ while (la.kind == 44 || la.kind == 86 || la.kind == 87) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1817,44 +1832,44 @@ 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 == 83) {
+ if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 84) {
+ } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(153);
+ } else SynErr(156);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 84: {
+ case 85: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 79: case 87: {
+ case 80: case 88: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 19: case 37: case 54: case 60: case 61: case 62: case 97: case 98: case 99: case 100: {
+ case 19: case 37: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
break;
}
- case 6: case 50: {
+ case 6: case 51: {
DisplayExpr(out e);
break;
}
@@ -1862,37 +1877,37 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
MultiSetExpr(out e);
break;
}
- case 2: case 17: case 32: case 88: case 89: case 90: case 91: case 92: case 93: case 94: {
+ case 2: case 17: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
ConstAtomExpression(out e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
break;
}
- default: SynErr(154); break;
+ default: SynErr(157); 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 == 43) {
+ if (la.kind == 44) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 85) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 86) {
+ } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(155);
+ } else SynErr(158);
}
void NegOp() {
- if (la.kind == 79) {
+ if (la.kind == 80) {
Get();
- } else if (la.kind == 87) {
+ } else if (la.kind == 88) {
Get();
- } else SynErr(156);
+ } else SynErr(159);
}
void EndlessExpression(out Expression e) {
@@ -1903,22 +1918,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<BoundVar> letVars; List<Expression> letRHSs;
switch (la.kind) {
- case 54: {
+ case 55: {
Get();
x = t;
Expression(out e);
- Expect(95);
+ Expect(96);
Expression(out e0);
- Expect(55);
+ Expect(56);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 60: {
+ case 61: {
MatchExpression(out e);
break;
}
- case 97: case 98: case 99: case 100: {
+ case 98: case 99: case 100: case 101: {
QuantifierGuts(out e);
break;
}
@@ -1926,7 +1941,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ComprehensionExpr(out e);
break;
}
- case 61: {
+ case 62: {
Get();
x = t;
Expression(out e0);
@@ -1935,7 +1950,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new AssertExpr(x, e0, e1);
break;
}
- case 62: {
+ case 63: {
Get();
x = t;
Expression(out e0);
@@ -1956,7 +1971,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(48);
+ Expect(49);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 20) {
@@ -1969,7 +1984,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new LetExpr(x, letVars, letRHSs, e);
break;
}
- default: SynErr(157); break;
+ default: SynErr(160); break;
}
}
@@ -1980,7 +1995,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
idents.Add(id);
- while (la.kind == 52) {
+ while (la.kind == 53) {
Get();
Ident(out id);
idents.Add(id);
@@ -1988,7 +2003,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 32) {
Get();
openParen = t; args = new List<Expression>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(33);
@@ -2002,37 +2017,37 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
Ident(out id);
if (la.kind == 32) {
Get();
args = new List<Expression/*!*/>(); func = true;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(33);
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (la.kind == 50) {
+ } else if (la.kind == 51) {
Get();
x = t;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
anyDots = true;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 48) {
+ } else if (la.kind == 49) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 20 || la.kind == 51) {
+ } else if (la.kind == 20 || la.kind == 52) {
while (la.kind == 20) {
Get();
Expression(out ee);
@@ -2043,15 +2058,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
multipleIndices.Add(ee);
}
- } else SynErr(158);
- } else if (la.kind == 96) {
+ } else SynErr(161);
+ } else if (la.kind == 97) {
Get();
anyDots = true;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(159);
+ } else SynErr(162);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2074,8 +2089,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- Expect(51);
- } else SynErr(160);
+ Expect(52);
+ } else SynErr(163);
}
void DisplayExpr(out Expression e) {
@@ -2086,20 +2101,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 6) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 50) {
+ } else if (la.kind == 51) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(51);
- } else SynErr(161);
+ Expect(52);
+ } else SynErr(164);
}
void MultiSetExpr(out Expression e) {
@@ -2112,7 +2127,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 6) {
Get();
elements = new List<Expression/*!*/>();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new MultiSetDisplayExpr(x, elements);
@@ -2123,9 +2138,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e);
e = new MultiSetFormingExpr(x, e);
Expect(33);
- } else if (StartOf(17)) {
+ } else if (StartOf(18)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(162);
+ } else SynErr(165);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2134,17 +2149,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
switch (la.kind) {
- case 88: {
+ case 89: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 89: {
+ case 90: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 90: {
+ case 91: {
Get();
e = new LiteralExpr(t);
break;
@@ -2154,12 +2169,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new LiteralExpr(t, n);
break;
}
- case 91: {
+ case 92: {
Get();
e = new ThisExpr(t);
break;
}
- case 92: {
+ case 93: {
Get();
x = t;
Expect(32);
@@ -2168,7 +2183,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new FreshExpr(x, e);
break;
}
- case 93: {
+ case 94: {
Get();
x = t;
Expect(32);
@@ -2177,7 +2192,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new AllocatedExpr(x, e);
break;
}
- case 94: {
+ case 95: {
Get();
x = t;
Expect(32);
@@ -2202,7 +2217,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(33);
break;
}
- default: SynErr(163); break;
+ default: SynErr(166); break;
}
}
@@ -2221,10 +2236,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(60);
+ Expect(61);
x = t;
Expression(out e);
- while (la.kind == 56) {
+ while (la.kind == 57) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2239,13 +2254,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression/*!*/ body;
- if (la.kind == 97 || la.kind == 98) {
+ if (la.kind == 98 || la.kind == 99) {
Forall();
x = t; univ = true;
- } else if (la.kind == 99 || la.kind == 100) {
+ } else if (la.kind == 100 || la.kind == 101) {
Exists();
x = t;
- } else SynErr(164);
+ } else SynErr(167);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -2276,7 +2291,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(17);
Expression(out range);
- if (la.kind == 101 || la.kind == 102) {
+ if (la.kind == 102 || la.kind == 103) {
QSep();
Expression(out body);
}
@@ -2291,7 +2306,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(56);
+ Expect(57);
x = t;
Ident(out id);
if (la.kind == 32) {
@@ -2305,33 +2320,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(33);
}
- Expect(57);
+ Expect(58);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 97) {
+ if (la.kind == 98) {
Get();
- } else if (la.kind == 98) {
+ } else if (la.kind == 99) {
Get();
- } else SynErr(165);
+ } else SynErr(168);
}
void Exists() {
- if (la.kind == 99) {
+ if (la.kind == 100) {
Get();
- } else if (la.kind == 100) {
+ } else if (la.kind == 101) {
Get();
- } else SynErr(166);
+ } else SynErr(169);
}
void QSep() {
- if (la.kind == 101) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 103) {
Get();
- } else SynErr(167);
+ } else SynErr(170);
}
void AttributeBody(ref Attributes attrs) {
@@ -2342,7 +2357,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(5);
Expect(1);
aName = t.val;
- if (StartOf(18)) {
+ if (StartOf(19)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 20) {
@@ -2366,25 +2381,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, x,x,x,T, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,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,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, T,x,x,T, T,T,T,T, x,x,x,T, x,T,x,x, T,T,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, T,T,T,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,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,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,x,T, x,x,x,x, 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,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},
- {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,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,T,x,T, 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,T,x, x,x,T,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, x,x,x,x, T,x,x,T, 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, T,x,x,x, x,T,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,T,T,T, x,x,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,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,T,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, x,x,x,x, T,x,x,T, 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, x,x,x,x, T,x,x,x, x,T,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,T,T,T, x,x,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,x, T,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,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,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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,T, x,x,x,x, x,T,T,x, x,T,T,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, x,x,x,x, T,x,x,T, 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,T,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, 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,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,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,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,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,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,T, x,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,T,x, 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,T,x,T, 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,T,x, x,x,T,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, x,x,x,x, T,x,x,T, 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, x,x,x,T, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,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, 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, T,x,x,T, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,T, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,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,T,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,T, x,x,x,T, 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,x,x,x, x,T,x,x, T,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, T,x,x,x, x,T,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, T,x,x,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, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, 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,x,x,x, x,T,x,x, T,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, x,x,x,x, T,x,x,x, x,T,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, T,x,x,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, x,T,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,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, 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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, 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,x,x,x, x,T,x,x, T,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,T,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,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,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, 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,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,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,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,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,T, x,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,T,x,T, 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,T, x,x,x,T, 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,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
@@ -2449,132 +2465,135 @@ public class Errors {
case 39: s = "\"seq\" expected"; break;
case 40: s = "\"object\" expected"; break;
case 41: s = "\"function\" expected"; break;
- case 42: s = "\"reads\" expected"; break;
- case 43: s = "\"*\" expected"; break;
- case 44: s = "\"`\" expected"; break;
- case 45: s = "\"label\" expected"; break;
- case 46: s = "\"break\" expected"; break;
- case 47: s = "\"return\" expected"; break;
- case 48: s = "\":=\" expected"; break;
- case 49: s = "\"new\" expected"; break;
- case 50: s = "\"[\" expected"; break;
- case 51: s = "\"]\" expected"; break;
- case 52: s = "\".\" expected"; break;
- case 53: s = "\"choose\" expected"; break;
- case 54: s = "\"if\" expected"; break;
- case 55: s = "\"else\" expected"; break;
- case 56: s = "\"case\" expected"; break;
- case 57: s = "\"=>\" expected"; break;
- case 58: s = "\"while\" expected"; break;
- case 59: s = "\"invariant\" expected"; break;
- case 60: s = "\"match\" expected"; break;
- case 61: s = "\"assert\" expected"; break;
- case 62: s = "\"assume\" expected"; break;
- case 63: s = "\"print\" expected"; break;
- case 64: s = "\"parallel\" expected"; break;
- case 65: s = "\"<==>\" expected"; break;
- case 66: s = "\"\\u21d4\" expected"; break;
- case 67: s = "\"==>\" expected"; break;
- case 68: s = "\"\\u21d2\" expected"; break;
- case 69: s = "\"&&\" expected"; break;
- case 70: s = "\"\\u2227\" expected"; break;
- case 71: s = "\"||\" expected"; break;
- case 72: s = "\"\\u2228\" expected"; break;
- case 73: s = "\"==\" expected"; break;
- case 74: s = "\"<=\" expected"; break;
- case 75: s = "\">=\" expected"; break;
- case 76: s = "\"!=\" expected"; break;
- case 77: s = "\"!!\" expected"; break;
- case 78: s = "\"in\" expected"; break;
- case 79: s = "\"!\" expected"; break;
- case 80: s = "\"\\u2260\" expected"; break;
- case 81: s = "\"\\u2264\" expected"; break;
- case 82: s = "\"\\u2265\" expected"; break;
- case 83: s = "\"+\" expected"; break;
- case 84: s = "\"-\" expected"; break;
- case 85: s = "\"/\" expected"; break;
- case 86: s = "\"%\" expected"; break;
- case 87: s = "\"\\u00ac\" expected"; break;
- case 88: s = "\"false\" expected"; break;
- case 89: s = "\"true\" expected"; break;
- case 90: s = "\"null\" expected"; break;
- case 91: s = "\"this\" expected"; break;
- case 92: s = "\"fresh\" expected"; break;
- case 93: s = "\"allocated\" expected"; break;
- case 94: s = "\"old\" expected"; break;
- case 95: s = "\"then\" expected"; break;
- case 96: s = "\"..\" expected"; break;
- case 97: s = "\"forall\" expected"; break;
- case 98: s = "\"\\u2200\" expected"; break;
- case 99: s = "\"exists\" expected"; break;
- case 100: s = "\"\\u2203\" expected"; break;
- case 101: s = "\"::\" expected"; break;
- case 102: s = "\"\\u2022\" expected"; break;
- case 103: s = "??? expected"; break;
- case 104: s = "this symbol not expected in ClassDecl"; break;
- case 105: s = "this symbol not expected in DatatypeDecl"; break;
+ case 42: s = "\"predicate\" expected"; break;
+ case 43: s = "\"reads\" expected"; break;
+ case 44: s = "\"*\" expected"; break;
+ case 45: s = "\"`\" expected"; break;
+ case 46: s = "\"label\" expected"; break;
+ case 47: s = "\"break\" expected"; break;
+ case 48: s = "\"return\" expected"; break;
+ case 49: s = "\":=\" expected"; break;
+ case 50: s = "\"new\" expected"; break;
+ case 51: s = "\"[\" expected"; break;
+ case 52: s = "\"]\" expected"; break;
+ case 53: s = "\".\" expected"; break;
+ case 54: s = "\"choose\" expected"; break;
+ case 55: s = "\"if\" expected"; break;
+ case 56: s = "\"else\" expected"; break;
+ case 57: s = "\"case\" expected"; break;
+ case 58: s = "\"=>\" expected"; break;
+ case 59: s = "\"while\" expected"; break;
+ case 60: s = "\"invariant\" expected"; break;
+ case 61: s = "\"match\" expected"; break;
+ case 62: s = "\"assert\" expected"; break;
+ case 63: s = "\"assume\" expected"; break;
+ case 64: s = "\"print\" expected"; break;
+ case 65: s = "\"parallel\" expected"; break;
+ case 66: s = "\"<==>\" expected"; break;
+ case 67: s = "\"\\u21d4\" expected"; break;
+ case 68: s = "\"==>\" expected"; break;
+ case 69: s = "\"\\u21d2\" expected"; break;
+ case 70: s = "\"&&\" expected"; break;
+ case 71: s = "\"\\u2227\" expected"; break;
+ case 72: s = "\"||\" expected"; break;
+ case 73: s = "\"\\u2228\" expected"; break;
+ case 74: s = "\"==\" expected"; break;
+ case 75: s = "\"<=\" expected"; break;
+ case 76: s = "\">=\" expected"; break;
+ case 77: s = "\"!=\" expected"; break;
+ case 78: s = "\"!!\" expected"; break;
+ case 79: s = "\"in\" expected"; break;
+ case 80: s = "\"!\" expected"; break;
+ case 81: s = "\"\\u2260\" expected"; break;
+ case 82: s = "\"\\u2264\" expected"; break;
+ case 83: s = "\"\\u2265\" expected"; break;
+ case 84: s = "\"+\" expected"; break;
+ case 85: s = "\"-\" expected"; break;
+ case 86: s = "\"/\" expected"; break;
+ case 87: s = "\"%\" expected"; break;
+ case 88: s = "\"\\u00ac\" expected"; break;
+ case 89: s = "\"false\" expected"; break;
+ case 90: s = "\"true\" expected"; break;
+ case 91: s = "\"null\" expected"; break;
+ case 92: s = "\"this\" expected"; break;
+ case 93: s = "\"fresh\" expected"; break;
+ case 94: s = "\"allocated\" expected"; break;
+ case 95: s = "\"old\" expected"; break;
+ case 96: s = "\"then\" expected"; break;
+ case 97: s = "\"..\" expected"; break;
+ case 98: s = "\"forall\" expected"; break;
+ case 99: s = "\"\\u2200\" expected"; break;
+ case 100: s = "\"exists\" expected"; break;
+ case 101: s = "\"\\u2203\" expected"; break;
+ case 102: s = "\"::\" expected"; break;
+ case 103: s = "\"\\u2022\" expected"; break;
+ case 104: s = "??? expected"; break;
+ case 105: s = "this symbol not expected in ClassDecl"; break;
case 106: s = "this symbol not expected in DatatypeDecl"; break;
- case 107: s = "this symbol not expected in ArbitraryTypeDecl"; break;
- case 108: s = "invalid ClassMemberDecl"; break;
- case 109: s = "this symbol not expected in FieldDecl"; break;
+ case 107: s = "this symbol not expected in DatatypeDecl"; break;
+ case 108: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 109: s = "invalid ClassMemberDecl"; break;
case 110: s = "this symbol not expected in FieldDecl"; break;
- case 111: s = "this symbol not expected in MethodDecl"; break;
- case 112: s = "invalid MethodDecl"; break;
- case 113: s = "invalid TypeAndToken"; break;
- case 114: s = "this symbol not expected in MethodSpec"; break;
- case 115: s = "this symbol not expected in MethodSpec"; break;
- case 116: s = "this symbol not expected in MethodSpec"; break;
+ case 111: s = "this symbol not expected in FieldDecl"; break;
+ case 112: s = "invalid FunctionDecl"; break;
+ case 113: s = "invalid FunctionDecl"; break;
+ case 114: s = "this symbol not expected in MethodDecl"; break;
+ case 115: s = "invalid MethodDecl"; break;
+ case 116: s = "invalid TypeAndToken"; break;
case 117: s = "this symbol not expected in MethodSpec"; break;
- case 118: s = "invalid MethodSpec"; break;
+ case 118: s = "this symbol not expected in MethodSpec"; break;
case 119: s = "this symbol not expected in MethodSpec"; break;
- case 120: s = "invalid MethodSpec"; break;
- case 121: s = "invalid ReferenceType"; break;
- case 122: s = "this symbol not expected in FunctionSpec"; break;
- case 123: s = "this symbol not expected in FunctionSpec"; break;
- case 124: s = "this symbol not expected in FunctionSpec"; break;
+ case 120: s = "this symbol not expected in MethodSpec"; break;
+ case 121: s = "invalid MethodSpec"; break;
+ case 122: s = "this symbol not expected in MethodSpec"; break;
+ case 123: s = "invalid MethodSpec"; break;
+ case 124: s = "invalid ReferenceType"; break;
case 125: s = "this symbol not expected in FunctionSpec"; break;
case 126: s = "this symbol not expected in FunctionSpec"; break;
- case 127: s = "invalid FunctionSpec"; break;
- case 128: s = "invalid PossiblyWildFrameExpression"; break;
- case 129: s = "invalid PossiblyWildExpression"; break;
- case 130: s = "this symbol not expected in OneStmt"; break;
- case 131: s = "invalid OneStmt"; break;
- case 132: s = "this symbol not expected in OneStmt"; break;
- case 133: s = "invalid OneStmt"; break;
- case 134: s = "invalid UpdateStmt"; break;
- case 135: s = "invalid IfStmt"; break;
- case 136: s = "invalid IfStmt"; break;
- case 137: s = "invalid WhileStmt"; break;
- case 138: s = "invalid Rhs"; break;
- case 139: s = "invalid Lhs"; break;
- case 140: s = "invalid Guard"; break;
- case 141: s = "this symbol not expected in LoopSpec"; break;
- case 142: s = "this symbol not expected in LoopSpec"; break;
- case 143: s = "this symbol not expected in LoopSpec"; break;
+ case 127: s = "this symbol not expected in FunctionSpec"; break;
+ case 128: s = "this symbol not expected in FunctionSpec"; break;
+ case 129: s = "this symbol not expected in FunctionSpec"; break;
+ case 130: s = "invalid FunctionSpec"; break;
+ case 131: s = "invalid PossiblyWildFrameExpression"; break;
+ case 132: s = "invalid PossiblyWildExpression"; break;
+ case 133: s = "this symbol not expected in OneStmt"; break;
+ case 134: s = "invalid OneStmt"; break;
+ case 135: s = "this symbol not expected in OneStmt"; break;
+ case 136: s = "invalid OneStmt"; break;
+ case 137: s = "invalid UpdateStmt"; break;
+ case 138: s = "invalid IfStmt"; break;
+ case 139: s = "invalid IfStmt"; break;
+ case 140: s = "invalid WhileStmt"; break;
+ case 141: s = "invalid Rhs"; break;
+ case 142: s = "invalid Lhs"; break;
+ case 143: s = "invalid Guard"; break;
case 144: s = "this symbol not expected in LoopSpec"; break;
case 145: s = "this symbol not expected in LoopSpec"; break;
- case 146: s = "this symbol not expected in Invariant"; break;
- case 147: s = "invalid AttributeArg"; break;
- case 148: s = "invalid EquivOp"; break;
- case 149: s = "invalid ImpliesOp"; break;
- case 150: s = "invalid AndOp"; break;
- case 151: s = "invalid OrOp"; break;
- case 152: s = "invalid RelOp"; break;
- case 153: s = "invalid AddOp"; break;
- case 154: s = "invalid UnaryExpression"; break;
- case 155: s = "invalid MulOp"; break;
- case 156: s = "invalid NegOp"; break;
- case 157: s = "invalid EndlessExpression"; break;
- case 158: s = "invalid Suffix"; break;
- case 159: s = "invalid Suffix"; break;
- case 160: s = "invalid Suffix"; break;
- case 161: s = "invalid DisplayExpr"; break;
- case 162: s = "invalid MultiSetExpr"; break;
- case 163: s = "invalid ConstAtomExpression"; break;
- case 164: s = "invalid QuantifierGuts"; break;
- case 165: s = "invalid Forall"; break;
- case 166: s = "invalid Exists"; break;
- case 167: s = "invalid QSep"; break;
+ case 146: s = "this symbol not expected in LoopSpec"; break;
+ case 147: s = "this symbol not expected in LoopSpec"; break;
+ case 148: s = "this symbol not expected in LoopSpec"; break;
+ case 149: s = "this symbol not expected in Invariant"; break;
+ case 150: s = "invalid AttributeArg"; break;
+ case 151: s = "invalid EquivOp"; break;
+ case 152: s = "invalid ImpliesOp"; break;
+ case 153: s = "invalid AndOp"; break;
+ case 154: s = "invalid OrOp"; break;
+ case 155: s = "invalid RelOp"; break;
+ case 156: s = "invalid AddOp"; break;
+ case 157: s = "invalid UnaryExpression"; break;
+ case 158: s = "invalid MulOp"; break;
+ case 159: s = "invalid NegOp"; break;
+ case 160: s = "invalid EndlessExpression"; break;
+ case 161: s = "invalid Suffix"; break;
+ case 162: s = "invalid Suffix"; break;
+ case 163: s = "invalid Suffix"; break;
+ case 164: s = "invalid DisplayExpr"; break;
+ case 165: s = "invalid MultiSetExpr"; break;
+ case 166: s = "invalid ConstAtomExpression"; break;
+ case 167: s = "invalid QuantifierGuts"; break;
+ case 168: s = "invalid Forall"; break;
+ case 169: s = "invalid Exists"; break;
+ case 170: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index fcedb829..af4f54c8 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -219,15 +219,18 @@ namespace Microsoft.Dafny {
public void PrintFunction(Function f, int indent) {
Contract.Requires(f != null);
+ var isPredicate = f is Predicate;
Indent(indent);
- string k = "function";
+ string k = isPredicate ? "predicate" : "function";
if (f.IsUnlimited) { k = "unlimited " + k; }
if (f.IsStatic) { k = "static " + k; }
if (!f.IsGhost) { k += " method"; }
PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);
PrintFormals(f.Formals);
- wr.Write(": ");
- PrintType(f.ResultType);
+ if (!isPredicate) {
+ wr.Write(": ");
+ PrintType(f.ResultType);
+ }
wr.WriteLine();
int ind = indent + IndentAmount;
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index d7fde895..3a3621ac 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -177,9 +177,7 @@ namespace Microsoft.Dafny {
return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
} else if (member is Function) {
var f = (Function)member;
- var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
- return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.Formals.ConvertAll(CloneFormal), CloneType(f.ResultType),
- f.Req.ConvertAll(CloneExpr), f.Reads.ConvertAll(CloneFrameExpr), f.Ens.ConvertAll(CloneExpr), CloneSpecExpr(f.Decreases), CloneExpr(f.Body), null);
+ return CloneFunction(f, null, null);
} else {
var m = (Method)member;
var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
@@ -511,6 +509,32 @@ namespace Microsoft.Dafny {
return new GuardedAlternative(Tok(alt.Tok), CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt));
}
+ Function CloneFunction(Function f, List<Expression> moreEnsures, Expression moreBody) {
+ Contract.Requires(moreBody == null || f is Predicate);
+
+ var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
+ var formals = f.Formals.ConvertAll(CloneFormal);
+ var req = f.Req.ConvertAll(CloneExpr);
+ var reads = f.Reads.ConvertAll(CloneFrameExpr);
+ var ens = f.Ens.ConvertAll(CloneExpr);
+ if (moreEnsures != null) {
+ ens.AddRange(moreEnsures);
+ }
+ var decreases = CloneSpecExpr(f.Decreases);
+ var body = CloneExpr(f.Body);
+ if (moreBody != null) {
+ body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, body, moreBody);
+ }
+
+ if (f is Predicate) {
+ return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, formals,
+ req, reads, ens, decreases, body, null);
+ } else {
+ return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, formals, CloneType(f.ResultType),
+ req, reads, ens, decreases, body, null);
+ }
+ }
+
// -------------------------------------------------- Merging ---------------------------------------------------------------
ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {
@@ -535,27 +559,27 @@ namespace Microsoft.Dafny {
} else if (nwMember is Function) {
var f = (Function)nwMember;
- if (!(member is Function)) {
- reporter.Error(nwMember, "a function declaration ({0}) can only refine a function", nwMember.Name);
+ bool isPredicate = f is Predicate;
+ string s = isPredicate ? "predicate" : "function";
+ if (!(member is Function) || isPredicate && !(member is Predicate)) {
+ reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", s, nwMember.Name);
} else {
- var clone = (Function)CloneMember(member);
if (f.Decreases.Expressions.Count != 0) {
- reporter.Error(nwMember, "decreases clause on refining function not supported");
+ reporter.Error(nwMember, "decreases clause on refining {0} not supported", s);
}
if (f.Reads.Count != 0) {
- reporter.Error(nwMember, "a refining function is not allowed to extend the reads clause");
+ reporter.Error(nwMember, "a refining {0} is not allowed to extend the reads clause", s);
}
if (f.Req.Count != 0) {
- reporter.Error(nwMember, "a refining function is not allowed to add preconditions");
+ reporter.Error(nwMember, "a refining {0} is not allowed to add preconditions", s);
}
// TODO: check agreement for f.TypeArgs, f.ResultType, f.Formals, and flags. For now, they are ignored and assumed to be the same.
- foreach (var e in f.Ens) {
- clone.Ens.Add(e);
+ var newBody = f.Body;
+ if (newBody != null && !isPredicate) {
+ reporter.Error(nwMember, "a refining function is not allowed to provided a body");
+ newBody = null;
}
- if (f.Body != null) {
- reporter.Error(nwMember, "body of refining function is not yet supported"); // TODO
- }
- nw.Members[index] = clone;
+ nw.Members[index] = CloneFunction((Function)member, f.Ens, f.Body);
}
} else {
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 0f2dfe39..7c3831a7 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -209,8 +209,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 103;
- const int noSym = 103;
+ const int maxT = 104;
+ const int noSym = 104;
[ContractInvariantMethod]
@@ -512,33 +512,34 @@ void objectInvariant(){
case "seq": t.kind = 39; break;
case "object": t.kind = 40; break;
case "function": t.kind = 41; break;
- case "reads": t.kind = 42; break;
- case "label": t.kind = 45; break;
- case "break": t.kind = 46; break;
- case "return": t.kind = 47; break;
- case "new": t.kind = 49; break;
- case "choose": t.kind = 53; break;
- case "if": t.kind = 54; break;
- case "else": t.kind = 55; break;
- case "case": t.kind = 56; break;
- case "while": t.kind = 58; break;
- case "invariant": t.kind = 59; break;
- case "match": t.kind = 60; break;
- case "assert": t.kind = 61; break;
- case "assume": t.kind = 62; break;
- case "print": t.kind = 63; break;
- case "parallel": t.kind = 64; break;
- case "in": t.kind = 78; break;
- case "false": t.kind = 88; break;
- case "true": t.kind = 89; break;
- case "null": t.kind = 90; break;
- case "this": t.kind = 91; break;
- case "fresh": t.kind = 92; break;
- case "allocated": t.kind = 93; break;
- case "old": t.kind = 94; break;
- case "then": t.kind = 95; break;
- case "forall": t.kind = 97; break;
- case "exists": t.kind = 99; break;
+ case "predicate": t.kind = 42; break;
+ case "reads": t.kind = 43; break;
+ case "label": t.kind = 46; break;
+ case "break": t.kind = 47; break;
+ case "return": t.kind = 48; break;
+ case "new": t.kind = 50; break;
+ case "choose": t.kind = 54; break;
+ case "if": t.kind = 55; break;
+ case "else": t.kind = 56; break;
+ case "case": t.kind = 57; break;
+ case "while": t.kind = 59; break;
+ case "invariant": t.kind = 60; break;
+ case "match": t.kind = 61; break;
+ case "assert": t.kind = 62; break;
+ case "assume": t.kind = 63; break;
+ case "print": t.kind = 64; break;
+ case "parallel": t.kind = 65; break;
+ case "in": t.kind = 79; break;
+ case "false": t.kind = 89; break;
+ case "true": t.kind = 90; break;
+ case "null": t.kind = 91; break;
+ case "this": t.kind = 92; break;
+ case "fresh": t.kind = 93; break;
+ case "allocated": t.kind = 94; break;
+ case "old": t.kind = 95; break;
+ case "then": t.kind = 96; break;
+ case "forall": t.kind = 98; break;
+ case "exists": t.kind = 100; break;
default: break;
}
}
@@ -649,71 +650,71 @@ void objectInvariant(){
case 22:
{t.kind = 33; break;}
case 23:
- {t.kind = 43; break;}
- case 24:
{t.kind = 44; break;}
+ case 24:
+ {t.kind = 45; break;}
case 25:
- {t.kind = 48; break;}
+ {t.kind = 49; break;}
case 26:
- {t.kind = 50; break;}
- case 27:
{t.kind = 51; break;}
+ case 27:
+ {t.kind = 52; break;}
case 28:
- {t.kind = 57; break;}
+ {t.kind = 58; break;}
case 29:
if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 65; break;}
- case 31:
{t.kind = 66; break;}
- case 32:
+ case 31:
{t.kind = 67; break;}
- case 33:
+ case 32:
{t.kind = 68; break;}
+ case 33:
+ {t.kind = 69; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 69; break;}
- case 36:
{t.kind = 70; break;}
- case 37:
+ case 36:
{t.kind = 71; break;}
- case 38:
+ case 37:
{t.kind = 72; break;}
+ case 38:
+ {t.kind = 73; break;}
case 39:
- {t.kind = 75; break;}
- case 40:
{t.kind = 76; break;}
- case 41:
+ case 40:
{t.kind = 77; break;}
+ case 41:
+ {t.kind = 78; break;}
case 42:
- {t.kind = 80; break;}
- case 43:
{t.kind = 81; break;}
- case 44:
+ case 43:
{t.kind = 82; break;}
- case 45:
+ case 44:
{t.kind = 83; break;}
- case 46:
+ case 45:
{t.kind = 84; break;}
- case 47:
+ case 46:
{t.kind = 85; break;}
- case 48:
+ case 47:
{t.kind = 86; break;}
- case 49:
+ case 48:
{t.kind = 87; break;}
+ case 49:
+ {t.kind = 88; break;}
case 50:
- {t.kind = 96; break;}
+ {t.kind = 97; break;}
case 51:
- {t.kind = 98; break;}
+ {t.kind = 99; break;}
case 52:
- {t.kind = 100; break;}
- case 53:
{t.kind = 101; break;}
- case 54:
+ case 53:
{t.kind = 102; break;}
+ case 54:
+ {t.kind = 103; break;}
case 55:
recEnd = pos; recKind = 5;
if (ch == '=') {AddCh(); goto case 25;}
@@ -737,22 +738,22 @@ void objectInvariant(){
if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 23; break;}
case 60:
- recEnd = pos; recKind = 52;
+ recEnd = pos; recKind = 53;
if (ch == '.') {AddCh(); goto case 50;}
- else {t.kind = 52; break;}
+ else {t.kind = 53; break;}
case 61:
- recEnd = pos; recKind = 79;
+ recEnd = pos; recKind = 80;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
- else {t.kind = 79; break;}
+ else {t.kind = 80; break;}
case 62:
- recEnd = pos; recKind = 73;
+ recEnd = pos; recKind = 74;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 73; break;}
+ else {t.kind = 74; break;}
case 63:
- recEnd = pos; recKind = 74;
+ recEnd = pos; recKind = 75;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 74; break;}
+ else {t.kind = 75; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index ce58ffe7..deb4a2fc 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1364,6 +1364,15 @@ Execution trace:
Dafny program verifier finished with 13 verified, 2 errors
+-------------------- Predicates.dfy --------------------
+Predicates.dfy[B](18,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[B](17,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(28,9): Related location: Related location
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 9 verified, 1 error
+
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
Execution trace:
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
new file mode 100644
index 00000000..76666ef0
--- /dev/null
+++ b/Test/dafny0/Predicates.dfy
@@ -0,0 +1,31 @@
+module A {
+ class C {
+ var x: int;
+ predicate P()
+ reads this;
+ {
+ x < 100
+ }
+ method M()
+ modifies this;
+ ensures P();
+ {
+ x := 28;
+ }
+ method N()
+ modifies this;
+ ensures P();
+ {
+ x := -28;
+ }
+ }
+}
+
+module B refines A {
+ class C {
+ predicate P()
+ {
+ 0 <= x
+ }
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 45c434a5..0da3b411 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
- CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do (
+ CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
+ Predicates.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 3811e2c0..56b56000 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "type" "function" "ghost" "var" "method" "constructor" "unlimited"
+ "class" "datatype" "type" "function" "predicate" "ghost" "var" "method" "constructor" "unlimited"
"module" "imports" "static" "refines"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index e35383b0..41923a98 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -24,7 +24,7 @@ namespace Demo
"break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
- "function", "free",
+ "function", "predicate", "free",
"in", "forall", "exists",
"seq", "set", "multiset", "array", "array2", "array3",
"match", "case",
@@ -301,6 +301,7 @@ namespace Demo
| "true"
| "null"
| "function"
+ | "predicate"
| "free"
| "in"
| "forall"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 78c5f8d9..650c01bd 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -272,6 +272,7 @@ namespace DafnyLanguage
case "object":
case "old":
case "parallel":
+ case "predicate":
case "print":
case "reads":
case "refines":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 28759fd4..b23e2dc4 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -6,7 +6,7 @@
\lstdefinelanguage{dafny}{
morekeywords={class,datatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%
- function,unlimited,
+ function,predicate,unlimited,
ghost,var,static,refines,
method,constructor,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index faac0cbb..37038f35 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -5,7 +5,7 @@
syntax clear
syntax case match
-syntax keyword dafnyFunction function method constructor
+syntax keyword dafnyFunction function predicate method constructor
syntax keyword dafnyTypeDef class datatype type
syntax keyword dafnyConditional if then else match case
syntax keyword dafnyRepeat while parallel
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 16:25:35 +0000