Re: [isabelle] Custom Haskell serialisation for datatype constructors



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.