diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-19 11:25:59 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-19 11:25:59 -0700 |
| commit | 3b51d9251d78bd3de763c951102677eecd764984 (patch) | |
| tree | c265e9a99caaf201c3e43f4384000ba6256158ba /Source | |
| parent | 78e74bf9fa5ad7175cafd171427f58f556256e4a (diff) | |
Handle underscores in lambda bound variable lists properly
+ add a test case with lambdas that don't get their types fully specified
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 23 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 23 |
2 files changed, 28 insertions, 18 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index deef9285..a9473202 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -120,6 +120,17 @@ bool IsParenStar() { return la.kind == _openparen && x.kind == _star;
}
+string UnwildIdent(string x, bool allowWildcardId) {
+ if (x.StartsWith("_")) {
+ if (allowWildcardId && x.Length == 1) {
+ return "_v" + anonymousIds++;
+ } else {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ }
+ return x;
+}
+
bool IsLambda(bool allowLambda)
{
return allowLambda &&
@@ -2032,7 +2043,7 @@ ParensExpression<out Expression e, bool allowSemi, bool allowLambda> if (ise.Arguments != null) {
SemErr(ise.OpenParen, "Expected variable binding.");
}
- bvs.Add(new BoundVar(id, id.val, tt ?? new InferredTypeProxy()));
+ bvs.Add(new BoundVar(id, UnwildIdent(id.val, true), tt ?? new InferredTypeProxy()));
} else {
SemErr(ee.tok, "Expected variable binding.");
}
@@ -2308,7 +2319,7 @@ DottedIdentifiersAndFunction<out Expression e, bool allowSemi, bool allowLambda> if (args != null) {
SemErr(openParen, "Expected variable binding.");
}
- BoundVar bv = new BoundVar(id, id.val, new InferredTypeProxy());
+ BoundVar bv = new BoundVar(id, UnwildIdent(id.val, true), new InferredTypeProxy());
e = new LambdaExpr(id, oneShot, new List<BoundVar>{ bv }, req, reads, body);
.)
]
@@ -2576,13 +2587,7 @@ NoUSIdent<out IToken/*!*/ x> WildIdent<out IToken/*!*/ x, bool allowWildcardId>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
ident (. x = t;
- if (x.val.StartsWith("_")) {
- if (allowWildcardId && x.val.Length == 1) {
- t.val = "_v" + anonymousIds++;
- } else {
- SemErr("cannot declare identifier beginning with underscore");
- }
- }
+ t.val = UnwildIdent(x.val, allowWildcardId);
.)
.
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 9da363a2..1a8e0e3c 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -151,6 +151,17 @@ bool IsParenStar() { return la.kind == _openparen && x.kind == _star;
}
+string UnwildIdent(string x, bool allowWildcardId) {
+ if (x.StartsWith("_")) {
+ if (allowWildcardId && x.Length == 1) {
+ return "_v" + anonymousIds++;
+ } else {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ }
+ return x;
+}
+
bool IsLambda(bool allowLambda)
{
return allowLambda &&
@@ -1126,13 +1137,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
x = t;
- if (x.val.StartsWith("_")) {
- if (allowWildcardId && x.val.Length == 1) {
- t.val = "_v" + anonymousIds++;
- } else {
- SemErr("cannot declare identifier beginning with underscore");
- }
- }
+ t.val = UnwildIdent(x.val, allowWildcardId);
}
@@ -3229,7 +3234,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (args != null) {
SemErr(openParen, "Expected variable binding.");
}
- BoundVar bv = new BoundVar(id, id.val, new InferredTypeProxy());
+ BoundVar bv = new BoundVar(id, UnwildIdent(id.val, true), new InferredTypeProxy());
e = new LambdaExpr(id, oneShot, new List<BoundVar>{ bv }, req, reads, body);
}
@@ -3633,7 +3638,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (ise.Arguments != null) {
SemErr(ise.OpenParen, "Expected variable binding.");
}
- bvs.Add(new BoundVar(id, id.val, tt ?? new InferredTypeProxy()));
+ bvs.Add(new BoundVar(id, UnwildIdent(id.val, true), tt ?? new InferredTypeProxy()));
} else {
SemErr(ee.tok, "Expected variable binding.");
}
|