From fc76541682ec019b8a2dc08ca9972ff517db9b74 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 10 Sep 2012 18:37:47 -0700 Subject: Dafny: did a little to extend the support of labeled statements in refinements (things like multiple labels are still not thought through very well) --- Source/Dafny/Compiler.cs | 2 +- Source/Dafny/RefinementTransformer.cs | 15 ++++++++++++--- 2 files changed, 13 insertions(+), 4 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 8715c047..a138f4d9 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -637,7 +637,7 @@ namespace Microsoft.Dafny { if (m.IsTailRecursive) { Indent(indent); wr.WriteLine("TAIL_CALL_START: ;"); if (!m.IsStatic) { - Indent(indent); wr.WriteLine("var _this = this;"); + Indent(indent + IndentAmount); wr.WriteLine("var _this = this;"); } } Contract.Assert(enclosingMethod == null); diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 60aa1bfd..31ecfc9c 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -785,8 +785,6 @@ namespace Microsoft.Dafny * * 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. - * - * TODO: should also handle labels and some form of new "replace" statement */ if (cur is SkeletonStatement) { var S = ((SkeletonStatement)cur).S; @@ -1071,10 +1069,21 @@ namespace Microsoft.Dafny } bool PotentialMatch(Statement nxt, Statement other) { + Contract.Requires(nxt != null); Contract.Requires(!(nxt is SkeletonStatement) || ((SkeletonStatement)nxt).S != null); // nxt is not "...;" Contract.Requires(other != null); - if (nxt is SkeletonStatement) { + if (nxt.Labels != null) { + for (var olbl = other.Labels; olbl != null; olbl = olbl.Next) { + var odata = olbl.Data; + for (var l = nxt.Labels; l != null; l = l.Next) { + if (odata.Name == l.Data.Name) { + return true; + } + } + } + return false; // labels of 'nxt' don't match any label of 'other' + } else if (nxt is SkeletonStatement) { var S = ((SkeletonStatement)nxt).S; if (S is AssertStmt) { return other is PredicateStmt; -- cgit v1.2.3