diff options
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 41 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.ssc | 4 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 37 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 5 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 3 |
5 files changed, 75 insertions, 15 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!>());
}
.)
.
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index 59d1d0ae..4b97edbd 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -645,13 +645,15 @@ namespace Microsoft.Dafny }
public class CallStmt : Statement {
+ public readonly List<VarDecl!>! NewVars;
public readonly List<IdentifierExpr!>! Lhs;
public readonly Expression! Receiver;
public readonly string! MethodName;
public readonly List<Expression!>! Args;
public Method Method; // filled in by resolution
- public CallStmt(Token! tok, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {
+ public CallStmt(Token! tok, List<VarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {
+ this.NewVars = newVars;
this.Lhs = lhs;
this.Receiver = receiver;
this.MethodName = methodName;
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 0dc7df24..0fd3e612 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -23,6 +23,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.
@@ -671,6 +693,7 @@ public static int Parse (List<ClassDecl!>! classes) { Token! x, id;
Expression! e;
List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
+ List<VarDecl!> newVars = new List<VarDecl!>();
Expect(42);
x = token;
@@ -678,8 +701,9 @@ public static int Parse (List<ClassDecl!>! classes) { if (t.kind == 8 || t.kind == 35) {
if (t.kind == 8) {
Get();
+ e = ConvertToLocal(e);
if (e is IdentifierExpr) {
- lhs.Add((IdentifierExpr)e);
+ 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 {
@@ -687,18 +711,19 @@ public static int Parse (List<ClassDecl!>! classes) { }
Ident(out id);
- lhs.Add(new IdentifierExpr(id, id.val));
+ RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
while (t.kind == 8) {
Get();
Ident(out id);
- lhs.Add(new IdentifierExpr(id, id.val));
+ RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
Expect(35);
CallStmtSubExpr(out e);
} else {
Get();
+ e = ConvertToLocal(e);
if (e is IdentifierExpr) {
- lhs.Add((IdentifierExpr)e);
+ 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 {
@@ -711,10 +736,10 @@ public static int Parse (List<ClassDecl!>! classes) { Expect(9);
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!>());
}
}
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 2159d3dc..47727562 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -684,6 +684,11 @@ namespace Microsoft.Dafny { } else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
+ // resolve any local variables declared here
+ foreach (VarDecl local in s.NewVars) {
+ ResolveStatement(local);
+ }
+
// resolve left-hand side
Dictionary<string!,object> lhsNameSet = new Dictionary<string!,object>();
foreach (IdentifierExpr lhs in s.Lhs) {
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 09be93fa..1028058f 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1304,6 +1304,9 @@ namespace Microsoft.Dafny { } else if (stmt is CallStmt) {
AddComment(builder, stmt, "call statement");
CallStmt s = (CallStmt)stmt;
+ foreach (VarDecl local in s.NewVars) {
+ TrStmt(local, builder, locals, etran);
+ }
Bpl.ExprSeq ins = new Bpl.ExprSeq();
ins.Add(etran.TrExpr(s.Receiver));
for (int i = 0; i < s.Args.Count; i++) {
|