Email Gateway (Aug 22 2022 at 13:55): Email Gateway (Aug 22 2022 at 13:55):From: Moa Johansson <moa.johansson@chalmers.se>
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
Email Gateway (Aug 22 2022 at 13:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Moa,
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.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 13:55):From: "C. Diekmann" <diekmann@in.tum.de>
Dear Florian,
first of all, thanks for the awesome work on the code generator!
2016-08-04 9:23 GMT+02:00 Florian Haftmann <
florian.haftmann@informatik.tu-muenchen.de>:
Hi Moa,
Am 03.08.2016 um 12:59 schrieb Moa Johansson:
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.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
Email Gateway (Aug 22 2022 at 13:56):From: Lars Hupel <hupel@in.tum.de>
Hi Cornelius,
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
Last updated: Apr 25 2024 at 04:18 UTC