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

6 files changed, 78 insertions, 1 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

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 230a8861..60d76af1 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -333,6 +333,16 @@ Execution trace:
     IfThenElse1.bpl(33,3): anon0

 

 Boogie program verifier finished with 2 verified, 2 errors

+

+-------------------- Lambda.bpl --------------------

+Lambda.bpl(37,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Lambda.bpl(36,5): anon0

+Lambda.bpl(38,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Lambda.bpl(36,5): anon0

+

+Boogie program verifier finished with 3 verified, 2 errors

 -------------------- sk_hack.bpl --------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl
new file mode 100644
index 00000000..48610ff1
--- /dev/null
+++ b/Test/test2/Lambda.bpl
@@ -0,0 +1,41 @@
+procedure foo()
+{
+  var a: [int]int;
+  var c:int,b:bool;
+  a := (lambda y:int :: if b then y + c else 7);
+  assume b;
+  assert a[3] == c+3;
+}
+
+procedure bar()
+{
+  assert (lambda x:int :: x > 0)[10];
+  
+}
+
+type t1;
+
+procedure baz()
+{
+  var m:[int,t1]int;
+  var t:t1, t2:t1;
+
+  m := (lambda i:int, tt:t1 :: if tt == t then i else 12);
+  assert m[1,t] == 1;
+  assert t == t2 || m[1,t2] == 12;
+  assert  m[12,t2] == 12;
+  
+}
+
+
+procedure fail()
+{
+  var m:[int,t1]int;
+  var t:t1, t2:t1;
+
+  m := (lambda i:int, tt:t1 :: if tt == t then i else 12);
+  assert m[1,t2] == 12;
+  assert m[1,t] == 2;
+}
+
+
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index ab9ec103..ea4376b6 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             strings-no-where.bpl strings-where.bpl

             Structured.bpl Where.bpl UpdateExpr.bpl

             NeverPattern.bpl NullaryMaps.bpl Implies.bpl

-	    IfThenElse1.bpl) do (

+	    IfThenElse1.bpl Lambda.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /noinfer %%f