Parameterize Thread on Symbolic Memory and Choice Monad on Thread

[filipeom]

This PR parameterizes the Thread module on the symbolic memory and the Choice_monad module on a Thread, with @krtab doing the heavy lifting.

Summary

This is needed for #357 because we're going to have to use the Symbolic_choice within the Symbolic_memory. The current implementation of Symbolic_choice would not allow us to do so since the original Thread module was defined using the symbolic memory itself, causing a circular dependency. Therefore, we parameterized Thread and subsequently Symbolic_choice, resulting in the following modules:

• Thread_with_memory: This is equivalent to the previous implementation of Thread in that it contains a reference to the symbolic memory. This module is used to construct Symbolic_choice_with_memory.
• Thread_without_memory: A thread without references to the symbolic memory.
• Symbolic_choice_with_memory: This is equivalent to the previous implementation of Symbolic_choice and is the module used to build the symbolic interpreter in symbolic.ml.
• Symbolic_choice_without_memory: A choice module built with Thread_without_memory to be used within the symbolic_memory module in [WIP] Make symbolic memory parametric #357.

Notes

The .mlis probably need more work. I purposefully removed symbolic_choice.mli to appease the type checker, but we should probably add it again to avoid having dead code within symbolic_choice.ml. Nevertheless, I think this is ready-ish for review 😄

[redianthus]

OK, I read the code a first time and left minor comments. I'll probably have to re-read it in a few days and spend more time on it if you want a proper review. Otherwise, I'm fine with merging as is. Did you get @chambart's feedback on the change? (We never know if there's a magic way to make this simpler...)

[filipeom]

OK, I read the code a first time and left minor comments. I'll probably have to re-read it in a few days and spend more time on it if you want a proper review.

Yeah this is not urgent so feel free to take your time :)

Did you get @chambart's feedback on the change? (We never know if there's a magic way to make this simpler...)

Arthur and I briefly discussed this with Pierre, but we haven't heard his take on it just yet.

[redianthus]

@filipeom, could you add the missing .mli and rebase? This is OK to merge for me. :)

[filipeom]

Reintroduced symbolic_choice.mli in 8a20a39. I think this might now break the isolation of the symbolic choice monad, but I don't see an alternative to exposing CoreImpl.State in symbolic_choice.mli to make Symbolic_choice_with_memory.lift_mem typecheck.

[redianthus]

Thanks!