Re: [isabelle] Simple selective code generation?



Hi Thomas,

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

fun f2::"toto ⇒ bool"
where
"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 */

code_printing
   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,
Andreas




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