diff options
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 274 |
1 files changed, 252 insertions, 22 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index bc394f04..5ddc1fac 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -62,10 +62,8 @@ namespace Microsoft.Dafny { private Queue<Action> postTasks = new Queue<Action>(); // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction
public void PreResolve(ModuleDefinition m) {
- if (m.RefinementBase == null) {
- // This Rewriter doesn't do anything
- return;
- }
+
+ if (m.RefinementBase == null) return;
if (moduleUnderConstruction != null) {
postTasks.Clear();
@@ -280,7 +278,7 @@ namespace Microsoft.Dafny { return new MapType(CloneType(tt.Domain), CloneType(tt.Range));
} else if (t is UserDefinedType) {
var tt = (UserDefinedType)t;
- return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : Tok(tt.ModuleName));
+ return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => Tok(x)));
} else if (t is InferredTypeProxy) {
return new InferredTypeProxy();
} else {
@@ -425,6 +423,9 @@ namespace Microsoft.Dafny { var e = (LetExpr)expr;
return new LetExpr(Tok(e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));
+ } else if (expr is NamedExpr) {
+ var e = (NamedExpr) expr;
+ return new NamedExpr(Tok(e.tok), e.Name, CloneExpr(e.Body));
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
var tk = Tok(e.tok);
@@ -702,8 +703,12 @@ namespace Microsoft.Dafny { } else {
var nwMember = nw.Members[index];
if (nwMember is Field) {
- reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) is not allowed replace an existing declaration in the refinement base", nwMember.Name, nw.Name);
-
+ if (member is Field && TypesAreEqual(((Field)nwMember).Type, ((Field)member).Type)) {
+ if (member.IsGhost || !nwMember.IsGhost)
+ reporter.Error(nwMember, "a field re-declaration ({0}) must be to ghostify the field", nwMember.Name, nw.Name);
+ } else {
+ reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) must replace a field in the refinement base", nwMember.Name, nw.Name);
+ }
} else if (nwMember is Function) {
var f = (Function)nwMember;
bool isPredicate = f is Predicate;
@@ -804,7 +809,228 @@ namespace Microsoft.Dafny { return nw;
}
+ private Statement SubstituteNamedExpr(Statement s, IToken p, Expression E, ref int subCount) {
+ if (s == null) {
+ return null;
+ } else if (s is AssertStmt) {
+ AssertStmt stmt = (AssertStmt)s;
+ return new AssertStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);
+ } else if (s is AssumeStmt) {
+ AssumeStmt stmt = (AssumeStmt)s;
+ return new AssumeStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);
+ } else if (s is PrintStmt) {
+ throw new NotImplementedException();
+ } else if (s is BreakStmt) {
+ return s;
+ } else if (s is ReturnStmt) {
+ return s;
+ } else if (s is VarDeclStmt) {
+ return s;
+ } else if (s is AssignSuchThatStmt) {
+ return s;
+ } else if (s is UpdateStmt) {
+ UpdateStmt stmt = (UpdateStmt)s;
+ List<Expression> lhs = new List<Expression>();
+ List<AssignmentRhs> rhs = new List<AssignmentRhs>();
+ foreach (Expression l in stmt.Lhss) {
+ lhs.Add(SubstituteNamedExpr(l, p, E, ref subCount));
+ }
+ foreach (AssignmentRhs r in stmt.Rhss) {
+ if (r is HavocRhs) {
+ rhs.Add(r); // no substitution on Havoc (*);
+ } else if (r is ExprRhs) {
+ rhs.Add(new ExprRhs(SubstituteNamedExpr(((ExprRhs)r).Expr, p, E, ref subCount)));
+ } else if (r is CallRhs) {
+ CallRhs rr = (CallRhs)r;
+ rhs.Add(new CallRhs(rr.Tok, SubstituteNamedExpr(rr.Receiver, p, E, ref subCount), rr.MethodName, SubstituteNamedExprList(rr.Args, p, E, ref subCount)));
+ } else if (r is TypeRhs) {
+ rhs.Add(r);
+ } else {
+ Contract.Assert(false); // unexpected AssignmentRhs
+ throw new cce.UnreachableException();
+ }
+ }
+ return new UpdateStmt(stmt.Tok, lhs, rhs);
+ } else if (s is AssignStmt) {
+ Contract.Assert(false); // AssignStmt is not generated by the parser
+ throw new cce.UnreachableException();
+ } else if (s is VarDecl) {
+ return s;
+ } else if (s is CallStmt) {
+ return s;
+ } else if (s is BlockStmt) {
+ BlockStmt stmt = (BlockStmt)s;
+ List<Statement> res = new List<Statement>();
+ foreach (Statement ss in stmt.Body) {
+ res.Add(SubstituteNamedExpr(ss, p, E, ref subCount));
+ }
+ return new BlockStmt(stmt.Tok, res);
+ } else if (s is IfStmt) {
+ IfStmt stmt = (IfStmt)s;
+ return new IfStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount),
+ (BlockStmt)SubstituteNamedExpr(stmt.Thn, p, E, ref subCount),
+ SubstituteNamedExpr(stmt.Els, p, E, ref subCount));
+ } else if (s is AlternativeStmt) {
+ return s;
+ } else if (s is WhileStmt) {
+ WhileStmt stmt = (WhileStmt)s;
+ return new WhileStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount), stmt.Invariants, stmt.Decreases, stmt.Mod, (BlockStmt)SubstituteNamedExpr(stmt.Body, p, E, ref subCount));
+ } else if (s is AlternativeLoopStmt) {
+ return s;
+ } else if (s is ParallelStmt) {
+ return s;
+ } else if (s is MatchStmt) {
+ return s;
+ } else if (s is SkeletonStatement) {
+ return s;
+ } else {
+ Contract.Assert(false); // unexpected statement
+ throw new cce.UnreachableException();
+ }
+ }
+ private Expression SubstituteNamedExpr(Expression expr, IToken p, Expression E, ref int subCount) {
+ if (expr == null) {
+ return null;
+ }
+ if (expr is NamedExpr) {
+ NamedExpr n = (NamedExpr)expr;
+ if (n.Name == p.val) {
+ subCount++;
+ return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), p);
+ } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, p, E, ref subCount));
+ } else if (expr is LiteralExpr || expr is WildcardExpr | expr is ThisExpr || expr is IdentifierExpr) {
+ return expr;
+ } else if (expr is DisplayExpression) {
+ DisplayExpression e = (DisplayExpression)expr;
+ List<Expression> newElements = SubstituteNamedExprList(e.Elements, p, E, ref subCount);
+ if (expr is SetDisplayExpr) {
+ return new SetDisplayExpr(expr.tok, newElements);
+ } else if (expr is MultiSetDisplayExpr) {
+ return new MultiSetDisplayExpr(expr.tok, newElements);
+ } else {
+ return new SeqDisplayExpr(expr.tok, newElements);
+ }
+ } else if (expr is FieldSelectExpr) {
+ FieldSelectExpr fse = (FieldSelectExpr)expr;
+ Expression substE = SubstituteNamedExpr(fse.Obj, p, E, ref subCount);
+ return new FieldSelectExpr(fse.tok, substE, fse.FieldName);
+ } else if (expr is SeqSelectExpr) {
+ SeqSelectExpr sse = (SeqSelectExpr)expr;
+ Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);
+ Expression e0 = sse.E0 == null ? null : SubstituteNamedExpr(sse.E0, p, E, ref subCount);
+ Expression e1 = sse.E1 == null ? null : SubstituteNamedExpr(sse.E1, p, E, ref subCount);
+ return new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr sse = (SeqUpdateExpr)expr;
+ Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);
+ Expression index = SubstituteNamedExpr(sse.Index, p, E, ref subCount);
+ Expression val = SubstituteNamedExpr(sse.Value, p, E, ref subCount);
+ return new SeqUpdateExpr(sse.tok, seq, index, val);
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr mse = (MultiSelectExpr)expr;
+ Expression array = SubstituteNamedExpr(mse.Array, p, E, ref subCount);
+ List<Expression> newArgs = SubstituteNamedExprList(mse.Indices, p, E, ref subCount);
+ return new MultiSelectExpr(mse.tok, array, newArgs);
+ } else if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+ Expression receiver = SubstituteNamedExpr(e.Receiver, p, E, ref subCount);
+ List<Expression> newArgs = SubstituteNamedExprList(e.Args, p, E, ref subCount);
+ return new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ List<Expression> newArgs = SubstituteNamedExprList(dtv.Arguments, p, E, ref subCount);
+ return new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);
+ } else if (expr is OldExpr) {
+ OldExpr e = (OldExpr)expr;
+ Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ return new OldExpr(expr.tok, se);
+ } else if (expr is FreshExpr) {
+ FreshExpr e = (FreshExpr)expr;
+ Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ return new FreshExpr(expr.tok, se);
+ } else if (expr is AllocatedExpr) {
+ AllocatedExpr e = (AllocatedExpr)expr;
+ Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ return new AllocatedExpr(expr.tok, se);
+ } else if (expr is UnaryExpr) {
+ UnaryExpr e = (UnaryExpr)expr;
+ Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ return new UnaryExpr(expr.tok, e.Op, se);
+ } else if (expr is BinaryExpr) {
+ BinaryExpr e = (BinaryExpr)expr;
+ Expression e0 = SubstituteNamedExpr(e.E0, p, E, ref subCount);
+ Expression e1 = SubstituteNamedExpr(e.E1, p, E, ref subCount);
+ return new BinaryExpr(expr.tok, e.Op, e0, e1);
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ var rhss = SubstituteNamedExprList(e.RHSs, p, E, ref subCount);
+ var body = SubstituteNamedExpr(e.Body, p, E, ref subCount);
+ return new LetExpr(e.tok, e.Vars, rhss, body);
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ Expression newRange = e.Range == null ? null : SubstituteNamedExpr(e.Range, p, E, ref subCount);
+ Expression newTerm = SubstituteNamedExpr(e.Term, p, E, ref subCount);
+ Attributes newAttrs = e.Attributes;//SubstituteNamedExpr(e.Attributes, p, E, ref subCount);
+ if (e is SetComprehension) {
+ return new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);
+ } else if (e is MapComprehension) {
+ return new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);
+ } else if (e is QuantifierExpr) {
+ var q = (QuantifierExpr)e;
+ if (expr is ForallExpr) {
+ return new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
+ } else {
+ return new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
+ }
+ } else {
+ Contract.Assert(false); // unexpected ComprehensionExpr
+ throw new cce.UnreachableException();
+ }
+
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Expression g = SubstituteNamedExpr(e.Guard, p, E, ref subCount);
+ Expression b = SubstituteNamedExpr(e.Body, p, E, ref subCount);
+ if (expr is AssertExpr) {
+ return new AssertExpr(e.tok, g, b);
+ } else {
+ return new AssumeExpr(e.tok, g, b);
+ }
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ Expression test = SubstituteNamedExpr(e.Test, p, E, ref subCount);
+ Expression thn = SubstituteNamedExpr(e.Thn, p, E, ref subCount);
+ Expression els = SubstituteNamedExpr(e.Els, p, E, ref subCount);
+ return new ITEExpr(expr.tok, test, thn, els);
+ } else if (expr is ConcreteSyntaxExpression) {
+ if (expr is ParensExpression) {
+ return SubstituteNamedExpr(((ParensExpression)expr).E, p, E, ref subCount);
+ } else if (expr is IdentifierSequence) {
+ return expr;
+ } else if (expr is ExprDotName) {
+ ExprDotName edn = (ExprDotName)expr;
+ return new ExprDotName(edn.tok, SubstituteNamedExpr(edn.Obj, p, E, ref subCount), edn.SuffixName);
+ } else if (expr is ChainingExpression) {
+ ChainingExpression ch = (ChainingExpression)expr;
+ return SubstituteNamedExpr(ch.E, p, E, ref subCount);
+ } else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ } else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ }
+
+ private List<Expression> SubstituteNamedExprList(List<Expression> list, IToken p, Expression E, ref int subCount) {
+ List<Expression> res = new List<Expression>();
+ foreach (Expression e in list) {
+ res.Add(SubstituteNamedExpr(e, p, E, ref subCount));
+ }
+ return res;
+ }
void CheckAgreement_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing) {
Contract.Requires(tok != null);
Contract.Requires(old != null);
@@ -920,7 +1146,8 @@ namespace Microsoft.Dafny { * while (G) LoopSpec ... while (*) LoopSpec' Body while (G) Merge(LoopSpec,LoopSpec') Body
* while (G) LoopSpec Body while (*) LoopSpec' Body' while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')
*
- * ...; S StmtThatDoesNotMatchS; S' StatementThatDoesNotMatchS; Merge( ...;S , S')
+ * ... where x = e; S StmtThatDoesNotMatchS; S' StatementThatDoesNotMatchS[e/x]; Merge( ... where x = e; S , S')
+ * ... where x = e; S StmtThatMatchesS; S' StmtThatMatchesS; S'
*
* Note, LoopSpec must contain only invariant declarations (as the parser ensures for the first three cases).
* Note, there is an implicit "...;" at the end of every block in a skeleton.
@@ -929,23 +1156,26 @@ namespace Microsoft.Dafny { */
if (cur is SkeletonStatement) {
var S = ((SkeletonStatement)cur).S;
+ var c = (SkeletonStatement) cur;
if (S == null) {
- if (i + 1 == skeleton.Body.Count) {
- // this "...;" is the last statement of the skeleton, so treat it like the default case
+ var nxt = i + 1 == skeleton.Body.Count ? null : skeleton.Body[i+1];
+ if (nxt != null && nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {
+ // "...; ...;" is the same as just "...;", so skip this one
} else {
- var nxt = skeleton.Body[i+1];
- if (nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {
- // "...; ...;" is the same as just "...;", so skip this one
- } else {
- // skip up until the next thing that matches "nxt"
- while (!PotentialMatch(nxt, oldS)) {
- // loop invariant: oldS == oldStmt.Body[j]
- body.Add(CloneStmt(oldS));
- j++;
- if (j == oldStmt.Body.Count) { break; }
- oldS = oldStmt.Body[j];
- }
+ int subCount = 0;
+ // skip up until the next thing that matches "nxt"
+ while (nxt == null || !PotentialMatch(nxt, oldS)) {
+ // loop invariant: oldS == oldStmt.Body[j]
+ var s = CloneStmt(oldS);
+ if (c.NameReplacements != null)
+ s = SubstituteNamedExpr(s, c.NameReplacements[0], c.ExprReplacements[0], ref subCount);
+ body.Add(s);
+ j++;
+ if (j == oldStmt.Body.Count) { break; }
+ oldS = oldStmt.Body[j];
}
+ if (c.NameReplacements != null && subCount == 0)
+ reporter.Error(c.NameReplacements[0], "did not find expression labeled {0}", c.NameReplacements[0].val);
}
i++;
|