<div dir="ltr"><div>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 <a href="https://github.com/CakeML/cakeml/issues/181">https://github.com/CakeML/cakeml/issues/181</a> completed.<br><br></div>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..)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 28 November 2016 at 14:11, Connor Cashman <span dir="ltr"><<a href="mailto:connorjcashman@gmail.com" target="_blank">connorjcashman@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
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.<br>
<br>
Your opinions would be much appreciated.<br>
<br>
Connor<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</blockquote></div><br></div>