[isabelle-dev] Should code_abort remove the corresponding code equations?
andreas.lochbihler at inf.ethz.ch
Thu Jul 18 12:28:42 CEST 2013
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"
"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.
More information about the isabelle-dev