lean4-htt/library
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
..
init perf(library/init/data/array/basic): remove inefficient mforeachAux and add new hmmap and hmap 2019-04-19 14:52:52 -07:00
leanpkg.path feat(leanpkg): add package manager 2017-05-01 14:11:38 -07:00
library.md chore(library/library.md): update documentation 2017-08-16 14:17:26 -07:00
Makefile.in feat(shell/CMakeLists): build stdlib using -g in debug mode 2019-03-29 14:32:12 +01:00
relative.py feat(library,src/CMakeLists): use simple Makefile by Simon Hudon to bring back some degree of parallel compilation 2018-10-19 09:52:01 +02:00