>> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
