[isabelle] Custom Haskell serialisation for datatype constructors

Dear list,

For Haskell code generation, I try to map some of my Isabelle types and definitions to Haskell types and functions as described in the code generator tutorial. As these Haskell types and functions are not imported automatically in the generated modules, I follow the usual way of rebinding them in a separate code_include module as follows:

code_include Haskell MyModule {*
import qualified <Haskell-Module>;
type MyType = <Haskell-Module>.MyType
myFun = <Haskell-Module>.myFun
code_reserved Haskell MyModule

code_type my_type (Haskell "MyModule.MyType")
code_const my_fun (Haskell "MyModule.myFun")

This works well except for one case: datatype constructors that the Haskell module exports
My definition of a datatype in Isabelle is the same as the definition in Haskell, so I would like to map it directly to Haskell's. However, I cannot rebind constructors in Haskell and code_include does not allow me to specify module reexports such that the imported datatype and its constructors become available.

I have seen that such imports are hard-coded for the HOL types bool and list in src/Tools/Code/code_haskell.ML, but I actually don't want to hack my Isabelle sources whenever I need to include another module. Is there currently any other way to achieve what I want?

If not, I'd also be willing to extend the code generator. It would suffice if one can declare globally that some import line is to be added to every generated module.


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