Dafny: allow "assume ..." as a refining statement (provided it replaces an "assume E")

1 files changed, 85 insertions, 70 deletions

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 0c1920a6..a4e51924 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1157,10 +1157,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AssertStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

-		Expression/*!*/ e = null; Attributes attrs = null;

+		Expression e = null; Attributes attrs = null;

 		

 		Expect(67);

-		x = t; s = null;

+		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1179,12 +1179,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AssumeStmt(out Statement/*!*/ s) {

-		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 

+		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

+		Expression e = null; Attributes attrs = null;

+		

 		Expect(55);

 		x = t; 

-		Expression(out e);

+		while (IsAttribute()) {

+			Attribute(ref attrs);

+		}

+		if (StartOf(9)) {

+			Expression(out e);

+		} else if (la.kind == 30) {

+			Get();

+		} else SynErr(145);

+		if (e == null) {

+		 s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

+		} else {

+		 s = new AssumeStmt(x, e, attrs);

+		}

+		

 		Expect(18);

-		s = new AssumeStmt(x, e); 

 	}

 

 	void PrintStmt(out Statement/*!*/ s) {

@@ -1247,12 +1261,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(145);

+			} else SynErr(146);

 			Expect(18);

 		} else if (la.kind == 5) {

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(146);

+		} else SynErr(147);

 		if (suchThat != null) {

 		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

 		} else {

@@ -1357,7 +1371,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				} else if (la.kind == 6) {

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; 

-				} else SynErr(147);

+				} else SynErr(148);

 			}

 			if (guardOmitted) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);

@@ -1368,7 +1382,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 6) {

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(148);

+		} else SynErr(149);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1400,7 +1414,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else if (la.kind == 30) {

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(149);

+			} else SynErr(150);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

@@ -1418,7 +1432,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 

-		} else SynErr(150);

+		} else SynErr(151);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

@@ -1568,7 +1582,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(9)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(151);

+		} else SynErr(152);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1589,7 +1603,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 44 || la.kind == 57) {

 				Suffix(ref e);

 			}

-		} else SynErr(152);

+		} else SynErr(153);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -1612,7 +1626,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(9)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(153);

+		} else SynErr(154);

 		Expect(24);

 	}

 

@@ -1647,20 +1661,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (StartOf(16)) {

 			if (la.kind == 32 || la.kind == 65) {

 				Invariant(out invariant);

-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(155); Get();}

 				Expect(18);

 				invariants.Add(invariant); 

 			} else if (la.kind == 35) {

-				while (!(la.kind == 0 || la.kind == 35)) {SynErr(155); Get();}

+				while (!(la.kind == 0 || la.kind == 35)) {SynErr(156); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();}

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(157); Get();}

 				Expect(18);

 			} else {

-				while (!(la.kind == 0 || la.kind == 31)) {SynErr(157); Get();}

+				while (!(la.kind == 0 || la.kind == 31)) {SynErr(158); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1675,7 +1689,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(158); Get();}

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(159); Get();}

 				Expect(18);

 			}

 		}

@@ -1683,7 +1697,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(159); Get();}

+		while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(160); Get();}

 		if (la.kind == 32) {

 			Get();

 			isFree = true; 

@@ -1732,7 +1746,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(9)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(160);

+		} else SynErr(161);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1784,7 +1798,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 71) {

 			Get();

-		} else SynErr(161);

+		} else SynErr(162);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

@@ -1822,7 +1836,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 73) {

 			Get();

-		} else SynErr(162);

+		} else SynErr(163);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e) {

@@ -1920,7 +1934,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 75) {

 			Get();

-		} else SynErr(163);

+		} else SynErr(164);

 	}

 

 	void OrOp() {

@@ -1928,7 +1942,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 77) {

 			Get();

-		} else SynErr(164);

+		} else SynErr(165);

 	}

 

 	void Term(out Expression/*!*/ e0) {

@@ -2020,7 +2034,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(165); break;

+		default: SynErr(166); break;

 		}

 	}

 

@@ -2042,7 +2056,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 88) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(166);

+		} else SynErr(167);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

@@ -2092,7 +2106,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			break;

 		}

-		default: SynErr(167); break;

+		default: SynErr(168); break;

 		}

 	}

 

@@ -2107,7 +2121,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 90) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(168);

+		} else SynErr(169);

 	}

 

 	void NegOp() {

@@ -2115,7 +2129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 91) {

 			Get();

-		} else SynErr(169);

+		} else SynErr(170);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -2192,7 +2206,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LetExpr(x, letVars, letRHSs, e); 

 			break;

 		}

-		default: SynErr(170); break;

+		default: SynErr(171); break;

 		}

 	}

 

@@ -2266,7 +2280,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(171);

+				} else SynErr(172);

 			} else if (la.kind == 100) {

 				Get();

 				anyDots = true; 

@@ -2274,7 +2288,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(172);

+			} else SynErr(173);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -2298,7 +2312,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			

 			Expect(58);

-		} else SynErr(173);

+		} else SynErr(174);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2322,7 +2336,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(58);

-		} else SynErr(174);

