Handle underscores in lambda bound variable lists properly

+ add a test case with lambdas that don't get their types fully specified

8 files changed, 61 insertions, 29 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.");

 			 }

diff --git a/Test/hofs/LambdaParsefail.dfy b/Test/hofs/LambdaParsefail.dfy
index a9da4c5e..3dc30100 100644
--- a/Test/hofs/LambdaParsefail.dfy
+++ b/Test/hofs/LambdaParsefail.dfy
@@ -1,16 +1,15 @@
 // RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method Fails() {
-    var g1 := x.x => x;   // fail
-    var g2 := x() => x;   // fail
-    var g3 := ((x)) => x; // fail
-
+method Fails() { // all these fail
+    var g1 := x.x => x;
+    var g2 := x() => x;
+    var g3 := ((x)) => x;
+    var g4 := _a => 5;
+    var g5 := x : int => x;
 }
 
-method Fail() {
-    var g8 := x : int => x;   // not ok!
-}
+// the rest of these are OK:
 
 function f():() {
   a.b(x); a.b(x)
diff --git a/Test/hofs/LambdaParsefail.dfy.expect b/Test/hofs/LambdaParsefail.dfy.expect
index b1334b85..d7ee9510 100644
--- a/Test/hofs/LambdaParsefail.dfy.expect
+++ b/Test/hofs/LambdaParsefail.dfy.expect
@@ -1,5 +1,6 @@
 LambdaParsefail.dfy(5,17): error: Invalid variable binding in lambda.

 LambdaParsefail.dfy(6,16): error: Expected variable binding.

 LambdaParsefail.dfy(7,16): error: Expected variable binding.

-LambdaParsefail.dfy(12,17): error: semi expected

-4 parse errors detected in LambdaParsefail.dfy

+LambdaParsefail.dfy(8,21): error: cannot declare identifier beginning with underscore

+LambdaParsefail.dfy(9,17): error: semi expected

+5 parse errors detected in LambdaParsefail.dfy

diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 31de9424..410842b3 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -61,3 +61,9 @@ method Pli(f : A -> B) requires f != null;
   var o : object;
   assert f != o;
 }
+
+method Underscores() {
+  var u := _ => 0;
+  var v := (_, _) => 0;
+  var w := (_, _, _) => _;
+}
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index d7de049a..0cb9413c 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -15,4 +15,5 @@ ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)
 ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool

 ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?)

 ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object)

-17 resolution/type errors detected in ResolveError.dfy

+ResolveError.dfy(68,24): Error: unresolved identifier: _

+18 resolution/type errors detected in ResolveError.dfy

diff --git a/Test/hofs/Underspecified.dfy b/Test/hofs/Underspecified.dfy
new file mode 100644
index 00000000..2cfd3379
--- /dev/null
+++ b/Test/hofs/Underspecified.dfy
@@ -0,0 +1,10 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Underspecified() {
+  // all these have underspecified types, which is not ok
+  var u := _ => 0;
+  var v := (_, _) => 0;
+  var w := a => a;
+}
+
diff --git a/Test/hofs/Underspecified.dfy.expect b/Test/hofs/Underspecified.dfy.expect
new file mode 100644
index 00000000..dfb4e978
--- /dev/null
+++ b/Test/hofs/Underspecified.dfy.expect
@@ -0,0 +1,5 @@
+Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not determined; please specify the type explicitly

+Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not determined; please specify the type explicitly

+Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not determined; please specify the type explicitly

+Underspecified.dfy(8,11): Error: type of bound variable 'a' could not determined; please specify the type explicitly

+4 resolution/type errors detected in Underspecified.dfy