From 3bb828b02a76167cc8aa25284663f1524e2b929b Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Wed, 29 Jun 2011 16:21:35 -0700
Subject: Initial implementation of return statments with parameters.

---
 Source/Dafny/Dafny.atg | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'Source/Dafny/Dafny.atg')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 033bc239..c69a6838 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -26,7 +26,7 @@ static BuiltIns theBuiltIns;
 
 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
-static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken);
+static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
 static int anonymousIds = 0;
 
@@ -696,11 +696,24 @@ OneStmt<out Statement/*!*/ s>
       }
     )
     ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
-  | "return"                           (. x = t; .)
-    ";"                                (. s = new ReturnStmt(x); .)
+  | ReturnStmt<out s>
   )
   .
 
+ReturnStmt<out Statement/*!*/ s>
+= (.
+   IToken returnTok = null;
+   List<AssignmentRhs> rhss = null;
+   AssignmentRhs r;
+   .)
+  "return"                           (. returnTok = t; .)
+  [
+	  Rhs<out r, null>               (. rhss = new List<AssignmentRhs>(); rhss.Add(r); .)
+      { "," Rhs<out r, null>         (. rhss.Add(r); .)
+        }
+  ]
+  ";"                                (. s = new ReturnStmt(returnTok, rhss); .)
+  .
 UpdateStmt<out Statement/*!*/ s>
 = (. List<Expression> lhss = new List<Expression>();
      List<AssignmentRhs> rhss = new List<AssignmentRhs>();
-- 
cgit v1.2.3