Exclude names starting with Haskell. from check for COMPILE pragma

agda · Nov 15, 2024 · d597a20 · d597a20
1 parent 4870d37
commit d597a20
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs
@@ -115,6 +115,7 @@ 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
@@ -64,6 +64,9 @@ primModules =
 isPrimModule :: Hs.ModuleName () -> Bool
 isPrimModule mod = any (`isPrefixOf` pp mod) primModules
 
+isHsModule :: Hs.ModuleName () -> Bool
+isHsModule mod = "Haskell." `isPrefixOf` pp mod
+
 concatUnzip :: [([a], [b])] -> ([a], [b])
 concatUnzip = (concat *** concat) . unzip