diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 18:44:52 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 18:44:52 -0700 |
| commit | 811efa1a56080a8f5c652352a384ae2dea4616ee (patch) | |
| tree | 96ef1be443d10fb6cca1f9b578aea195d164deda /Source/Dafny/RefinementTransformer.cs | |
| parent | 46b31d5f040c6849bf9053a97e1c9f2041070cea (diff) | |
Dafny: support assign-such-that in var declarations in refinements
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 57 |
1 files changed, 54 insertions, 3 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index f3e54b01..a10cb4bf 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -779,9 +779,13 @@ namespace Microsoft.Dafny { * assert ...; assert E; assert E;
* assert E; assert E;
*
- * var x:=E; var x; var x:=E;
+ * var x := E; var x; var x := E;
+ * var x := E; var x := *; var x := E;
+ * var x := E1; var x :| E0; var x := E1; assert E0;
* var VarProduction; var VarProduction;
*
+ * x := E; x := *; x := E;
+ *
* if ... Then else Else if (G) Then' else Else' if (G) Merge(Then,Then') else Merge(Else,Else')
* if (G) Then else Else if (*) Then' else Else' if (G) Merge(Then,Then') else Merge(Else,Else')
*
@@ -885,8 +889,55 @@ namespace Microsoft.Dafny { } else if (cur is VarDeclStmt) {
var cNew = (VarDeclStmt)cur;
var cOld = oldS as VarDeclStmt;
- if (cOld != null && cNew.Lhss.Count == 1 && cOld.Lhss.Count == 1 && cNew.Lhss[0].Name == cOld.Lhss[0].Name && cOld.Update == null) {
- // Note, we allow switching between ghost and non-ghost, since that seems unproblematic.
+ bool doMerge = false;
+ Expression addedAssert = null;
+ if (cOld != null && cNew.Lhss.Count == 1 && cOld.Lhss.Count == 1 && cNew.Lhss[0].Name == cOld.Lhss[0].Name) {
+ var update = cNew.Update as UpdateStmt;
+ if (update != null && update.Rhss.Count == 1 && update.Rhss[0] is ExprRhs) {
+ // Note, we allow switching between ghost and non-ghost, since that seems unproblematic.
+ if (cOld.Update == null) {
+ doMerge = true;
+ } else if (cOld.Update is AssignSuchThatStmt) {
+ doMerge = true;
+ addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Assume.Expr);
+ } else {
+ var updateOld = (UpdateStmt)cOld.Update; // if cast fails, there are more ConcreteUpdateStatement subclasses than expected
+ if (updateOld.Rhss.Count == 1 && updateOld.Rhss[0] is HavocRhs) {
+ doMerge = true;
+ }
+ }
+ }
+ }
+ if (doMerge) {
+ // Go ahead with the merge:
+ body.Add(cNew);
+ i++; j++;
+ if (addedAssert != null) {
+ body.Add(new AssertStmt(addedAssert.tok, addedAssert));
+ }
+ } else {
+ MergeAddStatement(cur, body);
+ i++;
+ }
+
+ } else if (cur is AssignStmt) {
+ var cNew = (AssignStmt)cur;
+ var cOld = oldS as AssignStmt;
+ if (cOld == null && oldS is UpdateStmt) {
+ var us = (UpdateStmt)oldS;
+ if (us.ResolvedStatements.Count == 1) {
+ cOld = us.ResolvedStatements[0] as AssignStmt;
+ }
+ }
+ bool doMerge = false;
+ if (cOld != null && cNew.Lhs.Resolved is IdentifierExpr && cOld.Lhs.Resolved is IdentifierExpr) {
+ if (((IdentifierExpr)cNew.Lhs.Resolved).Name == ((IdentifierExpr)cOld.Lhs.Resolved).Name) {
+ if (!(cNew.Rhs is TypeRhs) && cOld.Rhs is HavocRhs) {
+ doMerge = true;
+ }
+ }
+ }
+ if (doMerge) {
// Go ahead with the merge:
body.Add(cNew);
i++; j++;
|