diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-03-28 08:19:05 -0400 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-02 16:51:30 +0200 |
| commit | f10a4ac8e58917f0d9b11458465a963a562aa582 (patch) | |
| tree | 869bf59c4919689fd0bbc40058c62751906ce07d /plugins/extraction/haskell.ml | |
| parent | 3d8c7b24ac97e8d714f343cc0e49e8dff9c90aaf (diff) | |
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.
Diffstat (limited to 'plugins/extraction/haskell.ml')
| -rw-r--r-- | plugins/extraction/haskell.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 52459f78e..4bf576f64 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,18 +56,25 @@ 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 () else str "__ :: any" ++ fnl () ++ str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) |