Separate monadic translation from monadic defs

[talsewell]

The way the monadic translator is set up pushes things into one theory. This is awkward if we would like to define and verify an algorithm in one theory and translate it into a CakeML program in another.

I have an example CakeML verified algorithm (see #979 ) which is provided in a few logical steps:

1. Define and verify the logical algorithm in plain HOL.
2. Define the monadic variant, rearranging nested datatypes into flat arrays.
3. Prove that versions 1 + 2 are equivalent (or related).
4. Translate version 2 into CakeML AST using the monadic translator.

The key point here is that (3), the proof of simulation, is a bit involved. It would be nice to present (1) in its own theory, independent of any CakeML stuff, and to present (2) in its own theory which uses the monad type but is otherwise independent of translation infrastructure.

It's not clear if this is possible. It doesn't seem to be supported by the preferred "interface library". The interface library, for instance, defines the accessor and updator functions needed to define monadic things (in (2)) at the same time as turning on various translation infrastructure. It also seems to make assumptions about the theory location and naming scheme of various translation constants which seem to break when called with a state type that was defined previously.

The preferred outcome would be to adjust the interface library (and perhaps more of the monadic translator) to separate monad setup from monad translation setup, and provide an example which defines and verifies a monad in one theory and then translates it in another.

[talsewell]

I think that there are some simple deficiencies in the way the interface lib deals with the main translator. Everything about the way that store_exn_invariant_name and store_invariant_name are used to construct predicates looks like a buggy re-implementation of get_type_inv.