Open
Description
Currently, if you translate something with a side-condition from ARB
, the translator produces the code raise Bind
. It would be nice to tweak this a little to allow an arbitrary exception. For example:
val _ = register_exn ``Size``; (* made this up... not sure how it should work *)
val sub_def = Define`sub i ls = if i < LENGTH ls then EL i ls else FAIL Size ARB`;
to produce code that calls raise Size
rather than raise Bind
.
This requires the translator to support defining exceptions too.
For sophisticated use of exceptions, one must use CF, but for exceptions that correspond to side-conditions we expect to always be true, it would be nicer to just use the translator.