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

Christian Sternagel c.sternagel at gmail.com
Thu Sep 25 15:00:11 CEST 2014

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"

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.



More information about the isabelle-dev mailing list