summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar Nadia Polikarpova <nadia.polikarpova@gmail.com>2012-09-16 15:19:55 +0200
committerGravatar Nadia Polikarpova <nadia.polikarpova@gmail.com>2012-09-16 15:19:55 +0200
commit497c4e1792a3c6c2033ec19a114a87033c510136 (patch)
tree5f30fa8c437342f1b062c03acc3f780fcae2c5e4 /Source/Dafny
parentc987bdcca18980910c8089f7b585a4016dbc2c07 (diff)
Allowing calc as hint (without braces)
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Dafny.atg2
-rw-r--r--Source/Dafny/Parser.cs25
2 files changed, 17 insertions, 10 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index adb17fb7..7e608945 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1224,6 +1224,7 @@ CalcStmt<out Statement/*!*/ s>
List<Statement> hints = new List<Statement>();
Expression/*!*/ e;
BlockStmt/*!*/ block;
+ Statement/*!*/ h;
IToken bodyStart, bodyEnd;
.)
"calc" (. x = t; .)
@@ -1232,6 +1233,7 @@ CalcStmt<out Statement/*!*/ s>
";"
{
( BlockStmt<out block, out bodyStart, out bodyEnd> (. hints.Add(block); .)
+ | CalcStmt<out h> (. hints.Add(h); .)
| (. hints.Add(null); .)
)
Expression<out e> (. lines.Add(e); .)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 7c8cf8a2..89bf8292 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1623,6 +1623,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Statement> hints = new List<Statement>();
Expression/*!*/ e;
BlockStmt/*!*/ block;
+ Statement/*!*/ h;
IToken bodyStart, bodyEnd;
Expect(75);
@@ -1631,10 +1632,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e);
lines.Add(e);
Expect(14);
- while (StartOf(10)) {
+ while (StartOf(14)) {
if (la.kind == 6) {
BlockStmt(out block, out bodyStart, out bodyEnd);
hints.Add(block);
+ } else if (la.kind == 75) {
+ CalcStmt(out h);
+ hints.Add(h);
} else {
hints.Add(null);
}
@@ -1653,7 +1657,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(58);
returnTok = t;
- if (StartOf(14)) {
+ if (StartOf(15)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 24) {
@@ -1787,7 +1791,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (la.kind == 17 || la.kind == 62) {
Suffix(ref e);
}
- } else if (StartOf(15)) {
+ } else if (StartOf(16)) {
ConstAtomExpression(out e);
Suffix(ref e);
while (la.kind == 17 || la.kind == 62) {
@@ -1848,7 +1852,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(16)) {
+ while (StartOf(17)) {
if (la.kind == 36 || la.kind == 70) {
Invariant(out invariant);
while (!(la.kind == 0 || la.kind == 14)) {SynErr(165); Get();}
@@ -1994,7 +1998,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(17)) {
+ if (StartOf(18)) {
if (la.kind == 80 || la.kind == 81) {
AndOp();
x = t;
@@ -2043,7 +2047,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Term(out e0);
e = e0;
- if (StartOf(18)) {
+ if (StartOf(19)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
@@ -2051,7 +2055,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (op == BinaryExpr.Opcode.Disjoint)
acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
- while (StartOf(18)) {
+ while (StartOf(19)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -2301,7 +2305,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e);
- } else if (StartOf(19)) {
+ } else if (StartOf(20)) {
SemErr("map must be followed by literal in brackets or comprehension.");
} else SynErr(178);
break;
@@ -2548,7 +2552,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e);
e = new MultiSetFormingExpr(x, e);
Expect(28);
- } else if (StartOf(20)) {
+ } else if (StartOf(21)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
} else SynErr(187);
}
@@ -2850,7 +2854,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(5);
Expect(1);
aName = t.val;
- if (StartOf(21)) {
+ if (StartOf(22)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 24) {
@@ -2889,6 +2893,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,T,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},