Email Gateway (Aug 19 2022 at 11:27): Email Gateway (Aug 19 2022 at 11:27):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear all,
in writing Scala wrappers around code generated by the Isabelle Scala
generator I'm realising that things start becoming hard to maintain.
For now I'm mainly generating code for a few functions in one Isabelle
theory, but soon I will generate code from multiple Isabelle theories;
let's call them A.thy and B.thy.
Both Isabelle theories have shared dependencies in the Isabelle library.
This gives me redundant copies of such code, e.g. I end up having an
"object Set" defined both in A.scala and B.scala. Thus another thing I
want to do becomes infeasible:
I would like to implement user interfaces around A.scala and B.scala,
let me call them A_UI.scala and B_UI.scala, and these user interfaces
will need functions such as a pretty-printer that turns Set(List(1, 2))
into "{1, 2}". This pretty-printer I would like to implement once,
centrally, in a shared Scala module Shared.scala. However, this would
require me to be able to instruct the code generator to:
I did notice section "6.4 Intimate connection between logic and system
runtime" in the codegen manual, but I'm not sure whether this is of
general interest (and whether it's relevant to my problem), or whether
it only applies to ML code generation.
Assuming that what I want is not currently possible, is there at least a
workaround? What do other code generator users do?
I understand that once more it makes the generated code less trustable,
as now we'd also have to trust the module system of the target language.
But still I'd like to be able to maintain software that uses generated
code.
Cheers, and thanks in advance for any help,
Christoph
Email Gateway (Aug 19 2022 at 11:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Christoph,
The code generator always outputs all code for what is needed to implement the specified
constants. From a modularity point of view, this is a bit unsatisfactory. I usually use
one of two workarounds:
a) Do not use module_name when exporting code. Then, the code generator puts every theory
into a separate module (you can configure this to some extent with code_modulename).
Unless you have naming conflicts between your theories, this should give you the same
object Set for A.thy and B.thy (if both use the same operations on sets). This works
particularly well for Haskell because the code generator already puts every module into a
separate file. So if you set the same output directory for A and B, you just get the
module once. For SML and Scala, all modules are in a single file for A and once more in a
single file for B. But you can just split the files at the module boundaries with a simple
script.
Note that without module_name in the export_code statement, you face the notorious
"dependency cycle" problem. This occurs particularly if you heavily employ the refinement
features of the code generator. Then, you have to manually adjust the module assignment
with code_modulename.
b) Define a shared theory AB.thy that imports A and B and export all functions of A and B
in one export_code statement. Then, you only have one file and one instance of every
module. Your user interfaces then simply ignore the code that do not belong to A or B, resp.
To go this way, you must be able to merge theories A and B. In particular, they must not
have each a theory of the same name, and they must not instantiate the same type class for
the same type. You can avoid the former by renaming theories. And if the latter occurs,
sharing gets you in trouble anyway. For example, suppose that A uses the prefix order on
lists and B the lexicographic order from the appropriate HOL/Library theories.
If you shared the List module between A and B, your code would probably become incorrect,
because the List module also contains the instantiations for the type classes, i.e., you
would either run A with the lexicographic order or B with the prefix order.
Best,
Andreas
Email Gateway (Aug 19 2022 at 11:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christoph,
beyond what Andreas has mentioned, future Isabelle releases will bring
options for fine-grained control over the module name space of generated
code. This could also give a (partial) answer to your issues.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:37):From: Christoph LANGE <math.semantic.web@gmail.com>
Hi Andreas,
thanks for your help, and sorry for replying so late. I was at a
conference and on holiday and only resumed working with generated code
today.
2013-07-08 08:44 Andreas Lochbihler:
This is what I will try for now.
I wrote the following script; feel free to reuse it.
https://codex.cs.bham.ac.uk/svn/langec/formare/code/auction/isabelle/Auction/code/split-scala-modules.pl
(user: guest, password: guest)
For now please bear with the access control, but we are planning to move
to Github.
I will also make the script available in a nicer way at
http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/isabelle.
Cheers,
Christoph
Last updated: Nov 21 2024 at 12:39 UTC