From 3b51d9251d78bd3de763c951102677eecd764984 Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Tue, 19 Aug 2014 11:25:59 -0700
Subject: Handle underscores in lambda bound variable lists properly

+ add a test case with lambdas that don't get their types fully specified
---
 Test/hofs/LambdaParsefail.dfy        | 15 +++++++--------
 Test/hofs/LambdaParsefail.dfy.expect |  5 +++--
 Test/hofs/ResolveError.dfy           |  6 ++++++
 Test/hofs/ResolveError.dfy.expect    |  3 ++-
 Test/hofs/Underspecified.dfy         | 10 ++++++++++
 Test/hofs/Underspecified.dfy.expect  |  5 +++++
 6 files changed, 33 insertions(+), 11 deletions(-)
 create mode 100644 Test/hofs/Underspecified.dfy
 create mode 100644 Test/hofs/Underspecified.dfy.expect

(limited to 'Test/hofs')

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
-- 
cgit v1.2.3