// 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 x: A :: x) == (lambdax: A :: x); // fails because of type parameters. this could be fixed.
/* // more tests, when it is fixed
var k1 : [A1][B1]A1;
var k2 : [A2][B2]A2;
k1 := (lambda x: A :: (lambda y: B :: x));
k2 := (lambda x: A :: (lambda z: C :: x));
assert k1 == k2;
k2 := (lambda u: X :: (lambda 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) : Box;
function $Unbox(Box) : T;
procedure Coercion() {
assert (lambda x: Box :: $Box($Unbox(x): int))
== (lambda y: Box :: $Box($Unbox(y): int));
}