Array Equality Axiom

[DavePearce]

At the moment, the following test case (test_array_23) uses the empty array syntax:

assert:
  forall(int[] xs):
       (|xs| == 0) ==> (xs == [])

The problem is that, under the current typing rules, (int[])&(void[]) reduces to void.

The question is: do we want to bring back the empty array syntax?

[DavePearce]

UPDATE: I think the system is essentially already handling the empty array syntax quite well. The problem is more likely related to the lack of a connection between |xs| == 0 and xs == [] than anything else.

Specifically, we need an additional array equality axiom that does one of two things:

1. Array Inequality. For xs != [] we need to infer that |xs| < 0 || |xs| > 0.
2. Array Equality. For e.g. |xs| == 1 we need to infer exists(int x).(xs == [x]) or similar.

For some reason, I thought (1) was already handled.

[DavePearce]

UPDATE. Yes, case (1) should already be handled. The problem is that the subtype operator believes that void[] is void. That's consistent. For now, I'll probably just let it think that's OK.

[DavePearce]

Ok, hmmm. It's icky allowing void[] to be a subtype of int[] Perhaps it can be done, but for now I'm leaving it. Instead, I updated the parser to reject [].