readmePrefix

The CakeML type inferencer.

Includes a translation of "specification-level" code into a
cv_compute-based presentation. This is done in a number of stages. The
base complication is the fact that the HOL unification algorithm is
expressed over a different type (`α term` with constructors: `Var`,
`Const` and `Pair`) from the one we want to use (`infer_t` with
constructors: `Infer_Tvar_db`, `Infer_Tapp` and `Infer_Tuvar`), and
uses finite maps to represent its substitutions.

The HOL presentation does provide a version of `unify` that uses
sptrees instead of finite-maps (`sunify`), but we do the conversion to
the `infer_t` type with the functions

        encode_infer_t : infer_t -> atom term
        decode_infer_t : atom term -> infer_t

eventually deriving

        cunify : infer_t num_map -> infer_t -> infer_t -> 
                 infer_t num_map option

The second problem is that `cunify` features nested recursion and a
complicated precondition to guarantee termination. The next part of
the translation is to create an equivalent tail-recursive formulation
of `cunify` which can be more readily translated into cv_compute land.
This process generates a `tcunifywl`. The `tc` prefix indicates that
it tail-calls, and the `wl` suffix says that the process of
contification has made the presentation use a "work-list".

## Guard Removal

There are four important theorems proved for every tail-recursive
constant (cunify and its auxiliaries):

   {const}_preserves_precond:
     |- !x y. precond x /\ {const}_code x = INL y ==> precond y

   {const}_ensures_decrease:
     |- !x y. precond x /\ {const}_code x = INL y ==> {const}R y x

   WF_{const}R:
     |- !x. precond x ==> WF ({const}R x)

   {const}_tcallish:
     |- !x. precond x ==> {const} x = TAILCALL {const}_code {const} x

The `{const}_code` is of type returning a sum, where the `INL`
corresponds to a recursive tail-call and the `INR` case corresponds to
terminating. 

These can then be used to prove the {const}_pre results,
which are of the form

   precond x ==> {const}_pre args

The strategy is to set up a well-founded induction with WF_{const}R,
and to then exploit the fact that {const}_pre is "basically" an
inductive relation defined on the basis of

      !y. {const}_code x = INL y ==> {const}_pre y
    ----------------------------------------------
                    {const}_pre x

We can use the inversion ("cases") theorem for this inductive
relation, and the fact that {const}_code reduces the relation to get
the induction to go through.