Allow forall statements in refinements

3 files changed, 39 insertions, 4 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 2d32f78a..f430933b 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -1532,9 +1532,6 @@ namespace Microsoft.Dafny
         });

       } else if (s is CallStmt) {

         reporter.Error(s.Tok, "cannot have call statement");

-      } else if (s is ForallStmt) {

-        if (((ForallStmt)s).Kind == ForallStmt.ParBodyKind.Assign) // allow Proof and Call (as neither touch any existing state)

-          reporter.Error(s.Tok, "cannot have forall statement");

       } else {

         if (s is WhileStmt || s is AlternativeLoopStmt) {

           loopLevels++;

diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
index 121b33aa..8d60a8e4 100644
--- a/Test/dafny0/RefinementErrors.dfy
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -59,3 +59,40 @@ module BB refines B {
     { 10 }
   }
 }
+
+module Forall0 {
+  class C {
+    var a: int
+    method M()
+      modifies this
+    {
+    }
+    lemma Lemma(x: int)
+    {
+    }
+  }
+}
+module Forall1 refines Forall0 {
+  class C {
+    var b: int
+    method M...
+    {
+      forall x { Lemma(x); }  // allowed
+      var s := {4};
+      forall x | x in s ensures x == 4 { }  // allowed
+      forall x {  // allowed
+        calc {
+          x in s;
+        ==
+          x == 4;
+        }
+      }
+      forall c | c in {this} {
+        c.b := 17;  // allowed
+      }
+      forall c | c in {this} {
+        c.a := 17;  // error: not allowed to update previously defined field
+      }
+    }
+  }
+}
diff --git a/Test/dafny0/RefinementErrors.dfy.expect b/Test/dafny0/RefinementErrors.dfy.expect
index 40cdb081..bac6612d 100644
--- a/Test/dafny0/RefinementErrors.dfy.expect
+++ b/Test/dafny0/RefinementErrors.dfy.expect
@@ -9,4 +9,5 @@ RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be rename
 RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

 RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

 RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

-11 resolution/type errors detected in RefinementErrors.dfy

+RefinementErrors.dfy(94,10): Error: refinement method cannot assign to a field defined in parent module ('a')

+12 resolution/type errors detected in RefinementErrors.dfy