[isabelle-dev] Should code_abort remove the corresponding code equations?
florian.haftmann at informatik.tu-muenchen.de
Thu Jul 18 15:07:30 CEST 2013
Am 18.07.2013 12:28, schrieb Andreas Lochbihler:
> Hi Florian,
> On 18/07/13 12:00, Florian Haftmann wrote:
>>>> Should code_abort remove the code equation for test? Otherwise the
>>>> resulting program might be non-terminating.
>>> I have often run into this problem myself, too, especially in case of
>>> non-termination. I would find it sensible that code_abort deletes the
>>> code equation.
>> Good equestion. Generally, the code generator does not enforce any
>> constant to have corresponding code equations. Of the different target
>> mechanisms (simp, nbe, code) only the latter has an explicit check
>> whether code equations are present, and this is where code_abort comes
> Right, but it is not really about the check.
> A frequent use case for code_abort is the following:
> definition error_case_for_f where "error_case_for_f = f"
> code_abort error_case_for_f
> lemma [code]:
> "f x =
> (if <test for error condition> x
> then error_case_for_f x
> else <do something sensible>)"
> The definition implicitly declares "error_case_for_f = f" as a default
> code equation, and this is still present. If one then generates code (or
> use simp and nbe), one will get non-termination for the then branch (and
> quickcheck can be quite successful in picking the then branch!). It is
> just annoying that I have to manually delete the default code equation.
> And it is important to really delete it, it does not suffice to change
> the behaviour of code_abort in the code target: then, one would run into
> non-termination with simp and nbe, which are even harder to debug than
> the generated code.
The idea is to have an explicit delete declaration, e.g. something like
definition error_case_for_f where [code del]: "error_case_for_f = f"
which will both have the effect of leaving no code equations for
error_case *and* generate exception code (instead of aborting).
The ancient abort would only occur for constants which never have been
given any (default or explicit) code equation.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev