Checking for translator pre/side conditions.

[talsewell]

It's common to want the top-level translated functions to not have pre-conditions or side-conditions.

The CakeML development indirectly requires this with the top-level CF theorems stated about the final toplevel declarations. If a user accidentally introduces a silly side-condition or pre-condition then the CF proof will fail. Unfortunately a lot of CPU and human work is then required to discover the problem.

Simple solution: a one-line check that a translated function doesn't (currently) have any pre-conditions or side-conditions. The CakeML development, for instance, can run this check before its final topdecls and CF proof.

If a condition is found, the error message should try to identify where in the function call graph the problematic precondition came from.

[myreen]

I'm often annoyed by the names of the generated side conditions. The reason for the odd names is that the translator tries to not redefine already defined functions.

Would it make sense to have a mode (on by default) that stops translation at a function if the function generates a side condition but the translator has no user-specified name for the side condition?

Example: the following would fail in case translation of foo_def produces a side condition:

val res = translate foo_def

The new correct way would be to write:

val _ = set_side_cond_name `foo` "foo_side"  
val res = translate foo_def

This is compatible with recursive translation since one can specify many:

val _ = set_side_cond_name `bar` "bar_side"  
val _ = set_side_cond_name `baz` "baz_side"  
val _ = set_side_cond_name `foo` "foo_side"  
val res = translate foo_def

Maybe set_side_cond_name should take a list of qterms, names.

[xrchz]

Yes.

I also suggest making renames wherever necessary to fixate on a single piece of terminology from "side condition" and "precondition". (I think "side condition" is better.)

[xrchz]

(set_side_cond_name will also need a stateless version per #96)

[xrchz]

We should change the translator API to explicitly say whether you have a precondition or not, as in the cv translator.

[xrchz]

Can be done via a transitional API change (i.e. have a period with both old and new APIs in use)