Re: [isabelle] Scala code generator: how to write code generated from Isabelle library dependencies to a shared package?



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


On 07/07/13 22:05, Christoph LANGE wrote:
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:

* write "object Set" into another module, say, Set.scala
* and to let A.scala and B.scala import Set.scala instead of having
their own copies of "object Set".

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





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