[ fix #394 ] More uniform and consistent classification of modules

Author: jespercockx

src/Agda2Hs/Compile.hs

@@ -30,7 +30,7 @@ import Agda2Hs.Compile.Name ( hsTopLevelModuleName )
 import Agda2Hs.Compile.Postulate ( compilePostulate )
 import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )
 import Agda2Hs.Compile.Types
-import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isPrimModule, isHsModule, isClassName )
+import Agda2Hs.Compile.Utils
 import Agda2Hs.Pragma
 import qualified Language.Haskell.Exts.Syntax as Hs
 import qualified Language.Haskell.Exts.Pretty as Hs
@@ -138,13 +138,15 @@ verifyOutput _ _ _ m ls = do
 
     ensureNoOutputFromHsModules = unless (null $ concat $ map fst ls) $ do
       let hsModName = hsTopLevelModuleName m
-      when (isHsModule hsModName) $ do
-        reportSDoc "agda2hs.compile" 10 $ text "Haskell module" <+> prettyTCM m <+> text "has non-null output."
-        genericDocError =<< hsep
-          (  pwords "The `Haskell.` namespace are reserved for binding existing Haskell modules, so the module"
-          ++ [text "`" <> prettyTCM m <> text "`"]
-          ++ pwords "should not contain any"
-          ++ [text "`{-# COMPILE AGDA2HS ... #-}`"]
-          ++ pwords "pragmas that produce Haskell code."
-          )
-      when (isPrimModule hsModName) __IMPOSSIBLE__
+      case hsModuleKind hsModName of
+        HsModule -> do
+          reportSDoc "agda2hs.compile" 10 $ text "Haskell module" <+> prettyTCM m <+> text "has non-null output."
+          genericDocError =<< hsep
+            (  pwords "The `Haskell.` namespace are reserved for binding existing Haskell modules, so the module"
+            ++ [text "`" <> prettyTCM m <> text "`"]
+            ++ pwords "should not contain any"
+            ++ [text "`{-# COMPILE AGDA2HS ... #-}`"]
+            ++ pwords "pragmas that produce Haskell code."
+            )
+        PrimModule -> __IMPOSSIBLE__
+        AgdaModule -> return ()

src/Agda2Hs/Compile/Name.hs

@@ -109,12 +109,12 @@ compileQName f
     parent <- parentName f
     par <- traverse (compileName . qnameName) parent
     let mod0 = qnameModule $ fromMaybe f parent
-    mod <- compileModuleName mod0
+    (mkind, mod) <- compileModuleName mod0
 
     existsInHaskell <- orM
       [ pure $ isJust special
-      , pure $ isPrimModule mod
-      , pure $ isHsModule mod
+      , pure $ mkind == PrimModule
+      , pure $ mkind == HsModule
       , hasCompilePragma f
       , isClassFunction f
       , isWhereFunction f
@@ -137,8 +137,12 @@ compileQName f
           Hs.Symbol _ _ -> getNamespace f
           Hs.Ident  _ _ -> return (Hs.NoNamespace ()))
     let
-      (mod', mimp) = mkImport mod qual par hf namespace
-      qf = qualify mod' hf qual
+      -- We don't generate "import Prelude" for primitive modules,
+      -- unless a name is qualified.
+      mimp = if mkind /= PrimModule || isQualified qual
+             then Just (Import mod qual par hf namespace)
+             else Nothing
+      qf = qualify mod hf qual
 
     -- add (possibly qualified) import
     whenM (asks writeImports) $
@@ -202,21 +206,6 @@ compileQName f
       (Pi _ absType) -> getResultType $ unAbs absType
       _              -> typ
 
-    mkImport mod qual par hf maybeIsType
-      -- make sure the Prelude is properly qualified
-      | isPrimModule mod
-      = if isQualified qual then
-          let mod' = hsModuleName "Prelude"
-          in (mod', Just (Import mod' qual Nothing hf maybeIsType))
-        else (mod, Nothing)
-      | otherwise
-      = let mod' = dropHaskellPrefix mod
-        in (mod', Just (Import mod' qual par hf maybeIsType))
-
-    dropHaskellPrefix :: Hs.ModuleName () -> Hs.ModuleName ()
-    dropHaskellPrefix (Hs.ModuleName l s) =
-      Hs.ModuleName l $ fromMaybe s $ stripPrefix "Haskell." s
-
 isWhereFunction :: QName -> C Bool
 isWhereFunction f = do
   whereMods <- asks whereModules
@@ -228,17 +217,20 @@ hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack
 
 -- | Given a module name (assumed to be a toplevel module),
 -- compute the associated Haskell module name.
