Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] More parenthesis for generated Haskell code

Email Gateway (Aug 18 2022 at 13:36):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,

I ran into the following problem when generating Haskell code from an
Isabelle theory.

I use a custom error monad that has an infix `bind' operator >>=, with
corresponding >>.

In Isabelle I have a function with the following structure:

fun foo :: "_" where "
foo args = (
(let x = somethig_of args in (
monadic_function_on args
)) >> (
additional_monadic_stuff_on args
)
)"

This is in turn translated to Haskell code that does not have
parentheses around the `let' construct, i.e., part of the code looks as
follows

bind let {
x = something_of args;
} in monadic_function_on args
(\xa -> additional_monadic_stuff_on args)

but it should be

bind (let {
x = something_of args;
} in monadic_function_on args)
(\xa -> additional_monadic_stuff_on args)

How can I tell the code-generator to add the missing parentheses?

cheers

chris

Email Gateway (Aug 18 2022 at 13:37):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,

the printing of let-expressions for Haskell in Isabelle 2009 is indeed
broken.

There is a possibility to circumvent this. One is to use the built-in
monad pretty printing of the Haskell code generator:

theory Scratch
imports Main
begin

typedecl 'a M

axiomatization bind :: "'a M => ('a => 'b M) => 'b M" (infixl "»=" 54)

Specification of the monad (here, just an axiomatic placeholder)

abbreviation
chainM :: "'a M => 'b M => 'b M" (infixl "»" 54) where
"f » g => f »= (%_. g)"

Means: >> is just syntax for >>=

code_monad bind Haskell

Here "bind" is declared as monad operator.

definition "foo x y = (x »= (%. let z = y a a in z))"

export_code foo in Haskell file -

The example yield the following code:

foo :: forall b a. M b -> (b -> b -> M a) -> M a;
foo x y = do {a <- x; let z = y a a; z};

Do not hesitate to ask further question if you need further hints on this.

Alternatively, we can use special syntax for bind (which I will explain
on demand).

If this does not solve your problem either, I will provide you with a
patch for the Haskell code generator. The issue will be solved in next
Isabelle release (though there is no official schedule for this).

Hope this helps
Florian
signature.asc

Last updated: May 03 2024 at 04:19 UTC