Re: [isabelle] Simple selective code generation?

Le 11/09/14 10:01, Andreas Lochbihler a écrit :
Hi Thomas,

datatype toto= M | T

fun f2::"toto ⇒ bool"
"f2 M = True" |
"f2 _ = False"
In the following, I assume that you have already generated the Scala
code for toto in the module Scratch, say

object Scratch {

abstract sealed class toto
final case class M() extends toto
final case class T() extends toto

} /* object Scratch */

Then, the following code_printing declarations for the type and its type
constructors suffice.

code_printing type_constructor toto ⇀ (Scala) "Scratch.toto"
| constant M ⇀ (Scala) "Scratch.M"
| constant T ⇀ (Scala) "Scratch.T"

Then, "export_code f2 in Scala module_name Foobar" yields

object Foobar {

def f2(x0: Scratch.toto): Boolean = x0 match {
   case Scratch.M => true
   case Scratch.T => false

} /* object Foobar */

Yes! Thanks, that's exactly what I was looking for.

Bonus question: do you know how to perform this in Isabelle2012?
With code_type?

   type_constructor toto ⇀ (Scala) "toto"

It was accepted by Isabelle but export_code then fails.
You also have to provide serialisation instructions for all the
constructors of the datatype. Unfortunately, the error messages from
export_code are not particularly informative.

True, as you say "this is not particularly informative" :-)

Hope this helps,

Oh yes! Thanks again,

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at

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