diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs index f5402cbf..148722ad 100644 --- a/src/Agda2Hs/Compile.hs +++ b/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 () diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 2816b61a..ea69b29f 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/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 diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index be782b35..7c177910 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/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 diff --git a/test/.gitignore b/test/.gitignore index ccf6b5c8..96b1e895 100644 --- a/test/.gitignore +++ b/test/.gitignore @@ -1,4 +1,3 @@ build/ agda2hs -Haskell/ html/ diff --git a/test/AllTests.agda b/test/AllTests.agda index e829b337..147968ae 100644 --- a/test/AllTests.agda +++ b/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 #-} diff --git a/test/Haskell/Data/ByteString.agda b/test/Haskell/Data/ByteString.agda new file mode 100644 index 00000000..5de8842d --- /dev/null +++ b/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 diff --git a/test/Issue394.agda b/test/Issue394.agda new file mode 100644 index 00000000..c372edd2 --- /dev/null +++ b/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 #-} diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index 99247aa1..9ce1fcdf 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -90,4 +90,5 @@ import Issue308 import Issue324 import Assert import Issue377 +import Issue394 diff --git a/test/golden/CommonQualifiedImports.hs b/test/golden/CommonQualifiedImports.hs index f8d8715b..59d4341c 100644 --- a/test/golden/CommonQualifiedImports.hs +++ b/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 diff --git a/test/golden/Issue394.hs b/test/golden/Issue394.hs new file mode 100644 index 00000000..d5e0fc74 --- /dev/null +++ b/test/golden/Issue394.hs @@ -0,0 +1,7 @@ +module Issue394 where + +import Data.ByteString (ByteString) + +test :: ByteString -> ByteString -> Bool +test x y = x == y + diff --git a/test/golden/QualifiedPrelude.hs b/test/golden/QualifiedPrelude.hs index b8bd4add..eb7e2798 100644 --- a/test/golden/QualifiedPrelude.hs +++ b/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