[isabelle-dev] Should code_abort remove the corresponding code equations?
florian.haftmann at informatik.tu-muenchen.de
Thu Jul 18 12:00:10 CEST 2013
>> 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.
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev