diff options
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 12 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 59 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 63 |
4 files changed, 102 insertions, 36 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 88aa178a..692cd29b 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1466,17 +1466,27 @@ ModifyStmt<out Statement s> Attributes attrs = null;
FrameExpression fe; var mod = new List<FrameExpression>();
BlockStmt body = null; IToken bodyStart;
+ IToken ellipsisToken = null;
.)
"modify" (. tok = t; .)
{ IF(IsAttribute()) Attribute<ref attrs> }
+ /* Note, there is an ambiguity here, because a curly brace may look like a FrameExpression and
+ * may also look like a BlockStmt. We're happy to parse the former, because if the user intended
+ * the latter, then an explicit FrameExpression of {} could be given.
+ */
[ FrameExpression<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
+ | "..." (. ellipsisToken = t; .)
]
( BlockStmt<out body, out bodyStart, out endTok>
| SYNC ";" (. endTok = t; .)
)
- (. s = new ModifyStmt(tok, endTok, mod, attrs, body); .)
+ (. s = new ModifyStmt(tok, endTok, mod, attrs, body);
+ if (ellipsisToken != null) {
+ s = new SkeletonStmt(s, ellipsisToken, null);
+ }
+ .)
.
CalcStmt<out Statement/*!*/ s>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 51449440..1fc2d787 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3860,6 +3860,10 @@ namespace Microsoft.Dafny { /// ConditionOmitted == true && BodyOmitted == true
/// * while ... invariant J; { Stmt }
/// ConditionOmitted == true && BodyOmitted == false
+ /// * modify ...;
+ /// ConditionOmitted == true && BodyOmitted == false
+ /// * modify ... { Stmt }
+ /// ConditionOmitted == true && BodyOmitted == false
/// </summary>
public class SkeletonStatement : Statement
{
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 209d7273..36ccc433 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -53,6 +53,15 @@ namespace Microsoft.Dafny { }
}
+ public static string FrameExprListToString(List<FrameExpression> fexprs) {
+ Contract.Requires(fexprs != null);
+ using (var wr = new System.IO.StringWriter()) {
+ var pr = new Printer(wr);
+ pr.PrintFrameExpressionList(fexprs);
+ return wr.ToString();
+ }
+ }
+
public static string StatementToString(Statement stmt) {
Contract.Requires(stmt != null);
using (var wr = new System.IO.StringWriter()) {
@@ -728,24 +737,7 @@ namespace Microsoft.Dafny { } else if (stmt is ModifyStmt) {
var s = (ModifyStmt)stmt;
- wr.Write("modify");
- PrintAttributes(s.Mod.Attributes);
- wr.Write(" ");
- PrintFrameExpressionList(s.Mod.Expressions);
- if (s.Body != null) {
- // There's a possible syntactic ambiguity, namely if the frame is empty (more precisely,
- // if s.Mod.Expressions.Count is 0). Since the statement was parsed at some point, this
- // situation can occur only if the modify statement inherited its frame by refinement
- // and we're printing the post-resolve AST. In this special case, print an explicit
- // empty set as the frame.
- if (s.Mod.Expressions.Count == 0) {
- wr.Write(" {}");
- }
- wr.Write(" ");
- PrintStatement(s.Body, indent);
- } else {
- wr.Write(";");
- }
+ PrintModifyStmt(indent, s, false);
} else if (stmt is CalcStmt) {
CalcStmt s = (CalcStmt)stmt;
@@ -861,6 +853,8 @@ namespace Microsoft.Dafny { PrintIfStatement(indent, (IfStmt)s.S, s.ConditionOmitted);
} else if (s.S is WhileStmt) {
PrintWhileStatement(indent, (WhileStmt)s.S, s.ConditionOmitted, s.BodyOmitted);
+ } else if (s.S is ModifyStmt) {
+ PrintModifyStmt(indent, (ModifyStmt)s.S, true);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected skeleton statement
}
@@ -870,6 +864,35 @@ namespace Microsoft.Dafny { }
}
+ private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) {
+ Contract.Requires(0 <= indent);
+ Contract.Requires(s != null);
+ Contract.Requires(!omitFrame || s.Mod.Expressions.Count == 0);
+
+ wr.Write("modify");
+ PrintAttributes(s.Mod.Attributes);
+ wr.Write(" ");
+ if (omitFrame) {
+ wr.Write("...");
+ } else {
+ PrintFrameExpressionList(s.Mod.Expressions);
+ }
+ if (s.Body != null) {
+ // There's a possible syntactic ambiguity, namely if the frame is empty (more precisely,
+ // if s.Mod.Expressions.Count is 0). Since the statement was parsed at some point, this
+ // situation can occur only if the modify statement inherited its frame by refinement
+ // and we're printing the post-resolve AST. In this special case, print an explicit
+ // empty set as the frame.
+ if (s.Mod.Expressions.Count == 0) {
+ wr.Write(" {}");
+ }
+ wr.Write(" ");
+ PrintStatement(s.Body, indent);
+ } else {
+ wr.Write(";");
+ }
+ }
+
/// <summary>
/// Does not print LHS
/// </summary>
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 7333f950..3ba4b01d 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -875,32 +875,36 @@ namespace Microsoft.Dafny } else {
var oldS = oldStmt.Body[j];
/* See how the two statements match up.
- * cur oldS result
+ * oldS cur result
* ------ ------ ------
- * assert ...; assume E; assert E;
- * assert ...; assert E; assert E;
+ * assume E; assert ...; assert E;
+ * assert E; assert ...; assert E;
* assert E; assert E;
*
- * assume ...; assume E; assume E;
+ * assume E; assume ...; assume E;
*
- * var x := E; var x; var x := E;
- * var x := E; var x := *; var x := E;
- * var x := E1; var x :| P; var x := E1; assert P;
+ * var x; var x := E; var x := E;
+ * var x := *; var x := E; var x := E;
+ * var x :| P; var x := E1; var x := E1; assert P;
* var VarProduction; var VarProduction;
*
- * x := E; x := *; x := E;
- * x := E; x :| P; x := E; assert P;
+ * x := *; x := E; x := E;
+ * x :| P; x := E; x := E; assert P;
*
- * 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')
+ * modify E; modify ...; modify E;
+ * modify E; modify ... { S } modify E { S }
+ * modify E { S } modify ... { S' } modify E { Merge(S, S') }
*
- * while ... LoopSpec ... while (G) LoopSpec' Body while (G) Merge(LoopSpec,LoopSpec') Body
- * while ... LoopSpec Body while (G) LoopSpec' Body' while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')
- * 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')
+ * if (G) Then' else Else' if ... Then else Else if (G) Merge(Then,Then') else Merge(Else,Else')
+ * if (*) Then' else Else' if (G) Then else Else if (G) Merge(Then,Then') else Merge(Else,Else')
*
- * ... where x = e; S StmtThatDoesNotMatchS; S' StatementThatDoesNotMatchS[e/x]; Merge( ... where x = e; S , S')
- * ... where x = e; S StmtThatMatchesS; S' StmtThatMatchesS; S'
+ * while (G) LoopSpec' Body while ... LoopSpec ... while (G) Merge(LoopSpec,LoopSpec') Body
+ * while (G) LoopSpec' Body' while ... LoopSpec Body while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')
+ * while (*) LoopSpec' Body while (G) LoopSpec ... while (G) Merge(LoopSpec,LoopSpec') Body
+ * while (*) LoopSpec' Body' while (G) LoopSpec Body while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')
+ *
+ * StmtThatDoesNotMatchS; S' ... where x = e; S StatementThatDoesNotMatchS[e/x]; Merge( ... where x = e; S , S')
+ * StmtThatMatchesS; S' ... where x = e; 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.
@@ -1026,6 +1030,31 @@ namespace Microsoft.Dafny i++; j++;
}
+ } else if (S is ModifyStmt) {
+ var skel = (ModifyStmt)S;
+ Contract.Assert(c.ConditionOmitted);
+ var oldModifyStmt = oldS as ModifyStmt;
+ if (oldModifyStmt == null) {
+ reporter.Error(cur.Tok, "modify template does not match inherited statement");
+ i++;
+ } else {
+ var mod = refinementCloner.CloneSpecFrameExpr(oldModifyStmt.Mod);
+ BlockStmt mbody;
+ if (oldModifyStmt.Body == null && skel.Body == null) {
+ mbody = null;
+ } else if (oldModifyStmt.Body == null) {
+ mbody = oldModifyStmt.Body;
+ } else if (skel.Body == null) {
+ reporter.Error(cur.Tok, "modify template must have a body if the inherited modify statement does");
+ mbody = null;
+ } else {
+ mbody = MergeBlockStmt(skel.Body, oldModifyStmt.Body);
+ }
+ body.Add(new ModifyStmt(skel.Tok, skel.EndTok, mod.Expressions, mod.Attributes, mbody));
+ ReportAdditionalInformation(c.ConditionEllipsis, Printer.FrameExprListToString(mod.Expressions), 3);
+ i++; j++;
+ }
+
} else {
Contract.Assume(false); // unexpected skeleton statement
}
|