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

[Florian Haftmann]

>> 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
as exception.

Cheers,
	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/5d667c87/attachment.sig>