From f10a4ac8e58917f0d9b11458465a963a562aa582 Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Sat, 28 Mar 2015 08:19:05 -0400
Subject: Define Any in Haskell extraction when Tunknown is used.

Commit 84c2433a introduced the Any type alias as the Haskell extracted
version of MiniML's Tunknown.  However, the code to define the Any
type alias was generated conditional on usf.magic.  As it turns out,
sometimes Tunknown appears even if usf.magic is false (i.e., even if
MLmagic does not appear anywhere in the AST).  This produced Haskell
code that would not compile; e.g.:

  % coqtop
  Coq < Extraction Language Haskell.
  Coq < Extraction Library Datatypes.
  The file Datatypes.hs has been created by extraction.

  % ghc Datatypes.hs
  [1 of 1] Compiling Datatypes        ( Datatypes.hs, Datatypes.o )
  Datatypes.hs:261:17: Not in scope: type constructor or class `Any'
  Datatypes.hs:261:24: Not in scope: type constructor or class `Any'

The fix is straightforward: produce the code that defines the Any type
alias if usf.tunknown is true.
---
 plugins/extraction/haskell.ml | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction/haskell.ml')

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 52459f78eb..4bf576f640 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -38,7 +38,7 @@ let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
 let preamble mod_name comment used_modules usf =
   let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
   in
-  (if not usf.magic then mt ()
+  (if not (usf.magic || usf.tunknown) then mt ()
    else
      str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++
      str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
@@ -56,16 +56,23 @@ let preamble mod_name comment used_modules usf =
    else str "\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
-\nimport qualified GHC.Prim\
-\ntype Any = GHC.Prim.Any\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
 \nimport qualified IOExts\
-\ntype Any = ()\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
+\n#endif" ++ fnl2 ())
+  ++
+  (if not usf.tunknown then mt ()
+   else str "\
+\n#ifdef __GLASGOW_HASKELL__\
+\nimport qualified GHC.Prim\
+\ntype Any = GHC.Prim.Any\
+\n#else\
+\n-- HUGS\
+\ntype Any = ()\
 \n#endif" ++ fnl2 ())
   ++
   (if not usf.mldummy then mt ()
-- 
cgit v1.2.3


From aec237038d300ce7c81dddd154cbdc93fed5b226 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 2 Apr 2015 19:26:59 +0200
Subject: Fix some typos.

---
 plugins/extraction/haskell.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction/haskell.ml')

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 4bf576f640..5f31edfb60 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -356,7 +356,7 @@ and pp_module_expr = function
   | MEfunctor _ -> mt ()
       (* for the moment we simply discard unapplied functors *)
   | MEident _ | MEapply _ -> assert false
-      (* should be expansed in extract_env *)
+      (* should be expanded in extract_env *)
 
 let pp_struct =
   let pp_sel (mp,sel) =
-- 
cgit v1.2.3


From 6950837dd6e2a3a2bc3c3d748d06054a625bc661 Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Thu, 2 Apr 2015 21:46:19 +0200
Subject: Puts all the "import" statements first so as to accommodate the
 latest GHC.

---
 plugins/extraction/haskell.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'plugins/extraction/haskell.ml')

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 5f31edfb60..37b4142073 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -52,15 +52,23 @@ let preamble mod_name comment used_modules usf =
   str "import qualified Prelude" ++ fnl () ++
   prlist pp_import used_modules ++ fnl () ++
   (if List.is_empty used_modules then mt () else fnl ()) ++
-  (if not usf.magic then mt ()
+  (if not (usf.magic || usf.tunknown) then mt ()
    else str "\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
+\nimport qualified GHC.Prim\
+\n#else\
+\n-- HUGS\
+\nimport qualified IOExts\
+\n#endif" ++ fnl2 ())
+  ++
+  (if not usf.magic then mt ()
+   else str "\
+\n#ifdef __GLASGOW_HASKELL__\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
-\nimport qualified IOExts\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
 \n#endif" ++ fnl2 ())
@@ -68,7 +76,6 @@ let preamble mod_name comment used_modules usf =
   (if not usf.tunknown then mt ()
    else str "\
 \n#ifdef __GLASGOW_HASKELL__\
-\nimport qualified GHC.Prim\
 \ntype Any = GHC.Prim.Any\
 \n#else\
 \n-- HUGS\
-- 
cgit v1.2.3