From af409aa1b611ae1c9029015066d842e79b46aea2 Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Mon, 6 Jan 2025 17:02:05 +0100 Subject: [PATCH] Throw error if module under Haskell. namespace produces any Haskell output --- src/Agda2Hs/Compile.hs | 26 +++++++++++++++++++++----- src/Agda2Hs/Compile/Name.hs | 1 - src/Agda2Hs/Compile/Utils.hs | 4 +--- 3 files changed, 22 insertions(+), 9 deletions(-) diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs index cbf95314..b882437f 100644 --- a/src/Agda2Hs/Compile.hs +++ b/src/Agda2Hs/Compile.hs @@ -1,5 +1,7 @@ module Agda2Hs.Compile where +import Prelude hiding (null) + import Control.Monad.Trans.RWS.CPS ( evalRWST ) import Control.Monad.State ( gets ) import Control.Arrow ((>>>)) @@ -17,17 +19,18 @@ import Agda.TypeChecking.Monad.Signature ( isInlineFun ) import Agda.Utils.Impossible import Agda.Utils.List import Agda.Utils.Null -import Agda.Utils.Monad ( whenM, anyM, when ) +import Agda.Utils.Monad ( whenM, anyM, when, unless ) import qualified Language.Haskell.Exts.Extension as Hs import Agda2Hs.Compile.ClassInstance ( compileInstance ) import Agda2Hs.Compile.Data ( compileData ) import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma ) +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, isClassName ) +import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isPrimModule, isHsModule, isClassName ) import Agda2Hs.Pragma import qualified Language.Haskell.Exts.Syntax as Hs import qualified Language.Haskell.Exts.Pretty as Hs @@ -54,9 +57,6 @@ runC tlm rewrites c = evalRWST c (initCompileEnv tlm rewrites) initCompileState moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile ModuleEnv ModuleRes) moduleSetup _ _ m _ = do - -- we never compile primitive modules - if any (`isPrefixOf` prettyShow m) primModules then pure $ Skip () - else do reportSDoc "agda2hs.compile" 3 $ text "Compiling module: " <+> prettyTCM m setScope . iInsideScope =<< curIF return $ Recompile m @@ -120,6 +120,7 @@ verifyOutput :: verifyOutput _ _ _ m ls = do reportSDoc "agda2hs.compile" 5 $ text "Checking generated output before rendering: " <+> prettyTCM m ensureUniqueConstructors + ensureNoOutputFromPrimModules where ensureUniqueConstructors = do let allCons = do @@ -134,3 +135,18 @@ verifyOutput _ _ _ m ls = do duplicateCons = filter ((> 1) . length) . group . sort $ allCons when (length duplicateCons > 0) $ genericDocError =<< vcat (map (\x -> text $ "Cannot generate multiple constructors with the same identifier: " <> Hs.prettyPrint (headWithDefault __IMPOSSIBLE__ x)) duplicateCons) + + ensureNoOutputFromPrimModules = unless (null $ concat $ map fst ls) $ do + let hsModName = hsTopLevelModuleName m + when (isPrimModule hsModName) $ do + reportSDoc "agda2hs.compile" 10 $ text "Primitive module" <+> prettyTCM m <+> text "has non-null output." + if isHsModule hsModName + then 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." + ) + else do + __IMPOSSIBLE_VERBOSE__ "Primitive Agda module should not have any COMPILE AGDA2HS pragmas!" diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 69890638..8cd55e1d 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -115,7 +115,6 @@ compileQName f existsInHaskell <- orM [ pure $ isJust special , pure $ isPrimModule mod - , pure $ isHsModule mod , hasCompilePragma f , isClassFunction f , isWhereFunction f diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index 8e040355..62508157 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -57,9 +57,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) primModules = [ "Agda.Builtin" , "Agda.Primitive" - , "Haskell.Prim" - , "Haskell.Prelude" - , "Haskell.Law" + , "Haskell" ] isPrimModule :: Hs.ModuleName () -> Bool