implement compaction in the lazy memory model

[redianthus]

Here's a potential optimization.

The idea is to add a is_half_done : bool ref to each Symbolic_memory.t, initially set to false.

Once the status of a task is Now or Stop, we set this boolean to true in its parent.

Then, on every read or every write (it can also be done less often, I have to think about it), we check if our parent has is_half_done set to true. If this is the case, it means no one else is going to access it, so we can merge ourselves with the parent. This is done by merging the two data fields (start with the parent and add our data afterward), and then, we can throw away the parent and use our grand-parent as our new parent.

The new invariant is that each node of the tree has either its two children still working either it is going to disappear soon.

cc @filipeom, I'm not sure if this is going to improve anything in practice but it would be a nice experiment I believe.

[filipeom]

We can probably benefit a lot from this due to the principle of locality. However, I'm also concerned that you might spend more time merging memories than simply traversing the tree. But we should definitely experiment with this!

I would like to see the numbers from #433 in Test-Comp first. It would be interesting to see the time improvement for searching for a value in the memory tree.

[redianthus]

For the record, we will need to change the data field from being mutable to a reference (to be able to re-use our parent data and add our data on top of it when compacting), we could probably optimize the option ref by using something similar to @chambart's nullable-array, see the discussion in #433.

[redianthus]

However, I'm also concerned that you might spend more time merging memories than simply traversing the tree

We could change the data structure for something that can be easily merged

[redianthus]

We are now using a Map so it does not make sense anymore, closing :-)