summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2011-03-26 08:54:54 +0000
committerGravatar rustanleino <unknown>2011-03-26 08:54:54 +0000
commit53281904797b0d78e18a79cc2d140df7ba4b9086 (patch)
tree6f1b098b301fc8e6594c22199fb94a257164b7d5
parentcd3946b053478afdf7258ce23e34b9ccf51189b5 (diff)
Dafny: added "choose" operator on sets
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl11
-rw-r--r--Binaries/DafnyRuntime.cs6
-rw-r--r--Source/Dafny/Compiler.cs4
-rw-r--r--Source/Dafny/Dafny.atg20
-rw-r--r--Source/Dafny/DafnyAst.cs1
-rw-r--r--Source/Dafny/Parser.cs569
-rw-r--r--Source/Dafny/Printer.cs23
-rw-r--r--Source/Dafny/Resolver.cs7
-rw-r--r--Source/Dafny/Scanner.cs227
-rw-r--r--Source/Dafny/Translator.cs51
-rw-r--r--Test/dafny1/Answer2
-rw-r--r--Test/dafny1/Celebrity.dfy14
-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
17 files changed, 528 insertions, 417 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 1ef8aea7..646b16f1 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -80,6 +80,10 @@ function Set#Disjoint<T>(Set T, Set T) returns (bool);
axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }
Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
+function Set#Choose<T>(Set T, TickType) returns (T);
+axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
+ a != Set#Empty() ==> a[Set#Choose(a, tick)]);
+
// ---------------------------------------------------------------
// -- Axiomatization of sequences --------------------------------
// ---------------------------------------------------------------
@@ -347,6 +351,13 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
$HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
// ---------------------------------------------------------------
+// -- Non-determinism --------------------------------------------
+// ---------------------------------------------------------------
+
+type TickType;
+var $Tick: TickType;
+
+// ---------------------------------------------------------------
// -- Arithmetic -------------------------------------------------
// ---------------------------------------------------------------
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index f32cc85a..63cca64a 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -117,6 +117,12 @@ namespace Dafny
}
return new Set<T>(r);
}
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ }
}
public class Sequence<T>
{
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index decc5223..bd6f9240 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1119,6 +1119,10 @@ namespace Microsoft.Dafny {
wr.Write("!");
TrParenExpr(e.E);
break;
+ case UnaryExpr.Opcode.SetChoose:
+ TrParenExpr(e.E);
+ wr.Write(".Choose()");
+ break;
case UnaryExpr.Opcode.SeqLength:
if (cce.NonNull(e.E.Type).IsArrayType) {
wr.Write("new BigInteger(");
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 0d815bf4..ce067ec6 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -741,7 +741,7 @@ OneStmt<out Statement/*!*/ s>
| AssumeStmt<out s>
| UseStmt<out s>
| PrintStmt<out s>
- | AssignStmt<out s>
+ | AssignStmt<out s, true>
| HavocStmt<out s>
| CallStmt<out s>
| IfStmt<out s>
@@ -758,7 +758,7 @@ OneStmt<out Statement/*!*/ s>
)
.
-AssignStmt<out Statement/*!*/ s>
+AssignStmt<out Statement/*!*/ s, bool allowChoose>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ lhs;
List<Expression> rhs;
@@ -771,6 +771,12 @@ AssignStmt<out Statement/*!*/ s>
Contract.Assert(rhs != null);
Contract.Assert(rhs.Count == 1);
s = new AssignStmt(x, lhs, rhs[0]);
+ if (!allowChoose) {
+ var r = rhs[0] as UnaryExpr;
+ if (r != null && r.Op == UnaryExpr.Opcode.SetChoose) {
+ SemErr("choose operator not allowed as RHS in foreach assignment");
+ }
+ }
} else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
} else {
@@ -795,8 +801,12 @@ AssignRhs<.out List<Expression> ee, out Type ty.>
UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
.)
]
- | Expression<out e> (. ee = new List<Expression>(); ee.Add(e); .)
- ) (. if (ee == null && ty == null) { ee = new List<Expression>(); ee.Add(dummyExpr); } .)
+ | "choose" (. x = t; .)
+ "(" Expression<out e> ")" (. e = new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e);
+ ee = new List<Expression>() { e };
+ .)
+ | Expression<out e> (. ee = new List<Expression>() { e }; .)
+ ) (. if (ee == null && ty == null) { ee = new List<Expression>() { dummyExpr}; } .)
.
HavocStmt<out Statement/*!*/ s>
@@ -1015,7 +1025,7 @@ ForeachStmt<out Statement/*!*/ s>
| AssumeStmt<out s> (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
| UseStmt<out s> (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
}
- ( AssignStmt<out s> (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
+ ( AssignStmt<out s, false> (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
| HavocStmt<out s> (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
)
"}" (. if (bodyAssign != null) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0b736242..f5542b4c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2100,6 +2100,7 @@ namespace Microsoft.Dafny {
{
public enum Opcode {
Not,
+ SetChoose, // Important: SetChoose is not a function, so it can only be used in a statement context (in particular, the RHS of an assignment)
SeqLength
}
public readonly Opcode Op;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d49c78c6..7cc48f3b 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -20,12 +20,12 @@ public class Parser {
public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
- public const int maxT = 104;
+ public const int maxT = 105;
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -402,7 +402,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
mm.Add(m);
} else if (la.kind == 18) {
CouplingInvDecl(mmod, mm);
- } else SynErr(105);
+ } else SynErr(106);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -486,7 +486,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
- } else SynErr(106);
+ } else SynErr(107);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
@@ -515,7 +515,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
} else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(107);
+ } else SynErr(108);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
while (la.kind == 7) {
@@ -542,7 +542,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
BlockStmt(out bb, out bodyStart, out bodyEnd);
body = (BlockStmt)bb;
- } else SynErr(108);
+ } else SynErr(109);
parseVarScope.PopMarker();
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -634,18 +634,18 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; Expression/*!*/ e0; Expression/*!*/ e1 = dummyExpr;
e = dummyExpr;
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
x = t;
Expression(out e);
- Expect(64);
+ Expect(65);
Expression(out e0);
- Expect(53);
+ Expect(54);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(8)) {
EquivExpression(out e);
- } else SynErr(109);
+ } else SynErr(110);
}
void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
@@ -735,7 +735,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
} else if (la.kind == 1 || la.kind == 3 || la.kind == 36) {
ReferenceType(out tok, out ty);
- } else SynErr(110);
+ } else SynErr(111);
}
void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {
@@ -785,12 +785,12 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
Expect(15);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(111);
+ } else SynErr(112);
} else if (la.kind == 29) {
Get();
Expressions(decreases);
Expect(15);
- } else SynErr(112);
+ } else SynErr(113);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -872,7 +872,7 @@ List<Expression/*!*/>/*!*/ decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(113);
+ } else SynErr(114);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -904,7 +904,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
Expressions(decreases);
Expect(15);
- } else SynErr(114);
+ } else SynErr(115);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -915,7 +915,7 @@ List<Expression/*!*/>/*!*/ decreases) {
MatchExpression(out e);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(115);
+ } else SynErr(116);
Expect(8);
bodyEnd = t;
}
@@ -927,7 +927,7 @@ List<Expression/*!*/>/*!*/ decreases) {
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(9)) {
FrameExpression(out fe);
- } else SynErr(116);
+ } else SynErr(117);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -938,7 +938,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new WildcardExpr(t);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(117);
+ } else SynErr(118);
}
void MatchExpression(out Expression/*!*/ e) {
@@ -992,7 +992,7 @@ List<Expression/*!*/>/*!*/ decreases) {
MatchExpression(out e);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(118);
+ } else SynErr(119);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1008,7 +1008,7 @@ List<Expression/*!*/>/*!*/ decreases) {
ss.Add(s);
} else if (la.kind == 11 || la.kind == 16) {
VarDeclStmts(ss);
- } else SynErr(119);
+ } else SynErr(120);
}
void OneStmt(out Statement/*!*/ s) {
@@ -1016,39 +1016,39 @@ List<Expression/*!*/>/*!*/ decreases) {
s = dummyStmt; /* to please the compiler */
switch (la.kind) {
- case 60: {
+ case 61: {
AssertStmt(out s);
break;
}
- case 61: {
+ case 62: {
AssumeStmt(out s);
break;
}
- case 62: {
+ case 63: {
UseStmt(out s);
break;
}
- case 63: {
+ case 64: {
PrintStmt(out s);
break;
}
- case 1: case 30: case 96: case 97: {
- AssignStmt(out s);
+ case 1: case 30: case 97: case 98: {
+ AssignStmt(out s, true);
break;
}
- case 51: {
+ case 52: {
HavocStmt(out s);
break;
}
- case 56: {
+ case 57: {
CallStmt(out s);
break;
}
- case 52: {
+ case 53: {
IfStmt(out s);
break;
}
- case 54: {
+ case 55: {
WhileStmt(out s);
break;
}
@@ -1056,7 +1056,7 @@ List<Expression/*!*/>/*!*/ decreases) {
MatchStmt(out s);
break;
}
- case 57: {
+ case 58: {
ForeachStmt(out s);
break;
}
@@ -1086,7 +1086,7 @@ List<Expression/*!*/>/*!*/ decreases) {
s = new ReturnStmt(x);
break;
}
- default: SynErr(120); break;
+ default: SynErr(121); break;
}
}
@@ -1109,7 +1109,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(60);
+ Expect(61);
x = t;
Expression(out e);
Expect(15);
@@ -1118,7 +1118,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(61);
+ Expect(62);
x = t;
Expression(out e);
Expect(15);
@@ -1127,7 +1127,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void UseStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(62);
+ Expect(63);
x = t;
Expression(out e);
Expect(15);
@@ -1138,7 +1138,7 @@ List<Expression/*!*/>/*!*/ decreases) {
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);
@@ -1151,7 +1151,7 @@ List<Expression/*!*/>/*!*/ decreases) {
s = new PrintStmt(x, args);
}
- void AssignStmt(out Statement/*!*/ s) {
+ void AssignStmt(out Statement/*!*/ s, bool allowChoose) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ lhs;
List<Expression> rhs;
@@ -1166,6 +1166,12 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Assert(rhs != null);
Contract.Assert(rhs.Count == 1);
s = new AssignStmt(x, lhs, rhs[0]);
+ if (!allowChoose) {
+ var r = rhs[0] as UnaryExpr;
+ if (r != null && r.Op == UnaryExpr.Opcode.SetChoose) {
+ SemErr("choose operator not allowed as RHS in foreach assignment");
+ }
+ }
} else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
} else {
@@ -1177,7 +1183,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void HavocStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
- Expect(51);
+ Expect(52);
x = t;
LhsExpr(out lhs);
Expect(15);
@@ -1190,7 +1196,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<IdentifierExpr/*!*/> lhs = new List<IdentifierExpr/*!*/>();
List<AutoVarDecl/*!*/> newVars = new List<AutoVarDecl/*!*/>();
- Expect(56);
+ Expect(57);
x = t;
CallStmtSubExpr(out e);
if (la.kind == 17 || la.kind == 47) {
@@ -1247,19 +1253,19 @@ List<Expression/*!*/>/*!*/ decreases) {
Statement els = null;
IToken bodyStart, bodyEnd;
- Expect(52);
+ Expect(53);
x = t;
Guard(out guard);
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 53) {
+ if (la.kind == 54) {
Get();
- if (la.kind == 52) {
+ if (la.kind == 53) {
IfStmt(out s);
els = s;
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(121);
+ } else SynErr(122);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1273,18 +1279,18 @@ List<Expression/*!*/>/*!*/ decreases) {
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
- Expect(54);
+ Expect(55);
x = t;
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 26 || la.kind == 29 || la.kind == 55) {
- if (la.kind == 26 || la.kind == 55) {
+ while (la.kind == 26 || la.kind == 29 || la.kind == 56) {
+ if (la.kind == 26 || la.kind == 56) {
isFree = false;
if (la.kind == 26) {
Get();
isFree = true;
}
- Expect(55);
+ Expect(56);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(15);
@@ -1329,7 +1335,7 @@ List<Expression/*!*/>/*!*/ decreases) {
AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(57);
+ Expect(58);
x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1340,20 +1346,20 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
Type(out ty);
}
- Expect(58);
+ Expect(59);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
Expression(out range);
}
Expect(31);
Expect(7);
- while (la.kind == 60 || la.kind == 61 || la.kind == 62) {
- if (la.kind == 60) {
+ while (la.kind == 61 || la.kind == 62 || la.kind == 63) {
+ if (la.kind == 61) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (la.kind == 61) {
+ } else if (la.kind == 62) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1362,12 +1368,12 @@ List<Expression/*!*/>/*!*/ decreases) {
}
}
if (StartOf(13)) {
- AssignStmt(out s);
+ AssignStmt(out s, false);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (la.kind == 51) {
+ } else if (la.kind == 52) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else SynErr(122);
+ } else SynErr(123);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1403,21 +1409,30 @@ List<Expression/*!*/>/*!*/ decreases) {
UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
}
+ } else if (la.kind == 51) {
+ Get();
+ x = t;
+ Expect(30);
+ Expression(out e);
+ Expect(31);
+ e = new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e);
+ ee = new List<Expression>() { e };
+
} else if (StartOf(9)) {
Expression(out e);
- ee = new List<Expression>(); ee.Add(e);
- } else SynErr(123);
- if (ee == null && ty == null) { ee = new List<Expression>(); ee.Add(dummyExpr); }
+ ee = new List<Expression>() { e };
+ } else SynErr(124);
+ if (ee == null && ty == null) { ee = new List<Expression>() { dummyExpr}; }
}
void SelectExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {
+ } else if (la.kind == 30 || la.kind == 97 || la.kind == 98) {
ObjectExpression(out e);
- } else SynErr(124);
- while (la.kind == 49 || la.kind == 92) {
+ } else SynErr(125);
+ while (la.kind == 49 || la.kind == 93) {
SelectOrCallSuffix(ref e);
}
}
@@ -1462,7 +1477,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(125);
+ } else SynErr(126);
Expect(31);
}
@@ -1502,11 +1517,11 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {
+ } else if (la.kind == 30 || la.kind == 97 || la.kind == 98) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else SynErr(126);
- while (la.kind == 49 || la.kind == 92) {
+ } else SynErr(127);
+ while (la.kind == 49 || la.kind == 93) {
SelectOrCallSuffix(ref e);
}
}
@@ -1519,13 +1534,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(9)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(127);
+ } else SynErr(128);
}
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);
@@ -1536,7 +1551,7 @@ List<Expression/*!*/>/*!*/ decreases) {
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);
@@ -1545,23 +1560,23 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void EquivOp() {
- if (la.kind == 65) {
+ if (la.kind == 66) {
Get();
- } else if (la.kind == 66) {
+ } else if (la.kind == 67) {
Get();
- } else SynErr(128);
+ } else SynErr(129);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(14)) {
- if (la.kind == 69 || la.kind == 70) {
+ 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);
@@ -1572,7 +1587,7 @@ List<Expression/*!*/>/*!*/ decreases) {
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);
@@ -1583,11 +1598,11 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void ImpliesOp() {
- if (la.kind == 67) {
+ if (la.kind == 68) {
Get();
- } else if (la.kind == 68) {
+ } else if (la.kind == 69) {
Get();
- } else SynErr(129);
+ } else SynErr(130);
}
void RelationalExpression(out Expression/*!*/ e0) {
@@ -1601,25 +1616,25 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void AndOp() {
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
- } else if (la.kind == 70) {
+ } else if (la.kind == 71) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
void OrOp() {
- if (la.kind == 71) {
+ if (la.kind == 72) {
Get();
- } else if (la.kind == 72) {
+ } else if (la.kind == 73) {
Get();
- } else SynErr(131);
+ } else SynErr(132);
}
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 == 82 || la.kind == 83) {
+ while (la.kind == 83 || la.kind == 84) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1629,7 +1644,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 73: {
+ case 74: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1644,59 +1659,59 @@ List<Expression/*!*/>/*!*/ decreases) {
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 58: {
+ case 59: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 78: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(132); break;
+ default: SynErr(133); 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 == 39 || la.kind == 84 || la.kind == 85) {
+ while (la.kind == 39 || la.kind == 85 || la.kind == 86) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1705,23 +1720,23 @@ List<Expression/*!*/>/*!*/ decreases) {
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 == 82) {
+ if (la.kind == 83) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 83) {
+ } else if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(133);
+ } else SynErr(134);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 83) {
+ if (la.kind == 84) {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (la.kind == 86 || la.kind == 87) {
+ } else if (la.kind == 87 || la.kind == 88) {
NegOp();
x = t;
UnaryExpression(out e);
@@ -1730,7 +1745,7 @@ List<Expression/*!*/>/*!*/ decreases) {
SelectExpression(out e);
} else if (StartOf(16)) {
ConstAtomExpression(out e);
- } else SynErr(134);
+ } else SynErr(135);
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1738,21 +1753,21 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 39) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 84) {
+ } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 85) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(135);
+ } else SynErr(136);
}
void NegOp() {
- if (la.kind == 86) {
+ if (la.kind == 87) {
Get();
- } else if (la.kind == 87) {
+ } else if (la.kind == 88) {
Get();
- } else SynErr(136);
+ } else SynErr(137);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1760,17 +1775,17 @@ List<Expression/*!*/>/*!*/ decreases) {
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;
@@ -1780,11 +1795,11 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new LiteralExpr(t, n);
break;
}
- case 91: {
+ case 92: {
Get();
x = t;
Ident(out dtName);
- Expect(92);
+ Expect(93);
Ident(out id);
elements = new List<Expression/*!*/>();
if (la.kind == 30) {
@@ -1797,7 +1812,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new DatatypeValue(t, dtName.val, id.val, elements);
break;
}
- case 93: {
+ case 94: {
Get();
x = t;
Expect(30);
@@ -1806,7 +1821,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new FreshExpr(x, e);
break;
}
- case 94: {
+ case 95: {
Get();
x = t;
Expect(30);
@@ -1815,12 +1830,12 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new AllocatedExpr(x, e);
break;
}
- case 59: {
+ case 60: {
Get();
x = t;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(59);
+ Expect(60);
break;
}
case 7: {
@@ -1843,7 +1858,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(50);
break;
}
- default: SynErr(137); break;
+ default: SynErr(138); break;
}
}
@@ -1882,10 +1897,10 @@ List<Expression/*!*/>/*!*/ decreases) {
void ObjectExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
e = new ThisExpr(t);
- } else if (la.kind == 97) {
+ } else if (la.kind == 98) {
Get();
x = t;
Expect(30);
@@ -1898,9 +1913,9 @@ List<Expression/*!*/>/*!*/ decreases) {
QuantifierGuts(out e);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(138);
+ } else SynErr(139);
Expect(31);
- } else SynErr(139);
+ } else SynErr(140);
}
void SelectOrCallSuffix(ref Expression/*!*/ e) {
@@ -1909,7 +1924,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 92) {
+ if (la.kind == 93) {
Get();
Ident(out id);
if (la.kind == 30) {
@@ -1928,7 +1943,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (StartOf(9)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 95) {
+ if (la.kind == 96) {
Get();
anyDots = true;
if (StartOf(9)) {
@@ -1950,12 +1965,12 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(140);
- } else if (la.kind == 95) {
+ } else SynErr(141);
+ } else if (la.kind == 96) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(141);
+ } else SynErr(142);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
} else {
@@ -1977,7 +1992,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(50);
- } else SynErr(142);
+ } else SynErr(143);
}
void QuantifierGuts(out Expression/*!*/ q) {
@@ -1989,13 +2004,13 @@ List<Expression/*!*/>/*!*/ decreases) {
Triggers trigs = null;
Expression/*!*/ body;
- if (la.kind == 98 || la.kind == 99) {
+ if (la.kind == 99 || la.kind == 100) {
Forall();
x = t; univ = true;
- } else if (la.kind == 100 || la.kind == 101) {
+ } else if (la.kind == 101 || la.kind == 102) {
Exists();
x = t;
- } else SynErr(143);
+ } else SynErr(144);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -2019,19 +2034,19 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void Forall() {
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 99) {
+ } else if (la.kind == 100) {
Get();
- } else SynErr(144);
+ } else SynErr(145);
}
void Exists() {
- if (la.kind == 100) {
+ if (la.kind == 101) {
Get();
- } else if (la.kind == 101) {
+ } else if (la.kind == 102) {
Get();
- } else SynErr(145);
+ } else SynErr(146);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2044,16 +2059,16 @@ List<Expression/*!*/>/*!*/ decreases) {
es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(146);
+ } else SynErr(147);
Expect(8);
}
void QSep() {
- if (la.kind == 102) {
+ if (la.kind == 103) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 104) {
Get();
- } else SynErr(147);
+ } else SynErr(148);
}
void AttributeBody(ref Attributes attrs) {
@@ -2080,33 +2095,33 @@ List<Expression/*!*/>/*!*/ decreases) {
public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, 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,T,T, T,T,x,x, T,x,T,x, x,x,x,T, 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,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,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},
- {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,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},
- {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,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, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, 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,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,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, T,T,T,x, x,x,x,T, T,x,T,x, 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, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, 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,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, 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, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x, x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,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, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,T,x, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, 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,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, 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,T,T, T,T,x,x, T,x,T,x, x,x,x,T, 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,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,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,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,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,x},
+ {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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, 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,x,x,T, T,T,T,T, T,x,T,T, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,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, T,T,T,x, x,x,x,x, T,T,x,T, x,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,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,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, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, T,T,x,T, x,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,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x, x,x,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,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, x,x,x,x, x,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,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,x, 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,T,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, 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,x,x,T, T,T,T,T, T,x,T,T, x,T,T,x, x,x,x,x, x,x,x}
};
} // end Parser
@@ -2115,18 +2130,20 @@ List<Expression/*!*/>/*!*/ decreases) {
public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
- public virtual void SynErr(string filename, int line, int col, string msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+
+ public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
- string GetSyntaxErrorString(int n) {
+ }
+
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2180,107 +2197,108 @@ public class Errors {
case 48: s = "\"new\" expected"; break;
case 49: s = "\"[\" expected"; break;
case 50: s = "\"]\" expected"; break;
- case 51: s = "\"havoc\" expected"; break;
- case 52: s = "\"if\" expected"; break;
- case 53: s = "\"else\" expected"; break;
- case 54: s = "\"while\" expected"; break;
- case 55: s = "\"invariant\" expected"; break;
- case 56: s = "\"call\" expected"; break;
- case 57: s = "\"foreach\" expected"; break;
- case 58: s = "\"in\" expected"; break;
- case 59: s = "\"|\" expected"; break;
- case 60: s = "\"assert\" expected"; break;
- case 61: s = "\"assume\" expected"; break;
- case 62: s = "\"use\" expected"; break;
- case 63: s = "\"print\" expected"; break;
- case 64: s = "\"then\" 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 = "\"\\u2260\" expected"; break;
- case 80: s = "\"\\u2264\" expected"; break;
- case 81: s = "\"\\u2265\" expected"; break;
- case 82: s = "\"+\" 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 = "\"#\" expected"; break;
- case 92: s = "\".\" expected"; break;
- case 93: s = "\"fresh\" expected"; break;
- case 94: s = "\"allocated\" expected"; break;
- case 95: s = "\"..\" expected"; break;
- case 96: s = "\"this\" expected"; break;
- case 97: s = "\"old\" 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 = "invalid ClassMemberDecl"; break;
- case 106: s = "invalid FunctionDecl"; break;
- case 107: s = "invalid MethodDecl"; break;
+ case 51: s = "\"choose\" expected"; break;
+ case 52: s = "\"havoc\" expected"; break;
+ case 53: s = "\"if\" expected"; break;
+ case 54: s = "\"else\" expected"; break;
+ case 55: s = "\"while\" expected"; break;
+ case 56: s = "\"invariant\" expected"; break;
+ case 57: s = "\"call\" expected"; break;
+ case 58: s = "\"foreach\" expected"; break;
+ case 59: s = "\"in\" expected"; break;
+ case 60: s = "\"|\" expected"; break;
+ case 61: s = "\"assert\" expected"; break;
+ case 62: s = "\"assume\" expected"; break;
+ case 63: s = "\"use\" expected"; break;
+ case 64: s = "\"print\" expected"; break;
+ case 65: s = "\"then\" 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 = "\"\\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 = "\"!\" 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 = "\"#\" expected"; break;
+ case 93: s = "\".\" expected"; break;
+ case 94: s = "\"fresh\" expected"; break;
+ case 95: s = "\"allocated\" expected"; break;
+ case 96: s = "\"..\" expected"; break;
+ case 97: s = "\"this\" expected"; break;
+ case 98: s = "\"old\" expected"; break;
+ case 99: s = "\"forall\" expected"; break;
+ case 100: s = "\"\\u2200\" expected"; break;
+ case 101: s = "\"exists\" expected"; break;
+ case 102: s = "\"\\u2203\" expected"; break;
+ case 103: s = "\"::\" expected"; break;
+ case 104: s = "\"\\u2022\" expected"; break;
+ case 105: s = "??? expected"; break;
+ case 106: s = "invalid ClassMemberDecl"; break;
+ case 107: s = "invalid FunctionDecl"; break;
case 108: s = "invalid MethodDecl"; break;
- case 109: s = "invalid Expression"; break;
- case 110: s = "invalid TypeAndToken"; break;
- case 111: s = "invalid MethodSpec"; break;
+ case 109: s = "invalid MethodDecl"; break;
+ case 110: s = "invalid Expression"; break;
+ case 111: s = "invalid TypeAndToken"; break;
case 112: s = "invalid MethodSpec"; break;
- case 113: s = "invalid ReferenceType"; break;
- case 114: s = "invalid FunctionSpec"; break;
- case 115: s = "invalid FunctionBody"; break;
- case 116: s = "invalid PossiblyWildFrameExpression"; break;
- case 117: s = "invalid PossiblyWildExpression"; break;
- case 118: s = "invalid MatchOrExpr"; break;
- case 119: s = "invalid Stmt"; break;
- case 120: s = "invalid OneStmt"; break;
- case 121: s = "invalid IfStmt"; break;
- case 122: s = "invalid ForeachStmt"; break;
- case 123: s = "invalid AssignRhs"; break;
- case 124: s = "invalid SelectExpression"; break;
- case 125: s = "invalid Guard"; break;
- case 126: s = "invalid CallStmtSubExpr"; break;
- case 127: s = "invalid AttributeArg"; break;
- case 128: s = "invalid EquivOp"; break;
- case 129: s = "invalid ImpliesOp"; break;
- case 130: s = "invalid AndOp"; break;
- case 131: s = "invalid OrOp"; break;
- case 132: s = "invalid RelOp"; break;
- case 133: s = "invalid AddOp"; break;
- case 134: s = "invalid UnaryExpression"; break;
- case 135: s = "invalid MulOp"; break;
- case 136: s = "invalid NegOp"; break;
- case 137: s = "invalid ConstAtomExpression"; break;
- case 138: s = "invalid ObjectExpression"; break;
+ case 113: s = "invalid MethodSpec"; break;
+ case 114: s = "invalid ReferenceType"; break;
+ case 115: s = "invalid FunctionSpec"; break;
+ case 116: s = "invalid FunctionBody"; break;
+ case 117: s = "invalid PossiblyWildFrameExpression"; break;
+ case 118: s = "invalid PossiblyWildExpression"; break;
+ case 119: s = "invalid MatchOrExpr"; break;
+ case 120: s = "invalid Stmt"; break;
+ case 121: s = "invalid OneStmt"; break;
+ case 122: s = "invalid IfStmt"; break;
+ case 123: s = "invalid ForeachStmt"; break;
+ case 124: s = "invalid AssignRhs"; break;
+ case 125: s = "invalid SelectExpression"; break;
+ case 126: s = "invalid Guard"; break;
+ case 127: s = "invalid CallStmtSubExpr"; break;
+ case 128: s = "invalid AttributeArg"; break;
+ case 129: s = "invalid EquivOp"; break;
+ case 130: s = "invalid ImpliesOp"; break;
+ case 131: s = "invalid AndOp"; break;
+ case 132: s = "invalid OrOp"; break;
+ case 133: s = "invalid RelOp"; break;
+ case 134: s = "invalid AddOp"; break;
+ case 135: s = "invalid UnaryExpression"; break;
+ case 136: s = "invalid MulOp"; break;
+ case 137: s = "invalid NegOp"; break;
+ case 138: s = "invalid ConstAtomExpression"; break;
case 139: s = "invalid ObjectExpression"; break;
- case 140: s = "invalid SelectOrCallSuffix"; break;
+ case 140: s = "invalid ObjectExpression"; break;
case 141: s = "invalid SelectOrCallSuffix"; break;
case 142: s = "invalid SelectOrCallSuffix"; break;
- case 143: s = "invalid QuantifierGuts"; break;
- case 144: s = "invalid Forall"; break;
- case 145: s = "invalid Exists"; break;
- case 146: s = "invalid AttributeOrTrigger"; break;
- case 147: s = "invalid QSep"; break;
+ case 143: s = "invalid SelectOrCallSuffix"; break;
+ case 144: s = "invalid QuantifierGuts"; break;
+ case 145: s = "invalid Forall"; break;
+ case 146: s = "invalid Exists"; break;
+ case 147: s = "invalid AttributeOrTrigger"; break;
+ case 148: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2288,8 +2306,9 @@ public class Errors {
Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
+
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 0b6d4446..629a0f89 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -834,18 +834,29 @@ namespace Microsoft.Dafny {
string op;
int opBindingStrength;
switch (e.Op) {
+ case UnaryExpr.Opcode.SetChoose:
+ op = "choose"; opBindingStrength = -1; break;
case UnaryExpr.Opcode.Not:
op = "!"; opBindingStrength = 0x60; break;
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary opcode
}
- bool parensNeeded = opBindingStrength < contextBindingStrength ||
- (fragileContext && opBindingStrength == contextBindingStrength);
+ if (opBindingStrength == -1) {
+ // print as a function
+ wr.Write(op);
+ wr.Write("(");
+ PrintExpression(e.E);
+ wr.Write(")");
+ } else {
+ // print as an operator
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
- if (parensNeeded) { wr.Write("("); }
- wr.Write(op);
- PrintExpr(e.E, opBindingStrength, false, -1);
- if (parensNeeded) { wr.Write(")"); }
+ if (parensNeeded) { wr.Write("("); }
+ wr.Write(op);
+ PrintExpr(e.E, opBindingStrength, false, -1);
+ if (parensNeeded) { wr.Write(")"); }
+ }
}
} else if (expr is BinaryExpr) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index e261c8a1..7344e058 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2032,6 +2032,13 @@ namespace Microsoft.Dafny {
}
expr.Type = Type.Bool;
break;
+ case UnaryExpr.Opcode.SetChoose:
+ var elType = new InferredTypeProxy();
+ if (!UnifyTypes(e.E.Type, new SetType(elType))) {
+ Error(expr, "choose operator expects a set argument (instead got {0})", e.E.Type);
+ }
+ expr.Type = elType;
+ break;
case UnaryExpr.Opcode.SeqLength:
if (!UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
Error(expr, "length operator expects a sequence argument (instead got {0})", e.E.Type);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index b7e7f57b..e99d4770 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
// a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer {
Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
-[ContractInvariantMethod]
-void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);}
- [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+ [ContractInvariantMethod]
+ void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);
+ }
+
+// [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){
buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){
}
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){
Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){
}
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 104;
- const int noSym = 104;
-
-
-[ContractInvariantMethod]
-void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
-}
+ const int maxT = 105;
+ const int noSym = 105;
+
+
+ [ContractInvariantMethod]
+ void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+ }
+
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){
Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -291,9 +294,9 @@ void objectInvariant(){
start[Buffer.EOF] = -1;
}
-
- [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+// [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -303,15 +306,14 @@ void objectInvariant(){
Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
-
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
- [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+// [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -320,10 +322,9 @@ void objectInvariant(){
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
-
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -344,11 +345,11 @@ void objectInvariant(){
Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -359,7 +360,7 @@ void objectInvariant(){
}
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -367,9 +368,9 @@ void objectInvariant(){
// // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -419,7 +420,7 @@ void objectInvariant(){
return;
}
-
+
}
}
@@ -518,28 +519,29 @@ void objectInvariant(){
case "break": t.kind = 45; break;
case "return": t.kind = 46; break;
case "new": t.kind = 48; break;
- case "havoc": t.kind = 51; break;
- case "if": t.kind = 52; break;
- case "else": t.kind = 53; break;
- case "while": t.kind = 54; break;
- case "invariant": t.kind = 55; break;
- case "call": t.kind = 56; break;
- case "foreach": t.kind = 57; break;
- case "in": t.kind = 58; break;
- case "assert": t.kind = 60; break;
- case "assume": t.kind = 61; break;
- case "use": t.kind = 62; break;
- case "print": t.kind = 63; break;
- case "then": t.kind = 64; break;
- case "false": t.kind = 88; break;
- case "true": t.kind = 89; break;
- case "null": t.kind = 90; break;
- case "fresh": t.kind = 93; break;
- case "allocated": t.kind = 94; break;
- case "this": t.kind = 96; break;
- case "old": t.kind = 97; break;
- case "forall": t.kind = 98; break;
- case "exists": t.kind = 100; break;
+ case "choose": t.kind = 51; break;
+ case "havoc": t.kind = 52; break;
+ case "if": t.kind = 53; break;
+ case "else": t.kind = 54; break;
+ case "while": t.kind = 55; break;
+ case "invariant": t.kind = 56; break;
+ case "call": t.kind = 57; break;
+ case "foreach": t.kind = 58; break;
+ case "in": t.kind = 59; break;
+ case "assert": t.kind = 61; break;
+ case "assume": t.kind = 62; break;
+ case "use": t.kind = 63; break;
+ case "print": t.kind = 64; break;
+ case "then": t.kind = 65; break;
+ case "false": t.kind = 89; break;
+ case "true": t.kind = 90; break;
+ case "null": t.kind = 91; break;
+ case "fresh": t.kind = 94; break;
+ case "allocated": t.kind = 95; break;
+ case "this": t.kind = 97; break;
+ case "old": t.kind = 98; break;
+ case "forall": t.kind = 99; break;
+ case "exists": t.kind = 101; break;
default: break;
}
}
@@ -556,10 +558,13 @@ void objectInvariant(){
t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+ if (start.ContainsKey(ch)) {
+ Contract.Assert(start[ch] != null);
+ state = (int) start[ch];
+ }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -665,63 +670,63 @@ void objectInvariant(){
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:
if (ch == 'n') {AddCh(); goto case 43;}
else {goto case 0;}
case 43:
- {t.kind = 78; break;}
- case 44:
{t.kind = 79; break;}
- case 45:
+ case 44:
{t.kind = 80; break;}
- case 46:
+ case 45:
{t.kind = 81; break;}
- case 47:
+ case 46:
{t.kind = 82; break;}
- case 48:
+ case 47:
{t.kind = 83; break;}
- case 49:
+ case 48:
{t.kind = 84; break;}
- case 50:
+ case 49:
{t.kind = 85; break;}
+ case 50:
+ {t.kind = 86; break;}
case 51:
- {t.kind = 87; break;}
+ {t.kind = 88; break;}
case 52:
- {t.kind = 91; break;}
+ {t.kind = 92; break;}
case 53:
- {t.kind = 95; break;}
+ {t.kind = 96; break;}
case 54:
- {t.kind = 99; break;}
+ {t.kind = 100; break;}
case 55:
- {t.kind = 101; break;}
- case 56:
{t.kind = 102; break;}
- case 57:
+ case 56:
{t.kind = 103; break;}
+ case 57:
+ {t.kind = 104; break;}
case 58:
recEnd = pos; recKind = 20;
if (ch == '=') {AddCh(); goto case 26;}
@@ -740,40 +745,40 @@ void objectInvariant(){
else if (ch == '=') {AddCh(); goto case 66;}
else {goto case 0;}
case 62:
- recEnd = pos; recKind = 59;
+ recEnd = pos; recKind = 60;
if (ch == '|') {AddCh(); goto case 37;}
- else {t.kind = 59; break;}
+ else {t.kind = 60; break;}
case 63:
- recEnd = pos; recKind = 86;
+ recEnd = pos; recKind = 87;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
else if (ch == 'i') {AddCh(); goto case 42;}
- else {t.kind = 86; break;}
+ else {t.kind = 87; break;}
case 64:
- recEnd = pos; recKind = 92;
+ recEnd = pos; recKind = 93;
if (ch == '.') {AddCh(); goto case 53;}
- else {t.kind = 92; break;}
+ else {t.kind = 93; break;}
case 65:
- recEnd = pos; recKind = 74;
+ recEnd = pos; recKind = 75;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 74; break;}
+ else {t.kind = 75; break;}
case 66:
- recEnd = pos; recKind = 73;
+ recEnd = pos; recKind = 74;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 73; break;}
+ else {t.kind = 74; break;}
}
t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -794,7 +799,7 @@ void objectInvariant(){
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a480d2c4..aff8c86a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -41,6 +41,7 @@ namespace Microsoft.Dafny {
internal class PredefinedDecls {
public readonly Bpl.Type RefType;
public readonly Bpl.Type BoxType;
+ public readonly Bpl.Type TickType;
private readonly Bpl.TypeSynonymDecl setTypeCtor;
private readonly Bpl.TypeCtorDecl seqTypeCtor;
readonly Bpl.TypeCtorDecl fieldName;
@@ -55,6 +56,7 @@ namespace Microsoft.Dafny {
void ObjectInvariant() {
Contract.Invariant(RefType != null);
Contract.Invariant(BoxType != null);
+ Contract.Invariant(TickType != null);
Contract.Invariant(setTypeCtor != null);
Contract.Invariant(seqTypeCtor != null);
Contract.Invariant(fieldName != null);
@@ -98,7 +100,7 @@ namespace Microsoft.Dafny {
return new Bpl.IdentifierExpr(tok, allocField);
}
- public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType,
+ public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
@@ -106,6 +108,7 @@ namespace Microsoft.Dafny {
#region Non-null preconditions on parameters
Contract.Requires(refType != null);
Contract.Requires(boxType != null);
+ Contract.Requires(tickType != null);
Contract.Requires(setTypeCtor != null);
Contract.Requires(seqTypeCtor != null);
Contract.Requires(fieldNameType != null);
@@ -119,6 +122,7 @@ namespace Microsoft.Dafny {
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
+ this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new Bpl.TypeSeq());
this.setTypeCtor = setTypeCtor;
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
@@ -147,6 +151,7 @@ namespace Microsoft.Dafny {
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
+ Bpl.TypeCtorDecl tickType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
foreach (Bpl.Declaration d in prog.TopLevelDeclarations) {
@@ -166,6 +171,8 @@ namespace Microsoft.Dafny {
refType = dt;
} else if (dt.Name == "BoxType") {
boxType = dt;
+ } else if (dt.Name == "TickType") {
+ tickType = dt;
}
} else if (d is Bpl.TypeSynonymDecl) {
Bpl.TypeSynonymDecl dt = (Bpl.TypeSynonymDecl)d;
@@ -200,12 +207,14 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
} else if (boxType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type BoxType");
+ } else if (tickType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type TickType");
} else if (heap == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap");
} else if (allocField == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
} else {
- return new PredefinedDecls(refType, boxType,
+ return new PredefinedDecls(refType, boxType, tickType,
setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
allocField);
}
@@ -1425,7 +1434,10 @@ namespace Microsoft.Dafny {
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
Bpl.Expr t = IsTotal(e.E, etran);
- if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
+ if (e.Op == UnaryExpr.Opcode.SetChoose) {
+ Bpl.Expr emptySet = FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
+ return Bpl.Expr.And(t, Bpl.Expr.Neq(etran.TrExpr(e.E), emptySet));
+ } else if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
return Bpl.Expr.And(t, Bpl.Expr.Neq(etran.TrExpr(e.E), predef.Null));
}
return t;
@@ -1864,7 +1876,10 @@ namespace Microsoft.Dafny {
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
CheckWellformed(e.E, options, null, locals, builder, etran);
- if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
+ if (e.Op == UnaryExpr.Opcode.SetChoose) {
+ Bpl.Expr emptySet = FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
+ builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E), emptySet), "choose is defined only on nonempty sets"));
+ } else if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
CheckNonNull(expr.tok, e.E, builder, etran, options.AssertKv);
}
} else if (expr is BinaryExpr) {
@@ -2303,6 +2318,7 @@ namespace Microsoft.Dafny {
etran.InMethodContext());
req.Add(Requires(m.tok, true, context, null, null));
mod.Add(etran.HeapExpr);
+ mod.Add(etran.Tick());
if (!wellformednessProc) {
string comment = "user-defined preconditions";
@@ -3683,6 +3699,11 @@ namespace Microsoft.Dafny {
// assume $IsGoodHeap($Heap);
builder.Add(AssumeGoodHeap(tok, etran));
}
+ var ch = ((ExprRhs)rhs).Expr as UnaryExpr;
+ if (ch != null && ch.Op == UnaryExpr.Opcode.SetChoose) {
+ // havoc $Tick;
+ builder.Add(new Bpl.HavocCmd(ch.tok, new Bpl.IdentifierExprSeq(etran.Tick())));
+ }
} else if (rhs is HavocRhs) {
Contract.Assert(lhs is IdentifierExpr); // for this kind of RHS, the LHS is restricted to be a simple variable
@@ -3766,7 +3787,7 @@ namespace Microsoft.Dafny {
[ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(HeapExpr!=null);
+ Contract.Invariant(HeapExpr != null);
Contract.Invariant(predef != null);
Contract.Invariant(translator != null);
Contract.Invariant(This != null);
@@ -3862,7 +3883,14 @@ namespace Microsoft.Dafny {
Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);
return new Bpl.IdentifierExpr(tok, "$_Frame", ty);
}
-
+
+ public Bpl.IdentifierExpr Tick() {
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
+
+ return new Bpl.IdentifierExpr(Token.NoToken, "$Tick", predef.TickType);
+ }
+
public Bpl.IdentifierExpr ModuleContextHeight()
{
Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
@@ -4076,6 +4104,12 @@ namespace Microsoft.Dafny {
switch (e.Op) {
case UnaryExpr.Opcode.Not:
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
+ case UnaryExpr.Opcode.SetChoose:
+ var x = translator.FunctionCall(expr.tok, BuiltinFunction.SetChoose, predef.BoxType, arg, Tick());
+ if (!ModeledAsBoxType(e.Type)) {
+ x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, translator.TrType(e.Type), x);
+ }
+ return x;
case UnaryExpr.Opcode.SeqLength:
if (e.E.Type is SeqType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
@@ -4600,6 +4634,7 @@ namespace Microsoft.Dafny {
SetEqual,
SetSubset,
SetDisjoint,
+ SetChoose,
SeqLength,
SeqEmpty,
@@ -4680,6 +4715,10 @@ namespace Microsoft.Dafny {
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);
+ case BuiltinFunction.SetChoose:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "Set#Choose", typeInstantiation, args);
case BuiltinFunction.SeqLength:
Contract.Assert(args.Length == 1);
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index d9b32305..f54c87fd 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -81,7 +81,7 @@ Dafny program verifier finished with 132 verified, 0 errors
-------------------- Celebrity.dfy --------------------
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
-------------------- UltraFilter.dfy --------------------
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 77af9327..25e6cc5c 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,9 +1,5 @@
// Celebrity example, inspired by the Rodin tutorial
-method Pick<T>(S: set<T>) returns (t: T);
- requires S != {};
- ensures t in S;
-
static function method Knows<Person>(a: Person, b: Person): bool;
requires a != b; // forbid asking about the reflexive case
@@ -26,20 +22,20 @@ method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r:
ensures r == c;
{
var Q := people;
- call x := Pick(Q);
+ var x := choose(Q);
while (Q != {x})
//invariant Q <= people; // inv1 in Rodin's Celebrity_1, but it's not needed here
invariant IsCelebrity(c, Q); // inv2
invariant x in Q;
decreases Q;
{
- call y := Pick(Q - {x});
+ var y := choose(Q - {x});
if (Knows(x, y)) {
Q := Q - {x}; // remove_1
} else {
Q := Q - {y}; assert x in Q; // remove_2
}
- call x := Pick(Q);
+ x := choose(Q);
}
r := x;
}
@@ -48,7 +44,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
requires IsCelebrity(c, people);
ensures r == c;
{
- call b := Pick(people);
+ var b := choose(people);
var R := people - {b};
while (R != {})
invariant R <= people; // inv1
@@ -58,7 +54,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
decreases R;
{
- call x := Pick(R);
+ var x := choose(R);
if (Knows(x, b)) {
R := R - {x};
} else {
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index cc3d6fb2..a0f5f34c 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -36,7 +36,7 @@
"invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
- "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "print"
+ "assert" "assume" "break" "call" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"
"old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "allocated" "use"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "int" "object" "set" "seq")) . font-lock-type-face)
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 26d4f45a..80082ec9 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -27,7 +27,7 @@ namespace Demo
"in", "forall", "exists",
"seq", "set", "array", "array2", "array3",
"match", "case",
- "fresh", "allocated", "old"
+ "fresh", "allocated", "old", "choose"
);
StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);
@@ -337,6 +337,7 @@ namespace Demo
| "fresh"
| "allocated"
| "old"
+ | "choose"
| ident
| "}"
| "{"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index a4d67f0b..30e44a90 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -242,6 +242,7 @@ namespace DafnyLanguage
case "by":
case "call":
case "case":
+ case "choose":
case "class":
case "datatype":
case "decreases":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 11af30d4..4a98fa4c 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -11,7 +11,7 @@
method,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
- match,case,false,true,null,old,fresh,allocated,this,
+ match,case,false,true,null,old,fresh,allocated,choose,this,
% statements
assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,label,return,foreach,
},
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 5c492a31..bdf35f2e 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -13,7 +13,7 @@ syntax keyword dafnyStatement havoc assume assert return call new print break la
syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
syntax keyword dafnyType int bool seq set object array array2 array3
syntax keyword dafnyLogic requires ensures modifies reads decreases invariant
-syntax keyword dafnyOperator forall exists old fresh allocated
+syntax keyword dafnyOperator forall exists old fresh allocated choose
syntax keyword dafnyBoolean true false
syntax region dafnyString start=/"/ skip=/\\"/ end=/"/
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 17:48:15 +0000