Behaviour of Arrays

[mzuenni]

Is this intended behaviour that a variable is used like a special index in the array?
i.e. that those two programs are valid and accept:

SET(a=1)
ASSERT(INARRAY(1,a))

SET(a=1)
SET(a[1]=1)
ASSERT(!UNIQUE(a))

(My assumption would have been that a variable must either be an array or a value but not both at the same time)

[eldering]

Is this intended behaviour that a variable is used like a special index in the array? i.e. that those two programs are valid and accept:

So the way that variables and arrays at the same time are stored internally is as a map (variable name, index) -> value.

So when you call SET(a=42), then that is stored as ("a", []) -> 42, while if you call SET(a[1]=42), then that's stored as ("a", [1]) -> 42.

SET(a=1)
ASSERT(INARRAY(1,a))

So this actually checks if the value 1 exists inside the a variable for any index, including the empty list index associated to the "non-array" variable a. That's why it returns true.

SET(a=1)
SET(a[1]=1)
ASSERT(!UNIQUE(a))

Here, a contains 1 at two different indices: [] and [1], which is why UNIQUE returns false.

(My assumption would have been that a variable must either be an array or a value but not both at the same time)

I'm not arguing that this is intuitive or correct behaviour, just what is currently implemented. I think the options are either to clarify that a simple (non-array) variable is basically a special case of an array with empty index, or indeed somehow to disallow a variable to have both a non-array value (i.e. empty index) and any array values (i.e. non-empty indices) at the same time.

[mzuenni]

I'm not arguing that this is intuitive or correct behaviour, just what is currently implemented. I think the options are either to clarify that a simple (non-array) variable is basically a special case of an array with empty index, or indeed somehow to disallow a variable to have both a non-array value (i.e. empty index) and any array values (i.e. non-empty indices) at the same time.

I am fine with both. My python reqrite currently matches main, but if i remmeber correctly the antlr_rewrite differentiates between arrays and values.

[mzuenni]

maybe also relevant: if we force that a variable is either an array or a value, would we also force that it must have a fixed dimension?
In other words would SET(a[1]=1,a[1,1]=2) be an error or ok?

[eldering]

maybe also relevant: if we force that a variable is either an array or a value, would we also force that it must have a fixed dimension? In other words would SET(a[1]=1,a[1,1]=2) be an error or ok?

In the standard checktestdata specification that's currently allowed.

One the one hand I don't expect that people typically use/need that, but OTOH it would break backwards compatibility.

[mzuenni]

but OTOH it would break backwards compatibility

For me the questions would be a different: do people use this intentionally VS. do they use it by accident? or in other words if this happens, is it more likely to hint at a bug in the checker? If the answer is yes than we should warn/error?