[isabelle-dev] Imperative HOL: missing parenthesis for Haskell code generation of do-blocks

[Christian Sternagel]

Dear all,

while it is in principle nice that during Haskell code generation 
do-blocks are mapped to Haskell do-blocks when using the heap monad of 
Imperative HOL, it seems that the setup did not consider do-blocks as 
arguments to functions. As a minimal example

theory Test
imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
begin

definition "foo m = do { m; return () }"
definition "bar = foo (do { return (); return () })"

export_code bar in Haskell

the code for "bar" does not compile, since parenthesis are missing 
around its argument do-block.

cheers

chris