#603, #446. Enhancing :- to allow multiple LHSs and return values (#809)

Fixes #603 Fixes #446
dafny-lang · Sep 30, 2020 · 8ef8161 · 8ef8161
1 parent 2236b1f
commit 8ef8161
Show file tree

Hide file tree

Showing 22 changed files with 593 additions and 112 deletions.
diff --git a/Makefile b/Makefile
@@ -2,17 +2,17 @@ DIR=$(dir $(realpath $(firstword $(MAKEFILE_LIST))))
 
 default: parser runtime boogie exe
 
-all: parser runtime boogie exe refman
+all: runtime boogie exe refman
 
-exe: parser
-	(cd ${DIR} ; msbuild Source/Dafny.sln )
+exe:
+	(cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
 
 boogie: ${DIR}/../boogie/Binaries/Boogie.exe
 
 ${DIR}/../boogie/Binaries/Boogie.exe:
 	(cd ${DIR}/../boogie ; msbuild Source/Boogie.sln )
 
-parser: 
+parser:
 	make -C ${DIR}/Source/Dafny -f Makefile.linux all
 
 runtime: ${DIR}/Binaries/DafnyRuntime.jar

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
@@ -647,7 +647,7 @@ public virtual Statement CloneStmt(Statement stmt) {
 
       } else if (stmt is AssignOrReturnStmt) {
         var s = (AssignOrReturnStmt)stmt;
-        r = new AssignOrReturnStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Rhs), s.ExpectToken == null ? null : Tok(s.ExpectToken));
+        r = new AssignOrReturnStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Rhs), s.ExpectToken == null ? null : Tok(s.ExpectToken), s.Rhss == null ? null : s.Rhss.ConvertAll(e => CloneRHS(e)));
 
       } else if (stmt is VarDeclStmt) {
         var s = (VarDeclStmt)stmt;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
@@ -2208,7 +2208,9 @@ UpdateStmt<out Statement/*!*/ s>
         "expect"                   (. exceptionExpect = t; .)
       ]
       Expression<out exceptionExpr, false, false>
-    )
+      { "," Rhs<out r>             (. rhss.Add(r); .)
+      }
+     )
     ";"                            (. endTok = t; .)
   | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
   )
@@ -2217,16 +2219,14 @@ UpdateStmt<out Statement/*!*/ s>
      "expect"                      (. exceptionExpect = t; .)
    ]
    Expression<out exceptionExpr, false, false>
+   { "," Rhs<out r>                (. rhss.Add(r); .)
+   }
    ";"                             (. endTok = t; .)
 )
   (. if (suchThat != null) {
        s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume, null);
      } else if (exceptionExpr != null) {
-       if (lhss.Count > 1) {
-         SemErr(x, "':-' assignments can only have one LHS");
-         lhss = new List<Expression>() { lhss[0] };
-       }
-       s = new AssignOrReturnStmt(x, endTok, lhss, exceptionExpr, exceptionExpect);
+       s = new AssignOrReturnStmt(x, endTok, lhss, exceptionExpr, exceptionExpect, rhss);
      } else {
        if (lhss.Count == 0 && rhss.Count == 0) {
          s = new BlockStmt(x, endTok, new List<Statement>()); // error, give empty statement
@@ -2344,9 +2344,11 @@ VarDeclStatement<.out Statement/*!*/ s.>
       Expression<out suchThat, false, true>
     | ":-"                           (. assignTok = t; .)
       [ IF(la.kind == _expect)     /* an Expression can also begin with an "expect", so this says to resolve it to pick up any "expect" here */
-        "expect"                   (. exceptionExpect = t; .)
+        "expect"                     (. exceptionExpect = t; .)
       ]
       Expression<out exceptionExpr, false, false>
+      { "," Rhs<out r>               (. rhss.Add(r); .)
+      }
     ]
     SYNC ";"                         (. endTok = t; .)
     (. ConcreteUpdateStatement update;
@@ -2357,12 +2359,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
        if (suchThat != null) {
          update = new AssignSuchThatStmt(assignTok, endTok, lhsExprs, suchThat, suchThatAssume, attrs);
        } else if (exceptionExpr != null) {
-           Contract.Assert(lhss.Count >= 1);
-           if (lhss.Count != 1) {
-             SemErr(assignTok, "':-' assignments can only have one LHS");
-             lhsExprs = new List<Expression>() { lhsExprs[0] };
-           }
-           update = new AssignOrReturnStmt(assignTok, endTok, lhsExprs, exceptionExpr, exceptionExpect);
+         update = new AssignOrReturnStmt(assignTok, endTok, lhsExprs, exceptionExpr, exceptionExpect, rhss);
        } else if (rhss.Count == 0) {
          update = null;
        } else {

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
@@ -7239,6 +7239,7 @@ public UpdateStmt(IToken tok, IToken endTok, List<Expression> lhss, List<Assignm
   public class AssignOrReturnStmt : ConcreteUpdateStatement
   {
     public readonly Expression Rhs; // this is the unresolved RHS, and thus can also be a method call
+    public readonly List<AssignmentRhs> Rhss;
     public readonly IToken ExpectToken;
     public readonly List<Statement> ResolvedStatements = new List<Statement>();  // contents filled in during resolution
     public override IEnumerable<Statement> SubStatements {
@@ -7255,7 +7256,7 @@ void ObjectInvariant() {
       Contract.Invariant(Rhs != null);
     }
 
-    public AssignOrReturnStmt(IToken tok, IToken endTok, List<Expression> lhss, Expression rhs, IToken expectToken)
+    public AssignOrReturnStmt(IToken tok, IToken endTok, List<Expression> lhss, Expression rhs, IToken expectToken, List<AssignmentRhs> rhss = null)
       : base(tok, endTok, lhss)
     {
       Contract.Requires(tok != null);
@@ -7264,6 +7265,7 @@ public AssignOrReturnStmt(IToken tok, IToken endTok, List<Expression> lhss, Expr
       Contract.Requires(lhss.Count <= 1);
       Contract.Requires(rhs != null);
       Rhs = rhs;
+      Rhss = rhss;
       ExpectToken = expectToken;
     }
   }