make the translator as stateless as possible

Debugging the translator can sometimes be a right pain. Maybe it would be easier to debug if it was mostly stateless? The idea is to put all the current refs into a state datatype that can be passed around the translator's different functions. This helps with debugging because it is easy to roll back state changes by just using an older state value.

There are some things that cannot be made completely stateless: the translator makes intermediate definitions in order to speed up a few tedious proofs (about looking up definitions in the environment produced by a list of declaration). The translator uses a hook on export_theory to save its current state.

Question: should the translator's user-interface change so that it exposes the underlying state? Concretely, should the following

val _ = translate APPEND;
val _ = translate REVERSE;
val _ export_theory();

be turned into something like:

val ctxt = stateless_translate ctxt APPEND;
val ctxt = stateless_translate ctxt REVERSE;
val _ = save_translator_state ctxt;
val _ export_theory();

I prefer the stateful user interface. However, the code in ml_translatorLib can be reorganised to be stateful only in the very last part that defines translate in terms of stateless_translate. Note that one could mix the two styles:

val _ = translate APPEND;
val ctxt = get_translator_state ();
val ctxt = stateless_translate ctxt REVERSE;
val _ = set_translator_state ctxt;
val _ export_theory();

Issue #85 is related, but not the same.