Optimising Quantifier Evaluation

[DavePearce]

(see also #20)

The implementation of quantifiers looks something like this:

static private boolean block$217(BigInteger[] xs) {
  for(BigInteger k = BigInteger.valueOf(0L);0 < k.compareTo(BigInteger.valueOf(xs.length));k = k.add(BigInteger.ONE)) {
    if(...)  { return true; }
    }
  return false;
}

This is pretty horrendously inefficient. Realistically, we want k to have Java type int, since this is the optimal solution. However, the problem is that we then need to maintain an environment of some kind which allows us to know that k has type int when translating xs[k] above to avoid it becoming xs[k.intValue()].

NOTE: this might be partially fixed with the introduction of fixed-size integers. In such case, presumably k would have type uint anyway.