Email Gateway (Aug 19 2022 at 11:21): Email Gateway (Aug 19 2022 at 11:21):From: Andreas Lochbihler <andreas.lochbihler@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.
Best,
Andreas
Last updated: May 06 2024 at 20:16 UTC