Re: [isabelle] Simple selective code generation?



Dear Thomas,

Isabelle's code generator always generates self-contained code, i.e., it generates everything on which your functions depend. The only execption is if you adapt the serialisation such that pre-defined functions are used (as is done, e.g., for 'a list). This can be done with code_printing, see the code generator tutorial for details.

A word of warning, though. With respect to "correctness of the generated code", adapting the serialiser is like adding axioms to your theory. There are no checks that it is semantically correct whay you do, and you can even derive False when you prove by evaluation.

Andreas

On 10/09/14 16:02, Thomas Genet wrote:

Dear all Isabelle users,


For our "formal software engineering" course (1), we use Isabelle/HOL to generate Scala
code to be integrated into bigger Scala developments.

One problem that we have is that when generating the code for a function f ranging over a
datatype T the code of the datatype is systematically generated. Is it possible to filter
out some types/functions for the generation by export_code? and how?

We need this because, if the code for T is already present somewhere else in the project,
we have to manually edit the generated code.


Thanks in advance,

Thomas
(1) http://www.irisa.fr/celtique/genet/ACF/




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.