Re: [isabelle] Custom Haskell serialisation for datatype constructors



Hi Fabian,

Thanks for sharing your patches. As I do not know Florian's plans with the code generator, I will wait for him to comment on the idea and the fixes before I will add them my Isabelle version (and potentially later to the repository).

Andreas

On 06/06/13 16:52, Fabian Immler wrote:
Hi Andreas,

Am 06.06.2013 um 11:37 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:

Hi Fabian,

Adding import lines could also be another use case of "pragmas" (as mentioned in [1]) for serializers.
[1] http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.devel/4101

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?
 From what I know, the announced development still concentrates mostly on exporting functions (and esp. for Scala).
But perhaps Lukas can publish some of his changes.

I realized that the patch we currently use in the student project on DPH allows you to directly specify import statements. I pushed these patches to [2] if you want to have a look at them.
But beware that these are just quick "fixes" that work in our setting.

Fabian


[2] bitbucket.org/immler/isabelle-dph/commits/6402cbe928b5b012cdf05f96e556826ddd9f34f3


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

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

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.


Cheers,
Fabian







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