catch exception when evaluating translated Gospel terms

[n-osborne]

Some function in the Gospel standard library are not total. This means that there implementation in the Ortac_runtime module can raises exception, causing the evaluation of translated Gospel terms to fail.

Ortac_runtime also provides a Specification_failure exception that wrapper use to inform the user that the evaluation of a Gospel term has failed. This could be extended and used in qcheck-stm.

Another idea would be, as QCheck-STM expect postcond and precond to be pure, to catch the exceptions raised when evaluating a translated Gospel term (at least in those functions) and interpret that as the term being evaluated to false. List.hd [] = a would then be false.

[shym]

Interesting ideas! I think returning false would send a misleading signal, though: in the case of partial functions being used in the specification, we know that the specification is at fault, while false signals an inconsistency between the code and the specification. So we might guide the user in the right direction right away. I like the idea of reusing the strategy of wrapper and wrapping translations of Gospel specifications in try ... catch blocks because we could exploit the fact that we have a little bit more context (in particular the source location!). I would favour using a dedicated exception for that purpose rather than trying to reuse the Specification_failure error there, as it doesn’t quite fit, I think.

[n-osborne]

Closed by #157