diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 50 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 108 |
3 files changed, 93 insertions, 69 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 53d0b471..ca526173 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -357,6 +357,10 @@ axiom (forall<T> s: Seq T, v: T, n: int :: { Seq#Drop(Seq#Build(s, v), n) }
0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
+// Additional axioms about common things
+axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][..0] == []
+axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][0..] == []
+
// ---------------------------------------------------------------
// -- Axiomatization of Maps -------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 74e32823..3afdc061 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1411,8 +1411,15 @@ UnaryExpression<out Expression/*!*/ e> | DottedIdentifiersAndFunction<out e>
{ Suffix<ref e> }
| DisplayExpr<out e>
+ { Suffix<ref e> }
| MultiSetExpr<out e>
- | MapExpr<out e>
+ { Suffix<ref e> }
+ | "map" (. x = t; .)
+ ( MapDisplayExpr<x, out e>
+ { Suffix<ref e> }
+ | MapComprehensionExpr<x, out e>
+ | (. SemErr("map must be followed by literal in brackets or comprehension."); .)
+ )
| ConstAtomExpression<out e>
{ Suffix<ref e> }
)
@@ -1482,31 +1489,14 @@ MultiSetExpr<out Expression e> | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)
)
.
-MapExpr<out Expression e>
+MapDisplayExpr<IToken/*!*/ mapToken, out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = Token.NoToken;
- List<ExpressionPair/*!*/>/*!*/ elements;
+ List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
e = dummyExpr;
.)
- "map" (. x = t; .)
- ( "[" (. elements = new List<ExpressionPair/*!*/>(); .)
- [ MapLiteralExpressions<out elements> ] (. e = new MapDisplayExpr(x, elements);.)
- "]"
- | (
- (.
- BoundVar/*!*/ bv;
- List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- Expression/*!*/ range;
- Expression body = null;
- .)
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- "|" Expression<out range>
- QSep
- Expression<out body>
- (. e = new MapComprehension(x, bvars, range, body); .)
- )
- | (. SemErr("map must be followed by literal in brackets or comprehension."); .)
- )
+ "["
+ [ MapLiteralExpressions<out elements> ] (. e = new MapDisplayExpr(mapToken, elements);.)
+ "]"
.
MapLiteralExpressions<.out List<ExpressionPair> elements.>
= (. Expression/*!*/ d, r;
@@ -1515,6 +1505,20 @@ MapLiteralExpressions<.out List<ExpressionPair> elements.> { "," Expression<out d> ":=" Expression<out r>(. elements.Add(new ExpressionPair(d,r)); .)
}
.
+MapComprehensionExpr<IToken/*!*/ mapToken, out Expression e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ Expression range = null;
+ Expression body;
+ .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
+ [ "|" Expression<out range> ]
+ QSep
+ Expression<out body>
+ (. e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body);
+ .)
+ .
EndlessExpression<out Expression e>
= (. IToken/*!*/ x;
Expression e0, e1;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 489a233e..69d13347 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2245,14 +2245,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
case 6: case 62: {
DisplayExpr(out e);
+ while (la.kind == 17 || la.kind == 62) {
+ Suffix(ref e);
+ }
break;
}
case 44: {
MultiSetExpr(out e);
+ while (la.kind == 17 || la.kind == 62) {
+ Suffix(ref e);
+ }
break;
}
case 46: {
- MapExpr(out e);
+ Get();
+ x = t;
+ if (la.kind == 62) {
+ MapDisplayExpr(x, out e);
+ while (la.kind == 17 || la.kind == 62) {
+ Suffix(ref e);
+ }
+ } else if (la.kind == 1) {
+ MapComprehensionExpr(x, out e);
+ } else if (StartOf(19)) {
+ SemErr("map must be followed by literal in brackets or comprehension.");
+ } else SynErr(177);
break;
}
case 2: case 22: case 26: case 97: case 98: case 99: case 100: case 101: case 102: {
@@ -2262,7 +2279,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
break;
}
- default: SynErr(177); break;
+ default: SynErr(178); break;
}
}
@@ -2277,7 +2294,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 95) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(178);
+ } else SynErr(179);
}
void NegOp() {
@@ -2285,7 +2302,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 96) {
Get();
- } else SynErr(179);
+ } else SynErr(180);
}
void EndlessExpression(out Expression e) {
@@ -2343,7 +2360,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e);
break;
}
- default: SynErr(180); break;
+ default: SynErr(181); break;
}
}
@@ -2417,7 +2434,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(181);
+ } else SynErr(182);
} else if (la.kind == 104) {
Get();
anyDots = true;
@@ -2425,7 +2442,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee);
e1 = ee;
}
- } else SynErr(182);
+ } else SynErr(183);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2449,7 +2466,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(63);
- } else SynErr(183);
+ } else SynErr(184);
}
void DisplayExpr(out Expression e) {
@@ -2473,7 +2490,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SeqDisplayExpr(x, elements);
Expect(63);
- } else SynErr(184);
+ } else SynErr(185);
}
void MultiSetExpr(out Expression e) {
@@ -2497,43 +2514,41 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e);
e = new MultiSetFormingExpr(x, e);
Expect(28);
- } else if (StartOf(19)) {
+ } else if (StartOf(20)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(185);
+ } else SynErr(186);
}
- void MapExpr(out Expression e) {
+ void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = Token.NoToken;
- List<ExpressionPair/*!*/>/*!*/ elements;
+ List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
e = dummyExpr;
- Expect(46);
- x = t;
- if (la.kind == 62) {
+ Expect(62);
+ if (StartOf(10)) {
+ MapLiteralExpressions(out elements);
+ }
+ e = new MapDisplayExpr(mapToken, elements);
+ Expect(63);
+ }
+
+ void MapComprehensionExpr(IToken/*!*/ mapToken, out Expression e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ Expression range = null;
+ Expression body;
+
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ if (la.kind == 22) {
Get();
- elements = new List<ExpressionPair/*!*/>();
- if (StartOf(10)) {
- MapLiteralExpressions(out elements);
- }
- e = new MapDisplayExpr(x, elements);
- Expect(63);
- } else if (la.kind == 1) {
- BoundVar/*!*/ bv;
- List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- Expression/*!*/ range;
- Expression body = null;
-
- IdentTypeOptional(out bv);
- bvars.Add(bv);
- Expect(22);
Expression(out range);
- QSep();
- Expression(out body);
- e = new MapComprehension(x, bvars, range, body);
- } else if (StartOf(19)) {
- SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(186);
+ }
+ QSep();
+ Expression(out body);
+ e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body);
+
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2801,7 +2816,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(5);
Expect(1);
aName = t.val;
- if (StartOf(20)) {
+ if (StartOf(21)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 24) {
@@ -2846,6 +2861,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,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,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, 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, T,T,x,x, x,T,x,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,T,x, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,T, x,x,T,T, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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}
};
@@ -3049,15 +3065,15 @@ public class Errors { case 175: s = "invalid RelOp"; break;
case 176: s = "invalid AddOp"; break;
case 177: s = "invalid UnaryExpression"; break;
- case 178: s = "invalid MulOp"; break;
- case 179: s = "invalid NegOp"; break;
- case 180: s = "invalid EndlessExpression"; break;
- case 181: s = "invalid Suffix"; break;
+ case 178: s = "invalid UnaryExpression"; break;
+ case 179: s = "invalid MulOp"; break;
+ case 180: s = "invalid NegOp"; break;
+ case 181: s = "invalid EndlessExpression"; break;
case 182: s = "invalid Suffix"; break;
case 183: s = "invalid Suffix"; break;
- case 184: s = "invalid DisplayExpr"; break;
- case 185: s = "invalid MultiSetExpr"; break;
- case 186: s = "invalid MapExpr"; break;
+ case 184: s = "invalid Suffix"; break;
+ case 185: s = "invalid DisplayExpr"; break;
+ case 186: s = "invalid MultiSetExpr"; break;
case 187: s = "invalid ConstAtomExpression"; break;
case 188: s = "invalid QSep"; break;
case 189: s = "invalid QuantifierGuts"; break;
|