Email Gateway (Aug 19 2022 at 16:03): Email Gateway (Aug 19 2022 at 16:03):From: Thomas Genet <thomas.genet@irisa.fr>
Dear all Isabelle users,
For our "formal software engineering" course (1), we use Isabelle/HOL to
generate Scala code to be integrated into bigger Scala developments.
One problem that we have is that when generating the code for a function
f ranging over a datatype T the code of the datatype is systematically
generated. Is it possible to filter out some types/functions for the
generation by export_code? and how?
We need this because, if the code for T is already present somewhere
else in the project, we have to manually edit the generated code.
Thanks in advance,
Thomas
(1) http://www.irisa.fr/celtique/genet/ACF/
Email Gateway (Aug 19 2022 at 16:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
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.
Andreas
Email Gateway (Aug 19 2022 at 16:04):From: Thomas Genet <thomas.genet@irisa.fr>
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
Email Gateway (Aug 19 2022 at 16:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 16:04):From: Thomas Genet <thomas.genet@irisa.fr>
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, sayobject 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
Email Gateway (Aug 19 2022 at 16:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Thomas,
I don't have Isabelle2012 installed any more, but IIRC, the syntax was as follows:
code_type toto (Scala "Scratch.toto")
code_const M (Scala "Scratch.M")
code_const T (Scala "Scratch.T")
Andreas
Email Gateway (Aug 19 2022 at 16:04):From: Thomas Genet <thomas.genet@irisa.fr>
Yes, thanks to the explanation you gave me in your last e-mail + the
List.thy file I just managed to get it right by myself.
Thanks a lot,
Best regards,
Thomas
Email Gateway (Aug 19 2022 at 16:05):From: Thomas Genet <thomas.genet@irisa.fr>
Dear all,
In my case it was also necessary to NOT re-generate the code for
equality on the datatype (HOL.equal) and for some other given functions
(here f).
The function generated for equality on datatype toto is equal_toto so it
is enough to use this identifier directly in the code_printing command
(with a ' to quote the _)
To sum-up my code for Isabelle2014 is:
code_printing
type_constructor toto ⇀ (Scala) "toto"
| constant M ⇀ (Scala) "M"
| constant T ⇀ (Scala) "T"
| constant f ⇀ (Scala) "f"
| constant "HOL.equal :: toto ⇒ toto ⇒ bool" ⇀ (Scala) "equal'_toto"
And for Isabelle2012 it is:
code_abort f
code_type toto
(Scala "toto")
code_const M
(Scala "M")
code_const T
(Scala "T")
code_const "HOL.equal ::"toto ⇒ toto ⇒ bool"
(Scala "equal'_toto")
Best regards and thank you to Andreas!
Thomas
Last updated: Apr 25 2024 at 08:20 UTC