diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2014-09-16 14:52:03 +0000 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-10-28 09:09:56 +0100 |
| commit | 1545317ea8b6e7ca4965f06f00bc524d5af1ef47 (patch) | |
| tree | 0c40de308bd1e92dd14b859363f48df8e43c17a8 /plugins/extraction | |
| parent | 2d88f205592d279bc7a57e0901522214770c2948 (diff) | |
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.
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/haskell.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 86681e370..6008dffde 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 ()) ++ |