From d597a20982ee32e72c7f60a97d03205c174c40ce Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Fri, 15 Nov 2024 16:33:32 +0100 Subject: [PATCH] Exclude names starting with `Haskell.` from check for COMPILE pragma --- src/Agda2Hs/Compile/Name.hs | 1 + src/Agda2Hs/Compile/Utils.hs | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 52468cbb..42233e9b 100644 --- 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 index 6d8ef53f..038c1bd8 100644 --- 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