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



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

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
  Submission until 12 July; http://www.iaoa.org/womo/2013.html
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
  Submission until 15 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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