Re: [isabelle] Custom Haskell serialisation for datatype constructors

Hi Fabian,

> Adding import lines could also be another use case of "pragmas" (as mentioned in [1]) for serializers.
> [1]

Thanks for the link to the other thread with the patch. As far as I can see, the patch allows to adapt only the export list of generated modules, but not those from code_include. If I could change the export list of an included module, I could re-export the imported constructors. I still prefer to directly import Haskell libraries without going through a code_include, but at least that could get me going again and would allow to pattern-match on constructors.

How is the announced development going on? Are the results already available somewhere?


On 06/06/13 10:34, Fabian Immler wrote:
Hi Andreas,

Am 05.06.2013 um 16:51 schrieb Andreas Lochbihler <andreas.lochbihler at>:

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.