Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda expressions; they might not yet fully work for polymorphic maps.

3 files changed, 26 insertions, 0 deletions

diff --git a/Test/test1/Answer b/Test/test1/Answer
index 10ad5494..a8b73b53 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -139,3 +139,9 @@ IfThenElse0.bpl(5,7): Error: the first argument to if-then-else should be bool,
 IfThenElse0.bpl(6,7): Error: branches of if-then-else have incompatible types bool and int

 IfThenElse0.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to bool)

 3 type checking errors detected in IfThenElse0.bpl

+Lambda.bpl(5,2): Error: mismatched types in assignment command (cannot assign [int]int to [int,int]int)

+Lambda.bpl(6,2): Error: mismatched types in assignment command (cannot assign [int]int to [int]bool)

+Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lambda parameters

+Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)

+Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator +

+5 type checking errors detected in Lambda.bpl

diff --git a/Test/test1/Lambda.bpl b/Test/test1/Lambda.bpl
new file mode 100644
index 00000000..d0ccd3a1
--- /dev/null
+++ b/Test/test1/Lambda.bpl
@@ -0,0 +1,19 @@
+procedure foo()
+{
+  var a: [int,int]int;
+  var b: [int]bool;
+  a := (lambda y:int :: y + 1);
+  b := (lambda y:int :: y + 1);
+}
+
+procedure bar()
+{
+  var a: [int]int;
+  a := (lambda<T> y:int :: y + 1);
+}
+
+procedure baz()
+{
+  var a: [bool]int;
+  a := (lambda y:bool :: y + 1);
+}
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat
index dda3a0af..979c36e4 100644
--- a/Test/test1/runtest.bat
+++ b/Test/test1/runtest.bat
@@ -18,3 +18,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noVerify EmptyCallArgs.bpl

 %BGEXE% %* /noVerify FunBody.bpl

 %BGEXE% %* /noVerify IfThenElse0.bpl

+%BGEXE% %* /noVerify Lambda.bpl