Discussion:
[isabelle] Customise the Haskell code generator?
(too old to reply)
Moa Johansson
2016-08-03 11:05:38 UTC
Permalink
Raw Message
Hi!

I’m wondering if it’s possible to customise the Haskell code generator: A normal user probably want it to translate e.g. various list functions to the corresponding Haskell library functions. However, in our application it would make our lives slightly easier if we had the option to also include those (library) function definitions explicitly in the resulting .hs file, instead of creating a file that imports them. So just wanted to check if this is possible somehow, to maybe save myself some work.

I currently generate the code using the function Code_Target.export_code, which takes many arguments but it wasn’t obvious if any of them control what I want to do.

Best,
Moa
C. Diekmann
2016-08-05 07:26:11 UTC
Permalink
Raw Message
Dear Florian,

first of all, thanks for the awesome work on the code generator!

2016-08-04 9:23 GMT+02:00 Florian Haftmann <
Hi Moa,
Hi!
A normal user probably want it to translate e.g. various list functions to
the corresponding Haskell library functions. However, in our application it
would make our lives slightly easier if we had the option to also include
those (library) function definitions explicitly in the resulting .hs file,
instead of creating a file that imports them. So just wanted to check if
this is possible somehow, to maybe save myself some work.
you can reset those target language specific adaptations using
»code_printing«, e.g.
code_printing
constant append ⇀ (Haskell)
export_code append in Haskell
See the Isar Reference Manual and the Tutorial on Code Generation for
details.
Similar to <import "~~/src/HOL/Library/Code_Target_Int">, is there
something like
<import "~~/src/HOL/Library/Code_Trust_the_Target_Language_Standard_Library">?

Best,
Cornelius
Lars Hupel
2016-08-05 08:01:30 UTC
Permalink
Raw Message
Hi Cornelius,
Post by C. Diekmann
Similar to <import "~~/src/HOL/Library/Code_Target_Int">, is there
something like
<import "~~/src/HOL/Library/Code_Trust_the_Target_Language_Standard_Library">?
this is the default. There are a lot of adaptations for Haskell already
built-in.

(You can observe that from the things that get imported.)

Cheers
Lars

Loading...