[isabelle-dev] Should code_abort remove the corresponding code equations?

[Florian Haftmann]

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
>> in.
> 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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130718/084b675e/attachment.sig>