-compileModuleName :: ModuleName -> C (Hs.ModuleName ())
+compileModuleName :: ModuleName -> C (HsModuleKind, Hs.ModuleName ())
 compileModuleName m = do
   tlm <- liftTCM $ hsTopLevelModuleName <$> getTopLevelModuleForModuleName m
   reportSDoc "agda2hs.name" 25 $
     text "Top-level module name for" <+> prettyTCM m <+>
     text "is" <+> text (pp tlm)
-  return tlm
+  case hsModuleKind tlm of
+    PrimModule -> return (PrimModule, Hs.ModuleName () "Prelude")
+    HsModule   -> return (HsModule, dropHaskellPrefix tlm)
+    AgdaModule -> return (AgdaModule, tlm)
 
 importInstance :: QName -> C ()
 importInstance f = do
-  mod <- compileModuleName $ qnameModule f
-  unless (isPrimModule mod) $ do
+  (kind, mod) <- compileModuleName $ qnameModule f
+  unless (kind == PrimModule) $ do
     reportSLn "agda2hs.import" 20 $ "Importing instances from " ++ pp mod
     tellImport $ ImportInstances mod

src/Agda2Hs/Compile/Utils.hs

@@ -7,10 +7,9 @@ import Control.Monad.Reader
 import Control.Monad.Writer ( tell )
 import Control.Monad.State ( put, modify )
 
-import Data.List ( isPrefixOf )
+import Data.List ( isPrefixOf, stripPrefix )
 import Data.Maybe ( isJust )
 import qualified Data.Map as M
-import Data.List ( isPrefixOf )
 
 import qualified Language.Haskell.Exts as Hs
 
@@ -51,6 +50,11 @@ import Agda2Hs.Pragma
 import qualified Data.List as L
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
+data HsModuleKind
+  = PrimModule
+  | HsModule
+  | AgdaModule
+  deriving (Eq)
 
 -- | Primitive modules provided by the agda2hs library.
 -- None of those (and none of their children) will get processed.
@@ -61,11 +65,15 @@ primModules =
   , "Haskell.Prelude"
   ]
 
-isPrimModule :: Hs.ModuleName () -> Bool
-isPrimModule mod = any (`isPrefixOf` pp mod) primModules
+hsModuleKind :: Hs.ModuleName () -> HsModuleKind
+hsModuleKind mod
+  | any (`isPrefixOf` pp mod) primModules = PrimModule
+  | "Haskell." `isPrefixOf` pp mod        = HsModule
+  | otherwise                             = AgdaModule
 
-isHsModule :: Hs.ModuleName () -> Bool
-isHsModule mod = "Haskell." `isPrefixOf` pp mod
+dropHaskellPrefix :: Hs.ModuleName () -> Hs.ModuleName ()
+dropHaskellPrefix (Hs.ModuleName l s) =
+  Hs.ModuleName l $ fromMaybe s $ stripPrefix "Haskell." s
 
 concatUnzip :: [([a], [b])] -> ([a], [b])
 concatUnzip = (concat *** concat) . unzip

test/.gitignore

@@ -1,4 +1,3 @@
 build/
 agda2hs
-Haskell/
 html/

test/AllTests.agda

@@ -95,6 +95,7 @@ import Issue308
 import Issue324
 import Assert
 import Issue377
+import Issue394
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -187,4 +188,5 @@ import Issue308
 import Issue324
 import Assert
 import Issue377
+import Issue394
 #-}

test/Haskell/Data/ByteString.agda

@@ -0,0 +1,9 @@
+module Haskell.Data.ByteString where
+
+open import Haskell.Prelude
+
+postulate
+  ByteString : Set
+
+  instance
+    iEqByteString : Eq ByteString

test/Issue394.agda

@@ -0,0 +1,8 @@
+
+open import Haskell.Prelude
+open import Haskell.Data.ByteString using (ByteString)
+
+test : ByteString → ByteString → Bool
+test x y = x == y
+
+{-# COMPILE AGDA2HS test #-}

test/golden/AllTests.hs

@@ -90,4 +90,5 @@ import Issue308
 import Issue324
 import Assert
 import Issue377
+import Issue394
 

test/golden/CommonQualifiedImports.hs

@@ -1,7 +1,7 @@
 module CommonQualifiedImports where
 
 import qualified Importee as Common (foo)
-import qualified Prelude as Common (Int, (+))
+import qualified Prelude as Common (Int, Num((+)))
 import qualified SecondImportee as Common (anotherFoo)
 
 -- ** common qualification

test/golden/Issue394.hs

@@ -0,0 +1,7 @@
+module Issue394 where
+
+import Data.ByteString (ByteString)
+
+test :: ByteString -> ByteString -> Bool
+test x y = x == y
+

test/golden/QualifiedPrelude.hs

@@ -1,7 +1,7 @@
 module QualifiedPrelude where
 
 import Numeric.Natural (Natural)
-import qualified Prelude as Pre (foldr, (+), (.))
+import qualified Prelude as Pre (Foldable(foldr), Num((+)), (.))
 
 -- ** qualifying the Prelude