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



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

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


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.

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


Hope this helps,

Oh yes! Thanks again,

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.