[isabelle] Simple selective code generation?




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/
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet




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