From 3e050d0273c88db1b00c2d157ac1b970f2a5b4d7 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 5 Nov 2009 02:28:36 +0000
Subject: The Dafny call statement now automatically declares left-hand sides
 as local variables, if they were not already local variables.

---
 Source/Dafny/Dafny.atg | 41 +++++++++++++++++++++++++++++++++--------
 1 file changed, 33 insertions(+), 8 deletions(-)

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

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 9ab826ac..022dc912 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -25,6 +25,28 @@ static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
 static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");
 static Scope<string>! parseVarScope = new Scope<string>();
 
+// helper routine for parsing call statements
+private static void RecordCallLhs(IdentifierExpr! e,
+                                  List<IdentifierExpr!>! lhs,
+                                  List<VarDecl!>! newVars) {
+  lhs.Add(e);
+  if (parseVarScope.Find(e.Name) == null) {
+    VarDecl d = new VarDecl(e.tok, e.Name, new InferredTypeProxy(), null);
+    newVars.Add(d);
+    parseVarScope.Push(e.Name, e.Name);
+  }
+}
+
+// helper routine for parsing call statements
+private static Expression! ConvertToLocal(Expression! e)
+{
+  FieldSelectExpr fse = e as FieldSelectExpr;
+  if (fse != null && fse.Obj is ImplicitThisExpr) {
+    return new IdentifierExpr(fse.tok, fse.FieldName);
+  }
+  return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
+}
+
 ///<summary>
 /// Parses top level declarations from "filename" and appends them to "classes".
 /// Returns the number of parsing errors encountered.
@@ -522,28 +544,31 @@ CallStmt<out Statement! s>
 = (. Token! x, id;
      Expression! e;
      List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
+     List<VarDecl!> newVars = new List<VarDecl!>();
   .)
   "call"                       (. x = token; .)
   CallStmtSubExpr<out e>
   
   [ ","                        /* call a,b,c,... := ... */
-                               (. if (e is IdentifierExpr) {
-                                    lhs.Add((IdentifierExpr)e);
+                               (. e = ConvertToLocal(e);
+                                  if (e is IdentifierExpr) {
+                                    RecordCallLhs((IdentifierExpr)e, lhs, newVars);
                                   } else if (e is FieldSelectExpr) {
                                     SemErr(e.tok, "each LHS of call statement must be a variable, not a field");
                                   } else {
                                     SemErr(e.tok, "each LHS of call statement must be a variable");
                                   }
                                .)
-    Ident<out id>              (. lhs.Add(new IdentifierExpr(id, id.val)); .)
-    { "," Ident<out id>        (. lhs.Add(new IdentifierExpr(id, id.val)); .)
+    Ident<out id>              (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)
+    { "," Ident<out id>        (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)
     }
     ":="
     CallStmtSubExpr<out e>
 
   | ":="                       /* call a := ... */
-                               (. if (e is IdentifierExpr) {
-                                    lhs.Add((IdentifierExpr)e);
+                               (. e = ConvertToLocal(e);
+                                  if (e is IdentifierExpr) {
+                                    RecordCallLhs((IdentifierExpr)e, lhs, newVars);
                                   } else if (e is FieldSelectExpr) {
                                     SemErr(e.tok, "each LHS of call statement must be a variable, not a field");
                                   } else {
@@ -558,10 +583,10 @@ CallStmt<out Statement! s>
      It denotes the RHS, so to be legal it must be a FunctionCallExpr.  */
   (. if (e is FunctionCallExpr) {
        FunctionCallExpr fce = (FunctionCallExpr)e;
-       s = new CallStmt(x, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args
+       s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args
      } else {
        SemErr("RHS of call statement must denote a method invocation");
-       s = new CallStmt(x, lhs, dummyExpr, "dummyMethodName", new List<Expression!>());
+       s = new CallStmt(x, newVars, lhs, dummyExpr, "dummyMethodName", new List<Expression!>());
      }
   .)
   .
-- 
cgit v1.2.3