+		} else SynErr(175);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2348,7 +2362,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(24);

 		} else if (StartOf(19)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(175);

+		} else SynErr(176);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2382,7 +2396,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(19)) {

 			SemErr("map must be followed by literal in brackets or comprehension."); 

-		} else SynErr(176);

+		} else SynErr(177);

 	}

 

 	void ConstAtomExpression(out Expression/*!*/ e) {

@@ -2459,7 +2473,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(24);

 			break;

 		}

-		default: SynErr(177); break;

+		default: SynErr(178); break;

 		}

 	}

 

@@ -2495,7 +2509,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 106) {

 			Get();

-		} else SynErr(178);

+		} else SynErr(179);

 	}

 

 	void MatchExpression(out Expression/*!*/ e) {

@@ -2526,7 +2540,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 103 || la.kind == 104) {

 			Exists();

 			x = t; 

-		} else SynErr(179);

+		} else SynErr(180);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2596,7 +2610,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 102) {

 			Get();

-		} else SynErr(180);

+		} else SynErr(181);

 	}

 

 	void Exists() {

@@ -2604,7 +2618,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 104) {

 			Get();

-		} else SynErr(181);

+		} else SynErr(182);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2830,43 +2844,44 @@ public class Errors {
 			case 142: s = "this symbol not expected in OneStmt"; break;

 			case 143: s = "invalid OneStmt"; break;

 			case 144: s = "invalid AssertStmt"; break;

-			case 145: s = "invalid UpdateStmt"; break;

+			case 145: s = "invalid AssumeStmt"; break;

 			case 146: s = "invalid UpdateStmt"; break;

-			case 147: s = "invalid IfStmt"; break;

+			case 147: s = "invalid UpdateStmt"; break;

 			case 148: s = "invalid IfStmt"; break;

-			case 149: s = "invalid WhileStmt"; break;

+			case 149: s = "invalid IfStmt"; break;

 			case 150: s = "invalid WhileStmt"; break;

-			case 151: s = "invalid Rhs"; break;

-			case 152: s = "invalid Lhs"; break;

-			case 153: s = "invalid Guard"; break;

-			case 154: s = "this symbol not expected in LoopSpec"; break;

+			case 151: s = "invalid WhileStmt"; break;

+			case 152: s = "invalid Rhs"; break;

+			case 153: s = "invalid Lhs"; break;

+			case 154: s = "invalid Guard"; break;

 			case 155: s = "this symbol not expected in LoopSpec"; break;

 			case 156: s = "this symbol not expected in LoopSpec"; break;

 			case 157: s = "this symbol not expected in LoopSpec"; break;

 			case 158: s = "this symbol not expected in LoopSpec"; break;

-			case 159: s = "this symbol not expected in Invariant"; break;

-			case 160: s = "invalid AttributeArg"; break;

-			case 161: s = "invalid EquivOp"; break;

-			case 162: s = "invalid ImpliesOp"; break;

-			case 163: s = "invalid AndOp"; break;

-			case 164: s = "invalid OrOp"; break;

-			case 165: s = "invalid RelOp"; break;

-			case 166: s = "invalid AddOp"; break;

-			case 167: s = "invalid UnaryExpression"; break;

-			case 168: s = "invalid MulOp"; break;

-			case 169: s = "invalid NegOp"; break;

-			case 170: s = "invalid EndlessExpression"; break;

-			case 171: s = "invalid Suffix"; break;

+			case 159: s = "this symbol not expected in LoopSpec"; break;

+			case 160: s = "this symbol not expected in Invariant"; break;

+			case 161: s = "invalid AttributeArg"; break;

+			case 162: s = "invalid EquivOp"; break;

+			case 163: s = "invalid ImpliesOp"; break;

+			case 164: s = "invalid AndOp"; break;

+			case 165: s = "invalid OrOp"; break;

+			case 166: s = "invalid RelOp"; break;

+			case 167: s = "invalid AddOp"; break;

+			case 168: s = "invalid UnaryExpression"; break;

+			case 169: s = "invalid MulOp"; break;

+			case 170: s = "invalid NegOp"; break;

+			case 171: s = "invalid EndlessExpression"; break;

 			case 172: s = "invalid Suffix"; break;

 			case 173: s = "invalid Suffix"; break;

-			case 174: s = "invalid DisplayExpr"; break;

-			case 175: s = "invalid MultiSetExpr"; break;

-			case 176: s = "invalid MapExpr"; break;

-			case 177: s = "invalid ConstAtomExpression"; break;

-			case 178: s = "invalid QSep"; break;

-			case 179: s = "invalid QuantifierGuts"; break;

-			case 180: s = "invalid Forall"; break;

-			case 181: s = "invalid Exists"; break;

+			case 174: s = "invalid Suffix"; break;

+			case 175: s = "invalid DisplayExpr"; break;

+			case 176: s = "invalid MultiSetExpr"; break;

+			case 177: s = "invalid MapExpr"; break;

+			case 178: s = "invalid ConstAtomExpression"; break;

+			case 179: s = "invalid QSep"; break;

+			case 180: s = "invalid QuantifierGuts"; break;

+			case 181: s = "invalid Forall"; break;

+			case 182: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}