lean4-htt/library/init/data/array
Leonardo de Moura b1503f2c56 perf(library/init/data/array/basic): remove inefficient mforeachAux and add new hmmap and hmap
The `mforeachAux` function was keeping two references to the array
because it was implemented using `miterate a ⟨a, rfl⟩ ...`
Thus, we would have to allocate a new array even if `a` was not shared.

Another issue is that when invoking `x ← f i v`, the array would still
have a reference to `v`, and consequently `RC(v) > 1`, and `f` would not
be able to perform destructive updates to `v` or reuse its memory cell.

Thus, I removed `mforeach` (we only used it to implement `hmap`: the
homogeneous map), and implemented a new `hmap` which makes sure
destructive updates can be performed modulo the issue with float `let`
inwards I described in the previous commit.

@kha I found the problem described in the previous commit when I was
using `Array.hmap`. If we use `Array`s to implement `Syntax` as we discussed,
then a `hmap` that does not prevent destructive updates from happening is
a must-have. Otherwise, any benefit we get from using `Array`s instead
of `List`s is gone.
2019-04-19 14:52:52 -07:00
..
basic.lean perf(library/init/data/array/basic): remove inefficient mforeachAux and add new hmmap and hmap 2019-04-19 14:52:52 -07:00
default.lean chore(library): use lowercase in imports 2019-03-21 15:06:44 -07:00