[CakeML-dev] [CakeML-Dev] Exceptions in cakeML basis library

[Magnus Myreen]

I'm in favour of having as few preconditions / exceptions as possible
for operations on lists, options, strings etc. -- Magnus

On 28 November 2016 at 15:11, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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
>
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>