[CakeML-Dev] Exceptions in cakeML basis library

[Ramana Kumar]

I just realised it's probably possible to have the same HOL function both
produce translator preconditions and generate CakeML that raises
exceptions, once we have https://github.com/CakeML/cakeml/issues/181
completed.

So there's not really a choice to be made here. You should just write
functions that have preconditions where necessary, and eventually we can
make these translate to code that raises the correct exception. (If you
want to force the translator to produce a precondition, you can always use
ARB in your definition. It's usually better to avoid preconditions where
possible, though..)

On 28 November 2016 at 14:11, Connor Cashman <connorjcashman at gmail.com>
wrote:

> Hi,
>
> I’m working on creating the basis library for cakeML and Ramana told me to
> ask your opinions on the use of exceptions in its creation. I have
> initially based the library on definitions given in the standard ML basis
> library, but these have cases where exceptions need to be raised. My
> question is whether I should leave these to pre-conditions on HOL, or
> whether I should raise exceptions in my definitions. Usually, HOL gives
> pre-conditions which match the exceptions, but this is not always the case.
> For example, the take function, as defined in HOL’s TAKE_def, has no issue
> with using indexes outside of the length of the list, where SML raises an
> exception for this. This also often occurs in cases where SML raises
> exceptions for negative inputs. This could be fixed by writing new
> definitions for such functions but I am unsure if this is the best option.
>
> Your opinions would be much appreciated.
>
> Connor
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161128/0d54588f/attachment.html>