diff options
| author |  rustanleino <unknown> | 2009-11-05 02:28:36 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-05 02:28:36 +0000 |
| commit | 3e050d0273c88db1b00c2d157ac1b970f2a5b4d7 (patch) | |
| tree | 31bf1add9f2aba6a970d6eb21f3f83b987769e79 /Source/Dafny/Dafny.atg | |
| parent | ddede5ad5f9236d8ee4e1e75ba3ecfd7077d9296 (diff) | |
The Dafny call statement now automatically declares left-hand sides as local variables, if they were not already local variables.
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 41 |
1 files changed, 33 insertions, 8 deletions
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!>());
}
.)
.
|