Use arbitrary lookahead to determine if the next expression is a lambda expression.

9 files changed, 25 insertions, 25 deletions

diff --git a/Test/hofs/Apply.dfy.expect b/Test/hofs/Apply.dfy.expect
index fad1fe33..77d34c4c 100644
--- a/Test/hofs/Apply.dfy.expect
+++ b/Test/hofs/Apply.dfy.expect
@@ -1,7 +1,7 @@
 Apply.dfy(27,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Apply.dfy(26,35): anon15_Else

-    Apply.dfy(27,27): anon17_Else

+    Apply.dfy(26,27): anon15_Else

+    Apply.dfy(27,19): anon17_Else

 

 Dafny program verifier finished with 6 verified, 1 error

diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect
index 016ee494..0f6f2aa9 100644
--- a/Test/hofs/FnRef.dfy.expect
+++ b/Test/hofs/FnRef.dfy.expect
@@ -11,12 +11,12 @@ Execution trace:
 FnRef.dfy(46,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    FnRef.dfy(43,13): anon7_Else

+    FnRef.dfy(43,12): anon7_Else

     (0,0): anon9_Then

 FnRef.dfy(65,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    FnRef.dfy(56,13): anon8_Else

+    FnRef.dfy(56,12): anon8_Else

     (0,0): anon10_Then

 

 Dafny program verifier finished with 4 verified, 4 errors

diff --git a/Test/hofs/Frame.dfy.expect b/Test/hofs/Frame.dfy.expect
index a4d10c47..0ee2eadb 100644
--- a/Test/hofs/Frame.dfy.expect
+++ b/Test/hofs/Frame.dfy.expect
@@ -1,17 +1,17 @@
 Frame.dfy(23,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Frame.dfy(19,13): anon5_Else

+    Frame.dfy(19,12): anon5_Else

     (0,0): anon6_Then

 Frame.dfy(37,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Frame.dfy(33,13): anon3_Else

+    Frame.dfy(33,12): anon3_Else

 Frame.dfy(63,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon13_Then

-    Frame.dfy(55,13): anon14_Else

+    Frame.dfy(55,12): anon14_Else

     (0,0): anon15_Then

     (0,0): anon5

 Frame.dfy(66,19): Error: insufficient reads clause to read array element

diff --git a/Test/hofs/Lambda.dfy.expect b/Test/hofs/Lambda.dfy.expect
index a32c27ff..4fe8275f 100644
--- a/Test/hofs/Lambda.dfy.expect
+++ b/Test/hofs/Lambda.dfy.expect
@@ -2,13 +2,13 @@ Lambda.dfy(24,12): Error: assertion violation
 Execution trace:

     (0,0): anon0

     Lambda.dfy(6,24): anon31_Else

-    Lambda.dfy(7,26): anon32_Else

-    Lambda.dfy(8,27): anon33_Else

-    Lambda.dfy(10,39): anon34_Else

-    Lambda.dfy(11,23): anon35_Else

+    Lambda.dfy(7,24): anon32_Else

+    Lambda.dfy(8,26): anon33_Else

+    Lambda.dfy(10,34): anon34_Else

+    Lambda.dfy(11,15): anon35_Else

     Lambda.dfy(13,15): anon36_Else

     Lambda.dfy(14,15): anon39_Else

-    Lambda.dfy(18,16): anon42_Else

-    Lambda.dfy(23,16): anon44_Else

+    Lambda.dfy(18,15): anon42_Else

+    Lambda.dfy(23,15): anon44_Else

 

 Dafny program verifier finished with 7 verified, 1 error

diff --git a/Test/hofs/LambdaParsefail.dfy.expect b/Test/hofs/LambdaParsefail.dfy.expect
index d7ee9510..11deb9b0 100644
--- a/Test/hofs/LambdaParsefail.dfy.expect
+++ b/Test/hofs/LambdaParsefail.dfy.expect
@@ -1,6 +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(8,21): error: cannot declare identifier beginning with underscore

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

+LambdaParsefail.dfy(5,19): error: this symbol not expected in VarDeclStatement

+LambdaParsefail.dfy(6,19): error: this symbol not expected in VarDeclStatement

+LambdaParsefail.dfy(7,21): error: this symbol not expected in VarDeclStatement

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

+LambdaParsefail.dfy(9,17): error: this symbol not expected in VarDeclStatement

 5 parse errors detected in LambdaParsefail.dfy

diff --git a/Test/hofs/LambdaParsefail2.dfy.expect b/Test/hofs/LambdaParsefail2.dfy.expect
index 8bbf643c..0c9ecb83 100644
--- a/Test/hofs/LambdaParsefail2.dfy.expect
+++ b/Test/hofs/LambdaParsefail2.dfy.expect
@@ -1,2 +1,2 @@
-LambdaParsefail2.dfy(6,33): error: Type specification not allowed here, comma separator was expected.

+LambdaParsefail2.dfy(6,39): error: invalid LambdaArrow

 1 parse errors detected in LambdaParsefail2.dfy

diff --git a/Test/hofs/OneShot.dfy.expect b/Test/hofs/OneShot.dfy.expect
index 78a9864b..91b931b8 100644
--- a/Test/hofs/OneShot.dfy.expect
+++ b/Test/hofs/OneShot.dfy.expect
@@ -2,19 +2,19 @@ OneShot.dfy(20,12): Error: possible violation of function precondition
 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

-    OneShot.dfy(13,9): anon5_Else

+    OneShot.dfy(13,8): anon5_Else

     (0,0): anon6_Then

 OneShot.dfy(22,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

-    OneShot.dfy(13,9): anon5_Else

+    OneShot.dfy(13,8): anon5_Else

     (0,0): anon6_Else

 OneShot.dfy(22,13): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

-    OneShot.dfy(13,9): anon5_Else

+    OneShot.dfy(13,8): anon5_Else

     (0,0): anon6_Else

 

 Dafny program verifier finished with 1 verified, 3 errors

diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
index f1da2003..44a95b6d 100644
--- a/Test/hofs/ReadsReads.dfy.expect
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -28,12 +28,12 @@ Execution trace:
 ReadsReads.dfy(98,37): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ReadsReads.dfy(95,16): anon15_Else

+    ReadsReads.dfy(95,14): anon15_Else

     (0,0): anon19_Then

 ReadsReads.dfy(100,29): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ReadsReads.dfy(95,16): anon15_Else

+    ReadsReads.dfy(95,14): anon15_Else

     (0,0): anon21_Then

 

 Dafny program verifier finished with 17 verified, 9 errors

diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index 55fe50e0..b3c126d5 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -11,7 +11,7 @@ Execution trace:
 Simple.dfy(37,9): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Simple.dfy(35,15): anon5_Else

+    Simple.dfy(35,13): anon5_Else

 Simple.dfy(49,9): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0