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

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

> Maybe two situations should be distinguished:
> * Constants which didn't see any code declaration ever.
> * Constants whose code equations have been explicitly deleted.
>
> The first would raise an error, whether the latter would be translated
> as exception.
I am not sure I get what you mean here: Do you suggest that code_abort could be eliminated 
in favor of this heuristics (if one has deleted the code equation for a constant, the code 
generator will implicitly treat it like a code_abort? I am quite happy with explicit 
code_abort declarations, because this protects users from overlooking missing equations. I 
don't want to grep the generated code for such implicit exceptions all the time.

And I also don't fully understand the first situation. Today, the frequently used 
definition packages generate some default code declaration (function, primrec, definition 
do, but not (co)inductive(_set), defs, specification). So I'd argue that most constants 
nowadays see a code declaration.

Best,
Andreas