summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Mike Barnett <mbarnett@microsoft.com>2011-05-28 13:03:36 -0700
committerGravatar Mike Barnett <mbarnett@microsoft.com>2011-05-28 13:03:36 -0700
commitc7c9cd675bf6024a8f725c84fe22e17d3deb7a98 (patch)
treeaa14fc3477bfd361b38e39037a82cbffece90ed5
parent2ce23c96bfe860cfbe5662d3565037e556700ee8 (diff)
parent637c673e223e91ab81067391e2197516b4691840 (diff)
Merge
Diffstat
-rw-r--r--Source/Dafny/Compiler.cs101
-rw-r--r--Source/Dafny/Dafny.atg107
-rw-r--r--Source/Dafny/Parser.cs548
-rw-r--r--Source/Dafny/Printer.cs4
-rw-r--r--Source/Dafny/Resolver.cs10
-rw-r--r--Source/Dafny/Scanner.cs146
-rw-r--r--Source/Dafny/Translator.cs22
-rw-r--r--Test/dafny0/Answer8
-rw-r--r--Test/dafny0/Basics.dfy10
-rw-r--r--Test/dafny0/SmallTests.dfy15
-rw-r--r--Test/dafny1/Answer2
-rw-r--r--Test/dafny1/Induction.dfy13
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs43
13 files changed, 556 insertions, 473 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 82604794..0fbeb9d6 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -211,7 +211,7 @@ namespace Microsoft.Dafny {
Indent(ind);
wr.Write("public {0}(", DtCtorName(ctor));
- WriteFormals(ctor.Formals);
+ WriteFormals("", ctor.Formals);
wr.WriteLine(") {");
i = 0;
foreach (Formal arg in ctor.Formals) {
@@ -297,11 +297,11 @@ namespace Microsoft.Dafny {
wr.WriteLine("}");
}
- void WriteFormals(List<Formal/*!*/>/*!*/ formals)
+ void WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals)
{
+ Contract.Requires(sep != null);
Contract.Requires(cce.NonNullElements(formals));
int i = 0;
- string sep = "";
foreach (Formal arg in formals) {
if (!arg.IsGhost) {
string name = FormalName(arg, i);
@@ -349,47 +349,9 @@ namespace Microsoft.Dafny {
wr.Write("<{0}>", TypeParameters(f.TypeArgs));
}
wr.Write("(");
- WriteFormals(f.Formals);
+ WriteFormals("", f.Formals);
wr.WriteLine(") {");
- if (f.Body is MatchExpr) {
- MatchExpr me = (MatchExpr)f.Body;
- // Type source = e;
- // if (source._D is Dt_Ctor0) {
- // FormalType f0 = ((Dt_Ctor0)source._D).a0;
- // ...
- // return Body0;
- // } else if (...) {
- // ...
- // } else if (true) {
- // ...
- // }
-
- string source = "_source" + tmpVarCount;
- tmpVarCount++;
- Indent(indent);
- wr.Write("{0} {1} = ", TypeName(cce.NonNull(me.Source.Type)), source);
- TrExpr(me.Source);
- wr.WriteLine(";");
-
- int i = 0;
- foreach (MatchCaseExpr mc in me.Cases) {
- MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
-
- Indent(indent + 2*IndentAmount);
- wr.Write("return ");
- TrExpr(mc.Body);
- wr.WriteLine(";");
- i++;
- }
-
- Indent(indent); wr.WriteLine("}");
-
- } else {
- Indent(indent + IndentAmount);
- wr.Write("return ");
- TrExpr(f.Body);
- wr.WriteLine(";");
- }
+ CompileReturnBody(f.Body, indent);
Indent(indent); wr.WriteLine("}");
}
@@ -402,11 +364,8 @@ namespace Microsoft.Dafny {
wr.Write("<{0}>", TypeParameters(m.TypeArgs));
}
wr.Write("(");
- WriteFormals(m.Ins);
- if (m.Ins.Count != 0 && m.Outs.Count != 0) {
- wr.Write(", ");
- }
- WriteFormals(m.Outs);
+ WriteFormals("", m.Ins);
+ WriteFormals(", ", m.Outs);
wr.WriteLine(")");
Indent(indent); wr.WriteLine("{");
foreach (Formal p in m.Outs) {
@@ -453,7 +412,51 @@ namespace Microsoft.Dafny {
}
}
}
-
+
+ void CompileReturnBody(Expression body, int indent) {
+ body = body.Resolved;
+ if (body is MatchExpr) {
+ MatchExpr me = (MatchExpr)body;
+ // Type source = e;
+ // if (source._D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source._D).a0;
+ // ...
+ // return Body0;
+ // } else if (...) {
+ // ...
+ // } else if (true) {
+ // ...
+ // }
+
+ string source = "_source" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent);
+ wr.Write("{0} {1} = ", TypeName(cce.NonNull(me.Source.Type)), source);
+ TrExpr(me.Source);
+ wr.WriteLine(";");
+
+ if (me.Cases.Count == 0) {
+ // the verifier would have proved we never get here; still, we need some code that will compile
+ Indent(indent);
+ wr.WriteLine("throw new System.Exception();");
+ } else {
+ int i = 0;
+ foreach (MatchCaseExpr mc in me.Cases) {
+ MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
+ CompileReturnBody(mc.Body, indent + IndentAmount);
+ i++;
+ }
+ Indent(indent); wr.WriteLine("}");
+ }
+
+ } else {
+ Indent(indent + IndentAmount);
+ wr.Write("return ");
+ TrExpr(body);
+ wr.WriteLine(";");
+ }
+ }
+
// ----- Type ---------------------------------------------------------------------------------
readonly string DafnySetClass = "Dafny.Set";
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 11a2dfed..91028093 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -328,12 +328,12 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
.
-GIdentType<bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
-/* isGhost always returns as false if allowGhost is false */
+GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
+/* isGhost always returns as false if allowGhostKeyword is false */
= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false; .)
- [ "ghost" (. if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
+ [ "ghost" (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
]
IdentType<out id, out ty>
.
@@ -430,7 +430,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
[ GenericParameters<typeArgs> ]
Formals<true, !mmod.IsGhost, ins>
[ "returns"
- Formals<false, true, outs>
+ Formals<false, !mmod.IsGhost, outs>
]
( ";" { MethodSpec<req, mod, ens, dec> }
@@ -464,12 +464,12 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
)
.
-Formals<.bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals.>
+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .)
"("
[
- GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
- { "," GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
+ GIdentType<allowGhostKeyword, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
+ { "," GIdentType<allowGhostKeyword, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
}
]
")"
@@ -635,52 +635,10 @@ FrameExpression<out FrameExpression/*!*/ fe>
FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
"{" (. bodyStart = t; .)
- ( MatchExpression<out e>
- | Expression<out e>
- )
+ Expression<out e>
"}" (. bodyEnd = t; .)
.
-MatchExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
- List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- .)
- "match" (. x = t; .)
- Expression<out e>
- /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,
- but it's okay, because we want this closer match expression to bind as much as possible--use
- parens around it to limit its scope. */
- { CaseExpression<out c> (. cases.Add(c); .)
- }
- (. e = new MatchExpr(x, e, cases); .)
- .
-
-CaseExpression<out MatchCaseExpr/*!*/ c>
-= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
- List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
- Expression/*!*/ body;
- .)
- "case" (. x = t; .)
- Ident<out id>
- [ "("
- Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
- { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
- }
- ")" ]
- "=>"
- MatchOrExpr<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
- .
-
-/* Note, '(' is start of more than one alternative in MatchOrExpr, but the first intentionally hides
- the third alternative in this regard, in order to also allow match expressions to be parenthesized. */
-MatchOrExpr<out Expression/*!*/ e>
-= (. e = dummyExpr; .)
- ( "(" MatchOrExpr<out e> ")"
- | MatchExpression<out e>
- | Expression<out e>
- )
- .
-
/*------------------------------------------------------------------------*/
BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
@@ -1190,6 +1148,7 @@ UnaryExpression<out Expression/*!*/ e>
| EndlessExpression<out e> /* these have no further suffix */
| DottedIdentifiersAndFunction<out e>
{ Suffix<ref e> }
+ | DisplayExpr<out e>
| ConstAtomExpression<out e>
{ Suffix<ref e> }
)
@@ -1214,7 +1173,7 @@ NegOp = "!" | '\u00ac'.
*/
ConstAtomExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; BigInteger n; List<Expression/*!*/>/*!*/ elements;
+ IToken/*!*/ x; BigInteger n;
e = dummyExpr;
.)
( "false" (. e = new LiteralExpr(t, false); .)
@@ -1231,15 +1190,23 @@ ConstAtomExpression<out Expression/*!*/ e>
| "|" (. x = t; .)
Expression<out e> (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
"|"
- | "{" (. x = t; elements = new List<Expression/*!*/>(); .)
+ | "(" (. x = t; .)
+ Expression<out e> (. e = new ParensExpression(x, e); .)
+ ")"
+ )
+ .
+
+DisplayExpr<out Expression e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x; List<Expression/*!*/>/*!*/ elements;
+ e = dummyExpr;
+ .)
+ ( "{" (. x = t; elements = new List<Expression/*!*/>(); .)
[ Expressions<elements> ] (. e = new SetDisplayExpr(x, elements); .)
"}"
| "[" (. x = t; elements = new List<Expression/*!*/>(); .)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements); .)
"]"
- | "(" (. x = t; .)
- Expression<out e> (. e = new ParensExpression(x, e); .)
- ")"
)
.
@@ -1252,11 +1219,41 @@ EndlessExpression<out Expression e>
Expression<out e>
"then" Expression<out e0>
"else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
+ | MatchExpression<out e>
| QuantifierGuts<out e>
| ComprehensionExpr<out e>
)
.
+MatchExpression<out Expression/*!*/ e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
+ List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
+ .)
+ "match" (. x = t; .)
+ Expression<out e>
+ /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,
+ but it's okay, because we want this closer match expression to bind as much as possible--use
+ parens around it to limit its scope. */
+ { CaseExpression<out c> (. cases.Add(c); .)
+ }
+ (. e = new MatchExpr(x, e, cases); .)
+ .
+
+CaseExpression<out MatchCaseExpr/*!*/ c>
+= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
+ List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ Expression/*!*/ body;
+ .)
+ "case" (. x = t; .)
+ Ident<out id>
+ [ "("
+ Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
+ { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
+ }
+ ")" ]
+ "=>"
+ Expression<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
+ .
/*------------------------------------------------------------------------*/
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 840344bd..100e34e1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -144,10 +144,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);
}
@@ -160,15 +160,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 {
@@ -192,7 +192,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -511,7 +511,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Formals(true, !mmod.IsGhost, ins);
if (la.kind == 26) {
Get();
- Formals(false, true, outs);
+ Formals(false, !mmod.IsGhost, outs);
}
if (la.kind == 17) {
Get();
@@ -604,13 +604,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
EquivExpression(out e);
}
- void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
+ void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false;
if (la.kind == 11) {
Get();
- if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
+ if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
IdentType(out id, out ty);
}
@@ -723,15 +723,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
- void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {
+ void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
Expect(32);
if (la.kind == 1 || la.kind == 11) {
- GIdentType(allowGhosts, out id, out ty, out isGhost);
+ GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
while (la.kind == 19) {
Get();
- GIdentType(allowGhosts, out id, out ty, out isGhost);
+ GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
@@ -894,11 +894,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
Expect(7);
bodyStart = t;
- if (la.kind == 44) {
- MatchExpression(out e);
- } else if (StartOf(8)) {
- Expression(out e);
- } else SynErr(114);
+ Expression(out e);
Expect(8);
bodyEnd = t;
}
@@ -910,7 +906,7 @@ List<Expression/*!*/>/*!*/ decreases) {
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(115);
+ } else SynErr(114);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -921,58 +917,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(116);
- }
-
- void MatchExpression(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
- List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
-
- Expect(44);
- x = t;
- Expression(out e);
- while (la.kind == 45) {
- CaseExpression(out c);
- cases.Add(c);
- }
- e = new MatchExpr(x, e, cases);
- }
-
- void CaseExpression(out MatchCaseExpr/*!*/ c) {
- Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
- List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
- Expression/*!*/ body;
-
- Expect(45);
- x = t;
- Ident(out id);
- if (la.kind == 32) {
- Get();
- Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- while (la.kind == 19) {
- Get();
- Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- }
- Expect(33);
- }
- Expect(46);
- MatchOrExpr(out body);
- c = new MatchCaseExpr(x, id.val, arguments, body);
- }
-
- void MatchOrExpr(out Expression/*!*/ e) {
- e = dummyExpr;
- if (la.kind == 32) {
- Get();
- MatchOrExpr(out e);
- Expect(33);
- } else if (la.kind == 44) {
- MatchExpression(out e);
- } else if (StartOf(8)) {
- Expression(out e);
- } else SynErr(117);
+ } else SynErr(115);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -988,55 +933,85 @@ List<Expression/*!*/>/*!*/ decreases) {
IToken bodyStart, bodyEnd;
int breakCount;
- if (la.kind == 7) {
+ switch (la.kind) {
+ case 7: {
BlockStmt(out s, out bodyStart, out bodyEnd);
- } else if (la.kind == 63) {
+ break;
+ }
+ case 63: {
AssertStmt(out s);
- } else if (la.kind == 64) {
+ break;
+ }
+ case 64: {
AssumeStmt(out s);
- } else if (la.kind == 65) {
+ break;
+ }
+ case 65: {
PrintStmt(out s);
- } else if (StartOf(11)) {
+ break;
+ }
+ case 1: case 2: case 16: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
UpdateStmt(out s);
- } else if (la.kind == 56) {
+ break;
+ }
+ case 53: {
HavocStmt(out s);
- } else if (la.kind == 11 || la.kind == 18) {
+ break;
+ }
+ case 11: case 18: {
VarDeclStatement(out s);
- } else if (la.kind == 57) {
+ break;
+ }
+ case 54: {
IfStmt(out s);
- } else if (la.kind == 59) {
+ break;
+ }
+ case 58: {
WhileStmt(out s);
- } else if (la.kind == 44) {
+ break;
+ }
+ case 60: {
MatchStmt(out s);
- } else if (la.kind == 61) {
+ break;
+ }
+ case 61: {
ForeachStmt(out s);
- } else if (la.kind == 47) {
+ break;
+ }
+ case 44: {
Get();
x = t;
Ident(out id);
Expect(22);
OneStmt(out s);
s.Labels = new LabelNode(x, id.val, s.Labels);
- } else if (la.kind == 48) {
+ break;
+ }
+ case 45: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- } else if (la.kind == 17 || la.kind == 48) {
- while (la.kind == 48) {
+ } else if (la.kind == 17 || la.kind == 45) {
+ while (la.kind == 45) {
Get();
breakCount++;
}
- } else SynErr(118);
+ } else SynErr(116);
Expect(17);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
- } else if (la.kind == 49) {
+ break;
+ }
+ case 46: {
Get();
x = t;
Expect(17);
s = new ReturnStmt(x);
- } else SynErr(119);
+ break;
+ }
+ default: SynErr(117); break;
+ }
}
void AssertStmt(out Statement/*!*/ s) {
@@ -1086,14 +1061,14 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 17) {
Get();
rhss.Add(new ExprRhs(e));
- } else if (la.kind == 19 || la.kind == 50) {
+ } else if (la.kind == 19 || la.kind == 47) {
lhss.Add(e); lhs0 = e;
while (la.kind == 19) {
Get();
Lhs(out e);
lhss.Add(e);
}
- Expect(50);
+ Expect(47);
x = t;
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1106,13 +1081,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 22) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(120);
+ } else SynErr(118);
s = new UpdateStmt(x, lhss, rhss);
}
void HavocStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
- Expect(56);
+ Expect(53);
x = t;
Lhs(out lhs);
Expect(17);
@@ -1139,7 +1114,7 @@ List<Expression/*!*/>/*!*/ decreases) {
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 50) {
+ if (la.kind == 47) {
Get();
assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
Rhs(out r, lhs0);
@@ -1175,26 +1150,26 @@ List<Expression/*!*/>/*!*/ decreases) {
List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(57);
+ Expect(54);
x = t;
if (la.kind == 32) {
Guard(out guard);
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 58) {
+ if (la.kind == 55) {
Get();
- if (la.kind == 57) {
+ if (la.kind == 54) {
IfStmt(out s);
els = s;
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(121);
+ } else SynErr(119);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(122);
+ } else SynErr(120);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1207,7 +1182,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(59);
+ Expect(58);
x = t;
if (la.kind == 32) {
Guard(out guard);
@@ -1215,22 +1190,22 @@ List<Expression/*!*/>/*!*/ decreases) {
LoopSpec(out invariants, out decreases);
BlockStmt(out body, out bodyStart, out bodyEnd);
stmt = new WhileStmt(x, guard, invariants, decreases, body);
- } else if (StartOf(12)) {
+ } else if (StartOf(11)) {
LoopSpec(out invariants, out decreases);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
- } else SynErr(123);
+ } else SynErr(121);
}
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(44);
+ Expect(60);
x = t;
Expression(out e);
Expect(7);
- while (la.kind == 45) {
+ while (la.kind == 56) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1275,13 +1250,13 @@ List<Expression/*!*/>/*!*/ decreases) {
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
}
}
- if (StartOf(11)) {
+ if (StartOf(12)) {
UpdateStmt(out s);
bodyAssign = s;
- } else if (la.kind == 56) {
+ } else if (la.kind == 53) {
HavocStmt(out s);
bodyAssign = s;
- } else SynErr(124);
+ } else SynErr(122);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1296,16 +1271,16 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 52 || la.kind == 54) {
+ while (la.kind == 49 || la.kind == 51) {
Suffix(ref e);
}
} else if (StartOf(13)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 52 || la.kind == 54) {
+ while (la.kind == 49 || la.kind == 51) {
Suffix(ref e);
}
- } else SynErr(125);
+ } else SynErr(123);
}
void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {
@@ -1316,16 +1291,16 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> args;
r = null; // to please compiler
- if (la.kind == 51) {
+ if (la.kind == 48) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 52 || la.kind == 54) {
- if (la.kind == 52) {
+ if (la.kind == 49 || la.kind == 51) {
+ if (la.kind == 49) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(53);
+ Expect(50);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
@@ -1347,7 +1322,7 @@ List<Expression/*!*/>/*!*/ decreases) {
r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 55) {
+ } else if (la.kind == 52) {
Get();
x = t;
Expression(out e);
@@ -1355,7 +1330,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(126);
+ } else SynErr(124);
}
void Guard(out Expression e) {
@@ -1367,7 +1342,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(127);
+ } else SynErr(125);
Expect(33);
}
@@ -1378,11 +1353,11 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Statement> body;
Expect(7);
- while (la.kind == 45) {
+ while (la.kind == 56) {
Get();
x = t;
Expression(out e);
- Expect(46);
+ Expect(57);
body = new List<Statement>();
while (StartOf(9)) {
Stmt(body);
@@ -1397,14 +1372,14 @@ List<Expression/*!*/>/*!*/ decreases) {
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
- while (la.kind == 28 || la.kind == 31 || la.kind == 60) {
- if (la.kind == 28 || la.kind == 60) {
+ while (la.kind == 28 || la.kind == 31 || la.kind == 59) {
+ if (la.kind == 28 || la.kind == 59) {
isFree = false;
if (la.kind == 28) {
Get();
isFree = true;
}
- Expect(60);
+ Expect(59);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(17);
@@ -1428,7 +1403,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(45);
+ Expect(56);
x = t;
Ident(out id);
if (la.kind == 32) {
@@ -1442,7 +1417,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(33);
}
- Expect(46);
+ Expect(57);
while (StartOf(9)) {
Stmt(body);
}
@@ -1457,7 +1432,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(128);
+ } else SynErr(126);
}
void EquivExpression(out Expression/*!*/ e0) {
@@ -1487,7 +1462,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 67) {
Get();
- } else SynErr(129);
+ } else SynErr(127);
}
void LogicalExpression(out Expression/*!*/ e0) {
@@ -1525,7 +1500,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 69) {
Get();
- } else SynErr(130);
+ } else SynErr(128);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1608,7 +1583,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 71) {
Get();
- } else SynErr(131);
+ } else SynErr(129);
}
void OrOp() {
@@ -1616,7 +1591,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(132);
+ } else SynErr(130);
}
void Term(out Expression/*!*/ e0) {
@@ -1692,7 +1667,7 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(133); break;
+ default: SynErr(131); break;
}
}
@@ -1714,34 +1689,50 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(134);
+ } else SynErr(132);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 84) {
+ switch (la.kind) {
+ case 84: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (la.kind == 87 || la.kind == 88) {
+ break;
+ }
+ case 87: case 88: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
- } else if (StartOf(16)) {
+ break;
+ }
+ case 37: case 54: case 60: case 98: case 99: case 100: case 101: {
EndlessExpression(out e);
- } else if (la.kind == 1) {
+ break;
+ }
+ case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 52 || la.kind == 54) {
+ while (la.kind == 49 || la.kind == 51) {
Suffix(ref e);
}
- } else if (StartOf(13)) {
+ break;
+ }
+ case 7: case 49: {
+ DisplayExpr(out e);
+ break;
+ }
+ case 2: case 16: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
ConstAtomExpression(out e);
- while (la.kind == 52 || la.kind == 54) {
+ while (la.kind == 49 || la.kind == 51) {
Suffix(ref e);
}
- } else SynErr(135);
+ break;
+ }
+ default: SynErr(133); break;
+ }
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1755,7 +1746,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(136);
+ } else SynErr(134);
}
void NegOp() {
@@ -1763,7 +1754,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 88) {
Get();
- } else SynErr(137);
+ } else SynErr(135);
}
void EndlessExpression(out Expression e) {
@@ -1771,20 +1762,22 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression e0, e1;
e = dummyExpr;
- if (la.kind == 57) {
+ if (la.kind == 54) {
Get();
x = t;
Expression(out e);
Expect(96);
Expression(out e0);
- Expect(58);
+ Expect(55);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
- } else if (StartOf(17)) {
+ } else if (la.kind == 60) {
+ MatchExpression(out e);
+ } else if (StartOf(16)) {
QuantifierGuts(out e);
} else if (la.kind == 37) {
ComprehensionExpr(out e);
- } else SynErr(138);
+ } else SynErr(136);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1794,7 +1787,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Ident(out id);
idents.Add(id);
- while (la.kind == 54) {
+ while (la.kind == 51) {
Get();
Ident(out id);
idents.Add(id);
@@ -1816,7 +1809,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 54) {
+ if (la.kind == 51) {
Get();
Ident(out id);
if (la.kind == 32) {
@@ -1829,7 +1822,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (la.kind == 52) {
+ } else if (la.kind == 49) {
Get();
x = t;
if (StartOf(8)) {
@@ -1842,11 +1835,11 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 50) {
+ } else if (la.kind == 47) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 19 || la.kind == 53) {
+ } else if (la.kind == 19 || la.kind == 50) {
while (la.kind == 19) {
Get();
Expression(out ee);
@@ -1857,12 +1850,12 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(139);
+ } else SynErr(137);
} else if (la.kind == 97) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(140);
+ } else SynErr(138);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1885,13 +1878,37 @@ List<Expression/*!*/>/*!*/ decreases) {
}
}
- Expect(53);
- } else SynErr(141);
+ Expect(50);
+ } else SynErr(139);
+ }
+
+ void DisplayExpr(out Expression e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ x; List<Expression/*!*/>/*!*/ elements;
+ e = dummyExpr;
+
+ if (la.kind == 7) {
+ Get();
+ x = t; elements = new List<Expression/*!*/>();
+ if (StartOf(8)) {
+ Expressions(elements);
+ }
+ e = new SetDisplayExpr(x, elements);
+ Expect(8);
+ } else if (la.kind == 49) {
+ Get();
+ x = t; elements = new List<Expression/*!*/>();
+ if (StartOf(8)) {
+ Expressions(elements);
+ }
+ e = new SeqDisplayExpr(x, elements);
+ Expect(50);
+ } else SynErr(140);
}
void ConstAtomExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; BigInteger n; List<Expression/*!*/>/*!*/ elements;
+ IToken/*!*/ x; BigInteger n;
e = dummyExpr;
switch (la.kind) {
@@ -1955,26 +1972,6 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(16);
break;
}
- case 7: {
- Get();
- x = t; elements = new List<Expression/*!*/>();
- if (StartOf(8)) {
- Expressions(elements);
- }
- e = new SetDisplayExpr(x, elements);
- Expect(8);
- break;
- }
- case 52: {
- Get();
- x = t; elements = new List<Expression/*!*/>();
- if (StartOf(8)) {
- Expressions(elements);
- }
- e = new SeqDisplayExpr(x, elements);
- Expect(53);
- break;
- }
case 32: {
Get();
x = t;
@@ -1983,7 +1980,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(33);
break;
}
- default: SynErr(142); break;
+ default: SynErr(141); break;
}
}
@@ -1998,6 +1995,20 @@ List<Expression/*!*/>/*!*/ decreases) {
}
+ void MatchExpression(out Expression/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
+ List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
+
+ Expect(60);
+ x = t;
+ Expression(out e);
+ while (la.kind == 56) {
+ CaseExpression(out c);
+ cases.Add(c);
+ }
+ e = new MatchExpr(x, e, cases);
+ }
+
void QuantifierGuts(out Expression/*!*/ q) {
Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
bool univ = false;
@@ -2014,7 +2025,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 100 || la.kind == 101) {
Exists();
x = t;
- } else SynErr(143);
+ } else SynErr(142);
IdentTypeOptional(out bv);
bvars.Add(bv);
while (la.kind == 19) {
@@ -2067,12 +2078,36 @@ List<Expression/*!*/>/*!*/ decreases) {
}
+ void CaseExpression(out MatchCaseExpr/*!*/ c) {
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
+ List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ Expression/*!*/ body;
+
+ Expect(56);
+ x = t;
+ Ident(out id);
+ if (la.kind == 32) {
+ Get();
+ Ident(out arg);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ while (la.kind == 19) {
+ Get();
+ Ident(out arg);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ }
+ Expect(33);
+ }
+ Expect(57);
+ Expression(out body);
+ c = new MatchCaseExpr(x, id.val, arguments, body);
+ }
+
void Forall() {
if (la.kind == 98) {
Get();
} else if (la.kind == 99) {
Get();
- } else SynErr(144);
+ } else SynErr(143);
}
void Exists() {
@@ -2080,7 +2115,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 101) {
Get();
- } else SynErr(145);
+ } else SynErr(144);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2093,7 +2128,7 @@ List<Expression/*!*/>/*!*/ decreases) {
es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(146);
+ } else SynErr(145);
Expect(8);
}
@@ -2102,7 +2137,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 103) {
Get();
- } else SynErr(147);
+ } else SynErr(146);
}
void AttributeBody(ref Attributes attrs) {
@@ -2113,7 +2148,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(18)) {
+ if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2129,13 +2164,13 @@ 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, x,x,T,x, T,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,x,x,x, x,x,x,x, x,x},
@@ -2145,17 +2180,16 @@ List<Expression/*!*/>/*!*/ decreases) {
{x,x,x,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,T, 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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, T,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, 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, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,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, T,x,x,T, T,T,x,x, T,x,x,x, T,T,x,T, x,T,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,T,T,T, T,T,T,T, 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, T,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,T,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, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,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,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,T,x, x,x,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,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, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,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,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,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, T,T,T,x, x,x,x,x, x,T,T,x, x,x,T,x, T,T,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,T,T,T, T,T,T,T, 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, T,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,T,x, x,x,x,x, x,T,x,x, x,x,T,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,T,T,T, x,x,T,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, 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,T,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, 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,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, 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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, T,x,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, T,x,x,x, x,T,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, T,x,x,T, T,T,T,T, T,T,T,T, 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, T,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,T,x,x, x,x,T,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,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
@@ -2164,20 +2198,18 @@ 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;
@@ -2224,23 +2256,23 @@ public class Errors {
case 41: s = "\"reads\" expected"; break;
case 42: s = "\"*\" expected"; break;
case 43: s = "\"`\" expected"; break;
- case 44: s = "\"match\" expected"; break;
- case 45: s = "\"case\" expected"; break;
- case 46: s = "\"=>\" expected"; break;
- case 47: s = "\"label\" expected"; break;
- case 48: s = "\"break\" expected"; break;
- case 49: s = "\"return\" expected"; break;
- case 50: s = "\":=\" expected"; break;
- case 51: s = "\"new\" expected"; break;
- case 52: s = "\"[\" expected"; break;
- case 53: s = "\"]\" expected"; break;
- case 54: s = "\".\" expected"; break;
- case 55: s = "\"choose\" expected"; break;
- case 56: s = "\"havoc\" expected"; break;
- case 57: s = "\"if\" expected"; break;
- case 58: s = "\"else\" expected"; break;
- case 59: s = "\"while\" expected"; break;
- case 60: s = "\"invariant\" expected"; break;
+ case 44: s = "\"label\" expected"; break;
+ case 45: s = "\"break\" expected"; break;
+ case 46: s = "\"return\" expected"; break;
+ case 47: s = "\":=\" expected"; break;
+ case 48: s = "\"new\" expected"; break;
+ case 49: s = "\"[\" expected"; break;
+ case 50: s = "\"]\" expected"; break;
+ case 51: s = "\".\" expected"; break;
+ case 52: s = "\"choose\" expected"; break;
+ case 53: s = "\"havoc\" 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 = "\"foreach\" expected"; break;
case 62: s = "\"in\" expected"; break;
case 63: s = "\"assert\" expected"; break;
@@ -2294,44 +2326,43 @@ public class Errors {
case 111: s = "invalid MethodSpec"; break;
case 112: s = "invalid ReferenceType"; break;
case 113: s = "invalid FunctionSpec"; break;
- case 114: s = "invalid FunctionBody"; break;
- case 115: s = "invalid PossiblyWildFrameExpression"; break;
- case 116: s = "invalid PossiblyWildExpression"; break;
- case 117: s = "invalid MatchOrExpr"; break;
- case 118: s = "invalid OneStmt"; break;
- case 119: s = "invalid OneStmt"; break;
- case 120: s = "invalid UpdateStmt"; break;
- case 121: s = "invalid IfStmt"; break;
- case 122: s = "invalid IfStmt"; break;
- case 123: s = "invalid WhileStmt"; break;
- case 124: s = "invalid ForeachStmt"; break;
- case 125: s = "invalid Lhs"; break;
- case 126: s = "invalid Rhs"; break;
- case 127: s = "invalid Guard"; 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 EndlessExpression"; break;
+ case 114: s = "invalid PossiblyWildFrameExpression"; break;
+ case 115: s = "invalid PossiblyWildExpression"; break;
+ case 116: s = "invalid OneStmt"; break;
+ case 117: s = "invalid OneStmt"; break;
+ case 118: s = "invalid UpdateStmt"; break;
+ case 119: s = "invalid IfStmt"; break;
+ case 120: s = "invalid IfStmt"; break;
+ case 121: s = "invalid WhileStmt"; break;
+ case 122: s = "invalid ForeachStmt"; break;
+ case 123: s = "invalid Lhs"; break;
+ case 124: s = "invalid Rhs"; break;
+ case 125: s = "invalid Guard"; break;
+ case 126: s = "invalid AttributeArg"; break;
+ case 127: s = "invalid EquivOp"; break;
+ case 128: s = "invalid ImpliesOp"; break;
+ case 129: s = "invalid AndOp"; break;
+ case 130: s = "invalid OrOp"; break;
+ case 131: s = "invalid RelOp"; break;
+ case 132: s = "invalid AddOp"; break;
+ case 133: s = "invalid UnaryExpression"; break;
+ case 134: s = "invalid MulOp"; break;
+ case 135: s = "invalid NegOp"; break;
+ case 136: s = "invalid EndlessExpression"; break;
+ case 137: s = "invalid Suffix"; break;
+ case 138: s = "invalid Suffix"; break;
case 139: s = "invalid Suffix"; break;
- case 140: s = "invalid Suffix"; break;
- case 141: s = "invalid Suffix"; break;
- case 142: s = "invalid ConstAtomExpression"; 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 140: s = "invalid DisplayExpr"; break;
+ case 141: s = "invalid ConstAtomExpression"; break;
+ case 142: s = "invalid QuantifierGuts"; break;
+ case 143: s = "invalid Forall"; break;
+ case 144: s = "invalid Exists"; break;
+ case 145: s = "invalid AttributeOrTrigger"; break;
+ case 146: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2339,9 +2370,8 @@ 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 5ee2f0c9..6a84a361 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -712,7 +712,7 @@ namespace Microsoft.Dafny {
}
wr.Write(")");
}
- bool parensNeeded = !isLastCase && mc.Body is MatchExpr;
+ bool parensNeeded = !isLastCase && mc.Body.Resolved is MatchExpr;
if (parensNeeded) {
wr.WriteLine(" => (");
} else {
@@ -721,6 +721,8 @@ namespace Microsoft.Dafny {
PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, parensNeeded || (isLastCase && endWithCloseParen));
i++;
}
+ } else if (expr is ParensExpression) {
+ PrintExtendedExpr((ParensExpression)expr, indent, isRightmost, endWithCloseParen);
} else {
PrintExpression(expr, indent);
wr.WriteLine(endWithCloseParen ? ")" : "");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 96907777..b1bbe6c4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1993,6 +1993,10 @@ namespace Microsoft.Dafny {
ResolveExpression(expr, twoState, null);
}
+ /// <summary>
+ /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;
+ /// if null, no "match" expression will be allowed.
+ /// </summary>
void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {
Contract.Requires(expr != null);
Contract.Requires(currentClass != null);
@@ -2009,7 +2013,7 @@ namespace Microsoft.Dafny {
if (expr is ParensExpression) {
var e = (ParensExpression)expr;
- ResolveExpression(e.E, twoState);
+ ResolveExpression(e.E, twoState, matchVarContext); // allow "match" expressions inside e.E if the parenthetic expression had been allowed to be a "match" expression
e.ResolvedExpression = e.E;
e.Type = e.E.Type;
@@ -2464,6 +2468,10 @@ namespace Microsoft.Dafny {
} else if (expr is MatchExpr) {
MatchExpr me = (MatchExpr)expr;
Contract.Assert(!twoState); // currently, match expressions are allowed only at the outermost level of function bodies
+ if (matchVarContext == null) {
+ Error(me, "'match' expressions are not supported in this context");
+ matchVarContext = new List<IVariable>();
+ }
ResolveExpression(me.Source, twoState);
Contract.Assert(me.Source.Type != null); // follows from postcondition of ResolveExpression
UserDefinedType sourceType = null;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 083c0c0c..d45bbbbe 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,17 +31,15 @@ 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;
@@ -53,12 +51,12 @@ public class Buffer {
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;
@@ -75,14 +73,14 @@ public class Buffer {
}
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -102,7 +100,7 @@ public class Buffer {
Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -141,7 +139,7 @@ public class Buffer {
}
}
}
-
+
// 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.
@@ -215,20 +213,19 @@ public class Scanner {
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);
- }
-
+[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
@@ -239,13 +236,13 @@ public class Scanner {
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;
@@ -270,8 +267,8 @@ public class Scanner {
start[41] = 22;
start[42] = 23;
start[96] = 24;
- start[91] = 27;
- start[93] = 28;
+ start[91] = 26;
+ start[93] = 27;
start[46] = 62;
start[8660] = 31;
start[8658] = 33;
@@ -293,9 +290,9 @@ public class Scanner {
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;
@@ -305,14 +302,15 @@ public class Scanner {
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);
@@ -321,9 +319,10 @@ public class Scanner {
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
+
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -344,11 +343,11 @@ public class Scanner {
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 +358,7 @@ public class Scanner {
}
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -367,9 +366,9 @@ public class Scanner {
// // 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 +418,7 @@ public class Scanner {
return;
}
-
+
}
}
@@ -513,18 +512,18 @@ public class Scanner {
case "object": t.kind = 39; break;
case "function": t.kind = 40; break;
case "reads": t.kind = 41; break;
- case "match": t.kind = 44; break;
- case "case": t.kind = 45; break;
- case "label": t.kind = 47; break;
- case "break": t.kind = 48; break;
- case "return": t.kind = 49; break;
- case "new": t.kind = 51; break;
- case "choose": t.kind = 55; break;
- case "havoc": t.kind = 56; break;
- case "if": t.kind = 57; break;
- case "else": t.kind = 58; break;
- case "while": t.kind = 59; break;
- case "invariant": t.kind = 60; break;
+ case "label": t.kind = 44; break;
+ case "break": t.kind = 45; break;
+ case "return": t.kind = 46; break;
+ case "new": t.kind = 48; break;
+ case "choose": t.kind = 52; break;
+ case "havoc": 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 "foreach": t.kind = 61; break;
case "in": t.kind = 62; break;
case "assert": t.kind = 63; break;
@@ -556,13 +555,10 @@ public class Scanner {
t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) {
- Contract.Assert(start[ch] != null);
- state = (int) start[ch];
- }
+ if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -657,13 +653,13 @@ public class Scanner {
case 24:
{t.kind = 43; break;}
case 25:
- {t.kind = 46; break;}
+ {t.kind = 47; break;}
case 26:
- {t.kind = 50; break;}
+ {t.kind = 49; break;}
case 27:
- {t.kind = 52; break;}
+ {t.kind = 50; break;}
case 28:
- {t.kind = 53; break;}
+ {t.kind = 57; break;}
case 29:
if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
@@ -725,7 +721,7 @@ public class Scanner {
{t.kind = 103; break;}
case 57:
recEnd = pos; recKind = 15;
- if (ch == '>') {AddCh(); goto case 25;}
+ if (ch == '>') {AddCh(); goto case 28;}
else if (ch == '=') {AddCh(); goto case 64;}
else {t.kind = 15; break;}
case 58:
@@ -734,7 +730,7 @@ public class Scanner {
else {t.kind = 16; break;}
case 59:
recEnd = pos; recKind = 22;
- if (ch == '=') {AddCh(); goto case 26;}
+ if (ch == '=') {AddCh(); goto case 25;}
else if (ch == ':') {AddCh(); goto case 55;}
else {t.kind = 22; break;}
case 60:
@@ -746,9 +742,9 @@ public class Scanner {
if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 24; break;}
case 62:
- recEnd = pos; recKind = 54;
+ recEnd = pos; recKind = 51;
if (ch == '.') {AddCh(); goto case 52;}
- else {t.kind = 54; break;}
+ else {t.kind = 51; break;}
case 63:
recEnd = pos; recKind = 87;
if (ch == '=') {AddCh(); goto case 40;}
@@ -768,14 +764,14 @@ public class Scanner {
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);
@@ -796,7 +792,7 @@ public class Scanner {
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 19272ef4..8752ffea 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -460,12 +460,13 @@ namespace Microsoft.Dafny {
AddLimitedAxioms(f, 1);
}
for (int layerOffset = 0; layerOffset < 2; layerOffset++) {
- if (f.Body is MatchExpr) {
- AddFunctionAxiomCase(f, (MatchExpr)f.Body, null, layerOffset);
+ var body = f.Body == null ? null : f.Body.Resolved;
+ if (body is MatchExpr) {
+ AddFunctionAxiomCase(f, (MatchExpr)body, null, layerOffset);
Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null, layerOffset);
sink.TopLevelDeclarations.Add(axPost);
} else {
- Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null, layerOffset);
+ Bpl.Axiom ax = FunctionAxiom(f, body, f.Ens, null, layerOffset);
sink.TopLevelDeclarations.Add(ax);
}
if (!f.IsRecursive || f.IsUnlimited) { break; }
@@ -510,10 +511,11 @@ namespace Microsoft.Dafny {
foreach (MatchCaseExpr mc in me.Cases) {
Contract.Assert(mc.Ctor != null); // the field is filled in by resolution
Specialization s = new Specialization(formal, mc, prev);
- if (mc.Body is MatchExpr) {
- AddFunctionAxiomCase(f, (MatchExpr)mc.Body, s, layerOffset);
+ var body = mc.Body.Resolved;
+ if (body is MatchExpr) {
+ AddFunctionAxiomCase(f, (MatchExpr)body, s, layerOffset);
} else {
- Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), s, layerOffset);
+ Bpl.Axiom ax = FunctionAxiom(f, body, new List<Expression>(), s, layerOffset);
sink.TopLevelDeclarations.Add(ax);
}
}
@@ -2093,6 +2095,7 @@ namespace Microsoft.Dafny {
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
CheckWellformedWithResult(e.ResolvedExpression, options, result, resultType, locals, builder, etran);
+ result = null;
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
@@ -3067,7 +3070,8 @@ namespace Microsoft.Dafny {
Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
// TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
- oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, o)));
+ var boxO = etran.BoxIfNecessary(stmt.Tok, o, ((SeqType)s.Collection.Type).Arg);
+ oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));
}
oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);
@@ -5332,7 +5336,7 @@ namespace Microsoft.Dafny {
} else if (expandFunctions && expr is FunctionCallExpr) {
var fexp = (FunctionCallExpr)expr;
Contract.Assert(fexp.Function != null); // filled in during resolution
- if (fexp.Function.Body != null && !(fexp.Function.Body is MatchExpr)) {
+ if (fexp.Function.Body != null && !(fexp.Function.Body.Resolved is MatchExpr)) {
// inline this body
Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
Contract.Assert(fexp.Args.Count == fexp.Function.Formals.Count);
@@ -5533,7 +5537,7 @@ namespace Microsoft.Dafny {
// consider automatically applying induction
var inductionVariables = new List<BoundVar>();
foreach (var n in e.BoundVars) {
- if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
+ if (!n.Type.IsTypeParameter && VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
if (CommandLineOptions.Clo.Trace) {
Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);
new Printer(Console.Out).PrintExpression(e);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5cfee29d..05250fa8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -201,7 +201,7 @@ Execution trace:
(0,0): anon15
(0,0): anon25_Else
-Dafny program verifier finished with 41 verified, 14 errors
+Dafny program verifier finished with 43 verified, 14 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
@@ -579,6 +579,10 @@ Execution trace:
Dafny program verifier finished with 6 verified, 1 error
-------------------- Basics.dfy --------------------
+Basics.dfy(42,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
Basics.dfy(66,42): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -592,7 +596,7 @@ Execution trace:
Basics.dfy(66,95): anon18_Else
(0,0): anon12
-Dafny program verifier finished with 8 verified, 1 error
+Dafny program verifier finished with 7 verified, 2 errors
-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index c02f2c45..16fd7d87 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -1,6 +1,6 @@
class Global {
static function G(x: int): int { x+x }
- static method N(x: int) returns (ghost r: int)
+ static method N(ghost x: int) returns (ghost r: int)
ensures r == Global.G(x);
{
if {
@@ -23,8 +23,8 @@ method TestCalls(k: nat) {
ghost var r: int;
ghost var s := Global.G(k);
-// r := Global.N(k);
-// assert r == s;
+ r := Global.N(k);
+ assert r == s;
r := g.N(k);
assert r == s;
@@ -35,11 +35,11 @@ method TestCalls(k: nat) {
r := g.N(k);
assert r == s;
-// r := Global.N(r);
+ r := Global.N(r);
if (k == 0) {
assert r == s;
} else {
-// assert r == s; // error: G(k) and G(k+k) are different
+ assert r == s; // error: G(k) and G(k+k) are different
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index b4dc6599..ac7286e9 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -308,7 +308,7 @@ method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
}
}
-// ----------------------- tests that involve sequences of boxed booleans --------
+// ----------------------- tests that involve sequences of boxes --------
ghost method M(zeros: seq<bool>, Z: bool)
requires 1 <= |zeros| && Z == false;
@@ -317,3 +317,16 @@ ghost method M(zeros: seq<bool>, Z: bool)
var x := [Z];
assert zeros[0..1] == [Z];
}
+
+class SomeType
+{
+ var x: int;
+ method DoIt(stack: seq<SomeType>)
+ modifies stack;
+ {
+ // the following line once gave rise to a crash in the translation
+ foreach (n in stack) {
+ n.x := 10;
+ }
+ }
+}
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 0111f9af..5ee9f921 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -81,7 +81,7 @@ Dafny program verifier finished with 6 verified, 0 errors
-------------------- Induction.dfy --------------------
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 29 verified, 0 errors
-------------------- Rippling.dfy --------------------
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index de5a3358..15cc1ffe 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -153,6 +153,19 @@ class DatatypeInduction<T> {
}
// see also Test/dafny0/DTypes.dfy for more variations of this example
+
+ function OccurrenceCount<T>(tree: Tree<T>, x: T): int
+ {
+ match tree
+ case Leaf(t) => if x == t then 1 else 0
+ case Branch(left, right) => OccurrenceCount(left, x) + OccurrenceCount(right, x)
+ }
+ method RegressionTest(tree: Tree<T>)
+ // the translation of the following line once crashed Dafny
+ requires forall y :: 0 <= OccurrenceCount(tree, y);
+ {
+ }
+
}
// ----------------------- Induction and case splits -----------------
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs
index b9a0ca22..ce43e6e4 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs
@@ -176,21 +176,25 @@ namespace Demo
// the lines of interest have the form "filename(line,col): some_error_label: error_message"
// where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location"
if (line.Equals("")) continue;
- if (line.StartsWith("Dafny program verifier finished with") && line.Contains("time out"))
+ if (line.StartsWith("Dafny program verifier finished with"))
{
- try
+ if (line.Contains("time out"))
{
AddErrorBecauseOfToolProblems(req, "Verification timed out.");
}
- catch (System.FormatException)
+ else
{
- continue;
+ if (!line.Contains("inconclusive") && !line.Contains("out of memory"))
+ {
+ if (line.Contains(" 0 errors"))
+ AddMessage(req, "Verification successful.");
+ }
+ else
+ {
+ AddErrorBecauseOfToolProblems(req, "Internal verification fault.");
+ }
}
- catch (System.OverflowException)
- {
- continue;
- }
- continue;
+ break;
}
string message;
int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..."
@@ -271,12 +275,21 @@ namespace Demo
return new AuthoringScope(source.ParseResult);
}
- private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg) {
- TextSpan span = new TextSpan();
- span.iStartLine = span.iEndLine = 1;
- span.iStartIndex = 1;
- span.iEndIndex = 2;
- req.Sink.AddError(req.FileName, msg, span, Severity.Error);
+ private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg)
+ {
+ TextSpan span = new TextSpan();
+ span.iStartLine = span.iEndLine = 0;
+ span.iStartIndex = 0;
+ span.iEndIndex = 0;
+ req.Sink.AddError(req.FileName, msg, span, Severity.Error);
+ }
+ private static void AddMessage(ParseRequest req, string msg)
+ {
+ TextSpan span = new TextSpan();
+ span.iStartLine = span.iEndLine = 0;
+ span.iStartIndex = 0;
+ span.iEndIndex = 1;
+ req.Sink.AddError(req.FileName, msg, span, Severity.Hint);
}
/// <summary>
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 11:49:01 +0000