Re: [isabelle] Simple selective code generation?






Dear Andreas,


Le 11/09/14 08:28, Andreas Lochbihler a écrit :
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.


thank you for the pointer to the code generator manual. However I already looked (rapidly though) to this manual and also to the source files List.thy and also to the Code_Integer etc. file to figure out how to achieve my goal... But I did not manage to do it. My feeling is that the reason for this is that I cannot associate to my Isabelle type any existing Scala type but only one that has been generated separately.

Let me explain on a small example:

If I have the following Isabelle code:

-------------------------
datatype toto= M | T

fun f2::"toto ⇒ bool"
where
"f2 M = True" |
"f2 _ = False"
-------------------------

It produces Scala code:

-------------------------
object test2 {
abstract sealed class toto
final case class M() extends toto
final case class T() extends toto

def f2(x0: toto): Boolean = x0 match {
  case M() => true
  case T() => false
}
} /* object test2 */
-------------------------

But I would like to be abble to select what abstract data type definitions to generate. For instance I would like to avoid to generate the
-------------------------
abstract sealed class toto
final case class M() extends toto
final case class T() extends toto
-------------------------
part but only the function declaration f2. I found the "code_abort" command that permits to avoid the generation for constants but (as far as I understand) not for datatype declarations.
I tried also with a code_printing command something of the form:

code_printing
  type_constructor toto ⇀ (Scala) "toto"

It was accepted by Isabelle but export_code then fails.



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.

Yes of course... this is only for a basic "software engineering" purpose. Distinct program parts use the same "toto" type: one part that has been programmed in Scala and one that has been verified and exported from Isabelle. If generation exports again the "toto" implementation this imposes to manually edit the generated file before integration. This can be rapidly done when one datatype is under concern... but not that fast when 5, 10, ... datatypes are concerned... and this has to be done each time that you correct your Isabelle file and re-generate :/


Best regards,

Thomas
--
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.