#trace;

define a = wrapInt(1);
a == 1; // ok

define b(i:[int]) = a == i; // should give b :[ int] -> boolean but gives b : int -> boolean instead
b; // however this returns <function> : [int] -> boolean !!!

// same here:
// **6 AQL> define c(i:[int]) = i;
// *** Defined c : int -> int
// **7 AQL> c;
// <function> : [int] -> [int]
// **8 AQL> c(a);
// 1 : [int]


define b = 1;
b == wrapInt(1); // ok

a == b; // ok

// define a = 1;
// let i = wrapInt(1); in a = i; // should return true but gives  
// *** Dynamic Semantics Error: (array bound violation) - see  (line 12, columns 1...29)

// The problem is that the code this generates is:
// 	[0]	PUSH_I(1)
// 	[1]	I_TO_O
// 	[2]	PUSH_SCOPE(CODE: #0,5,<0,0,0,1>)
// 	[3]	ENTER(0,1,0,0)
// 	[4]	END
// 	[5]	PUSH_OFFSET_O(0)
// 	[6]	SET_GLOBAL([defined] a : [int])
// 	[7]	RETURN_O

// which is wrong : [3] should be ENTER(0,0,0,1) like the CODE in the
// PUSH_SCOPE of [2].  It looks like the typing of the args in the code
// for instruction Enter.java gets the wrong typing kind from the test
// in the switch statement: (type.domain(i).boxSort())! Need to review
// carefully the un/boxing analysis in the the type checker of
// Scope.java - it does work for abstractions.

// In fact, there should be no need for the generating the I_TO_O as the
// arg should be unwrapped beforehand and the the PUSH_SCOPE should be
// PUSH_SCOPE(CODE: #0,5,<0,1,0,0>) and then the ENTER is correct as
// is. This is what happens for abstractions - but then there too there
// is a spurious I_TO_O that messes up application! For example:

// (function (i:int) i) (wrapInt(1));

// Gives the code:

// 	[0]	PUSH_I(1)
// 	[1]	I_TO_O
// 	[2]	PUSH_CLOSURE(CODE: #4,5,<0,1,0,0>,<0,0,0>)
// 	[3]	ENTER(0,1,0,0)
// 	[4]	END
// 	[5]	PUSH_OFFSET_I(0)
// 	[6]	RETURN_I

// This has the right CODE in the closure and the right ENTER, but the
// I_TO_O screws things up!

// On the other hand this works fine if a is defined as wrapInt(1). For example,
// (function (i:int) i) (a); gives the following code - which runs fine:

// 	[0]	CALL([defined] a : [int])
// 	[1]	PUSH_CLOSURE(CODE: #3,4,<0,1,0,0>,<0,0,0>)
// 	[2]	ENTER(0,1,0,0)
// 	[3]	END
// 	[4]	PUSH_OFFSET_I(0)
// 	[5]	RETURN_I

// There, the value of a is a boxed int but is automatically unboxed (as it should be)!
// Need to fix this mess! (The un/boxing analysis)


// define a = 1;
// let i = wrapInt(1); in a == i; // should return true

// class Foo { a : int; };
// let i = wrapInt(1); foo = new Foo; in foo.a = i;

[+,new{}] { x | x <- set{"b", "a"}, x != "b" }; // ok

[+,new{}] { x | <x,x+1> <- set { <1,2>,<5,6> } }; // ok

[+,new{}] { x | <x,x+1> <- set { <1,2>,<5,6>, <3,4> } }; // ok

[+,new{}] { x | x <- 1..4 }; // ok
