Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;

1 files changed, 25 insertions, 7 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 740926e5..c6609b4c 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -712,6 +712,7 @@ UpdateStmt<out Statement/*!*/ s>
      Expression lhs0;

      IToken x;

      Attributes attrs = null;

+     Expression suchThat = null;

   .)

   Lhs<out e>                       (. x = e.tok; .)

   ( { Attribute<ref attrs> }

@@ -719,14 +720,22 @@ UpdateStmt<out Statement/*!*/ s>
   |                                (. lhss.Add(e);  lhs0 = e; .)

     { "," Lhs<out e>               (. lhss.Add(e); .)

     }

-    ":="                           (. x = t; .)

-    Rhs<out r, lhs0>               (. rhss.Add(r); .)

-    { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

-    }

+    ( ":="                         (. x = t; .)

+      Rhs<out r, lhs0>             (. rhss.Add(r); .)

+      { "," Rhs<out r, lhs0>       (. rhss.Add(r); .)

+      }

+    | ":|"                         (. x = t; .)

+      Expression<out suchThat>

+    )

     ";"

   | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)

   )

-  (. s = new UpdateStmt(x, lhss, rhss); .)

+  (. if (suchThat != null) {

+       s = new AssignSuchThatStmt(x, lhss, suchThat);

+     } else {

+       s = new UpdateStmt(x, lhss, rhss);

+     }

+  .)

   .

 Rhs<out AssignmentRhs r, Expression receiverForInitCall>

 = (. IToken/*!*/ x, newToken;  Expression/*!*/ e;

@@ -770,6 +779,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
      AssignmentRhs r;  IdentifierExpr lhs0;

      List<VarDecl> lhss = new List<VarDecl>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

+     Expression suchThat = null;

   .)

   [ "ghost"                                 (. isGhost = true;  x = t; .)

   ]

@@ -785,10 +795,18 @@ VarDeclStatement<.out Statement/*!*/ s.>
     Rhs<out r, lhs0>               (. rhss.Add(r); .)

     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

     }

+  | ":|"                           (. assignTok = t; .)

+    Expression<out suchThat>

   ]

   ";"

-  (. UpdateStmt update;

-     if (rhss.Count == 0) {

+  (. ConcreteUpdateStatement update;

+     if (suchThat != null) {

+       var ies = new List<Expression>();

+       foreach (var lhs in lhss) {

+         ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));

+       }

+       update = new AssignSuchThatStmt(assignTok, ies, suchThat);

+     } else if (rhss.Count == 0) {

        update = null;

      } else {

        var ies = new List<Expression>();