[isabelle] Code generation Module Cycles



Hi
I wish to Haskell code generating from two theories, LinearOut and Range_Simp that both import from a third theory Ftype_Data where a common data structure is defined.

To stop the data structure from being defined in both Haskell modules I tried

code_modulename Haskell
    LinearOut LO
and
code_modulename Haskell
   Range_Simp RS

But each generated a lot of (6 and 10) small Modules with the same name Nat.hs List.hs Integer.hs ...

So I added these to the new module
code_modulename Haskell
    LinearOut LO
    List  LO
   Integer LO
...
and
code_modulename Haskell
   Range_Simp RS
   List  RS
   Integer RS
...

This resulted in less Haskelle modules List.hs .... disappeared and was incoperated in the larger module (as expected)
But Nat.hs and Integer.hs was still generated.
Any ideas how to stop this?

Worse still Integer.hs imports LO and LO imports Integer. So GHC would not compile these modules.

I found out that only incorerating List into the new Module by using

code_modulename Haskell
    LinearOut LO
List LO and
code_modulename Haskell
   Range_Simp RS
   List  RS

the resulting Integer.hs did not import LO so at least GCH would compile. But this still leaves me with the problem that I have a group of pairs of Haskell modules where each module in a pair has the same name but different code.

Now I am stuck Any ideas what I am doing wrong?

david










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