[CakeML-Dev] Exceptions in cakeML basis library

[Connor Cashman]

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