From 1545317ea8b6e7ca4965f06f00bc524d5af1ef47 Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Tue, 16 Sep 2014 14:52:03 +0000
Subject: Haskell extraction: put unsafeCoerce type declaration later

When Haskell extraction requires magic type coersion, Coq produces
the following code:

  unsafeCoerce :: a -> b
  #ifdef __GLASGOW_HASKELL__
  import qualified GHC.Base
  unsafeCoerce = GHC.Base.unsafeCoerce#
  #else
  -- HUGS
  import qualified IOExts
  unsafeCoerce = IOExts.unsafeCoerce
  #endif

GHC version 7.6.3 does not allow imports after a type declaration,
and produces this error:

  xx.hs:20:1: parse error on input `import'

(referring to the first import statement above).  This patch moves
the unsafeCoerce type declaration to just after the import statement,
fixing this compile error.
---
 plugins/extraction/haskell.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 86681e3709..6008dffde6 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -54,13 +54,14 @@ let preamble mod_name comment used_modules usf =
   (if List.is_empty used_modules then mt () else fnl ()) ++
   (if not usf.magic then mt ()
    else str "\
-\nunsafeCoerce :: a -> b\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
+\nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
 \nimport qualified IOExts\
+\nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
 \n#endif" ++ fnl2 ())
   ++
-- 
cgit v1.2.3