Improve implementation of Vector.tabulate

Currently, `Vector.tabluate` is a straightforward translation of the
following function from `mlvectorScript.sml`:

val tabulate_def = Define`
tabulate n f = Vector (GENLIST f n)`;

For large `n`, this is a bad implementation since a list of size `n`
requires `3 * n` words of space on the heap. Furthermore, the final
vector requires `n` words of space, and when the vector is created in
`data_to_word` both the list and the space for the new vector must be
present in the heap simultaneously. Thus the space required to create
a vector of length `n` is a total of `4 * n` words of memory during
creation. (Once the vector has been created the intermediate list
becomes garbage which will eventually be removed by the GC.)

With the current implementation of the compiler, where vectors are
represented as `Block` in BVL and the only operation to produce such
in `data_to_word`is `FromList`, this space inefficiency is
unavoidable.

**Option 1**

I propose that each vector is implemented in BVL as a `ValueArray`
instead of a `Block`. The idea is that the source would have a new
primitive, `VectorFromArray` with which `Vector.tabluate` would be
implemented, i.e. first producing an array with the desired content,
then apply the primitive to this array in order to turn it into
vector. By doing so, `Vector.tabluate` could perform allocation with a
cost of `2 * n` words of memory, instead of `4 * n` words of
memory. This wouldn't be much of a speed boost, but it would reduce
this momentary peak in space consumption by half.

One benefit of this scheme is that the slightly involved verification
of `FromList` in `data_to_word_assignProof` could be replaced by a
higher-level and easier-to-maintain verification proofs of `FromList`
and `FromArray` stub code in `pat_to_closProof`.

The downside of this scheme is that all vectors (of which there aren't
many) are treated less efficiently by the generational garbage
collector, because it treats them as potentially mutable.

An even more space efficient (but much more challenging) approach
would be to insert a `VecTabluate` primitive to source and compile it
only in `pat_to_clos`. This avoids the intermediate array and can thus
consume only `n` words of memory at creation. However, this requires
supporting a primitive that calls `evaluate` internally for the
function `f` and it requires changing `pat_to_clos` to have an
existential in the proof goal (changes the current nice shape of the
proof completely). I do not recommend this option.

**Option 2**

I propose that we keep representing vectors as `Block`s in BVL, and
instead (1) add a new primitive `FromArray` to every intermediate
language down to and including `dataLang`, and (2) compile this in
`data_to_word` to a call to a memcopy stub.

**Recommendation**

I prefer option 2 because it has the same peak space consumption as
option 1 but is better in that it allows the GC to treat vectors as
immutable data.

---

This was motivated by problems with space consumption that
@tanyongkiam found when benchmarking the compiler.

Start with the recommended Option 2 and trace Vector.tabulate from mlvectorScript.sml through the intermediate languages to dataLang and data_to_word. Read data_to_word_assignProof and pat_to_closProof to understand the existing FromList verification and stub proofs. Done means adding the proposed FromArray path and memcopy stub while preserving immutable Block vectors and reducing peak allocation.

Written by the indexing model from the issue text.