Re: [isabelle] Simple selective code generation?

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 */

   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.

Hope this helps,

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