[CakeML-Dev] x64_enc undefined on Div

[Magnus Myreen]

On 31 October 2016 at 01:59, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> x64_enc0 is not defined for the new Div instruction in asm. This is probably
> intentional since Div is not supported on x64. However, for translating the
> compiler into CakeML, this causes a problem, since the translator prefers
> functions to be total.

All functions that go through the bootstrap needs to be as fully
specified as possible. Anything else causes unnecessary work in the
side condition proofs for the bootstrap.

> Should we work on propagating the side condition that
> Div is never passed to x64_enc?

no

> Or can we make the definition total by
> providing a dummy encoding?

yes, e.g. the encoding for Skip.

> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>