summaryrefslogtreecommitdiff
path: root/Test/test2/LambdaExt.bpl
diff options
context:
space:
mode:
authorGravatar Dan Rosén <danr@chalmers.se>2014-08-01 09:57:25 -0700
committerGravatar Dan Rosén <danr@chalmers.se>2014-08-01 09:57:25 -0700
commita32ac3bff9a24b812d133883fb9f8df5341b7bb9 (patch)
tree917d9933ee9b8b126d02b5c09ee0f36efe6052bc /Test/test2/LambdaExt.bpl
parent315922109c235044f985ca19e1bfbe5b95d1873c (diff)
Add alpha equivalence check for Expr, and use it when lambda lifting
Diffstat (limited to 'Test/test2/LambdaExt.bpl')
-rw-r--r--Test/test2/LambdaExt.bpl146
1 files changed, 146 insertions, 0 deletions
diff --git a/Test/test2/LambdaExt.bpl b/Test/test2/LambdaExt.bpl
new file mode 100644
index 00000000..be0d84ee
--- /dev/null
+++ b/Test/test2/LambdaExt.bpl
@@ -0,0 +1,146 @@
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure Simplest() {
+ var id1, id2 : [int]int;
+ id1 := (lambda x: int :: x);
+ id2 := (lambda x: int :: x);
+ assert id1 == id2;
+ id2 := (lambda x: int :: 0);
+ assert id1 == id2; // fail
+}
+
+procedure Const() {
+ var v, w : [int][int]int;
+ var f, g : [int, int]int;
+
+ v := (lambda x : int :: (lambda y : int :: x));
+
+ w := (lambda x : int :: (lambda i : int :: x));
+ assert v == w;
+
+ w := (lambda i : int :: (lambda y : int :: i));
+ assert v == w;
+
+ w := (lambda a : int :: (lambda b : int :: b));
+ assert v == w; // should fail, now two different functions
+
+ f := (lambda x : int, y : int :: x);
+ assert f == (lambda p : int, q : int :: p);
+ assert f == (lambda p : int, q : int :: q); // should fail, different functions
+}
+
+procedure PolyConst() {
+ assert (lambda<A> x: A :: x) == (lambda<A>x: A :: x); // fails because of type parameters. this could be fixed.
+ /* // more tests, when it is fixed
+ var k1 : <A1>[A1]<B1>[B1]A1;
+ var k2 : <A2>[A2]<B2>[B2]A2;
+ k1 := (lambda<A> x: A :: (lambda<B> y: B :: x));
+ k2 := (lambda<A> x: A :: (lambda<C> z: C :: x));
+ assert k1 == k2;
+ k2 := (lambda<X> u: X :: (lambda<Y> v: Y :: u));
+ assert k1 == k2; */
+}
+
+procedure FreeVarP() {
+ var k : real;
+ var m : [int]real;
+ m := (lambda x:int :: k);
+ assert m[0] == k;
+}
+
+procedure FreeVarQ() {
+ var k : int;
+ var m : [int]int;
+ m := (lambda x:int :: k); // should be a different lambda from in FreeVarP, because they have different types
+ assert m[0] == k;
+}
+
+procedure Quantifiers() {
+ var k1 : [int]bool;
+ var k2 : [int]bool;
+ k1 := (lambda x: int :: (exists y: int :: x > y));
+ k2 := (lambda x: int :: (exists y: int :: x > y));
+ assert k1 == k2;
+ k2 := (lambda x: int :: (exists z: int :: x > z));
+ assert k1 == k2;
+}
+
+procedure FreeVariables() {
+ var m : [bool,bool,bool]bool;
+ var k : [bool,bool]bool;
+
+ var f : [bool]bool;
+ var g : [bool]bool;
+
+ var a : bool;
+ var b : bool;
+
+ f := (lambda r: bool :: a);
+ g := (lambda s: bool :: b);
+ if (a == b) {
+ assert f == g; // should be OK
+ } else {
+ assert f == g; // should fail
+ }
+
+ f := (lambda r: bool :: k[a,b]);
+ g := (lambda s: bool :: k[b,a]);
+ if (a == b) {
+ assert f == g; // should be OK
+ } else {
+ assert f == g; // should fail
+ }
+
+ f := (lambda r: bool :: m[a,a,b]);
+ g := (lambda s: bool :: m[a,b,b]);
+ if (a == b) {
+ assert f == g; // should fail because they are different lambda
+ } else {
+ assert f == g; // should fail because they are different lambda
+ }
+}
+
+function f(int) : int;
+
+procedure Triggers() {
+ var a,b : [int]bool;
+ a := (lambda x:int :: (forall u:int :: { f(u) } x == f(u)));
+ b := (lambda y:int :: (forall v:int :: { f(v) } y == f(v)));
+ assert a == b;
+ b := (lambda y:int :: (forall v:int :: y == f(v)));
+ assert a == b; // should fail because triggers are different
+}
+
+procedure Attributes() {
+ var a,b : [int]bool;
+ a := (lambda x:int :: (forall u:int :: {:attrib f(u) } x == f(u)));
+ b := (lambda y:int :: (forall v:int :: {:attrib f(v) } y == f(v)));
+ assert a == b;
+ b := (lambda y:int :: (forall v:int :: {:battrib f(v) } y == f(v)));
+ assert a == b; // should fail since attributes are different
+ a := (lambda x:int :: (forall u:int :: {:battrib f(x) } x == f(u)));
+ assert a == b; // should fail since attributes are different
+}
+
+procedure Old() {
+ var u,v : [int]int;
+ var a,b : int;
+ u := (lambda x:int :: old(x+a));
+ v := (lambda y:int :: old(y+b));
+ if (a == b) {
+ assert u == v; // ok
+ } else {
+ assert u == v; // fails
+ }
+}
+
+type Box;
+function $Box<T>(T) : Box;
+function $Unbox<T>(Box) : T;
+
+procedure Coercion() {
+ assert (lambda x: Box :: $Box($Unbox(x): int))
+ == (lambda y: Box :: $Box($Unbox(y): int));
+}
+